diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 30 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 17 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 34 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 24 |
4 files changed, 70 insertions, 35 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 7df5fb492..1d622cd1b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -42,10 +42,14 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap, +CnfStream::CnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap, std::string name) - : d_satSolver(satSolver), + : d_env(env), + d_satSolver(satSolver), d_booleanVariables(context), d_nodeToLiteralMap(context), d_literalToNodeMap(context), @@ -54,13 +58,17 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, d_registrar(registrar), d_name(name), d_cnfProof(NULL), - d_removable(false) { + d_removable(false) +{ } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, +TseitinCnfStream::TseitinCnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, context::Context* context, - bool fullLitToNodeMap, std::string name) - : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name) + bool fullLitToNodeMap, + std::string name) + : CnfStream(env, satSolver, registrar, context, fullLitToNodeMap, name) {} void CnfStream::assertClause(TNode node, SatClause& c) { @@ -155,8 +163,8 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { n = n[0]; } - if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL && - !n.isVar() ) { + if (d_env->theoryOf(n) == theory::THEORY_BOOL && !n.isVar()) + { // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. @@ -166,7 +174,9 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // These may already exist d_literalToNodeMap.insert_safe(lit, n); d_literalToNodeMap.insert_safe(~lit, n.notNode()); - } else { + } + else + { // We have a theory atom or variable. lit = convertAtom(n, noPreregistration); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a9b786615..3a4cfe209 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -31,6 +31,7 @@ #include "proof/proof_manager.h" #include "prop/registrar.h" #include "prop/theory_proxy.h" +#include "smt/environment.h" #include "smt_util/lemma_channels.h" namespace CVC4 { @@ -54,6 +55,8 @@ class CnfStream { NodeToLiteralMap; protected: + Environment* d_env; + /** The SAT solver we will be using */ SatSolver* d_satSolver; @@ -171,8 +174,11 @@ class CnfStream { * @param name string identifier to distinguish between different instances * even for non-theory literals. */ - CnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap = false, + CnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap = false, std::string name = ""); /** @@ -257,8 +263,11 @@ class TseitinCnfStream : public CnfStream { * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, - context::Context* context, bool fullLitToNodeMap = false, + TseitinCnfStream(Environment* env, + SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + bool fullLitToNodeMap = false, std::string name = ""); /** diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8a0cc9f15..abb90e569 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -74,19 +74,25 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, - Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels) : - d_inCheckSat(false), - d_theoryEngine(te), - d_decisionEngine(de), - d_context(satContext), - d_theoryProxy(NULL), - d_satSolver(NULL), - d_registrar(NULL), - d_cnfStream(NULL), - d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) +PropEngine::PropEngine(Environment* env, + TheoryEngine* te, + DecisionEngine* de, + Context* satContext, + Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* channels) + : d_env(env), + d_inCheckSat(false), + d_theoryEngine(te), + d_decisionEngine(de), + d_context(satContext), + d_theoryProxy(NULL), + d_satSolver(NULL), + d_registrar(NULL), + d_cnfStream(NULL), + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -95,7 +101,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream( - d_satSolver, d_registrar, userContext, true); + d_env, d_satSolver, d_registrar, userContext, true); d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index aaa65b85a..735c82bde 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,6 +28,7 @@ #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" +#include "smt/environment.h" #include "smt_util/lemma_channels.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -54,6 +55,7 @@ class PropEngine; * solving the SAT problem and conversion to CNF (via the CnfStream). */ class PropEngine { + Environment* d_env; /** * Indicates that the SAT solver is currently solving something and we should @@ -93,14 +95,18 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); -public: - + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, - context::Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels); + PropEngine(Environment* env, + TheoryEngine*, + DecisionEngine*, + context::Context* satContext, + context::Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream, + LemmaChannels* channels); /** * Destructor. @@ -114,7 +120,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { } + void shutdown() {} /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -134,7 +140,11 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); + void assertLemma(TNode node, + bool negated, + bool removable, + ProofRule rule, + TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This |