diff options
Diffstat (limited to 'src/decision/decision_engine.h')
-rw-r--r-- | src/decision/decision_engine.h | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 3ec6aaf2a..ea516aa54 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -27,6 +27,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" +#include "util/ite_removal.h" #include "util/output.h" using namespace std; @@ -38,7 +39,7 @@ namespace CVC4 { class DecisionEngine { vector <DecisionStrategy* > d_enabledStrategies; - vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions; + vector <ITEDecisionStrategy* > d_needIteSkolemMap; vector <Node> d_assertions; @@ -47,13 +48,16 @@ class DecisionEngine { DPLLSatSolverInterface* d_satSolver; context::Context* d_satContext; + context::Context* d_userContext; SatValue d_result; + // Disable creating decision engine without required parameters + DecisionEngine() {} public: // Necessary functions /** Constructor, enables decision stragies based on options */ - DecisionEngine(context::Context *c); + DecisionEngine(context::Context *sc, context::Context *uc); /** Destructor, currently does nothing */ ~DecisionEngine() { @@ -88,6 +92,11 @@ public: /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool &stopSearch) { + Assert(d_cnfStream != NULL, + "Forgot to set cnfStream for decision engine?"); + Assert(d_satSolver != NULL, + "Forgot to set satSolver for decision engine?"); + SatLiteral ret = undefSatLiteral; for(unsigned i = 0; i < d_enabledStrategies.size() @@ -113,7 +122,7 @@ public: case SAT_VALUE_TRUE: return Result(Result::SAT); case SAT_VALUE_FALSE: return Result(Result::UNSAT); case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - default: Assert(false); + default: Assert(false, "d_result is garbage"); } return Result(); } @@ -137,11 +146,24 @@ public: // External World helping us help the Strategies /** If one of the enabled strategies needs them */ - bool needSimplifiedPreITEAssertions() { - return d_needSimplifiedPreITEAssertions.size() > 0; - } - void informSimplifiedPreITEAssertions(const vector<Node> &assertions); + /* bool needIteSkolemMap() { */ + /* return d_needIteSkolemMap.size() > 0; */ + /* } */ + /* add a set of assertions */ + void addAssertions(const vector<Node> &assertions); + + /** + * add a set of assertions, while providing a mapping between skolem + * variables and corresponding assertions. It is assumed that all + * assertions after assertionEnd were generated by ite + * removal. Hence, iteSkolemMap maps into only these. + */ + void addAssertions(const vector<Node> &assertions, + int assertionsEnd, + IteSkolemMap iteSkolemMap); + + /* add a single assertion */ void addAssertion(Node n); // Interface for Strategies to use stuff stored in Decision Engine @@ -157,15 +179,18 @@ public: // Interface for Strategies to get information about External World - bool hasSatLiteral(Node n) { + bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } - SatLiteral getSatLiteral(Node n) { + SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } + SatValue getSatValue(TNode n) { + return getSatValue(getSatLiteral(n)); + } Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } |