summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2012-06-08 05:56:08 +0000
committerKshitij Bansal <kshitij@cs.nyu.edu>2012-06-08 05:56:08 +0000
commit8cd22903675724e29249ce089ee77c7c4d3897fb (patch)
tree64ea92a2a0f8721b7e1b15796824f6259567aa75 /src/decision
parent6685546d585212559b97d5722161ad52ff5c4121 (diff)
Merge from decision branch (till r3663)
(no performace or search behavior changes expected)
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/Makefile.am4
-rw-r--r--src/decision/decision_engine.cpp45
-rw-r--r--src/decision/decision_engine.h10
-rw-r--r--src/decision/decision_strategy.h11
-rw-r--r--src/decision/justification_heuristic.cpp6
-rw-r--r--src/decision/relevancy.cpp376
-rw-r--r--src/decision/relevancy.h423
7 files changed, 864 insertions, 11 deletions
diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am
index c399cbf71..4f454e9bf 100644
--- a/src/decision/Makefile.am
+++ b/src/decision/Makefile.am
@@ -10,4 +10,6 @@ libdecision_la_SOURCES = \
decision_engine.cpp \
decision_strategy.h \
justification_heuristic.h \
- justification_heuristic.cpp
+ justification_heuristic.cpp \
+ relevancy.h \
+ relevancy.cpp
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 1afe835fb..b1ecabf81 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -18,6 +18,7 @@
#include "decision/decision_engine.h"
#include "decision/justification_heuristic.h"
+#include "decision/relevancy.h"
#include "expr/node.h"
#include "util/options.h"
@@ -30,6 +31,7 @@ namespace CVC4 {
context::Context *uc) :
d_enabledStrategies(),
d_needIteSkolemMap(),
+ d_relevancyStrategy(NULL),
d_assertions(),
d_cnfStream(NULL),
d_satSolver(NULL),
@@ -49,6 +51,13 @@ namespace CVC4 {
enableStrategy(ds);
d_needIteSkolemMap.push_back(ds);
}
+ if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) {
+ RelevancyStrategy* ds =
+ new decision::Relevancy(this, d_satContext, options->decisionOptions);
+ enableStrategy(ds);
+ d_needIteSkolemMap.push_back(ds);
+ d_relevancyStrategy = ds;
+ }
}
void DecisionEngine::enableStrategy(DecisionStrategy* ds)
@@ -57,6 +66,35 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds)
}
+bool DecisionEngine::isRelevant(SatVariable var)
+{
+ Debug("decision") << "isRelevant(" << var <<")" << std::endl;
+ if(d_relevancyStrategy != NULL) {
+ //Assert(d_cnfStream->hasNode(var));
+ return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
+ } else {
+ return true;
+ }
+}
+
+SatValue DecisionEngine::getPolarity(SatVariable var)
+{
+ Debug("decision") << "getPolariry(" << var <<")" << std::endl;
+ if(d_relevancyStrategy != NULL) {
+ Assert(isRelevant(var));
+ return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
+ } else {
+ return SAT_VALUE_UNKNOWN;
+ }
+}
+
+
+
+
+
+
+
+
void DecisionEngine::addAssertions(const vector<Node> &assertions)
{
Assert(false); // doing this so that we revisit what to do
@@ -68,10 +106,9 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions)
// d_assertions.push_back(assertions[i]);
}
-void DecisionEngine::addAssertions
- (const vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap)
+void DecisionEngine::addAssertions(const vector<Node> &assertions,
+ unsigned assertionsEnd,
+ IteSkolemMap iteSkolemMap)
{
// new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 545ae1770..fb6f673d9 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -40,6 +40,7 @@ class DecisionEngine {
vector <DecisionStrategy* > d_enabledStrategies;
vector <ITEDecisionStrategy* > d_needIteSkolemMap;
+ RelevancyStrategy* d_relevancyStrategy;
vector <Node> d_assertions;
@@ -107,6 +108,15 @@ public:
return ret;
}
+ /** Is a sat variable relevant */
+ bool isRelevant(SatVariable var);
+
+ /**
+ * Try to get tell SAT solver what polarity to try for a
+ * decision. Return SAT_VALUE_UNKNOWN if it can't help
+ */
+ SatValue getPolarity(SatVariable var);
+
/** Is the DecisionEngine in a state where it has solved everything? */
bool isDone() {
Trace("decision") << "DecisionEngine::isDone() returning "
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 6ee583ec2..ee7d340c4 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -63,6 +63,17 @@ public:
IteSkolemMap iteSkolemMap) = 0;
};
+class RelevancyStrategy : public ITEDecisionStrategy {
+public:
+ RelevancyStrategy(DecisionEngine* de, context::Context *c) :
+ ITEDecisionStrategy(de, c) {
+ }
+
+ virtual bool isRelevant(TNode n) = 0;
+ virtual prop::SatValue getPolarity(TNode n) = 0;
+};
+
+
}/* decision namespace */
}/* CVC4 namespace */
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c859e5d07..68c11295f 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -68,12 +68,6 @@ 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
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
new file mode 100644
index 000000000..c5e1f7fbc
--- /dev/null
+++ b/src/decision/relevancy.cpp
@@ -0,0 +1,376 @@
+/********************* */
+/*! \file relevancy.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Justification heuristic for decision making
+ **
+ ** A ATGP-inspired justification-based decision heuristic. See
+ ** [insert reference] for more details. This code is, or not, based
+ ** on the CVC3 implementation of the same heuristic -- note below.
+ **
+ ** It needs access to the simplified but non-clausal formula.
+ **/
+/*****************************************************************************/
+
+#include "relevancy.h"
+
+#include "expr/node_manager.h"
+#include "expr/kind.h"
+#include "theory/rewriter.h"
+#include "util/ite_removal.h"
+
+// Relevancy stuff
+
+void Relevancy::setJustified(TNode n)
+{
+ Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
+ d_justified.insert(n);
+ if(d_opt.computeRelevancy) {
+ d_relevancy[n] = d_maxRelevancy[n];
+ updateRelevancy(n);
+ }
+}
+
+bool Relevancy::checkJustified(TNode n)
+{
+ return d_justified.find(n) != d_justified.end();
+}
+
+SatValue Relevancy::tryGetSatValue(Node n)
+{
+ 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 Relevancy::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);
+ }
+}
+
+const IteList& Relevancy::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 Relevancy::findSplitterRec(TNode node,
+ SatValue desiredVal)
+{
+ Trace("decision")
+ << "findSplitterRec([" << node.getId() << "]" << node << ", "
+ << desiredVal << ", .. )" << std::endl;
+
+ ++d_expense;
+
+ /* Handle NOT as a special case */
+ while (node.getKind() == kind::NOT) {
+ desiredVal = invertValue(desiredVal);
+ node = node[0];
+ }
+
+ /* Avoid infinite loops */
+ if(d_visited.find(node) != d_visited.end()) {
+ Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl;
+ Assert(false);
+ Assert(node.getKind() == kind::ITE);
+ return false;
+ }
+
+ /* Base case */
+ if(checkJustified(node)) {
+ return false;
+ }
+
+ /**
+ * If we have already explored the subtree for some desiredVal, we
+ * skip this and continue exploring the rest
+ */
+ if(d_polarityCache.find(node) == d_polarityCache.end()) {
+ d_polarityCache[node] = desiredVal;
+ } else {
+ Assert(d_multipleBacktrace || d_opt.computeRelevancy);
+ return true;
+ }
+
+ d_visited.insert(node);
+
+#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;
+ }
+ }
+ //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");
+
+ /* Good luck, hope you can get what you want */
+ 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);
+
+ /* Some debugging stuff */
+ 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.
+ */
+ 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);
+ Debug("jh-ite") << " ite size = " << l.size() << std::endl;
+ 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(d_visited.find(node) != d_visited.end() ) continue;
+ if(findSplitterRec(l[i], SAT_VALUE_TRUE)) {
+ d_visited.erase(node);
+ return true;
+ }
+ }
+ Debug("jh-ite") << " ite done " << l.size() << std::endl;
+
+ if(litVal != SAT_VALUE_UNKNOWN) {
+ d_visited.erase(node);
+ 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();
+ *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+ Trace("decision") << "decision " << *d_curDecision << std::endl;
+ Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
+ d_visited.erase(node);
+ return true;
+ }
+ }
+
+ bool ret = false;
+ SatValue flipCaseVal = 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);
+ break;
+
+ case kind::AND:
+ if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE);
+ else ret = handleOrFalse(node, SAT_VALUE_TRUE);
+ break;
+
+ case kind::OR:
+ if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE);
+ else ret = handleOrTrue(node, SAT_VALUE_TRUE);
+ break;
+
+ case kind::IMPLIES:
+ Assert(node.getNumChildren() == 2, "Expected 2 fanins");
+ if (desiredVal == SAT_VALUE_FALSE) {
+ ret = findSplitterRec(node[0], SAT_VALUE_TRUE);
+ if(ret) break;
+ ret = findSplitterRec(node[1], SAT_VALUE_FALSE);
+ break;
+ }
+ else {
+ if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
+ ret = findSplitterRec(node[0], SAT_VALUE_FALSE);
+ //if(!ret || !d_multipleBacktrace)
+ break;
+ }
+ if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
+ ret = findSplitterRec(node[1], SAT_VALUE_TRUE);
+ break;
+ }
+ Assert(d_multipleBacktrace, "No controlling input found (3)");
+ }
+ break;
+
+ case kind::XOR:
+ flipCaseVal = SAT_VALUE_TRUE;
+ case kind::IFF: {
+ SatValue val = tryGetSatValue(node[0]);
+ if (val != SAT_VALUE_UNKNOWN) {
+ ret = findSplitterRec(node[0], val);
+ if (ret) break;
+ if (desiredVal == flipCaseVal) val = invertValue(val);
+ ret = findSplitterRec(node[1], val);
+ }
+ else {
+ val = tryGetSatValue(node[1]);
+ if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+ if (desiredVal == flipCaseVal) val = invertValue(val);
+ ret = findSplitterRec(node[0], val);
+ if(ret) break;
+ Assert(false, "Unable to find controlling input (4)");
+ }
+ break;
+ }
+
+ case kind::ITE:
+ ret = handleITE(node, desiredVal);
+ break;
+
+ default:
+ Assert(false, "Unexpected Boolean operator");
+ break;
+ }//end of switch(k)
+
+ d_visited.erase(node);
+ if(ret == false) {
+ Assert(litPresent == false || litVal == desiredVal,
+ "Output should be justified");
+ setJustified(node);
+ }
+ return ret;
+
+ Unreachable();
+}/* findRecSplit method */
+
+bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) {
+ Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", "
+ << desiredVal << std::endl;
+
+ Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or
+ (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) );
+
+ int n = node.getNumChildren();
+ bool ret = false;
+ for(int i = 0; i < n; ++i) {
+ if (findSplitterRec(node[i], desiredVal)) {
+ if(!d_opt.computeRelevancy)
+ return true;
+ else
+ ret = true;
+ }
+ }
+ return ret;
+}
+
+bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) {
+ Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", "
+ << desiredVal << std::endl;
+
+ Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or
+ (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) );
+
+ int n = node.getNumChildren();
+ SatValue desiredValInverted = invertValue(desiredVal);
+ for(int i = 0; i < n; ++i) {
+ if ( tryGetSatValue(node[i]) != desiredValInverted ) {
+ // PRE RELEVANCY return findSplitterRec(node[i], desiredVal);
+ bool ret = findSplitterRec(node[i], desiredVal);
+ if(ret) {
+ // Splitter could be found... so can't justify this node
+ if(!d_multipleBacktrace)
+ return true;
+ }
+ else {
+ // Splitter couldn't be found... should be justified
+ return false;
+ }
+ }
+ }
+ // Multiple backtrace is on, so must have reached here because
+ // everything had splitter
+ if(d_multipleBacktrace) return true;
+
+ 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");
+ return false;
+}
+
+bool Relevancy::handleITE(TNode node, SatValue desiredVal)
+{
+ Debug("jh-findSplitterRec") << " 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
+ 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;
+ int chVal = tryGetSatValue(node[ch]);
+ if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) &&
+ findSplitterRec(node[ch], desiredVal) ) {
+ return true;
+ }
+ }// else (...ifVal...)
+ return false;
+}//handleITE
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
new file mode 100644
index 000000000..93fb3c999
--- /dev/null
+++ b/src/decision/relevancy.h
@@ -0,0 +1,423 @@
+/********************* */
+/*! \file relevancy.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Justification heuristic for decision making
+ **
+ ** A ATGP-inspired justification-based decision heuristic. See
+ ** [insert reference] for more details. This code is, or not, based
+ ** on the CVC3 implementation of the same heuristic.
+ **
+ ** It needs access to the simplified but non-clausal formula.
+ **
+ ** Relevancy
+ ** ---------
+ **
+ ** This class also currently computes the may-relevancy of a node
+ **
+ ** A node is may-relevant if there is a path from the root of the
+ ** formula to the node such that no node on the path is justified. As
+ ** contrapositive, a node is not relevant (with the may-notion) if all
+ ** path from the root to the node go through a justified node.
+ **/
+
+#ifndef __CVC4__DECISION__RELEVANCY
+#define __CVC4__DECISION__RELEVANCY
+
+#include "decision_engine.h"
+#include "decision_strategy.h"
+
+#include "context/cdhashset.h"
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "prop/sat_solver_types.h"
+#include "util/options.h"
+
+namespace CVC4 {
+
+namespace decision {
+
+typedef std::vector<TNode> IteList;
+
+class RelGiveUpException : public Exception {
+public:
+ RelGiveUpException() :
+ Exception("relevancy: giving up") {
+ }
+};/* class GiveUpException */
+
+class Relevancy : public RelevancyStrategy {
+ typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
+ typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
+ typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
+
+ // being 'justified' is monotonic with respect to decisions
+ context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+ context::CDO<unsigned> d_prvsIndex;
+
+ IntStat d_helfulness;
+ IntStat d_polqueries;
+ IntStat d_polhelp;
+ IntStat d_giveup;
+ IntStat d_expense; /* Total number of nodes considered over
+ all calls to the findSplitter function */
+ 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;
+
+ /**
+ * May-relevancy of a node is an integer. For a node n, it becomes
+ * irrelevant when d_maxRelevancy[n] = d_relevancy[n]
+ */
+ hash_map<TNode,int,TNodeHashFunction> d_maxRelevancy;
+ context::CDHashMap<TNode,int,TNodeHashFunction> d_relevancy;
+ PolarityCache d_polarityCache;
+
+ /** **** * * *** * * OPTIONS *** * * ** * * **** */
+
+ /**
+ * do we do "multiple-backtrace" to try to justify a node
+ */
+ bool d_multipleBacktrace;
+ //bool d_computeRelevancy; // are we in a mode where we compute relevancy?
+
+ /** Only leaves can be relevant */
+ Options::DecisionOptions d_opt; // may be we shouldn't be caching them?
+
+ static const double secondsPerDecision = 0.001;
+ static const double secondsPerExpense = 1e-7;
+ static const double EPS = 1e-9;
+ /** Maximum time this algorithm should spent as part of whole algorithm */
+ double d_maxTimeAsPercentageOfTotalTime;
+
+ /** current decision for the recursive call */
+ SatLiteral* d_curDecision;
+public:
+ Relevancy(CVC4::DecisionEngine* de, context::Context *c, const Options::DecisionOptions &decOpt):
+ RelevancyStrategy(de, c),
+ d_justified(c),
+ d_prvsIndex(c, 0),
+ d_helfulness("decision::rel::preventedDecisions", 0),
+ d_polqueries("decision::rel::polarityQueries", 0),
+ d_polhelp("decision::rel::polarityHelp", 0),
+ d_giveup("decision::rel::giveup", 0),
+ d_expense("decision::rel::expense", 0),
+ d_timestat("decision::rel::time"),
+ d_relevancy(c),
+ d_multipleBacktrace(decOpt.computeRelevancy),
+ // d_computeRelevancy(decOpt.computeRelevancy),
+ d_opt(decOpt),
+ d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0),
+ d_curDecision(NULL)
+ {
+ StatisticsRegistry::registerStat(&d_helfulness);
+ StatisticsRegistry::registerStat(&d_polqueries);
+ StatisticsRegistry::registerStat(&d_polhelp);
+ StatisticsRegistry::registerStat(&d_giveup);
+ StatisticsRegistry::registerStat(&d_expense);
+ StatisticsRegistry::registerStat(&d_timestat);
+ Trace("decision") << "relevancy enabled with" << std::endl;
+ Trace("decision") << " * computeRelevancy: " << (d_opt.computeRelevancy ? "on" : "off")
+ << std::endl;
+ Trace("decision") << " * relevancyLeaves: " << (d_opt.relevancyLeaves ? "on" : "off")
+ << std::endl;
+ Trace("decision") << " * mustRelevancy [unimplemented]: " << (d_opt.mustRelevancy ? "on" : "off")
+ << std::endl;
+ }
+ ~Relevancy() {
+ StatisticsRegistry::unregisterStat(&d_helfulness);
+ StatisticsRegistry::unregisterStat(&d_polqueries);
+ StatisticsRegistry::unregisterStat(&d_polhelp);
+ StatisticsRegistry::unregisterStat(&d_giveup);
+ StatisticsRegistry::unregisterStat(&d_expense);
+ StatisticsRegistry::unregisterStat(&d_timestat);
+ }
+ prop::SatLiteral getNext(bool &stopSearch) {
+ Debug("decision") << std::endl;
+ Trace("decision") << "Relevancy::getNext()" << std::endl;
+ TimerStat::CodeTimer codeTimer(d_timestat);
+
+ if( d_maxTimeAsPercentageOfTotalTime < 100.0 - EPS &&
+ double(d_polqueries.getData())*secondsPerDecision <
+ d_maxTimeAsPercentageOfTotalTime*double(d_expense.getData())*secondsPerExpense
+ ) {
+ ++d_giveup;
+ return undefSatLiteral;
+ }
+
+ d_visited.clear();
+ d_polarityCache.clear();
+
+ for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
+ Trace("decision") << 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 = findSplitter(d_assertions[i], desiredVal);
+
+ if(!d_opt.computeRelevancy && litDecision != undefSatLiteral) {
+ d_prvsIndex = i;
+ return litDecision;
+ }
+ }
+
+ if(d_opt.computeRelevancy) return undefSatLiteral;
+
+ Trace("decision") << "jh: Nothing to split on " << std::endl;
+
+#if defined CVC4_ASSERTIONS || 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;
+ }
+
+ void addAssertions(const std::vector<Node> &assertions,
+ unsigned assertionsEnd,
+ IteSkolemMap iteSkolemMap) {
+ Trace("decision")
+ << "Relevancy::addAssertions()"
+ << " size = " << assertions.size()
+ << " assertionsEnd = " << assertionsEnd
+ << std::endl;
+
+ // 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];
+ }
+
+ // Save the 'real' assertions locally
+ for(unsigned i = 0; i < assertionsEnd; ++i) {
+ d_assertions.push_back(assertions[i]);
+ d_visited.clear();
+ if(d_opt.computeRelevancy) increaseMaxRelevancy(assertions[i]);
+ d_visited.clear();
+ }
+
+ }
+
+ bool isRelevant(TNode n) {
+ Trace("decision") << "isRelevant(" << n << "): ";
+
+ if(Debug.isOn("decision")) {
+ if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) {
+ // we are becuase of not getting information about literals
+ // created using newLiteral command... need to figure how to
+ // handle that
+ Warning() << "isRelevant: WARNING: didn't find node when we should had" << std::endl;
+ // Warning() doesn't work for some reason
+ cout << "isRelevant: WARNING: didn't find node when we should had" << std::endl;
+ }
+ }
+
+ if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) {
+ Trace("decision") << "yes [not found in db]" << std::endl;
+ return true;
+ }
+
+ if(d_opt.relevancyLeaves && !isAtomicFormula(n)) {
+ Trace("decision") << "no [not a leaf]" << std::endl;
+ return false;
+ }
+
+ Trace("decision") << (d_maxRelevancy[n] == d_relevancy[n] ? "no":"yes")
+ << std::endl;
+
+ Debug("decision") << " maxRel: " << (d_maxRelevancy[n] )
+ << " rel: " << d_relevancy[n].get() << std::endl;
+ // Assert(d_maxRelevancy.find(n) != d_maxRelevancy.end());
+ Assert(0 <= d_relevancy[n] && d_relevancy[n] <= d_maxRelevancy[n]);
+
+ if(d_maxRelevancy[n] == d_relevancy[n]) {
+ ++d_helfulness; // preventedDecisions
+ return false;
+ } else {
+ return true;
+ }
+ }
+
+ SatValue getPolarity(TNode n) {
+ Trace("decision") << "getPolarity([" << n.getId() << "]" << n << "): ";
+ Assert(n.getKind() != kind::NOT);
+ ++d_polqueries;
+ PolarityCache::iterator it = d_polarityCache.find(n);
+ if(it == d_polarityCache.end()) {
+ Trace("decision") << "don't know" << std::endl;
+ return SAT_VALUE_UNKNOWN;
+ } else {
+ ++d_polhelp;
+ Trace("decision") << it->second << std::endl;
+ return it->second;
+ }
+ }
+
+ /* Compute justified */
+ /*bool computeJustified() {
+
+ }*/
+private:
+ SatLiteral findSplitter(TNode node, SatValue desiredVal)
+ {
+ bool ret;
+ SatLiteral litDecision;
+ try {
+ // init
+ d_curDecision = &litDecision;
+
+ // solve
+ ret = findSplitterRec(node, desiredVal);
+
+ // post
+ d_curDecision = NULL;
+ }catch(RelGiveUpException &e) {
+ return prop::undefSatLiteral;
+ }
+ if(ret == true) {
+ Trace("decision") << "Yippee!!" << std::endl;
+ return litDecision;
+ } else {
+ return undefSatLiteral;
+ }
+ }
+
+ /**
+ * Do all the hardwork.
+ * Return 'true' if the node cannot be justfied, 'false' it it can be.
+ * Sets 'd_curDecision' if unable to justify (depending on the mode)
+ * If 'd_computeRelevancy' is on does multiple backtrace
+ */
+ bool findSplitterRec(TNode node, SatValue value);
+ // Functions to make findSplitterRec modular...
+ bool handleOrFalse(TNode node, SatValue desiredVal);
+ bool handleOrTrue(TNode node, SatValue desiredVal);
+ bool handleITE(TNode node, SatValue desiredVal);
+
+ /* Helper functions */
+ void setJustified(TNode);
+ bool checkJustified(TNode);
+
+ /* If literal exists corresponding to the node return
+ that. Otherwise an 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);
+
+ /* Checks whether something is an atomic formula or not */
+ bool isAtomicFormula(TNode n) {
+ return theory::kindToTheoryId(n.getKind()) != theory::THEORY_BOOL;
+ }
+
+ /** Recursively increase relevancies */
+ void updateRelevancy(TNode n) {
+ if(d_visited.find(n) != d_visited.end()) return;
+
+ Assert(d_relevancy[n] <= d_maxRelevancy[n]);
+
+ if(d_relevancy[n] != d_maxRelevancy[n])
+ return;
+
+ d_visited.insert(n);
+ if(isAtomicFormula(n)) {
+ const IteList& l = getITEs(n);
+ for(unsigned i = 0; i < l.size(); ++i) {
+ if(d_visited.find(l[i]) == d_visited.end()) continue;
+ d_relevancy[l[i]] = d_relevancy[l[i]] + 1;
+ updateRelevancy(l[i]);
+ }
+ } else {
+ for(unsigned i = 0; i < n.getNumChildren(); ++i) {
+ if(d_visited.find(n[i]) == d_visited.end()) continue;
+ d_relevancy[n[i]] = d_relevancy[n[i]] + 1;
+ updateRelevancy(n[i]);
+ }
+ }
+ d_visited.erase(n);
+ }
+
+ /* */
+ void increaseMaxRelevancy(TNode n) {
+
+ Debug("decision")
+ << "increaseMaxRelevancy([" << n.getId() << "]" << n << ")"
+ << std::endl;
+
+ d_maxRelevancy[n]++;
+
+ // don't update children multiple times
+ if(d_visited.find(n) != d_visited.end()) return;
+
+ d_visited.insert(n);
+ // Part to make the recursive call
+ if(isAtomicFormula(n)) {
+ const IteList& l = getITEs(n);
+ for(unsigned i = 0; i < l.size(); ++i)
+ if(d_visited.find(l[i]) == d_visited.end())
+ increaseMaxRelevancy(l[i]);
+ } else {
+ for(unsigned i = 0; i < n.getNumChildren(); ++i)
+ increaseMaxRelevancy(n[i]);
+ } //else (...atomic formula...)
+ }
+
+};/* class Relevancy */
+
+}/* namespace decision */
+
+}/* namespace CVC4 */
+
+#endif /* __CVC4__DECISION__RELEVANCY */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback