From 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 2 Sep 2011 20:41:08 +0000
Subject: 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.
---
 src/main/main.cpp | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

(limited to 'src/main/main.cpp')

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);
-- 
cgit v1.2.3