diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/main/main.cpp | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 27 |
1 files changed, 17 insertions, 10 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 1423befb6..ef19e1604 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -183,6 +183,7 @@ int runCvc4(int argc, char* argv[]) { Chat.setStream(CVC4::null_os); Message.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); } else { if(options.verbosity < 2) { Chat.setStream(CVC4::null_os); @@ -228,7 +229,10 @@ int runCvc4(int argc, char* argv[]) { } } - OutputLanguage outLang = language::toOutputLanguage(options.inputLanguage); + if(options.outputLanguage == language::output::LANG_AUTO) { + options.outputLanguage = language::toOutputLanguage(options.inputLanguage); + } + // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { Debug.setStream(CVC4::null_os); @@ -237,6 +241,7 @@ int runCvc4(int argc, char* argv[]) { Chat.setStream(CVC4::null_os); Message.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); } else { if(options.verbosity < 2) { Chat.setStream(CVC4::null_os); @@ -249,12 +254,15 @@ int runCvc4(int argc, char* argv[]) { Warning.setStream(CVC4::null_os); } - Debug.getStream() << Expr::setlanguage(outLang); - Trace.getStream() << Expr::setlanguage(outLang); - Notice.getStream() << Expr::setlanguage(outLang); - Chat.getStream() << Expr::setlanguage(outLang); - Message.getStream() << Expr::setlanguage(outLang); - Warning.getStream() << Expr::setlanguage(outLang); + Debug.getStream() << Expr::setlanguage(options.outputLanguage); + Trace.getStream() << Expr::setlanguage(options.outputLanguage); + Notice.getStream() << Expr::setlanguage(options.outputLanguage); + Chat.getStream() << Expr::setlanguage(options.outputLanguage); + Message.getStream() << Expr::setlanguage(options.outputLanguage); + Warning.getStream() << Expr::setlanguage(options.outputLanguage); + Dump.getStream() << Expr::setlanguage(options.outputLanguage) + << Expr::setdepth(-1) + << Expr::printtypes(false); } Parser* replayParser = NULL; @@ -271,7 +279,7 @@ int runCvc4(int argc, char* argv[]) { options.replayStream = new Parser::ExprStream(replayParser); } if( options.replayLog != NULL ) { - *options.replayLog << Expr::setlanguage(outLang) << Expr::setdepth(-1); + *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); } // Parse and execute commands until we are done @@ -296,8 +304,7 @@ int runCvc4(int argc, char* argv[]) { delete cmd; } } else { - ParserBuilder parserBuilder = - ParserBuilder(&exprMgr, filename, options); + ParserBuilder parserBuilder(&exprMgr, filename, options); if( inputFromStdin ) { parserBuilder.withStreamInput(cin); |