changed the smt parser as well to return objects

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@188 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 3331ab96937ebdf744c198b8ee9fb1b75eb99c0f..8a25a4b9b11996c393691116967333334f98b83c 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -15,7 +15,7 @@ using namespace __gnu_cxx;
 #endif
 using namespace BEEV;
 
-extern int smtparse();
+extern int smtparse(void*);
 extern int cvcparse(void*);
 
 // Amount of memory to ask for at beginning of main.
@@ -173,14 +173,17 @@ int main(int argc, char ** argv) {
   GlobalBeevMgr = new BeevMgr();
   ASTVec * AssertsQuery = new ASTVec;
 
-  if (smtlib_parser_flag) {
-    smtparse();
-  }
-  else {
-    cvcparse((void*)AssertsQuery);      
-    ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
-    ASTNode query   = (*(ASTVec*)AssertsQuery)[1];
-    GlobalBeevMgr->TopLevelSAT(asserts, query);
-  }
+  if (smtlib_parser_flag) 
+    {
+      smtparse((void*)AssertsQuery);
+    }
+  else 
+    {
+      cvcparse((void*)AssertsQuery);      
+    }
+
+  ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
+  ASTNode query   = (*(ASTVec*)AssertsQuery)[1];
+  GlobalBeevMgr->TopLevelSAT(asserts, query);
   return 0;
 }//end of Main

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 54c2d2c245f46903b68d12a04df26199c72ab997..251fbf4a5b00749bb7f816b4cd15e4e405dc1ff8 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -30,7 +30,6 @@
 #define YYMAXDEPTH 10485760
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
-
 #define YYPARSE_PARAM AssertsQuery
 %}
 
@@ -182,14 +181,12 @@ counterexample  :      COUNTEREXAMPLE_TOK ';'
 other_cmd       :      other_cmd1
                 |      Query 
                        { 
-                        //GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(TRUE),*$1);
                         ((ASTVec*)AssertsQuery)->push_back(GlobalBeevMgr->CreateNode(TRUE));
                         ((ASTVec*)AssertsQuery)->push_back(*$1);                        
                         delete $1;
                       }
                 |      VarDecls Query 
                        { 
-                        //GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(TRUE),*$2); 
                         ((ASTVec*)AssertsQuery)->push_back(GlobalBeevMgr->CreateNode(TRUE));
                         ((ASTVec*)AssertsQuery)->push_back(*$2);
                         delete $2;
@@ -198,15 +195,9 @@ other_cmd       :      other_cmd1
                        {
                         ASTVec aaa = GlobalBeevMgr->GetAsserts();
                         if(aaa.size() == 0)
-                          yyerror("Fatal Error: parsing:  GetAsserts() call: no assertions: ");
-                        /* if(aaa.size() == 1) */
-                        /*                        { */
-                        /*GlobalBeevMgr->TopLevelSAT(aaa[0],*$2); */
-                        /*                        } */
-                        /*                      else */
-                        /*                        { */
-                        /*GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(AND,aaa),*$2); */
-                        /*                        } */
+                          {
+                            yyerror("Fatal Error: parsing:  GetAsserts() call: no assertions: ");
+                          }
                         ASTNode asserts = GlobalBeevMgr->CreateNode(AND,aaa);
                         ((ASTVec*)AssertsQuery)->push_back(asserts);
                         ((ASTVec*)AssertsQuery)->push_back(*$2);

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index ccec3904f9e0b0400c545c0472114da540999dd5..1903ac00ffee0b2b605533ba12a8d283385b3b78 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -60,6 +60,7 @@
 #define YYMAXDEPTH 104857600
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
+#define YYPARSE_PARAM AssertsQuery
 %}
 
 %union {  
@@ -206,19 +207,23 @@ cmd:
     benchmark
     {
       ASTNode assumptions;
-      if($1 == NULL) {
-        assumptions = GlobalBeevMgr->CreateNode(TRUE);
-      } else {
+      if($1 == NULL) 
+       {
+         assumptions = GlobalBeevMgr->CreateNode(TRUE);
+       } 
+      else 
+       {
         assumptions = *$1;
-      }
-
-      if(query.IsNull()) {
-        query = GlobalBeevMgr->CreateNode(FALSE);
-      }
+       }
+      
+      if(query.IsNull()) 
+       {
+         query = GlobalBeevMgr->CreateNode(FALSE);
+       }
 
-      GlobalBeevMgr->TopLevelSAT(assumptions, query);
+      ((ASTVec*)AssertsQuery)->push_back(assumptions);
+      ((ASTVec*)AssertsQuery)->push_back(query);
       delete $1;
-
       YYACCEPT;
     }
 ;