diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 4 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 4 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 16 | ||||
-rw-r--r-- | src/main/options | 2 |
4 files changed, 14 insertions, 12 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index aa63846cf..6b09fcc27 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -61,13 +61,13 @@ BUILT_SOURCES = \ TOKENS_FILES = \ cvc_tokens.h \ - smt_tokens.h \ + smt1_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 >$@ -smt_tokens.h: @srcdir@/../parser/smt/Smt.g +smt1_tokens.h: @srcdir@/../parser/smt1/Smt1.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 >$@ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 20b4c2bc2..a3086d96c 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -153,7 +153,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB); + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); + } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) { + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { opts.set(options::inputLanguage, language::input::LANG_TPTP); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index b0934c0ee..719c8f61d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -64,9 +64,9 @@ static const std::string cvc_commands[] = { #include "main/cvc_tokens.h" };/* cvc_commands */ -static const std::string smt_commands[] = { -#include "main/smt_tokens.h" -};/* smt_commands */ +static const std::string smt1_commands[] = { +#include "main/smt1_tokens.h" +};/* smt1_commands */ static const std::string smt2_commands[] = { #include "main/smt2_tokens.h" @@ -105,10 +105,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; - case output::LANG_SMTLIB: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib"; - commandsBegin = smt_commands; - commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands); + case output::LANG_SMTLIB_V1: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1"; + commandsBegin = smt1_commands; + commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands); break; case output::LANG_SMTLIB_V2: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; diff --git a/src/main/options b/src/main/options index 58ea5e544..02c4643b3 100644 --- a/src/main/options +++ b/src/main/options @@ -20,7 +20,7 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl show all available tags for tracing expert-option earlyExit --early-exit bool :default true - do not run destructors at exit; default on except in debug mode + do not run destructors at exit; default on except in debug builds # portfolio options option printWinner bool |