diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-16 12:36:32 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-16 12:36:32 +0200 |
| commit | 9aac1a22c4ff4b4be16800b86e34a94d358b0deb (patch) | |
| tree | 4874bcad55c1a40d8776e367b1bba0ad6c80f46e /source/CommandLine.hs | |
| parent | 92efa0fe16152c0f42cb9d05d6ef127955b03a18 (diff) | |
Add quantified calcs and relax tokenization
Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
Diffstat (limited to 'source/CommandLine.hs')
| -rw-r--r-- | source/CommandLine.hs | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/source/CommandLine.hs b/source/CommandLine.hs index b8c170e..3502b9a 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,6 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix -import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -94,7 +93,7 @@ run = do Text.putStrLn task Text.putStrLn err Text.putStrLn tptp - + WithFailList -> liftIO case result of VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" VerificationFailure [] -> error "Empty verification fail" @@ -187,4 +186,4 @@ withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to M withFailListParser :: Parser WithFailList withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") - <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file + <|> pure WithoutFailList -- Default to using the cache. |