Improvement. The SMT-LIB2 parser no longer stores a copy of the asserts/query locally...

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 4592366f5829495f1543f910891f233aaa012272..11df009c002fa5cb8188a97762dae3cf57d3305c 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -485,6 +485,32 @@ namespace BEEV
     return _current_query;
   }
 
+  // return a vector of the levels.
+  // before returning any vector with >1 nodes is turned into a conjunct.
+  const ASTVec STPMgr::getVectorOfAsserts()
+  {
+    vector<ASTVec *>::iterator it = _asserts.begin();
+    vector<ASTVec *>::iterator itend = _asserts.end();
+
+    ASTVec result;
+    for(; it != itend; it++)
+      {
+        ASTVec& a = (**it);
+        if (a.size() ==0)
+          a.push_back(ASTTrue);
+        else if (a.size() > 1)
+          {
+            ASTNode conjunct = defaultNodeFactory->CreateNode(AND,a);
+            a.resize(0);
+            a.push_back(conjunct);
+          }
+
+        result.push_back(a[0]);
+     }
+
+    return result;
+  }
+
   const ASTVec
   STPMgr::GetAsserts(void)
   {

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 937e2cb3211678f7d39795c5d84812c5ec209024..bf472824536cc7e094a32d16bd0aae6b7d1894d7 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -113,6 +113,11 @@ namespace BEEV
             {(*it)->iteration = 0;}
     }
 
+    int getAssertLevel()
+    {
+      return _asserts.size();
+    }
+
   private:
 
     // Stack of Logical Context. each entry in the stack is a logical
@@ -388,7 +393,9 @@ namespace BEEV
     void Push(void);    
     const ASTNode PopQuery();
     const ASTNode GetQuery();
-    const ASTVec GetAsserts(void);
+    const ASTVec GetAsserts();
+    const ASTVec getVectorOfAsserts();
+
 
     //add a query/assertion to the current logical context
     void AddQuery(const ASTNode& q);

diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
index f1ebb5095d38ea0cf89cad90ed133640ea51218f..cca62c6c4e2a8c1a70a96df71a4b84595bf61fcf 100644 (file)
--- a/src/cpp_interface/cpp_interface.cpp
+++ b/src/cpp_interface/cpp_interface.cpp
@@ -2,22 +2,19 @@
 
 namespace BEEV
 {
-
-
-// Does some simple caching of prior results.
+    // Does some simple caching of prior results.
+    // Assumes that there is one node for each level!!!
     void
-    Cpp_interface::checkSat(vector<ASTVec> & assertionsSMT2)
+    Cpp_interface::checkSat(const ASTVec & assertionsSMT2)
     {
       bm.GetRunTimes()->stop(RunTimes::Parsing);
+
       assert(assertionsSMT2.size() == cache.size());
 
       Entry& cacheEntry = cache.back();
 
-      //cerr << "------------" << endl;
-      //printStatus();
-
       if ((cacheEntry.result ==  SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE)
-          && (assertionsSMT2.back().size() ==1 && assertionsSMT2.back()[0] == cacheEntry.node))
+          && (assertionsSMT2.back() == cacheEntry.node))
         { // If we already know the answer then return.
           if (bm.UserFlags.quick_statistics_flag)
             {
@@ -32,30 +29,12 @@ namespace BEEV
       bm.ClearAllTables();
       GlobalSTP->ClearAllTables();
 
-      // Loop through the set of assertions converting them to single nodes..
-      ASTVec v;
-      for (int i = 0; i < assertionsSMT2.size(); i++)
-        {
-          if (assertionsSMT2[i].size() == 1)
-            {}
-          else if (assertionsSMT2[i].size() == 0)
-            assertionsSMT2[i].push_back(bm.ASTTrue);
-          else
-            {
-              ASTNode v = parserInterface->CreateNode(AND, assertionsSMT2[i]);
-              assertionsSMT2[i].clear();
-              assertionsSMT2[i].push_back(v);
-            }
-          assert(assertionsSMT2[i].size() ==1);
-          v.push_back(assertionsSMT2[i][0]);
-        }
-
       ASTNode query;
 
-      if (v.size() > 1)
-        query = parserInterface->CreateNode(AND, v);
-      else if (v.size() > 0)
-        query = v[0];
+      if (assertionsSMT2.size() >= 1)
+        query = parserInterface->CreateNode(AND, assertionsSMT2);
+      else if (assertionsSMT2.size() == 1)
+        query = assertionsSMT2[0];
       else
         query = bm.ASTTrue;
 
@@ -65,7 +44,7 @@ namespace BEEV
       if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE)
           {
             Entry e(last_result);
-            e.node = assertionsSMT2.back()[0];
+            e.node = assertionsSMT2.back();
             cacheEntry = e;
             assert (!cacheEntry.node.IsNull());
           }

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index 5b7e4a970547b9fae8c053e3b39bd8a85f7bdfbe..3e2b39f0641fb5ff89c7629d3c5efcc99cd1b4ba 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -48,6 +48,11 @@ namespace BEEV
     vector<Entry> cache;
     vector<vector<ASTNode> > symbols;
 
+    void checkInvariant()
+    {
+      assert(bm.getAssertLevel() == cache.size());
+      assert(bm.getAssertLevel() == symbols.size());
+    }
 
   public:
     LETMgr letMgr;
@@ -58,8 +63,13 @@ namespace BEEV
     {
       assert(nf != NULL);
       alreadyWarned = false;
+
       cache.push_back(Entry(SOLVER_UNDECIDED));
       symbols.push_back(ASTVec());
+
+      if (bm.getVectorOfAsserts().size() ==0)
+        bm.Push();
+
       print_success = false;
     }
 
@@ -79,6 +89,12 @@ namespace BEEV
       return bm.GetAsserts();
     }
 
+    const ASTVec
+    getAssertVector(void)
+    {
+      return bm.getVectorOfAsserts();
+    }
+
     UserDefinedFlags&
     getUserFlags()
     {
@@ -239,12 +255,15 @@ namespace BEEV
       if (symbols.size() == 1)
         FatalError("Can't pop away the default base element.");
 
+      bm.Pop();
+
       assert(symbols.size() == cache.size());
       cache.erase(cache.end() - 1);
       ASTVec & current = symbols.back();
       for (int i = 0; i < current.size(); i++)
         letMgr._parser_symbol_table.erase(current[i]);
       symbols.erase(symbols.end() - 1);
+      checkInvariant();
     }
 
     void
@@ -256,8 +275,10 @@ namespace BEEV
       else
         cache.push_back(Entry(SOLVER_UNDECIDED));
 
+      bm.Push();
       symbols.push_back(ASTVec());
       assert(symbols.size() == cache.size());
+      checkInvariant();
     }
 
     void
@@ -271,7 +292,7 @@ namespace BEEV
     }
 
     void
-    checkSat(vector<ASTVec> & assertionsSMT2);
+    checkSat(const ASTVec & assertionsSMT2);
 
     void
     cleanUp()

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d40acb4feacda37941cde4a7e827d5edc5bf194b..d5e127d3871d2ac2bba81c84be2500af0f373223 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -25,12 +25,11 @@ using namespace __gnu_cxx;
 using namespace BEEV;
 
 extern int smtparse(void*);
-extern int smt2parse(void*);
+extern int smt2parse();
 extern int cvcparse(void*);
 extern int cvclex_destroy(void);
 extern int smtlex_destroy(void);
 extern int smt2lex_destroy(void);
-extern vector<ASTVec> assertionsSMT2;
 
 // callback for SIGALRM.
 void handle_time_out(int parameter){
@@ -446,9 +445,7 @@ int main(int argc, char ** argv) {
                        smtparse((void*) AssertsQuery);
                        smtlex_destroy();
                } else if (bm->UserFlags.smtlib2_parser_flag) {
-                       assertionsSMT2.push_back(ASTVec());
-                       smt2parse((void*) AssertsQuery);
-                       //parserInterface->letMgr.cleanupParserSymbolTable();
+                       smt2parse();
                        smt2lex_destroy();
                } else {
                        cvcparse((void*) AssertsQuery);

diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index 332fbb6cec2929ff6575bff3085ffe46b8eb22c1..aa79897ad03a3eb933210d41ef537a2d04afeb9e 100644 (file)
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -65,14 +65,12 @@
     return 1;
   }
 
-  ASTNode querysmt2;
-  vector<ASTVec> assertionsSMT2;
-    
+   
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 104857600
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
-#define YYPARSE_PARAM AssertsQuery
+
   %}
 
 %union {  
@@ -195,8 +193,6 @@
 %%
 cmd: commands END
 {
-       querysmt2 = ASTNode();
-       assertionsSMT2.clear();
        parserInterface->cleanUp();
        YYACCEPT;
 }
@@ -211,14 +207,12 @@ commands: commands cmdi
 cmdi:
        LPAREN_TOK EXIT_TOK RPAREN_TOK
        {
-          querysmt2 = ASTNode();
-       assertionsSMT2.clear();
        parserInterface->cleanUp();
        YYACCEPT;
        }
 |      LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK
        {
-               parserInterface->checkSat(assertionsSMT2);
+               parserInterface->checkSat(parserInterface->getAssertVector());
        }
 |
        LPAREN_TOK LOGIC_TOK STRING_TOK RPAREN_TOK
@@ -247,17 +241,13 @@ cmdi:
                for (int i=0; i < $3;i++)
                {
                        parserInterface->push();
-                       assertionsSMT2.push_back(ASTVec());
                }
                parserInterface->success();
        }
 |      LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK
        {
                for (int i=0; i < $3;i++)
-               {
                        parserInterface->pop();
-                       assertionsSMT2.erase(assertionsSMT2.end()-1);
-               }
                parserInterface->success();
        }
 |   LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK
@@ -266,7 +256,7 @@ cmdi:
     }
 |   LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK
        {
-       assertionsSMT2.back().push_back(*$3);
+       parserInterface->AddAssert(*$3);
        parserInterface->deleteNode($3);
        parserInterface->success();
        }