diff options
| -rw-r--r-- | readme.md | 8 | ||||
| -rw-r--r-- | source/Meaning.hs | 2 | ||||
| -rw-r--r-- | source/Provers.hs | 12 |
3 files changed, 13 insertions, 9 deletions
@@ -34,6 +34,10 @@ and [E](https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html) to discharge proof tasks. +You may also need to install `zlib` on certain operating systems. +For example, on Ubuntu you can install the development version of +`zlib` by running `sudo apt install zlib1g-dev`. + #### Obtaining Vampire The default prover is Vampire and the included library is written against a specific release of Vampire. @@ -99,8 +103,8 @@ When looking for imported files, the following list of base directories is consi - the current working directory in the command line - the user library directory, set with the environment variable `NAPROCHE_LIB`, defaulting to `~/formalizations` -- the source code library directory, set with the environment variable `NAPROCHE_SCR_LIB`, defaulting to `~/code/zf/library` -- the source code examples directory, set with the environment variable `NAPROCHE_SCR_EXAMPLES`, defaulting to `~/code/zf/examples` +- the source code library directory, set with the environment variable `NAPROCHE_SCR_LIB`, defaulting to `~/code/naproche-zf/library` +- the source code examples directory, set with the environment variable `NAPROCHE_SCR_EXAMPLES`, defaulting to `~/code/naproche-zf/examples` ### Running the tests diff --git a/source/Meaning.hs b/source/Meaning.hs index 00a944f..9b4bc45 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -406,7 +406,7 @@ glossStmt = \case f' <- glossStmt f quantify <- glossQuantifier quantifier pure (quantify vars [constraints] f') - Raw.StmtExists np -> do + Raw.StmtExists np -> do (vars, constraints) <- glossNPList np pure (Sem.makeExists vars constraints) Raw.SymbolicQuantified quant vs bound suchThat have -> do diff --git a/source/Provers.hs b/source/Provers.hs index 37e02ca..273751c 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -82,10 +82,10 @@ vampire path _verbosity timeLimit memoryLimit = Prover , "--time_limit", toSeconds timeLimit , "--memory_limit", toMegabytes memoryLimit ] - , proverSaysYes = ["% SZS output end Proof for"] - , proverSaysNo = ["% SZS status CounterSatisfiable for"] - , proverDoesNotKnow = ["% SZS status Timeout for"] - , proverWarnsContradiction = ["% SZS status ContradictoryAxioms for"] + , proverSaysYes = ["% SZS status Theorem"] + , proverSaysNo = ["% SZS status CounterSatisfiable"] + , proverDoesNotKnow = ["% SZS status Timeout"] + , proverWarnsContradiction = ["% SZS status ContradictoryAxioms"] } -- WIP: setting up a clausifier @@ -96,8 +96,8 @@ iprover _verbosity timeLimit _memoryLimit = Prover , proverArgs = [ "--time_out_real " <> toSeconds timeLimit ] - , proverSaysYes = ["% SZS status Theorem for"] - , proverSaysNo = ["% SZS status CounterSatisfiable for"] + , proverSaysYes = ["% SZS status Theorem"] + , proverSaysNo = ["% SZS status CounterSatisfiable"] , proverDoesNotKnow = ["% SZS status Unknown"] , proverWarnsContradiction = [] } |