work on propositional layer, expression builder support for large expressions, output classes, and minisat

2 files changed, 33 insertions, 3 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 2daead11b..7f515c58b 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -25,6 +25,7 @@
 #include "util/exception.h"
 #include "usage.h"
 #include "about.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
@@ -66,7 +67,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
     progName = x + 1;
   opts->binary_name = string(progName);
 
-  while((c = getopt_long(argc, argv, "+:hVvqL:", cmdlineOptions, NULL)) != -1) {
+  while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
@@ -104,6 +105,9 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       fputs(lang_help, stdout);
       exit(1);
 
+    case 'd':
+      Debug.on(optarg);
+
     case STATS:
       opts->statistics = true;
       break;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4c3a21811..d4ee8fd0d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -13,6 +13,7 @@
 #include <iostream>
 #include <fstream>
 #include <cstdlib>
+#include <cstring>
 #include <new>
 
 #include "config.h"
@@ -22,6 +23,7 @@
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
@@ -44,18 +46,42 @@ int main(int argc, char *argv[]) {
     if(options.smtcomp_mode)
       cout << unitbuf;
 
-        // We only accept one input file
+    // We only accept one input file
     if(argc > firstArgIndex + 1)
       throw new Exception("Too many input files specified.");
 
     // Create the expression manager
     ExprManager exprMgr;
+
     // Create the SmtEngine
     SmtEngine smt(&exprMgr, &options);
 
     // If no file supplied we read from standard input
     bool inputFromStdin = firstArgIndex >= argc;
 
+    if(!inputFromStdin && options.lang == Options::LANG_AUTO) {
+      if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4))
+        options.lang = Options::LANG_SMTLIB;
+      else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) ||
+              !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5))
+        options.lang = Options::LANG_CVC4;
+    }
+
+    if(options.smtcomp_mode) {
+      Debug.setStream(CVC4::null_os);
+      Trace.setStream(CVC4::null_os);
+      Notice.setStream(CVC4::null_os);
+      Chat.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    } else {
+      if(options.verbosity < 2)
+        Chat.setStream(CVC4::null_os);
+      if(options.verbosity < 1)
+        Notice.setStream(CVC4::null_os);
+      if(options.verbosity < 0)
+        Warning.setStream(CVC4::null_os);
+    }
+
     // Create the parser
     Parser* parser;
     switch(options.lang) {
@@ -79,7 +105,7 @@ int main(int argc, char *argv[]) {
       abort();
     }
 
-    // Parse the and execute commands until we are done
+    // Parse and execute commands until we are done
     while(!parser->done()) {
       // Parse the next command
       Command *cmd = parser->parseNextCommand();