From 48dda8decef2928f8924a61c6e897e3a6d3e3fde Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 4 Apr 2012 02:43:37 +0000 Subject: [PATCH] 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 --- src/cpp_interface/cpp_interface.cpp | 3 +++ src/cpp_interface/cpp_interface.h | 9 +++++++++ 2 files changed, 12 insertions(+) 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 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() { -- 2.47.3