Fix the SMTLIB2 application language parser.

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

diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
index cca62c6c4e2a8c1a70a96df71a4b84595bf61fcf..eeccaaae84e2bfae463ad8aa608affca84a5340b 100644 (file)
--- a/src/cpp_interface/cpp_interface.cpp
+++ b/src/cpp_interface/cpp_interface.cpp
@@ -2,70 +2,62 @@
 
 namespace BEEV
 {
-    // Does some simple caching of prior results.
-    // Assumes that there is one node for each level!!!
-    void
-    Cpp_interface::checkSat(const ASTVec & assertionsSMT2)
-    {
-      bm.GetRunTimes()->stop(RunTimes::Parsing);
-
-      assert(assertionsSMT2.size() == cache.size());
-
-      Entry& cacheEntry = cache.back();
-
-      if ((cacheEntry.result ==  SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE)
-          && (assertionsSMT2.back() == cacheEntry.node))
-        { // If we already know the answer then return.
-          if (bm.UserFlags.quick_statistics_flag)
-            {
-              bm.GetRunTimes()->print();
-            }
-
-          (GlobalSTP->tosat)->PrintOutput(cache.back().result);
-          bm.GetRunTimes()->start(RunTimes::Parsing);
-          return;
-        }
-
-      bm.ClearAllTables();
-      GlobalSTP->ClearAllTables();
+  // Does some simple caching of prior results.
+  void
+  Cpp_interface::checkSat(const ASTVec & assertionsSMT2)
+  {
+    bm.GetRunTimes()->stop(RunTimes::Parsing);
+
+    checkInvariant();
+    assert(assertionsSMT2.size() == cache.size());
+
+    Entry& last_run = cache.back();
+    if ((last_run.node_number != assertionsSMT2.back().GetNodeNum()) && (last_run.result == SOLVER_SATISFIABLE))
+      {
+        // extra asserts might have been added to it,
+        // flipping from sat to unsat. But never from unsat to sat.
+        last_run.result =  SOLVER_UNDECIDED;
+      }
+
+    // We might have run this query before, or it might already be shown to be unsat. If it was sat,
+    // we've stored the result (but not the model), so we can shortcut and return what we know.
+    if (!((last_run.result == SOLVER_SATISFIABLE) || last_run.result == SOLVER_UNSATISFIABLE))
+        {
+          resetSolver();
 
-      ASTNode query;
+          ASTNode query;
 
-      if (assertionsSMT2.size() >= 1)
-        query = parserInterface->CreateNode(AND, assertionsSMT2);
-      else if (assertionsSMT2.size() == 1)
-        query = assertionsSMT2[0];
-      else
-        query = bm.ASTTrue;
+          if (assertionsSMT2.size() >= 1)
+            query = parserInterface->CreateNode(AND, assertionsSMT2);
+          else if (assertionsSMT2.size() == 1)
+            query = assertionsSMT2[0];
+          else
+            query = bm.ASTTrue;
 
-      SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse);
+          SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse);
 
-      // Write in the answer to the current slot.
-      if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE)
-          {
-            Entry e(last_result);
-            e.node = assertionsSMT2.back();
-            cacheEntry = e;
-            assert (!cacheEntry.node.IsNull());
-          }
+          // Store away the answer. Might be timeout, or error though..
+          last_run = Entry(last_result);
+          last_run.node_number = assertionsSMT2.back().GetNodeNum();
 
-      // It's satisfiable, so everything beneath it is satisfiable too.
-      if (last_result ==SOLVER_SATISFIABLE)
-        {
-          for (int i=0; i < cache.size(); i++)
-              {
-              assert(cache[i].result != SOLVER_UNSATISFIABLE);
-              cache[i].result = SOLVER_SATISFIABLE;
-              }
+          // It's satisfiable, so everything beneath it is satisfiable too.
+          if (last_result == SOLVER_SATISFIABLE)
+            {
+              for (int i = 0; i < cache.size(); i++)
+                {
+                  assert(cache[i].result != SOLVER_UNSATISFIABLE);
+                  cache[i].result = SOLVER_SATISFIABLE;
+                }
+            }
         }
 
-      if (bm.UserFlags.quick_statistics_flag)
-        {
-          bm.GetRunTimes()->print();
-        }
+    if (bm.UserFlags.quick_statistics_flag)
+      {
+        bm.GetRunTimes()->print();
+      }
 
-      (GlobalSTP->tosat)->PrintOutput(last_result);
-      //printStatus();
-      bm.GetRunTimes()->start(RunTimes::Parsing);
-    }
-};
+    (GlobalSTP->tosat)->PrintOutput(last_run.result);
+    bm.GetRunTimes()->start(RunTimes::Parsing);
+  }
+}
+;

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index 3e2b39f0641fb5ff89c7629d3c5efcc99cd1b4ba..1f41f77e4489f555f985b5ed9de8b334ae68af83 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -29,10 +29,11 @@ namespace BEEV
       Entry(SOLVER_RETURN_TYPE result_)
       {
         result = result_;
+        node_number = -1;
       }
 
       SOLVER_RETURN_TYPE result;
-      ASTNode node;
+      int node_number; // a weak pointer.
 
       void
       print()
@@ -247,6 +248,14 @@ namespace BEEV
         }
     }
 
+    // Resets the tables used by STP, but keeps all the nodes that have been created.
+    void
+    resetSolver()
+    {
+      bm.ClearAllTables();
+      GlobalSTP->ClearAllTables();
+    }
+
     void
     pop()
     {
@@ -257,7 +266,10 @@ namespace BEEV
 
       bm.Pop();
 
-      assert(symbols.size() == cache.size());
+      // These tables might hold references to symbols that have been
+      // removed.
+      resetSolver();
+
       cache.erase(cache.end() - 1);
       ASTVec & current = symbols.back();
       for (int i = 0; i < current.size(); i++)
@@ -277,7 +289,7 @@ namespace BEEV
 
       bm.Push();
       symbols.push_back(ASTVec());
-      assert(symbols.size() == cache.size());
+
       checkInvariant();
     }