From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 4 Apr 2012 02:43:37 +0000 (+0000)
Subject: improvement. Add the ability to the cpp interface to ignore calls to sat.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=48dda8decef2928f8924a61c6e897e3a6d3e3fde;p=francis%2Fstp.git

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 ae62ba2..c96a8b2 100644
--- 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 bfc8618..b3a891b 100644
--- 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()
     {