diff options
author | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:37 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:37 +0000 |
commit | 84c4269f3b9edb8de4134fe464dfc70679da2bb1 (patch) | |
tree | b0c8f33e04d925064ffa9d85f1caeb6a3ff745b2 /src/main/interactive_shell.cpp | |
parent | eda7d4df5481030d4e9cb6ef4a33d52afc8f7e0a (diff) |
TPTP: add parser for cnf and fof
- include directive works
- no keyword : 'fof', 'cnf', ... can be used for symbols name
- real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
- same thing for string
But:
- string not distinct by projection to real, not sure if the current state of string theory make them distinct
- filtering in include is not done
- the result is not printed in the TPTP way (currently SMT2 way)
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r-- | src/main/interactive_shell.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index d8e7df2f2..03a3a0ae3 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -72,6 +72,10 @@ static const char* const smt2_commands[] = { #include "main/smt2_tokens.h" };/* smt2_commands */ +static const char* const tptp_commands[] = { +#include "main/tptp_tokens.h" +};/* tptp_commands */ + static const char* const* commandsBegin; static const char* const* commandsEnd; @@ -110,6 +114,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); + case output::LANG_TPTP: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; + commandsBegin = tptp_commands; + commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); break; default: Unhandled(lang); } |