summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.cpp57
-rw-r--r--src/decision/decision_engine.h43
-rw-r--r--src/decision/decision_strategy.h17
-rw-r--r--src/decision/justification_heuristic.cpp389
-rw-r--r--src/decision/justification_heuristic.h172
-rw-r--r--src/prop/minisat/core/Solver.cc2
-rw-r--r--src/prop/prop_engine.cpp14
-rw-r--r--src/smt/smt_engine.cpp27
-rw-r--r--src/theory/theory_engine.h33
-rw-r--r--src/util/ite_removal.h16
10 files changed, 472 insertions, 298 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 7c8718370..1d4f2fd42 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -26,13 +26,15 @@ using namespace std;
namespace CVC4 {
-DecisionEngine::DecisionEngine(context::Context *c) :
+ DecisionEngine::DecisionEngine(context::Context *sc,
+ context::Context *uc) :
d_enabledStrategies(),
- d_needSimplifiedPreITEAssertions(),
+ d_needIteSkolemMap(),
d_assertions(),
d_cnfStream(NULL),
d_satSolver(NULL),
- d_satContext(c),
+ d_satContext(sc),
+ d_userContext(uc),
d_result(SAT_VALUE_UNKNOWN)
{
const Options* options = Options::current();
@@ -42,37 +44,56 @@ DecisionEngine::DecisionEngine(context::Context *c) :
if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
- DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext);
+ ITEDecisionStrategy* ds =
+ new decision::JustificationHeuristic(this, d_satContext);
enableStrategy(ds);
+ d_needIteSkolemMap.push_back(ds);
}
}
void DecisionEngine::enableStrategy(DecisionStrategy* ds)
{
d_enabledStrategies.push_back(ds);
- if( ds->needSimplifiedPreITEAssertions() )
- d_needSimplifiedPreITEAssertions.push_back(ds);
}
-void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
+
+void DecisionEngine::addAssertions(const vector<Node> &assertions)
+{
+ Assert(false); // doing this so that we revisit what to do
+ // here. Currently not being used.
+
+ // d_result = SAT_VALUE_UNKNOWN;
+ // d_assertions.reserve(assertions.size());
+ // for(unsigned i = 0; i < assertions.size(); ++i)
+ // d_assertions.push_back(assertions[i]);
+}
+
+void DecisionEngine::addAssertions
+ (const vector<Node> &assertions,
+ int assertionsEnd,
+ IteSkolemMap iteSkolemMap)
{
+ // new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
+
d_assertions.reserve(assertions.size());
for(unsigned i = 0; i < assertions.size(); ++i)
d_assertions.push_back(assertions[i]);
- for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
- d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+
+ for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
+ d_needIteSkolemMap[i]->
+ addAssertions(assertions, assertionsEnd, iteSkolemMap);
}
-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();
-}
+// void DecisionEngine::addAssertion(Node n)
+// {
+// d_result = SAT_VALUE_UNKNOWN;
+// if(needIteSkolemMap()) {
+// d_assertions.push_back(n);
+// }
+// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
+// d_needIteSkolemMap[i]->notifyAssertionsAvailable();
+// }
}/* CVC4 namespace */
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);
}
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 6746b13cc..6ee583ec2 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -20,6 +20,7 @@
#define __CVC4__DECISION__DECISION_STRATEGY_H
#include "prop/sat_solver_types.h"
+#include "util/ite_removal.h"
namespace CVC4 {
@@ -43,11 +44,25 @@ public:
virtual prop::SatLiteral getNext(bool&) = 0;
- virtual bool needSimplifiedPreITEAssertions() { return false; }
+ virtual bool needIteSkolemMap() { return false; }
virtual void notifyAssertionsAvailable() { return; }
};
+class ITEDecisionStrategy : public DecisionStrategy {
+public:
+ ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
+ DecisionStrategy(de, c) {
+ }
+
+
+ bool needIteSkolemMap() { return true; }
+
+ virtual void addAssertions(const std::vector<Node> &assertions,
+ unsigned assertionsEnd,
+ IteSkolemMap iteSkolemMap) = 0;
+};
+
}/* decision namespace */
}/* CVC4 namespace */
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 62bd71f6a..c859e5d07 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -41,13 +41,18 @@
#include "justification_heuristic.h"
+#include "expr/node_manager.h"
#include "expr/kind.h"
+#include "theory/rewriter.h"
+#include "util/ite_removal.h"
/***
+Here's the main idea
-Summary of the algorithm:
-
-
+ Given a boolean formula "node", the goal is to try to make it
+evaluate to "desiredVal" (true/false). for instance if "node" is a AND
+formula we want to make it evaluate to true, we'd like one of the
+children to be true. this is done recursively.
***/
@@ -60,6 +65,19 @@ CVC3 code <----> this code
***/
+
+// Local helper functions for just this file
+
+SatValue invertValue(SatValue v)
+{
+ if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
+ else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
+ else return SAT_VALUE_TRUE;
+}
+
+
+// JustificationHeuristic stuff
+
void JustificationHeuristic::setJustified(TNode n)
{
d_justified.insert(n);
@@ -70,49 +88,75 @@ bool JustificationHeuristic::checkJustified(TNode n)
return d_justified.find(n) != d_justified.end();
}
-SatValue invertValue(SatValue v)
+SatValue JustificationHeuristic::tryGetSatValue(Node n)
{
- if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
- else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
- else return SAT_VALUE_TRUE;
+ Debug("decision") << " " << n << " has sat value " << " ";
+ if(d_decisionEngine->hasSatLiteral(n) ) {
+ Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl;
+ return d_decisionEngine->getSatValue(n);
+ } else {
+ Debug("decision") << "NO SAT LITERAL" << std::endl;
+ return SAT_VALUE_UNKNOWN;
+ }//end of else
+}
+
+void JustificationHeuristic::computeITEs(TNode n, IteList &l)
+{
+ Debug("jh-ite") << " computeITEs( " << n << ", &l)\n";
+ for(unsigned i=0; i<n.getNumChildren(); ++i) {
+ SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
+ if(it2 != d_iteAssertions.end())
+ l.push_back(it2->second);
+ computeITEs(n[i], l);
+ }
}
-bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, SatLiteral* litDecision)
-//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
+const IteList& JustificationHeuristic::getITEs(TNode n)
+{
+ IteCache::iterator it = d_iteCache.find(n);
+ if(it != d_iteCache.end()) {
+ return it->second;
+ } else {
+ // Compute the list of ITEs
+ // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
+ d_iteCache[n] = vector<TNode>();
+ computeITEs(n, d_iteCache[n]);
+ return d_iteCache[n];
+ }
+}
+
+bool JustificationHeuristic::findSplitterRec(TNode node,
+ SatValue desiredVal,
+ SatLiteral* litDecision)
{
Trace("decision")
- << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl;
+ << "findSplitterRec(" << node << ", "
+ << desiredVal << ", .. )" << std::endl;
/* Handle NOT as a special case */
- if (node.getKind() == kind::NOT) {
+ while (node.getKind() == kind::NOT) {
desiredVal = invertValue(desiredVal);
node = node[0];
}
- if (checkJustified(node)) return false;
-
- SatValue litVal = tryGetSatValue(node);
-
-#ifdef CVC4_ASSERTIONS
- bool litPresent = false;
-#endif
-
- if(d_decisionEngine->hasSatLiteral(node) ) {
- SatLiteral lit = d_decisionEngine->getSatLiteral(node);
-
-#ifdef CVC4_ASSERTIONS
- litPresent = true;
-#endif
-
- SatVariable v = lit.getSatVariable();
- // if (lit.isFalse() || lit.isTrue()) return false;
- if (v == 0) {
- setJustified(node);
- return false;
+ /* Base case */
+ if (checkJustified(node) || d_visited.find(node) != d_visited.end())
+ return false;
+
+#if defined CVC4_ASSERTIONS || defined CVC4_TRACING
+ // We don't always have a sat literal, so remember that. Will need
+ // it for some assertions we make.
+ bool litPresent = d_decisionEngine->hasSatLiteral(node);
+ if(Trace.isOn("decision")) {
+ if(!litPresent) {
+ Trace("decision") << "no sat literal for this node" << std::endl;
}
- } else {
- Trace("decision") << "no sat literal for this node" << std::endl;
}
+ //Assert(litPresent); -- fails
+#endif
+
+ // Get value of sat literal for the node, if there is one
+ SatValue litVal = tryGetSatValue(node);
/* You'd better know what you want */
Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
@@ -122,123 +166,104 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
"invariant voilated");
/* What type of node is this */
- Kind k = node.getKind();
+ Kind k = node.getKind();
theory::TheoryId tId = theory::kindToTheoryId(k);
/* 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 (getValue(v) != Var::UNKNOWN) {
- setJustified(v);
- return false;
- }
- else {
- *litDecision = Lit(v, value == Var::TRUE_VAL);
- return true;
- }
- }
- */
-
+ Trace("jh-findSplitterRec") << "kind = " << k << std::endl;
+ Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
+ Trace("jh-findSplitterRec") << "node = " << node << std::endl;
+ Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
/**
* If not in theory of booleans, and not a "boolean" EQUAL (IFF),
- * then check if this is something to split-on?
+ * 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(node);
- return false;
- } else {
- 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;
- }
- }
+ // if node has embedded ites -- which currently happens iff it got
+ // replaced during ite removal -- then try to resolve that first
+ const IteList& l = getITEs(node);
+ Debug("jh-ite") << " ite size = " << l.size() << std::endl;
+ d_visited.insert(node);
+ for(unsigned i = 0; i < l.size(); ++i) {
+ Assert(l[i].getKind() == kind::ITE, "Expected ITE");
+ Debug("jh-ite") << " i = " << i
+ << " l[i] = " << l[i] << std::endl;
+ if (checkJustified(l[i])) continue;
+
+ SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable
+#ifdef CVC4_ASSERTIONS
+ bool litPresent = d_decisionEngine->hasSatLiteral(l[i]);
+#endif
- /*** TODO: Term ITEs ***/
- /*
- else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
- // This node represents a predicate with embedded ITE's
- // We handle this case specially in order to catch the
- // corner case when a variable is in its own fanin.
- n = d_cnfManager->numFanins(v);
- for (i=0; i < n; ++i) {
- litTmp = d_cnfManager->getFanin(v, i);
- varTmp = litTmp.getVar();
- DebugAssert(!litTmp.isInverted(),"Expected positive fanin");
- if (checkJustified(varTmp)) continue;
- DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE,
- "Expected ITE");
- DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE");
- Lit cIf = d_cnfManager->getFanin(varTmp,0);
- Lit cThen = d_cnfManager->getFanin(varTmp,1);
- Lit cElse = d_cnfManager->getFanin(varTmp,2);
- if (getValue(cIf) == Var::UNKNOWN) {
- if (getValue(cElse) == Var::TRUE_VAL ||
- getValue(cThen) == Var::FALSE_VAL) {
- ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
- }
- else {
- ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
- }
- if (!ret) {
- cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
- DebugAssert(false,"No controlling input found (1)");
- }
- return true;
- }
- else if (getValue(cIf) == Var::TRUE_VAL) {
- if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
- return true;
- }
- if (cThen.getVar() != v &&
- (getValue(cThen) == Var::UNKNOWN ||
- getValue(cThen) == Var::TRUE_VAL) &&
- findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) {
+ // Handle the ITE to catch the case when a variable is its own
+ // fanin
+ SatValue ifVal = tryGetSatValue(l[i][0]);
+ if (ifVal == SAT_VALUE_UNKNOWN) {
+ // are we better off trying false? if not, try true
+ SatValue ifDesiredVal =
+ (tryGetSatValue(l[i][2]) == desiredVal ||
+ tryGetSatValue(l[i][1]) == invertValue(desiredVal))
+ ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
+
+ if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) {
return true;
}
- }
- else {
- if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
+ Assert(false, "No controlling input found (1)");
+ } else {
+
+ // Try to justify 'if'
+ if (findSplitterRec(l[i][0], ifVal, litDecision)) {
return true;
}
- if (cElse.getVar() != v &&
- (getValue(cElse) == Var::UNKNOWN ||
- getValue(cElse) == Var::TRUE_VAL) &&
- findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) {
+
+ // If that was successful, we need to go into only one of 'then'
+ // or 'else'
+ int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
+ int chVal = tryGetSatValue(l[i][ch]);
+ if( d_visited.find(l[i]) == d_visited.end()
+ && (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal)
+ && findSplitterRec(l[i][ch], desiredVal, litDecision) ) {
return true;
}
}
- setJustified(varTmp);
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
+ setJustified(l[i]);
}
- if (getValue(v) != Var::UNKNOWN) {
- setJustified(v);
+ d_visited.erase(node);
+
+ if(litVal != SAT_VALUE_UNKNOWN) {
+ setJustified(node);
return false;
- }
- else {
- *litDecision = Lit(v, value == Var::TRUE_VAL);
+ } else {
+ Assert(d_decisionEngine->hasSatLiteral(node));
+ /* 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;
}
}
- */
SatValue valHard = SAT_VALUE_FALSE;
switch (k) {
+
+ case kind::CONST_BOOLEAN:
+ Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE);
+ Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE);
+ setJustified(node);
+ return false;
+
case kind::AND:
valHard = SAT_VALUE_TRUE;
+
case kind::OR:
if (desiredVal == valHard) {
int n = node.getNumChildren();
@@ -247,7 +272,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
return true;
}
}
- Assert(litPresent == false || litVal == valHard, "Output should be justified");
+ Assert(litPresent == false || litVal == valHard,
+ "Output should be justified");
setJustified(node);
return false;
}
@@ -255,9 +281,10 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
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;
+ Debug("jh-findSplitterRec") << " node[i] = " << node[i] << " "
+ << tryGetSatValue(node[i]) << std::endl;
if ( tryGetSatValue(node[i]) != valHard) {
- Trace("findSplitterRec") << "hi"<< std::endl;
+ Debug("jh-findSplitterRec") << "hi"<< std::endl;
if (findSplitterRec(node[i], valEasy, litDecision)) {
return true;
}
@@ -266,11 +293,16 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
return false;
}
}
- 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;
+ if(Debug.isOn("jh-findSplitterRec")) {
+ Debug("jh-findSplitterRec") << " * ** " << std::endl;
+ Debug("jh-findSplitterRec") << node.getKind() << " "
+ << node << std::endl;
+ for(unsigned i = 0; i < node.getNumChildren(); ++i)
+ Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i])
+ << std::endl;
+ Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node)
+ << std::endl;
+ }
Assert(false, "No controlling input found (2)");
}
break;
@@ -285,7 +317,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) {
return true;
}
- Assert(litPresent == false || litVal == SAT_VALUE_FALSE, "Output should be justified");
+ Assert(litPresent == false || litVal == SAT_VALUE_FALSE,
+ "Output should be justified");
setJustified(node);
return false;
}
@@ -294,7 +327,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) {
return true;
}
- Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+ Assert(litPresent == false || litVal == SAT_VALUE_TRUE,
+ "Output should be justified");
setJustified(node);
return false;
}
@@ -302,13 +336,15 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) {
return true;
}
- Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+ 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();
{
@@ -322,7 +358,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
if (findSplitterRec(node[1], val, litDecision)) {
return true;
}
- Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
setJustified(node);
return false;
}
@@ -351,7 +388,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
if (findSplitterRec(node[1], val, litDecision)) {
return true;
}
- Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
setJustified(node);
return false;
}
@@ -367,62 +405,47 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat
break;
}
- case kind::ITE:
- throw GiveUpException();
- /*
- case ITE: {
- Lit cIf = d_cnfManager->getFanin(v, 0);
- Lit cThen = d_cnfManager->getFanin(v, 1);
- Lit cElse = d_cnfManager->getFanin(v, 2);
- if (getValue(cIf) == Var::UNKNOWN) {
- if (getValue(cElse) == value ||
- getValue(cThen) == Var::invertValue(value)) {
- ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
- }
- else {
- ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
- }
- if (!ret) {
- cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
- DebugAssert(false,"No controlling input found (6)");
- }
- return true;
+ case kind::ITE: {
+ //[0]: if, [1]: then, [2]: else
+ SatValue ifVal = tryGetSatValue(node[0]);
+ if (ifVal == SAT_VALUE_UNKNOWN) {
+
+ // are we better off trying false? if not, try true
+ SatValue ifDesiredVal =
+ (tryGetSatValue(node[2]) == desiredVal ||
+ tryGetSatValue(node[1]) == invertValue(desiredVal))
+ ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
+
+ if(findSplitterRec(node[0], ifDesiredVal, litDecision)) {
+ return true;
}
- else if (getValue(cIf) == Var::TRUE_VAL) {
- if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
- return true;
- }
- if (cThen.isVar() && cThen.getVar() != v &&
- (getValue(cThen) == Var::UNKNOWN ||
- getValue(cThen) == value) &&
- findSplitterRec(cThen, value, litDecision)) {
- return true;
- }
+ Assert(false, "No controlling input found (6)");
+ } else {
+
+ // Try to justify 'if'
+ if (findSplitterRec(node[0], ifVal, litDecision)) {
+ return true;
}
- else {
- if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
- return true;
- }
- if (cElse.isVar() && cElse.getVar() != v &&
- (getValue(cElse) == Var::UNKNOWN ||
- getValue(cElse) == value) &&
- findSplitterRec(cElse, value, litDecision)) {
- return true;
- }
+
+ // If that was successful, we need to go into only one of 'then'
+ // or 'else'
+ int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
+ int chVal = tryGetSatValue(node[ch]);
+ if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal)
+ && findSplitterRec(node[ch], desiredVal, litDecision) ) {
+ return true;
}
- DebugAssert(getValue(v) == value, "Output should be justified");
- setJustified(v);
- return false;
}
- */
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
+ setJustified(node);
+ return false;
+ }
+
default:
Assert(false, "Unexpected Boolean operator");
break;
- }
+ }//end of switch(k)
- /* Swap order of these two once we handle all cases */
- return false;
Unreachable();
-
-
}/* findRecSplit method */
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 0457e6d3c..acf2b3cfa 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -34,6 +34,8 @@ namespace CVC4 {
namespace decision {
+typedef std::vector<TNode> IteList;
+
class GiveUpException : public Exception {
public:
GiveUpException() :
@@ -41,15 +43,42 @@ public:
}
};/* class GiveUpException */
-class JustificationHeuristic : public DecisionStrategy {
+class JustificationHeuristic : public ITEDecisionStrategy {
+ typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
+ typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
+
+ // being 'justified' is monotonic with respect to decisions
context::CDHashSet<TNode,TNodeHashFunction> d_justified;
context::CDO<unsigned> d_prvsIndex;
+
IntStat d_helfulness;
IntStat d_giveup;
TimerStat d_timestat;
+
+ /**
+ * A copy of the assertions that need to be justified
+ * directly. Doesn't have ones introduced during during ITE-removal.
+ */
+ std::vector<TNode> d_assertions;
+ //TNode is fine since decisionEngine has them too
+
+ /** map from ite-rewrite skolem to a boolean-ite assertion */
+ SkolemMap d_iteAssertions;
+ // 'key' being TNode is fine since if a skolem didn't exist anywhere,
+ // we won't look it up. as for 'value', same reason as d_assertions
+
+ /** Cache for ITE skolems present in a atomic formula */
+ IteCache d_iteCache;
+
+ /**
+ * This is used to prevent infinite loop when trying to find a
+ * splitter. Can happen when exploring assertion corresponding to a
+ * term-ITE.
+ */
+ hash_set<TNode,TNodeHashFunction> d_visited;
public:
JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
- DecisionStrategy(de, c),
+ ITEDecisionStrategy(de, c),
d_justified(c),
d_prvsIndex(c, 0),
d_helfulness("decision::jh::helpfulness", 0),
@@ -66,74 +95,100 @@ public:
}
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;
-
- Trace("decision") << assertions[i] << std::endl;
+ d_visited.clear();
- SatValue desiredVal = SAT_VALUE_UNKNOWN;
+ for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
+ Trace("decision") << d_assertions[i] << std::endl;
- 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());
- }
+ // Sanity check: if it was false, aren't we inconsistent?
+ Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
- if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE;
+ SatValue desiredVal = SAT_VALUE_TRUE;
+ SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal);
- bool ret;
- try {
- ret = findSplitterRec(assertions[i], desiredVal, &litDecision);
- }catch(GiveUpException &e) {
- return prop::undefSatLiteral;
- }
- if(ret == true) {
- Trace("decision") << "Yippee!!" << std::endl;
- //d_prvsIndex = i;
- ++d_helfulness;
+ if(litDecision != undefSatLiteral)
return litDecision;
- }
}
- Trace("decision") << "Nothing to split on " << std::endl;
+ Trace("decision") << "jh: Nothing to split on " << std::endl;
+#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
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]);
+ for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
+ TNode curass = d_assertions[i];
+ while(curass.getKind() == kind::NOT)
+ curass = curass[0];
+ alljustified &= checkJustified(curass);
+
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;
+ if(!checkJustified(curass))
+ Debug("decision") << "****** Not justified [i="<<i<<"]: "
+ << d_assertions[i] << std::endl;
}
}
Assert(alljustified);
+#endif
- stopSearch = alljustified;
+ // SAT solver can stop...
+ stopSearch = true;
d_decisionEngine->setResult(SAT_VALUE_TRUE);
-
return prop::undefSatLiteral;
- }
- bool needSimplifiedPreITEAssertions() { return true; }
- void notifyAssertionsAvailable() {
- Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()"
- << " size = " << d_decisionEngine->getAssertions().size()
- << std::endl;
- /* clear the justifcation labels -- reconsider if/when to do
- this */
- //d_justified.clear();
- //d_prvsIndex = 0;
+ }
+
+ void addAssertions(const std::vector<Node> &assertions,
+ unsigned assertionsEnd,
+ IteSkolemMap iteSkolemMap) {
+ Trace("decision")
+ << "JustificationHeuristic::addAssertions()"
+ << " size = " << assertions.size()
+ << " assertionsEnd = " << assertionsEnd
+ << std::endl;
+
+ // Save the 'real' assertions locally
+ for(unsigned i = 0; i < assertionsEnd; ++i)
+ d_assertions.push_back(assertions[i]);
+
+ // Save mapping between ite skolems and ite assertions
+ for(IteSkolemMap::iterator i = iteSkolemMap.begin();
+ i != iteSkolemMap.end(); ++i) {
+ Assert(i->second >= assertionsEnd && i->second < assertions.size());
+ Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to "
+ << assertions[(i->second)] << std::endl;
+ d_iteAssertions[i->first] = assertions[i->second];
+ }
+ }
+
+ /* Compute justified */
+ bool computeJustified() {
+
}
private:
- /* Do all the hardwork. */
- bool findSplitterRec(Node node, SatValue value, SatLiteral* litDecision);
+ SatLiteral findSplitter(TNode node, SatValue desiredVal)
+ {
+ bool ret;
+ SatLiteral litDecision;
+ try {
+ ret = findSplitterRec(node, desiredVal, &litDecision);
+ }catch(GiveUpException &e) {
+ return prop::undefSatLiteral;
+ }
+ if(ret == true) {
+ Trace("decision") << "Yippee!!" << std::endl;
+ //d_prvsIndex = i;
+ ++d_helfulness;
+ return litDecision;
+ } else {
+ return undefSatLiteral;
+ }
+ }
+
+ /**
+ * Do all the hardwork.
+ * @param findFirst returns
+ */
+ bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
/* Helper functions */
void setJustified(TNode);
@@ -141,18 +196,13 @@ private:
/* 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;
- }
- }
+ SatValue tryGetSatValue(Node n);
+
+ /* Get list of all term-ITEs for the atomic formula v */
+ const IteList& getITEs(TNode n);
+ /* Compute all term-ITEs in a node recursively */
+ void computeITEs(TNode n, IteList &l);
};/* class JustificationHeuristic */
}/* namespace decision */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ea6cafdcd..5e1b032a3 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1099,6 +1099,8 @@ lbool Solver::search(int nof_conflicts)
if (next == lit_Undef) {
// We need to do a full theory check to confirm
+ Debug("minisat::search") << "Doing a full theoy check..."
+ << std::endl;
check_type = CHECK_FINAL;
continue;
}
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 03746c9b2..5b71e5ec5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -109,13 +109,13 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
}
/* Tell decision engine */
- if(negated) {
- NodeBuilder<> nb(kind::NOT);
- nb << node;
- d_decisionEngine->addAssertion(nb.constructNode());
- } else {
- d_decisionEngine->addAssertion(node);
- }
+ // if(negated) {
+ // NodeBuilder<> nb(kind::NOT);
+ // nb << node;
+ // d_decisionEngine->addAssertion(nb.constructNode());
+ // } else {
+ // d_decisionEngine->addAssertion(node);
+ // }
//TODO This comment is now false
// Assert as removable
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 81af14031..e636b9142 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -272,9 +272,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
CVC4_FOR_EACH_THEORY;
- d_decisionEngine = new DecisionEngine(d_context);
+ d_decisionEngine = new DecisionEngine(d_context, d_userContext);
d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
d_theoryEngine->setPropEngine(d_propEngine);
+ d_theoryEngine->setDecisionEngine(d_decisionEngine);
// d_decisionEngine->setPropEngine(d_propEngine);
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
@@ -1034,14 +1035,16 @@ void SmtEnginePrivate::processAssertions() {
// Simplify the assertions
simplifyAssertions();
- if(d_smt.d_decisionEngine->needSimplifiedPreITEAssertions()) {
- d_smt.d_decisionEngine->informSimplifiedPreITEAssertions(d_assertionsToCheck);
- }
+ // any assertions beyond realAssertionsEnd _must_ be introduced by
+ // removeITEs().
+ int realAssertionsEnd = d_assertionsToCheck.size();
+
+ // Remove ITEs, updating d_iteSkolemMap
+ removeITEs();
- // Remove ITEs
- removeITEs(); // This may need to be in a try-catch
- // block. make regress is passing, so
- // skipping for now --K
+ // begin: INVARIANT to maintain: no reordering of assertions or
+ // introducing new ones
+ int iteRewriteAssertionsEnd = d_assertionsToCheck.size();
Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
@@ -1061,7 +1064,13 @@ void SmtEnginePrivate::processAssertions() {
d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
}
- // TODO: send formulas and iteSkolemMap to decision engine
+ // Push the formula to decision engine
+ Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+ d_smt.d_decisionEngine->addAssertions
+ (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap);
+
+ // end: INVARIANT to maintain: no reordering of assertions or
+ // introducing new ones
// Push the formula to SAT
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0a0778ebc..5c73da1f6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -25,6 +25,7 @@
#include <vector>
#include <utility>
+#include "decision/decision_engine.h"
#include "expr/node.h"
#include "expr/command.h"
#include "prop/prop_engine.h"
@@ -77,6 +78,9 @@ class TheoryEngine {
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
+ /** Access to decision engine */
+ DecisionEngine* d_decisionEngine;
+
/** Our context */
context::Context* d_context;
@@ -430,26 +434,42 @@ class TheoryEngine {
Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
}
- // Remove the ITEs and assert to prop engine
+ // Remove the ITEs
std::vector<Node> additionalLemmas;
IteSkolemMap iteSkolemMap;
additionalLemmas.push_back(node);
RemoveITE::run(additionalLemmas, iteSkolemMap);
additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
+
+ // assert to prop engine
d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
d_propEngine->assertLemma(additionalLemmas[i], false, removable);
}
+ // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+ // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+ if(negated) {
+ // Can't we just get rid of passing around this 'negated' stuff?
+ // Is it that hard for the propEngine to figure that out itself?
+ // (I like the use of triple negation <evil laugh>.) --K
+ additionalLemmas[0] = additionalLemmas[0].notNode();
+ negated = false;
+ }
+ // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+ // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+
+ // assert to decision engine
+ if(!removable)
+ d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
+
// Mark that we added some lemmas
d_lemmasAdded = true;
// Lemma analysis isn't online yet; this lemma may only live for this
// user level.
- Node finalForm =
- negated ? additionalLemmas[0].notNode() : additionalLemmas[0];
- return theory::LemmaStatus(finalForm, d_userContext->getLevel());
+ return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
}
/** Time spent in theory combination */
@@ -485,6 +505,11 @@ public:
d_propEngine = propEngine;
}
+ inline void setDecisionEngine(DecisionEngine* decisionEngine) {
+ Assert(d_decisionEngine == NULL);
+ d_decisionEngine = decisionEngine;
+ }
+
/**
* Get a pointer to the underlying propositional engine.
*/
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 248ce4efa..7327d4a64 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -33,16 +33,20 @@ class RemoveITE {
public:
/**
- * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions.
- * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new
- * Boolean ite created in conjunction with that skolem variable.
+ * Removes the ITE nodes by introducing skolem variables. All
+ * additional assertions are pushed into assertions. iteSkolemMap
+ * contains a map from introduced skolem variables to the index in
+ * assertions containing the new Boolean ite created in conjunction
+ * with that skolem variable.
*/
static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
/**
- * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions.
- * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new
- * Boolean ite created in conjunction with that skolem variable.
+ * Removes the ITE from the node by introducing skolem
+ * variables. All additional assertions are pushed into
+ * assertions. iteSkolemMap contains a map from introduced skolem
+ * variables to the index in assertions containing the new Boolean
+ * ite created in conjunction with that skolem variable.
*/
static Node run(TNode node, std::vector<Node>& additionalAssertions,
IteSkolemMap& iteSkolemMap);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback