From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 5 Sep 2009 00:13:52 +0000 (+0000)
Subject: changed the smt parser as well to return objects
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e5cdb222b3a9094b41ddb87d7881e86a6c39c1ab;p=francis%2Fstp.git

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 3331ab9..8a25a4b 100644
--- 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 54c2d2c..251fbf4 100644
--- 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 ccec390..1903ac0 100644
--- 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;
     }
 ;