From 61937ea05bff33070cc8252bc3b6c7d6fed7c9c3 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 24 Nov 2009 22:51:35 +0000
Subject: various fixes and updates to use and support parser

---
 src/main/getopt.cpp |  8 ++------
 src/main/main.cpp   | 38 +++++++++++++++++++++++++++-----------
 2 files changed, 29 insertions(+), 17 deletions(-)

(limited to 'src/main')

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index dcb23c303..5af3b5d21 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -25,9 +25,11 @@
 #include "util/exception.h"
 #include "usage.h"
 #include "about.h"
+#include "parser/language.h"
 
 using namespace std;
 using namespace CVC4;
+using namespace CVC4::parser;
 
 namespace CVC4 {
 namespace main {
@@ -39,12 +41,6 @@ Languages currently supported to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
-enum Language {
-  AUTO = 0,
-  PL,
-  SMTLIB,
-};/* enum Language */
-
 enum OptionValue {
   SMTCOMP = 256, /* no clash with char options */
   STATS
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8529f2ca2..1fc616fe6 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -10,6 +10,8 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <iostream>
+#include <fstream>
 #include <cstdio>
 #include <cstdlib>
 #include <cerrno>
@@ -23,9 +25,14 @@
 #include "config.h"
 #include "main.h"
 #include "usage.h"
+#include "parser/parser.h"
+#include "expr/expr_manager.h"
+#include "smt/smt_engine.h"
+#include "parser/language.h"
 
 using namespace std;
 using namespace CVC4;
+using namespace CVC4::parser;
 using namespace CVC4::main;
 
 int main(int argc, char *argv[]) {
@@ -36,28 +43,37 @@ int main(int argc, char *argv[]) {
 
     int firstArgIndex = parseOptions(argc, argv, &opts);
 
-    FILE *infile;
+    istream *in;
+    ifstream infile;
+    Language lang = PL;
 
     if(firstArgIndex >= argc) {
-      infile = stdin;
+      in = &cin;
     } else if(argc > firstArgIndex + 1) {
       throw new Exception("Too many input files specified.");
     } else {
-      infile = fopen(argv[firstArgIndex], "r");
+      in = &infile;
+      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);
       }
+    }
 
-      // ExprManager *exprMgr = ...;
-      // SmtEngine smt(exprMgr, &opts);
-      // Parser parser(infile, exprMgr, &opts);
-      // while(!parser.done) {
-      //   Command *cmd = parser.get();
-      //   cmd->invoke(smt);
-      //   delete cmd;
-      // }
+    ExprManager *exprMgr = new ExprManager();
+    SmtEngine smt(exprMgr, &opts);
+    Parser parser(&smt, lang, *in, &opts);
+    while(!parser.done()) {
+      Command *cmd = parser.next();
+      cmd->invoke();
+      delete cmd;
     }
+
+    if(infile)
+      infile.close();
   } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
-- 
cgit v1.2.3