namespace CVC4 {
-DecisionEngine::DecisionEngine() :
+DecisionEngine::DecisionEngine(context::Context *c) :
+ d_enabledStrategies(),
d_needSimplifiedPreITEAssertions(),
+ d_assertions(),
d_cnfStream(NULL),
- d_satSolver(NULL)
+ d_satSolver(NULL),
+ d_satContext(c),
+ d_result(SAT_VALUE_UNKNOWN)
{
const Options* options = Options::current();
Trace("decision") << "Creating decision engine" << std::endl;
+
+ if(options->incrementalSolving) return;
+
if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
- DecisionStrategy* ds = new decision::JustificationHeuristic(this);
+ DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext);
enableStrategy(ds);
}
}
void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
{
+ d_result = SAT_VALUE_UNKNOWN;
d_assertions.reserve(assertions.size());
for(unsigned i = 0; i < assertions.size(); ++i)
d_assertions.push_back(assertions[i]);
d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
}
+void DecisionEngine::addAssertion(Node n)
+{
+ d_result = SAT_VALUE_UNKNOWN;
+ if(needSimplifiedPreITEAssertions()) {
+ d_assertions.push_back(n);
+ }
+ for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
+ d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+}
+
+
}/* CVC4 namespace */
// PropEngine* d_propEngine;
CnfStream* d_cnfStream;
DPLLSatSolverInterface* d_satSolver;
+
+ SatValue d_result;
+
+ context::Context* d_satContext;
public:
// Necessary functions
/** Constructor, enables decision stragies based on options */
- DecisionEngine();
+ DecisionEngine(context::Context *c);
/** Destructor, currently does nothing */
~DecisionEngine() {
Trace("decision") << "Destroying decision engine" << std::endl;
+ for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
+ delete d_enabledStrategies[i];
}
// void setPropEngine(PropEngine* pe) {
// Interface for External World to use our services
/** Gets the next decision based on strategies that are enabled */
- SatLiteral getNext() {
+ SatLiteral getNext(bool &stopSearch) {
SatLiteral ret = undefSatLiteral;
- for(unsigned i = 0; i < d_enabledStrategies.size()
- and ret == undefSatLiteral; ++i) {
- ret = d_enabledStrategies[i]->getNext();
+ for(unsigned i = 0;
+ i < d_enabledStrategies.size()
+ and ret == undefSatLiteral
+ and stopSearch == false; ++i) {
+ ret = d_enabledStrategies[i]->getNext(stopSearch);
}
return ret;
}
+ /** Is the DecisionEngine in a state where it has solved everything? */
+ bool isDone() {
+ Trace("decision") << "DecisionEngine::isDone() returning "
+ << (d_result != SAT_VALUE_UNKNOWN)
+ << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
+ << std::endl;
+ return (d_result != SAT_VALUE_UNKNOWN);
+ }
+
+ /** */
+ Result getResult() {
+ switch(d_result) {
+ 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);
+ }
+ return Result();
+ }
+
+ /** */
+ void setResult(SatValue val) {
+ d_result = val;
+ }
+
/**
* This is called by SmtEngine, at shutdown time, just before
* destruction. It is important because there are destruction
}
void informSimplifiedPreITEAssertions(const vector<Node> &assertions);
+ void addAssertion(Node n);
// Interface for Strategies to use stuff stored in Decision Engine
// (which was possibly requested by them on initialization)
class DecisionEngine;
+namespace context {
+class Context;
+}
+
namespace decision {
class DecisionStrategy {
protected:
DecisionEngine* d_decisionEngine;
public:
- DecisionStrategy(DecisionEngine* de) :
+ DecisionStrategy(DecisionEngine* de, context::Context *c) :
d_decisionEngine(de) {
}
virtual ~DecisionStrategy() { }
- virtual prop::SatLiteral getNext() = 0;
+ virtual prop::SatLiteral getNext(bool&) = 0;
virtual bool needSimplifiedPreITEAssertions() { return false; }
#include "justification_heuristic.h"
+#include "expr/kind.h"
/***
***/
-void JustificationHeuristic::setJustified(SatVariable v)
+void JustificationHeuristic::setJustified(TNode n)
{
- d_justified.insert(v);
+ d_justified.insert(n);
}
-bool JustificationHeuristic::checkJustified(SatVariable v)
+bool JustificationHeuristic::checkJustified(TNode n)
{
- return d_justified.find(v) != d_justified.end();
+ return d_justified.find(n) != d_justified.end();
}
SatValue invertValue(SatValue v)
else return SAT_VALUE_TRUE;
}
-bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision)
+bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, SatLiteral* litDecision)
//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
{
- // if(not ) {
- // // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
- // return false;
- // // Assert(not lit.isNull());
- // }
-
- /**
- * TODO -- Base case. Way CVC3 seems to handle is that it has
- * literals correpsonding to true and false. We'll have to take care
- * somewhere else.
- */
+ Trace("decision")
+ << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl;
- // Var v = lit.getVar();
- SatVariable v = lit.getSatVariable();
- SatValue litVal = d_decisionEngine->getSatValue(lit);
+ /* Handle NOT as a special case */
+ if (node.getKind() == kind::NOT) {
+ desiredVal = invertValue(desiredVal);
+ node = node[0];
+ }
- // if (lit.isFalse() || lit.isTrue()) return false;
- if (v == 0) return false;
+ if (checkJustified(node)) return false;
+
+ SatValue litVal = tryGetSatValue(node);
+ bool litPresent = false;
+ if(d_decisionEngine->hasSatLiteral(node) ) {
+ SatLiteral lit = d_decisionEngine->getSatLiteral(node);
+ litPresent = true;
+
+ SatVariable v = lit.getSatVariable();
+ // if (lit.isFalse() || lit.isTrue()) return false;
+ if (v == 0) {
+ setJustified(node);
+ return false;
+ }
+ } else {
+ Trace("decision") << "no sat literal for this node" << std::endl;
+ }
/* You'd better know what you want */
- // DebugAssert(value != Var::UNKNOWN, "expected known value");
Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
/* Good luck, hope you can get what you want */
- // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
- // "invariant violated");
Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
"invariant voilated");
+ /* What type of node is this */
+ Kind k = node.getKind();
+ theory::TheoryId tId = theory::kindToTheoryId(k);
- if (checkJustified(v)) return false;
-
- if (lit.isNegated()) {
- desiredVal = invertValue(desiredVal);
- }
-
- Node node = d_decisionEngine->getNode(lit);
- Trace("decision") << "lit = " << lit << std::endl;
- Trace("decision") << node.getKind() << std::endl;
- Trace("decision") << node << std::endl;
+ /* Some debugging stuff */
+ Trace("findSpitterRec") << "kind = " << k << std::endl;
+ Trace("findSplitterRec") << "theoryId = " << tId << std::endl;
+ Trace("findSplitterRec") << "node = " << node << std::endl;
+ Trace("findSplitterRec") << "litVal = " << litVal << std::endl;
/*
if (d_cnfManager->numFanins(v) == 0) {
}
}
*/
- if(node.getNumChildren() == 0) {
+
+
+ /**
+ * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
+ * then check if this is something to split-on?
+ */
+ if(tId != theory::THEORY_BOOL
+ // && !(k == kind::EQUAL && node[0].getType().isBoolean())
+ ) {
if(litVal != SAT_VALUE_UNKNOWN) {
- setJustified(v);
+ setJustified(node);
return false;
} else {
- *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE );
+ if(not d_decisionEngine->hasSatLiteral(node))
+ throw GiveUpException();
+ Assert(d_decisionEngine->hasSatLiteral(node));
+ SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
+ *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+ Trace("decision") << "decision " << *litDecision << std::endl;
+ Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
return true;
}
}
+ /*** TODO: Term ITEs ***/
/*
else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
// This node represents a predicate with embedded ITE's
return true;
}
}
+ */
- int kind = d_cnfManager->concreteVar(v).getKind();
- Var::Val valHard = Var::FALSE_VAL;
- switch (kind) {
- case AND:
- valHard = Var::TRUE_VAL;
- case OR:
- if (value == valHard) {
- n = d_cnfManager->numFanins(v);
- for (i=0; i < n; ++i) {
- litTmp = d_cnfManager->getFanin(v, i);
- if (findSplitterRec(litTmp, valHard, litDecision)) {
- return true;
- }
- }
- DebugAssert(getValue(v) == valHard, "Output should be justified");
- setJustified(v);
- return false;
- }
- else {
- Var::Val valEasy = Var::invertValue(valHard);
- n = d_cnfManager->numFanins(v);
- for (i=0; i < n; ++i) {
- litTmp = d_cnfManager->getFanin(v, i);
- if (getValue(litTmp) != valHard) {
- if (findSplitterRec(litTmp, valEasy, litDecision)) {
- return true;
- }
- DebugAssert(getValue(v) == valEasy, "Output should be justified");
- setJustified(v);
- return false;
- }
- }
- DebugAssert(false, "No controlling input found (2)");
- }
- break;
- case IMPLIES:
- DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins");
- if (value == Var::FALSE_VAL) {
- litTmp = d_cnfManager->getFanin(v, 0);
- if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+ SatValue valHard = SAT_VALUE_FALSE;
+ switch (k) {
+ case kind::AND:
+ valHard = SAT_VALUE_TRUE;
+ case kind::OR:
+ if (desiredVal == valHard) {
+ int n = node.getNumChildren();
+ for(int i = 0; i < n; ++i) {
+ if (findSplitterRec(node[i], valHard, litDecision)) {
return true;
}
- litTmp = d_cnfManager->getFanin(v, 1);
- if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
- return true;
- }
- DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified");
- setJustified(v);
- return false;
}
- else {
- litTmp = d_cnfManager->getFanin(v, 0);
- if (getValue(litTmp) != Var::TRUE_VAL) {
- if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
- return true;
- }
- DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
- setJustified(v);
- return false;
- }
- litTmp = d_cnfManager->getFanin(v, 1);
- if (getValue(litTmp) != Var::FALSE_VAL) {
- if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+ Assert(litPresent == false || litVal == valHard, "Output should be justified");
+ setJustified(node);
+ return false;
+ }
+ else {
+ SatValue valEasy = invertValue(valHard);
+ int n = node.getNumChildren();
+ for(int i = 0; i < n; ++i) {
+ Trace("findSplitterRec") << " node[i] = " << node[i] << " " << tryGetSatValue(node[i]) << std::endl;
+ if ( tryGetSatValue(node[i]) != valHard) {
+ Trace("findSplitterRec") << "hi"<< std::endl;
+ if (findSplitterRec(node[i], valEasy, litDecision)) {
return true;
}
- DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
- setJustified(v);
+ Assert(litPresent == false || litVal == valEasy, "Output should be justified");
+ setJustified(node);
return false;
}
- DebugAssert(false, "No controlling input found (3)");
}
- break;
- case IFF: {
- litTmp = d_cnfManager->getFanin(v, 0);
- Var::Val val = getValue(litTmp);
- if (val != Var::UNKNOWN) {
- if (findSplitterRec(litTmp, val, litDecision)) {
- return true;
- }
- if (value == Var::FALSE_VAL) val = Var::invertValue(val);
- litTmp = d_cnfManager->getFanin(v, 1);
+ Trace("findSplitterRec") << " * ** " << std::endl;
+ Trace("findSplitterRec") << node.getKind() << " " << node << std::endl;
+ for(unsigned i = 0; i < node.getNumChildren(); ++i)
+ Trace("findSplitterRec") << "child: " << tryGetSatValue(node[i]) << std::endl;
+ Trace("findSplitterRec") << "node: " << tryGetSatValue(node) << std::endl;
+ Assert(false, "No controlling input found (2)");
+ }
+ break;
- if (findSplitterRec(litTmp, val, litDecision)) {
- return true;
- }
- DebugAssert(getValue(v) == value, "Output should be justified");
- setJustified(v);
- return false;
+ case kind::IMPLIES:
+ //throw GiveUpException();
+ Assert(node.getNumChildren() == 2, "Expected 2 fanins");
+ if (desiredVal == SAT_VALUE_FALSE) {
+ if (findSplitterRec(node[0], SAT_VALUE_TRUE, litDecision)) {
+ return true;
}
- else {
- val = getValue(d_cnfManager->getFanin(v, 1));
- if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
- if (value == Var::FALSE_VAL) val = Var::invertValue(val);
- if (findSplitterRec(litTmp, val, litDecision)) {
- return true;
- }
- DebugAssert(false, "Unable to find controlling input (4)");
+ if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) {
+ return true;
}
- break;
+ Assert(litPresent == false || litVal == SAT_VALUE_FALSE, "Output should be justified");
+ setJustified(node);
+ return false;
}
- case XOR: {
- litTmp = d_cnfManager->getFanin(v, 0);
- Var::Val val = getValue(litTmp);
- if (val != Var::UNKNOWN) {
- if (findSplitterRec(litTmp, val, litDecision)) {
- return true;
- }
- if (value == Var::TRUE_VAL) val = Var::invertValue(val);
- litTmp = d_cnfManager->getFanin(v, 1);
- if (findSplitterRec(litTmp, val, litDecision)) {
+ else {
+ if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
+ if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) {
return true;
}
- DebugAssert(getValue(v) == value, "Output should be justified");
- setJustified(v);
+ Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+ setJustified(node);
return false;
}
- else {
- val = getValue(d_cnfManager->getFanin(v, 1));
- if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
- if (value == Var::TRUE_VAL) val = Var::invertValue(val);
- if (findSplitterRec(litTmp, val, litDecision)) {
+ if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
+ if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) {
return true;
}
- DebugAssert(false, "Unable to find controlling input (5)");
+ Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+ setJustified(node);
+ return false;
+ }
+ Assert(false, "No controlling input found (3)");
+ }
+ break;
+ case kind::IFF:
+ //throw GiveUpException();
+ {
+ SatValue val = tryGetSatValue(node[0]);
+ if (val != SAT_VALUE_UNKNOWN) {
+ if (findSplitterRec(node[0], val, litDecision)) {
+ return true;
}
- break;
+ if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+
+ if (findSplitterRec(node[1], val, litDecision)) {
+ return true;
+ }
+ Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+ setJustified(node);
+ return false;
}
+ else {
+ val = tryGetSatValue(node[1]);
+ if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+ if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+ if (findSplitterRec(node[0], val, litDecision)) {
+ return true;
+ }
+ Assert(false, "Unable to find controlling input (4)");
+ }
+ break;
+ }
+
+ case kind::XOR:
+ //throw GiveUpException();
+ {
+ SatValue val = tryGetSatValue(node[0]);
+ if (val != SAT_VALUE_UNKNOWN) {
+ if (findSplitterRec(node[0], val, litDecision)) {
+ return true;
+ }
+ if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+
+ if (findSplitterRec(node[1], val, litDecision)) {
+ return true;
+ }
+ Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+ setJustified(node);
+ return false;
+ }
+ else {
+ SatValue val = tryGetSatValue(node[1]);
+ if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+ if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+ if (findSplitterRec(node[0], val, litDecision)) {
+ return true;
+ }
+ Assert(false, "Unable to find controlling input (5)");
+ }
+ break;
+ }
+
+ case kind::ITE:
+ throw GiveUpException();
+ /*
case ITE: {
Lit cIf = d_cnfManager->getFanin(v, 0);
Lit cThen = d_cnfManager->getFanin(v, 1);
setJustified(v);
return false;
}
- default:
- DebugAssert(false, "Unexpected Boolean operator");
- break;
+ */
+ default:
+ Assert(false, "Unexpected Boolean operator");
+ break;
}
- FatalAssert(false, "Should be unreachable");
- ------------------------------------------------ */
- return false;
+ /* Swap order of these two once we handle all cases */
+ return false;
Unreachable();
+
}/* findRecSplit method */
#include "decision_engine.h"
#include "decision_strategy.h"
-#include "prop/sat_solver_types.h"
+#include "context/cdhashset.h"
#include "expr/node.h"
-
-using namespace CVC4::prop;
+#include "prop/sat_solver_types.h"
namespace CVC4 {
namespace decision {
+class GiveUpException : public Exception {
+public:
+ GiveUpException() :
+ Exception("justification hueristic: giving up") {
+ }
+};/* class GiveUpException */
+
class JustificationHeuristic : public DecisionStrategy {
- set<SatVariable> d_justified;
- unsigned d_prvsIndex;
+ context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+ context::CDO<unsigned> d_prvsIndex;
+ IntStat d_helfulness;
+ IntStat d_giveup;
+ TimerStat d_timestat;
public:
- JustificationHeuristic(CVC4::DecisionEngine* de) :
- DecisionStrategy(de) {
+ JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
+ DecisionStrategy(de, c),
+ d_justified(c),
+ d_prvsIndex(c, 0),
+ d_helfulness("decision::jh::helpfulness", 0),
+ d_giveup("decision::jh::giveup", 0),
+ d_timestat("decision::jh::time") {
+ StatisticsRegistry::registerStat(&d_helfulness);
+ StatisticsRegistry::registerStat(&d_giveup);
+ StatisticsRegistry::registerStat(&d_timestat);
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
- prop::SatLiteral getNext() {
+ ~JustificationHeuristic() {
+ StatisticsRegistry::unregisterStat(&d_helfulness);
+ StatisticsRegistry::unregisterStat(&d_timestat);
+ }
+ prop::SatLiteral getNext(bool &stopSearch) {
Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
+ TimerStat::CodeTimer codeTimer(d_timestat);
+
const vector<Node>& assertions = d_decisionEngine->getAssertions();
for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) {
SatLiteral litDecision;
- /* Make sure there is a literal corresponding to the node */
- if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) {
- // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
- continue;
+ Trace("decision") << assertions[i] << std::endl;
+
+ SatValue desiredVal = SAT_VALUE_UNKNOWN;
+
+ if(d_decisionEngine->hasSatLiteral(assertions[i]) ) {
+ //desiredVal = d_decisionEngine->getSatValue( d_decisionEngine->getSatLiteral(assertions[i]) );
+ Trace("decision") << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
+ // continue;
// Assert(not lit.isNull());
}
-
- SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]);
- SatValue desiredVal = d_decisionEngine->getSatValue(lit);
+
if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE;
- bool ret = findSplitterRec(lit, desiredVal, &litDecision);
+
+ bool ret;
+ try {
+ ret = findSplitterRec(assertions[i], desiredVal, &litDecision);
+ }catch(GiveUpException &e) {
+ return prop::undefSatLiteral;
+ }
if(ret == true) {
- d_prvsIndex = i;
+ Trace("decision") << "Yippee!!" << std::endl;
+ //d_prvsIndex = i;
+ ++d_helfulness;
return litDecision;
}
}
+ Trace("decision") << "Nothing to split on " << std::endl;
+
+ bool alljustified = true;
+ for(unsigned i = 0 ; i < assertions.size() && alljustified ; ++i) {
+ alljustified &= assertions[i].getKind() == kind::NOT ?
+ checkJustified(assertions[i][0]) : checkJustified(assertions[i]);
+ if(Debug.isOn("decision")) {
+ bool x = assertions[i].getKind() == kind::NOT ?
+ checkJustified(assertions[i][0]) : checkJustified(assertions[i]);
+ if(x==false)
+ Debug("decision") << "****** Not justified [i="<<i<<"]: " << assertions[i] << std::endl;
+ }
+ }
+ Assert(alljustified);
+
+ stopSearch = alljustified;
+ d_decisionEngine->setResult(SAT_VALUE_TRUE);
+
return prop::undefSatLiteral;
}
bool needSimplifiedPreITEAssertions() { return true; }
<< std::endl;
/* clear the justifcation labels -- reconsider if/when to do
this */
- d_justified.clear();
- d_prvsIndex = 0;
+ //d_justified.clear();
+ //d_prvsIndex = 0;
}
private:
/* Do all the hardwork. */
- bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision);
+ bool findSplitterRec(Node node, SatValue value, SatLiteral* litDecision);
/* Helper functions */
- void setJustified(SatVariable v);
- bool checkJustified(SatVariable v);
+ void setJustified(TNode);
+ bool checkJustified(TNode);
+
+ /* If literal exists corresponding to the node return
+ that. Otherwise an UNKNOWN */
+ SatValue tryGetSatValue(Node n)
+ {
+ Debug("decision") << " " << n << " has sat value " << " ";
+ if(d_decisionEngine->hasSatLiteral(n) ) {
+ Debug("decision") << d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n)) << std::endl;
+ return d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n));
+ } else {
+ Debug("decision") << "NO SAT LITERAL" << std::endl;
+ return SAT_VALUE_UNKNOWN;
+ }
+ }
+
};/* class JustificationHeuristic */
}/* namespace decision */
}
#endif /* CVC4_REPLAY */
- // Theory requests
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+ // Theory/DE requests
+ bool stopSearch = false;
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
while (nextLit != lit_Undef) {
if(value(var(nextLit)) == l_Undef) {
Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
} else {
Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
}
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+ }
+ if(stopSearch) {
+ return lit_Undef;
}
Var next = var_Undef;
// If this was a final check, we are satisfiable
if (check_type == CHECK_FINAL) {
+ bool decisionEngineDone = proxy->isDecisionEngineDone();
// Unless a lemma has added more stuff to the queues
- if (!order_heap.empty() || qhead < trail.size()) {
+ if (!decisionEngineDone &&
+ (!order_heap.empty() || qhead < trail.size()) ) {
check_type = CHECK_WITH_THEORY;
continue;
- } else if (recheck) {
+ } else if (!decisionEngineDone && recheck) {
// There some additional stuff added, so we go for another full-check
continue;
} else {
// Yes, we're truly satisfiable
+ if(decisionEngineDone) {
+ // but we might know that only because of decision engine
+ Trace("decision") << decisionEngineDone << " decision engine stopping us" << std::endl;
+ interrupt();
+ return l_Undef;
+ }
return l_True;
}
}
// Create the solver
d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
- Options::current()->incrementalSolving);
+ Options::current()->incrementalSolving ||
+ Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION );
// Setup the verbosity
d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
}
+ /* Tell decision engine */
+ if(negated) {
+ NodeBuilder<> nb(kind::NOT);
+ nb << node;
+ d_decisionEngine->addAssertion(nb.constructNode());
+ }
+
//TODO This comment is now false
// Assert as removable
d_cnfStream->convertAndAssert(node, removable, negated);
d_theoryEngine->assertFact(literalNode);
}
-SatLiteral TheoryProxy::getNextDecisionRequest() {
+SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
TNode n = d_theoryEngine->getNextDecisionRequest();
if(not n.isNull())
return d_cnfStream->getLiteral(n);
// may return in undefSatLiteral in which case the sat solver figure
// it out something
Assert(d_decisionEngine != NULL);
- return d_decisionEngine->getNext();
+ Assert(stopSearch != true);
+ SatLiteral ret = d_decisionEngine->getNext(stopSearch);
+ if(stopSearch) {
+ Trace("decision") << " *** Decision Engine stopped search *** " << std::endl;
+ }
+ return ret;
}
bool TheoryProxy::theoryNeedCheck() const {
d_propEngine->checkTime();
}
+bool TheoryProxy::isDecisionEngineDone() {
+ return d_decisionEngine->isDone();
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
void enqueueTheoryLiteral(const SatLiteral& l);
- SatLiteral getNextDecisionRequest();
+ SatLiteral getNextDecisionRequest(bool& stopSearch);
bool theoryNeedCheck() const;
void checkTime();
+ bool isDecisionEngineDone();
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
d_private(new smt::SmtEnginePrivate(*this)),
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
- d_staticLearningTime("smt::SmtEngine::staticLearningTime") {
+ d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
+ d_statResultSource("smt::resultSource", "unknown") {
NodeManagerScope nms(d_nodeManager);
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::registerStat(&d_staticLearningTime);
+ StatisticsRegistry::registerStat(&d_statResultSource);
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
CVC4_FOR_EACH_THEORY;
- d_decisionEngine = new DecisionEngine();
+ d_decisionEngine = new DecisionEngine(d_context);
d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
d_theoryEngine->setPropEngine(d_propEngine);
// d_decisionEngine->setPropEngine(d_propEngine);
StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+ StatisticsRegistry::unregisterStat(&d_statResultSource);
+
delete d_private;
delete d_userContext;
delete d_theoryEngine;
delete d_propEngine;
+ //delete d_decisionEngine;
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
Trace("smt") << "SmtEngine::check(): running check" << endl;
Result result = d_propEngine->checkSat(millis, resource);
+ d_statResultSource.setData("satSolver");
// PropEngine::checkSat() returns the actual amount used in these
// variables.
Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
<< ", conflicts " << d_cumulativeResourceUsed << endl;
+ if(result.isUnknown() and d_decisionEngine != NULL) {
+ Result deResult = d_decisionEngine->getResult();
+ if(not deResult.isUnknown()) {
+ d_statResultSource.setData("decisionEngine");
+ result = deResult;
+ }
+ }
+
return result;
}
TimerStat d_nonclausalSimplificationTime;
/** time spent in static learning */
TimerStat d_staticLearningTime;
+ /** how the SMT engine got the answer -- SAT solver or DE */
+ BackedStat<std::string> d_statResultSource;
+
public:
--print-expr-types print types with variables when printing exprs\n\
--lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
--simplification=MODE choose simplification mode, see --simplification=help\n\
+ --decision=MODE choose decision mode, see --decision=help\n\
--no-static-learning turn off static learning (e.g. diamond-breaking)\n\
--replay=file replay decisions from file\n\
--replay-log=file log decisions and propagations to file\n\
+ do not perform nonclausal simplification\n\
";
+static const string decisionHelp = "\
+Decision modes currently supported by the --decision option:\n\
+\n\
+internal (default)\n\
++ Use the internal decision hueristics of the SAT solver\n\
+\n\
+justification\n\
++ An ATGP-inspired justification heuristic\n\
+";
+
static const string dumpHelp = "\
Dump modes currently supported by the --dump option:\n\
\n\
UF_THEORY,
LAZY_DEFINITION_EXPANSION,
SIMPLIFICATION_MODE,
+ DECISION_MODE,
NO_STATIC_LEARNING,
INTERACTIVE,
NO_INTERACTIVE,
{ "uf" , required_argument, NULL, UF_THEORY },
{ "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
{ "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
+ { "decision", required_argument, NULL, DECISION_MODE },
{ "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
{ "interactive", no_argument , NULL, INTERACTIVE },
{ "no-interactive", no_argument , NULL, NO_INTERACTIVE },
}
break;
+ case DECISION_MODE:
+ if(!strcmp(optarg, "internal")) {
+ decisionMode = DECISION_STRATEGY_INTERNAL;
+ decisionModeSetByUser = true;
+ } else if(!strcmp(optarg, "justification")) {
+ decisionMode = DECISION_STRATEGY_JUSTIFICATION;
+ decisionModeSetByUser = true;
+ } else if(!strcmp(optarg, "help")) {
+ puts(decisionHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(string("unknown option for --decision: `") +
+ optarg + "'. Try --decision help.");
+ }
+ break;
+
case NO_STATIC_LEARNING:
doStaticLearning = false;
break;
projects / cvc5.git / commitdiff