improvement. Add the ability to the cpp interface to ignore calls to sat.

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

diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
index ae62ba2720c68c313aac93a94074c449a5bea3e5..c96a8b20339d78e46bca96b5b3b751ffebbeeb07 100644 (file)
--- a/src/cpp_interface/cpp_interface.cpp
+++ b/src/cpp_interface/cpp_interface.cpp
@@ -6,6 +6,9 @@ namespace BEEV
   void
   Cpp_interface::checkSat(const ASTVec & assertionsSMT2)
   {
+    if (ignoreCheckSatRequest)
+      return;
+
     bm.GetRunTimes()->stop(RunTimes::Parsing);
 
     checkInvariant();

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index bfc86181d7cc60d29b24f4fca3b8670d3629a15e..b3a891b89913f83d6992df16d5dad6bafdc4e1c6 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -21,6 +21,7 @@ namespace BEEV
     //boost::object_pool<ASTNode> node_pool;
     bool alreadyWarned;
     bool print_success;
+    bool ignoreCheckSatRequest;
 
     // Used to cache prior queries.
     struct Entry
@@ -72,6 +73,7 @@ namespace BEEV
         bm.Push();
 
       print_success = false;
+      ignoreCheckSatRequest=false;
     }
 
     void
@@ -304,6 +306,13 @@ namespace BEEV
       checkInvariant();
     }
 
+    // Useful when printing back, so that you can parse, but ignore the request.
+    void
+    ignoreCheckSat()
+    {
+      ignoreCheckSatRequest=  true;
+    }
+
     void
     printStatus()
     {