parsing/expr/command/result/various other fixes

3 files changed, 26 insertions, 14 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index dddfb3219..36e4c0342 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -10,5 +10,5 @@ cvc4_SOURCES = \
 	util.cpp
 
 cvc4_LDADD = \
-	../parser/libparser.la \
+	../parser/libcvc4parser.la \
 	../libcvc4.la
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 5af3b5d21..f60dd6e24 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -68,7 +68,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
     progName = x + 1;
   opts->binary_name = string(progName);
 
-  while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) {
+  while((c = getopt_long(argc, argv, "+:hVvqL:", cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 58d86a42d..323a989c8 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -27,8 +27,11 @@
 #include "usage.h"
 #include "parser/parser.h"
 #include "expr/expr_manager.h"
+#include "expr/expr.h"
+#include "expr/kind.h"
 #include "smt/smt_engine.h"
 #include "parser/language.h"
+#include "util/command.h"
 
 using namespace std;
 using namespace CVC4;
@@ -53,23 +56,32 @@ int main(int argc, char *argv[]) {
       throw new Exception("Too many input files specified.");
     } else {
       in = &infile;
-      if(strlen(argv[firstArgIndex]) >= 4 && !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt"))
+      if(strlen(argv[firstArgIndex]) >= 4 &&
+         !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt"))
         lang = SMTLIB;
       infile.open(argv[firstArgIndex], ifstream::in);
 
       if(!infile) {
-        throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
-        exit(1);
+        throw new Exception(string("Could not open input file `") +
+                            argv[firstArgIndex] + "' for reading: " +
+                            strerror(errno));
       }
     }
 
-    ExprManager *exprMgr = new ExprManager();
+    ExprManager *exprMgr = new ExprManager;
     SmtEngine smt(exprMgr, &opts);
-    Parser parser(&smt, lang, *in, &opts);
+    Parser parser(&smt, exprMgr, lang, *in, &opts);
     while(!parser.done()) {
-      Command *cmd = parser.next();
-      cmd->invoke();
-      delete cmd;
+      Command *cmd = parser.parseNextCommand(opts.verbosity > 1);
+      if(opts.verbosity > 0) {
+        cout << "invoking cmd: ";
+        cout << cmd << endl;
+      }
+      if(cmd) {
+        if(opts.verbosity >= 0)
+          cout << cmd->invoke(&smt) << endl;
+        delete cmd;
+      }
     }
   } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
@@ -78,24 +90,24 @@ int main(int argc, char *argv[]) {
     }
     fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str());
     printf(usage, opts.binary_name.c_str());
-    exit(1);
+    abort();
   } catch(CVC4::Exception* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
       fflush(stdout);
     }
     fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str());
-    exit(1);
+    abort();
   } catch(bad_alloc) {
     if(opts.smtcomp_mode) {
       printf("unknown");
       fflush(stdout);
     }
     fprintf(stderr, "CVC4 ran out of memory.\n");
-    exit(1);
+    abort();
   } catch(...) {
     fprintf(stderr, "CVC4 threw an exception of unknown type.\n");
-    exit(1);
+    abort();
   }
 
   return 0;