summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/decision_engine.cpp25
-rw-r--r--src/decision/decision_engine.h14
-rw-r--r--src/decision/decision_strategy.h2
-rw-r--r--src/decision/justification_heuristic.cpp594
-rw-r--r--src/decision/justification_heuristic.h148
-rw-r--r--src/decision/relevancy.h2
6 files changed, 380 insertions, 405 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 22c70eb6d..08a3e49d0 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -33,7 +33,7 @@ DecisionEngine::DecisionEngine(context::Context *sc,
d_enabledStrategies(),
d_needIteSkolemMap(),
d_relevancyStrategy(NULL),
- d_assertions(),
+ d_assertions(uc),
d_cnfStream(NULL),
d_satSolver(NULL),
d_satContext(sc),
@@ -50,18 +50,6 @@ void DecisionEngine::init()
d_engineState = 1;
Trace("decision-init") << "DecisionEngine::init()" << std::endl;
- if(options::incrementalSolving()) {
- if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) {
- if(options::decisionMode.wasSetByUser()) {
- Warning() << "Ignorning decision option since using incremental mode (currently not supported together)"
- << std::endl;
- } else {
- Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)"
- << std::endl;
- }
- }
- return;
- }
Trace("decision-init") << " * options->decisionMode: "
<< options::decisionMode() << std:: endl;
Trace("decision-init") << " * options->decisionStopOnly: "
@@ -70,11 +58,16 @@ void DecisionEngine::init()
if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
ITEDecisionStrategy* ds =
- new decision::JustificationHeuristic(this, d_satContext);
+ new decision::JustificationHeuristic(this, d_userContext, d_satContext);
enableStrategy(ds);
d_needIteSkolemMap.push_back(ds);
}
if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
+ if(options::incrementalSolving()) {
+ Warning() << "Relevancy decision heuristic and incremental not supported together"
+ << std::endl;
+ return; // Currently not supported with incremental
+ }
RelevancyStrategy* ds =
new decision::Relevancy(this, d_satContext);
enableStrategy(ds);
@@ -103,7 +96,7 @@ bool DecisionEngine::isRelevant(SatVariable var)
SatValue DecisionEngine::getPolarity(SatVariable var)
{
- Debug("decision") << "getPolariry(" << var <<")" << std::endl;
+ Debug("decision") << "getPolarity(" << var <<")" << std::endl;
if(d_relevancyStrategy != NULL) {
Assert(isRelevant(var));
return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
@@ -137,7 +130,7 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions,
// new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
- d_assertions.reserve(assertions.size());
+ // d_assertions.reserve(assertions.size());
for(unsigned i = 0; i < assertions.size(); ++i)
d_assertions.push_back(assertions[i]);
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 4d354af2a..ea16cec16 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -42,7 +42,8 @@ class DecisionEngine {
vector <ITEDecisionStrategy* > d_needIteSkolemMap;
RelevancyStrategy* d_relevancyStrategy;
- vector <Node> d_assertions;
+ typedef context::CDList<Node> AssertionsList;
+ AssertionsList d_assertions;
// PropEngine* d_propEngine;
CnfStream* d_cnfStream;
@@ -55,7 +56,7 @@ class DecisionEngine {
context::CDO<SatValue> d_result;
// Disable creating decision engine without required parameters
- DecisionEngine() : d_result(NULL) {}
+ DecisionEngine();
// init/shutdown state
unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
@@ -68,8 +69,6 @@ public:
/** 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) {
@@ -99,14 +98,15 @@ public:
/**
* This is called by SmtEngine, at shutdown time, just before
* destruction. It is important because there are destruction
- * ordering issues between some parts of the system. For now,
- * there's nothing to do here in the DecisionEngine.
+ * ordering issues between some parts of the system.
*/
void shutdown() {
Assert(d_engineState == 1);
d_engineState = 2;
Trace("decision") << "Shutting down decision engine" << std::endl;
+ for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
+ delete d_enabledStrategies[i];
}
// Interface for External World to use our services
@@ -191,7 +191,7 @@ public:
/**
* Get the assertions. Strategies are notified when these are available.
*/
- const vector<Node>& getAssertions() {
+ AssertionsList& getAssertions() {
return d_assertions;
}
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index a3c0d1684..a2fda44fe 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -9,7 +9,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Decision stategy
+ ** \brief Decision strategy
**
** Decision strategy
**/
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 4ec4588f3..0b63dfbe1 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -16,25 +16,6 @@
**
** It needs access to the simplified but non-clausal formula.
**/
-/*****************************************************************************/
-/*!
- * file search_sat.cpp
- * brief Implementation of Search engine with generic external sat solver
- *
- * Author: Clark Barrett
- *
- * Created: Wed Dec 7 21:00:24 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- *
- * <hr>
- */
-/*****************************************************************************/
#include "justification_heuristic.h"
@@ -43,7 +24,158 @@
#include "theory/rewriter.h"
#include "util/ite_removal.h"
-// JustificationHeuristic stuff
+
+using namespace CVC4;
+
+JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
+ context::Context *uc,
+ context::Context *c):
+ ITEDecisionStrategy(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"),
+ d_assertions(uc),
+ d_iteAssertions(uc),
+ d_iteCache(),
+ d_visited(),
+ d_visitedComputeITE(),
+ d_curDecision() {
+ StatisticsRegistry::registerStat(&d_helfulness);
+ StatisticsRegistry::registerStat(&d_giveup);
+ StatisticsRegistry::registerStat(&d_timestat);
+ Trace("decision") << "Justification heuristic enabled" << std::endl;
+}
+
+JustificationHeuristic::~JustificationHeuristic() {
+ StatisticsRegistry::unregisterStat(&d_helfulness);
+ StatisticsRegistry::unregisterStat(&d_giveup);
+ StatisticsRegistry::unregisterStat(&d_timestat);
+}
+
+CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) {
+ Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
+ TimerStat::CodeTimer codeTimer(d_timestat);
+
+ d_visited.clear();
+
+ if(Trace.isOn("justified")) {
+ for(JustifiedSet::key_iterator i = d_justified.key_begin();
+ i != d_justified.key_end(); ++i) {
+ TNode n = *i;
+ SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
+ d_decisionEngine->getSatLiteral(n) : -1;
+ SatValue v = tryGetSatValue(n);
+ Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
+ }
+ }
+
+ for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
+ Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
+
+ // Sanity check: if it was false, aren't we inconsistent?
+ Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
+
+ SatValue desiredVal = SAT_VALUE_TRUE;
+ SatLiteral litDecision;
+
+ litDecision = findSplitter(d_assertions[i], desiredVal);
+
+ if(litDecision != undefSatLiteral) {
+ d_prvsIndex = i;
+ return litDecision;
+ }
+ }
+
+ Trace("decision") << "jh: Nothing to split on " << std::endl;
+
+#if defined CVC4_DEBUG
+ bool alljustified = true;
+ 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")) {
+ if(!checkJustified(curass))
+ Debug("decision") << "****** Not justified [i="<<i<<"]: "
+ << d_assertions[i] << std::endl;
+ }
+ }
+ Assert(alljustified);
+#endif
+
+ // SAT solver can stop...
+ stopSearch = true;
+ d_decisionEngine->setResult(SAT_VALUE_TRUE);
+ return prop::undefSatLiteral;
+}
+
+
+inline void computeXorIffDesiredValues
+(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2)
+{
+ Assert(k == kind::IFF || k == kind::XOR);
+
+ bool shouldInvert =
+ (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) ||
+ (desiredVal == SAT_VALUE_FALSE && k == kind::XOR);
+
+ if(desiredVal1 == SAT_VALUE_UNKNOWN &&
+ desiredVal2 == SAT_VALUE_UNKNOWN) {
+ // CHOICE: pick one of them arbitarily
+ desiredVal1 = SAT_VALUE_FALSE;
+ }
+
+ if(desiredVal2 == SAT_VALUE_UNKNOWN) {
+ desiredVal2 = shouldInvert ? invertValue(desiredVal1) : desiredVal1;
+ } else if(desiredVal1 == SAT_VALUE_UNKNOWN) {
+ desiredVal1 = shouldInvert ? invertValue(desiredVal2) : desiredVal2;
+ }
+}
+
+
+
+void JustificationHeuristic::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) {
+
+ Trace("decision::jh::ite")
+ << " jh-ite: " << (i->first) << " maps to "
+ << assertions[(i->second)] << std::endl;
+ Assert(i->second >= assertionsEnd && i->second < assertions.size());
+
+ d_iteAssertions[i->first] = assertions[i->second];
+ }
+}
+
+SatLiteral JustificationHeuristic::findSplitter(TNode node,
+ SatValue desiredVal)
+{
+ d_curDecision = undefSatLiteral;
+ if(findSplitterRec(node, desiredVal)) {
+ ++d_helfulness;
+ }
+ return d_curDecision;
+}
+
void JustificationHeuristic::setJustified(TNode n)
{
@@ -67,14 +199,30 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
}//end of else
}
+const JustificationHeuristic::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] = IteList();
+ d_visitedComputeITE.clear();
+ computeITEs(n, d_iteCache[n]);
+ return d_iteCache[n];
+ }
+}
+
void JustificationHeuristic::computeITEs(TNode n, IteList &l)
{
- Trace("jh-ite") << " computeITEs( " << n << ", &l)\n";
+ Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n";
d_visitedComputeITE.insert(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(make_pair(n[i], it2->second));
+ l.push_back(make_pair(n[i], (*it2).second));
Assert(n[i].getNumChildren() == 0);
}
if(d_visitedComputeITE.find(n[i]) ==
@@ -84,26 +232,19 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l)
}
}
-const JustificationHeuristic::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] = IteList();
- d_visitedComputeITE.clear();
- computeITEs(n, d_iteCache[n]);
- return d_iteCache[n];
- }
-}
-
bool JustificationHeuristic::findSplitterRec(TNode node,
- SatValue desiredVal,
- SatLiteral* litDecision)
+ SatValue desiredVal)
{
- Trace("jh-findSplitterRec")
+ /**
+ * Main idea
+ *
+ * Given a boolean formula "node", the goal is to try to make it
+ * evaluate to "desiredVal" (true/false). for instance if "node" is a OR
+ * formula we want to make it evaluate to true, we'd like one of the
+ * children to be true. this is done recursively.
+ */
+
+ Trace("decision::jh")
<< "findSplitterRec(" << node << ", "
<< desiredVal << ", .. )" << std::endl;
@@ -113,13 +254,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
node = node[0];
}
- if(Debug.isOn("decision")) {
- if(checkJustified(node))
- Debug("decision") << " justified, returning" << std::endl;
- }
-
/* Base case */
if (checkJustified(node)) {
+ Debug("decision::jh") << " justified, returning" << std::endl;
return false;
}
@@ -132,7 +269,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
Debug("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
@@ -142,11 +278,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
/* Good luck, hope you can get what you want */
- // if(not (litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN)) {
- // Warning() << "WARNING: IMPORTANT: Please look into this. Sat solver is asking for a decision" << std::endl
- // << "when the assertion we are trying to justify is already unsat. OR there is a bug" << std::endl;
- // GiveUpException();
- // }
Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
"invariant violated");
@@ -155,247 +286,192 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
theory::TheoryId tId = theory::kindToTheoryId(k);
/* Some debugging stuff */
- Debug("jh-findSplitterRec") << "kind = " << k << std::endl;
- Debug("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
- Debug("jh-findSplitterRec") << "node = " << node << std::endl;
- Debug("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
+ Debug("decision::jh") << "kind = " << k << std::endl
+ << "theoryId = " << tId << std::endl
+ << "node = " << node << std::endl
+ << "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.
+ * If not in theory of booleans, check if this is something to split-on.
*/
- if(tId != theory::THEORY_BOOL
- // && !(k == kind::EQUAL && node[0].getType().isBoolean())
- ) {
-
- // 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);
- Trace("jh-ite") << " ite size = " << l.size() << std::endl;
- /*d_visited.insert(node);*/
- for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
- if(d_visited.find(i->first) == d_visited.end()) {
- d_visited.insert(i->first);
- Debug("jh-ite") << "jh-ite: adding visited " << i->first << std::endl;
- if(findSplitterRec(i->second, SAT_VALUE_TRUE, litDecision))
- return true;
- Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl;
- d_visited.erase(i->first);
- } else {
- Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl;
- }
- }
+ if(tId != theory::THEORY_BOOL) {
+
+ // if node has embedded ites, resolve that first
+ if(handleEmbeddedITEs(node))
+ return true;
if(litVal != SAT_VALUE_UNKNOWN) {
setJustified(node);
return false;
- } else {
- Assert(d_decisionEngine->hasSatLiteral(node));
- /* if(not d_decisionEngine->hasSatLiteral(node))
- throw GiveUpException(); */
+ }
+ else {
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;
+ SatVariable v =
+ d_decisionEngine->getSatLiteral(node).getSatVariable();
+ d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
return true;
}
}
- SatValue valHard = SAT_VALUE_FALSE;
+ bool ret = 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;
+ Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE);
+ break;
case kind::AND:
- valHard = SAT_VALUE_TRUE;
+ if (desiredVal == SAT_VALUE_FALSE)
+ ret = handleAndOrEasy(node, desiredVal);
+ else
+ ret = handleAndOrHard(node, desiredVal);
+ break;
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;
- }
- }
- 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) {
- Debug("jh-findSplitterRec") << " node[i] = " << node[i] << " "
- << tryGetSatValue(node[i]) << std::endl;
- if ( tryGetSatValue(node[i]) != valHard) {
- Debug("jh-findSplitterRec") << "hi"<< std::endl;
- if (findSplitterRec(node[i], valEasy, litDecision)) {
- return true;
- }
- Assert(litPresent == false || litVal == valEasy, "Output should be justified");
- setJustified(node);
- return false;
- }
- }
- 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)");
- }
+ if (desiredVal == SAT_VALUE_FALSE)
+ ret = handleAndOrHard(node, desiredVal);
+ else
+ ret = handleAndOrEasy(node, desiredVal);
break;
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;
- }
- if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) {
- return true;
- }
- Assert(litPresent == false || litVal == SAT_VALUE_FALSE,
- "Output should be justified");
- setJustified(node);
- return false;
- }
- else {
- if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
- if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) {
- return true;
- }
- Assert(litPresent == false || litVal == SAT_VALUE_TRUE,
- "Output should be justified");
- setJustified(node);
- return false;
- }
- if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
- if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) {
- return true;
- }
- Assert(litPresent == false || litVal == SAT_VALUE_TRUE,
- "Output should be justified");
- setJustified(node);
- return false;
- }
- Assert(false, "No controlling input found (3)");
- }
- break;
+ if (desiredVal == SAT_VALUE_FALSE)
+ ret = handleBinaryHard(node[0], SAT_VALUE_TRUE,
+ node[1], SAT_VALUE_FALSE);
- case kind::IFF:
- //throw GiveUpException();
- {
- SatValue val = tryGetSatValue(node[0]);
- if (val != SAT_VALUE_UNKNOWN) {
- if (findSplitterRec(node[0], val, litDecision)) {
- return true;
- }
- 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)");
- }
+ else
+ ret = handleBinaryEasy(node[0], SAT_VALUE_FALSE,
+ node[1], SAT_VALUE_TRUE);
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)");
- }
+ case kind::XOR:
+ case kind::IFF: {
+ SatValue desiredVal1 = tryGetSatValue(node[0]);
+ SatValue desiredVal2 = tryGetSatValue(node[1]);
+ computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2);
+ ret = handleBinaryHard(node[0], desiredVal1,
+ node[1], desiredVal2);
break;
}
- 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;
- }
- Assert(false, "No controlling input found (6)");
- } else {
-
- // Try to justify 'if'
- if (findSplitterRec(node[0], ifVal, 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;
- }
- }
- Assert(litPresent == false || litVal == desiredVal,
- "Output should be justified");
- setJustified(node);
- return false;
- }
+ case kind::ITE:
+ ret = handleITE(node, desiredVal);
+ break;
default:
Assert(false, "Unexpected Boolean operator");
break;
}//end of switch(k)
- Unreachable();
+ if(ret == false) {
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
+ setJustified(node);
+ }
+ return ret;
}/* findRecSplit method */
+
+bool JustificationHeuristic::handleAndOrEasy(TNode node,
+ SatValue desiredVal)
+{
+ Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or
+ (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) );
+
+ int numChildren = node.getNumChildren();
+ SatValue desiredValInverted = invertValue(desiredVal);
+ for(int i = 0; i < numChildren; ++i)
+ if ( tryGetSatValue(node[i]) != desiredValInverted )
+ return findSplitterRec(node[i], desiredVal);
+ Assert(false, "handleAndOrEasy: No controlling input found");
+ return false;
+}
+
+bool JustificationHeuristic::handleAndOrHard(TNode node,
+ SatValue desiredVal) {
+ Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or
+ (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) );
+
+ int numChildren = node.getNumChildren();
+ for(int i = 0; i < numChildren; ++i)
+ if (findSplitterRec(node[i], desiredVal))
+ return true;
+ return false;
+}
+
+bool JustificationHeuristic::handleBinaryEasy(TNode node1,
+ SatValue desiredVal1,
+ TNode node2,
+ SatValue desiredVal2)
+{
+ if ( tryGetSatValue(node1) != invertValue(desiredVal1) )
+ return findSplitterRec(node1, desiredVal1);
+ if ( tryGetSatValue(node2) != invertValue(desiredVal2) )
+ return findSplitterRec(node2, desiredVal2);
+ Assert(false, "handleBinaryEasy: No controlling input found");
+ return false;
+}
+
+bool JustificationHeuristic::handleBinaryHard(TNode node1,
+ SatValue desiredVal1,
+ TNode node2,
+ SatValue desiredVal2)
+{
+ if( findSplitterRec(node1, desiredVal1) )
+ return true;
+ return findSplitterRec(node2, desiredVal2);
+}
+
+bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
+{
+ Debug("decision::jh") << " handleITE (" << node << ", "
+ << desiredVal << std::endl;
+
+ //[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 [CHOICE]
+ SatValue ifDesiredVal =
+ (tryGetSatValue(node[2]) == desiredVal ||
+ tryGetSatValue(node[1]) == invertValue(desiredVal))
+ ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
+
+ if(findSplitterRec(node[0], ifDesiredVal)) return true;
+
+ Assert(false, "No controlling input found (6)");
+ } else {
+ // Try to justify 'if'
+ if(findSplitterRec(node[0], ifVal)) 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;
+
+ // STALE code: remove after tests or mar 2013, whichever earlier
+ // int chVal = tryGetSatValue(node[ch]);
+ // Assert(chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal);
+ // end STALE code: remove
+
+ if( findSplitterRec(node[ch], desiredVal) ) {
+ return true;
+ }
+ }// else (...ifVal...)
+ return false;
+}
+
+bool JustificationHeuristic::handleEmbeddedITEs(TNode node)
+{
+ const IteList& l = getITEs(node);
+ Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+
+ for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+ if(d_visited.find(i->first) == d_visited.end()) {
+ d_visited.insert(i->first);
+ if(findSplitterRec(i->second, SAT_VALUE_TRUE))
+ return true;
+ d_visited.erase(i->first);
+ }
+ }
+ return false;
+}
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 5d13d2dd2..91c21d981 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -27,6 +27,8 @@
#include "decision_strategy.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/cdhashmap.h"
#include "expr/node.h"
#include "prop/sat_solver_types.h"
@@ -34,20 +36,13 @@ namespace CVC4 {
namespace decision {
-class GiveUpException : public Exception {
-public:
- GiveUpException() :
- Exception("justification heuristic: giving up") {
- }
-};/* class GiveUpException */
-
class JustificationHeuristic : public ITEDecisionStrategy {
typedef std::vector<pair<TNode,TNode> > IteList;
typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
- typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
+ typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
// being 'justified' is monotonic with respect to decisions
- typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+ typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
JustifiedSet d_justified;
context::CDO<unsigned> d_prvsIndex;
@@ -59,7 +54,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
* 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;
+ context::CDList<TNode> d_assertions;
//TNode is fine since decisionEngine has them too
/** map from ite-rewrite skolem to a boolean-ite assertion */
@@ -82,127 +77,29 @@ class JustificationHeuristic : public ITEDecisionStrategy {
* function
*/
hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+
+ /** current decision for the recursive call */
+ SatLiteral d_curDecision;
public:
- JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
- ITEDecisionStrategy(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;
- }
- ~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);
-
- d_visited.clear();
-
- if(Trace.isOn("justified")) {
- for(JustifiedSet::iterator i = d_justified.begin();
- i != d_justified.end(); ++i) {
- TNode n = *i;
- SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
- d_decisionEngine->getSatLiteral(n) : -1;
- SatValue v = tryGetSatValue(n);
- Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
- }
- }
-
- for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
- Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
-
- // Sanity check: if it was false, aren't we inconsistent?
- Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
-
- SatValue desiredVal = SAT_VALUE_TRUE;
- SatLiteral litDecision;
- try {
- litDecision = findSplitter(d_assertions[i], desiredVal);
- }catch(GiveUpException &e) {
- return prop::undefSatLiteral;
- }
-
- if(litDecision != undefSatLiteral) {
- d_prvsIndex = i;
- return litDecision;
- }
- }
-
- Trace("decision") << "jh: Nothing to split on " << std::endl;
-
-#if defined CVC4_DEBUG
- bool alljustified = true;
- 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")) {
- if(!checkJustified(curass))
- Debug("decision") << "****** Not justified [i="<<i<<"]: "
- << d_assertions[i] << std::endl;
- }
- }
- Assert(alljustified);
-#endif
-
- // SAT solver can stop...
- stopSearch = true;
- d_decisionEngine->setResult(SAT_VALUE_TRUE);
- return prop::undefSatLiteral;
- }
+ JustificationHeuristic(CVC4::DecisionEngine* de,
+ context::Context *uc,
+ context::Context *c);
+
+ ~JustificationHeuristic();
+
+ prop::SatLiteral getNext(bool &stopSearch);
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) {
- Trace("jh-ite") << " jh-ite: " << (i->first) << " maps to "
- << assertions[(i->second)] << std::endl;
- Assert(i->second >= assertionsEnd && i->second < assertions.size());
- d_iteAssertions[i->first] = assertions[i->second];
- }
- }
+ IteSkolemMap iteSkolemMap);
private:
- SatLiteral findSplitter(TNode node, SatValue desiredVal)
- {
- bool ret;
- SatLiteral litDecision;
- ret = findSplitterRec(node, desiredVal, &litDecision);
- if(ret == true) {
- Debug("decision") << "Yippee!!" << std::endl;
- ++d_helfulness;
- return litDecision;
- } else {
- return undefSatLiteral;
- }
- }
+ SatLiteral findSplitter(TNode node, SatValue desiredVal);
/**
* Do all the hard work.
*/
- bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
+ bool findSplitterRec(TNode node, SatValue value);
/* Helper functions */
void setJustified(TNode);
@@ -217,6 +114,15 @@ private:
/* Compute all term-ITEs in a node recursively */
void computeITEs(TNode n, IteList &l);
+
+ bool handleAndOrEasy(TNode node, SatValue desiredVal);
+ bool handleAndOrHard(TNode node, SatValue desiredVal);
+ bool handleBinaryEasy(TNode node1, SatValue desiredVal1,
+ TNode node2, SatValue desiredVal2);
+ bool handleBinaryHard(TNode node1, SatValue desiredVal1,
+ TNode node2, SatValue desiredVal2);
+ bool handleITE(TNode node, SatValue desiredVal);
+ bool handleEmbeddedITEs(TNode node);
};/* class JustificationHeuristic */
}/* namespace decision */
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index 8a6eb54ef..bfd30ddde 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -60,7 +60,7 @@ class Relevancy : public RelevancyStrategy {
typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
// being 'justified' is monotonic with respect to decisions
- context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+ context::CDHashSet<Node, NodeHashFunction> d_justified;
context::CDO<unsigned> d_prvsIndex;
IntStat d_helfulness;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback