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 | |
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')
-rw-r--r-- | src/main/Makefile.am | 5 | ||||
-rw-r--r-- | src/main/driver.cpp | 3 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 3 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 8 |
4 files changed, 18 insertions, 1 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index e6aa6b423..594751358 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -53,7 +53,8 @@ BUILT_SOURCES = \ TOKENS_FILES = \ cvc_tokens.h \ smt_tokens.h \ - smt2_tokens.h + smt2_tokens.h \ + tptp_tokens.h cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ @@ -61,6 +62,8 @@ smt_tokens.h: @srcdir@/../parser/smt/Smt.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ +tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ clean-local: rm -f $(BUILT_SOURCES) diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 742cba8d2..44457841d 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -182,6 +182,9 @@ int runCvc4(int argc, char* argv[], Options& options) { options.inputLanguage = language::input::LANG_SMTLIB_V2; } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { options.inputLanguage = language::input::LANG_SMTLIB; + } else if((len >= 2 && !strcmp(".p", filename + len - 2)) + || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { + options.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { options.inputLanguage = language::input::LANG_CVC4; diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index 7972cd94d..a8da88173 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -261,6 +261,9 @@ int runCvc4(int argc, char *argv[], Options& options) { options.inputLanguage = language::input::LANG_SMTLIB_V2; } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { options.inputLanguage = language::input::LANG_SMTLIB; + } else if((len >= 2 && !strcmp(".p", filename + len - 2)) + || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { + options.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { options.inputLanguage = language::input::LANG_CVC4; 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); } |