diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 11 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 8 | ||||
-rw-r--r-- | src/prop/sat_solver_types.h | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 13 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 9 |
5 files changed, 36 insertions, 8 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index abe22cb48..848c63a18 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): barrett, taking, cconway + ** Minor contributors (to current version): barrett, taking, cconway, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -22,6 +22,7 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "decision/decision_engine.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/Assert.h" @@ -61,9 +62,10 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, Context* context) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : d_inCheckSat(false), d_theoryEngine(te), + d_decisionEngine(de), d_context(context), d_satSolver(NULL), d_cnfStream(NULL), @@ -77,7 +79,10 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) : theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1); - d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_context, d_cnfStream)); + d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); + + d_decisionEngine->setSatSolver(d_satSolver); + d_decisionEngine->setCnfStream(d_cnfStream); } PropEngine::~PropEngine() { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 93c35bbf3..3d114db3a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking, dejan - ** Minor contributors (to current version): cconway, barrett + ** Minor contributors (to current version): cconway, barrett, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -31,6 +31,7 @@ namespace CVC4 { +class DecisionEngine; class TheoryEngine; namespace prop { @@ -127,6 +128,9 @@ class PropEngine { /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; + /** The decision engine we will be using */ + DecisionEngine *d_decisionEngine; + /** The context */ context::Context* d_context; @@ -153,7 +157,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, context::Context*); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context*); /** * Destructor. diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 406782468..0da4d7a6a 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -26,6 +26,9 @@ #include "cvc4_private.h" +#include <string> +#include <sstream> + namespace CVC4 { namespace prop { diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 43f7f75af..f024dccf3 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: dejan, taking, mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -24,6 +24,8 @@ #include "theory/theory_engine.h" #include "theory/rewriter.h" #include "expr/expr_stream.h" +#include "decision/decision_engine.h" + namespace CVC4 { namespace prop { @@ -73,7 +75,14 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { SatLiteral TheoryProxy::getNextDecisionRequest() { TNode n = d_theoryEngine->getNextDecisionRequest(); - return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); + if(not n.isNull()) + return d_cnfStream->getLiteral(n); + + // If theory doesn't give us a deicsion ask the decision engine. It + // may return in undefSatLiteral in which case the sat solver figure + // it out something + Assert(d_decisionEngine != NULL); + return d_decisionEngine->getNext(); } bool TheoryProxy::theoryNeedCheck() const { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 8b585710f..ceb328d90 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking, cconway, dejan - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): barrett, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -33,6 +33,7 @@ namespace CVC4 { +class DecisionEngine; class TheoryEngine; namespace prop { @@ -51,6 +52,9 @@ class TheoryProxy { /** The CNF engine we are using */ CnfStream* d_cnfStream; + /** The decision engine we are using */ + DecisionEngine* d_decisionEngine; + /** The theory engine we are using */ TheoryEngine* d_theoryEngine; @@ -66,6 +70,7 @@ class TheoryProxy { public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream); @@ -113,10 +118,12 @@ public: inline TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), + d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), d_context(context) {} |