summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.h1
-rw-r--r--src/decision/decision_mode.h9
-rw-r--r--src/decision/justification_heuristic.cpp346
-rw-r--r--src/decision/justification_heuristic.h58
-rw-r--r--src/decision/options12
-rw-r--r--src/decision/options_handlers.h13
-rw-r--r--src/prop/minisat/core/Solver.cc18
-rw-r--r--src/prop/theory_proxy.cpp11
-rw-r--r--src/prop/theory_proxy.h4
-rw-r--r--src/theory/bv/bitblaster.cpp7
-rw-r--r--src/theory/bv/bitblaster.h1
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp7
-rw-r--r--src/theory/bv/theory_bv.cpp6
-rw-r--r--src/theory/bv/theory_bv.h1
-rw-r--r--src/theory/bv/theory_bv_utils.h22
-rw-r--r--src/theory/decision_attributes.h36
-rw-r--r--test/regress/regress0/bv/Makefile.am1
-rw-r--r--test/regress/regress0/bv/decision-weight00.smt219
-rw-r--r--test/regress/regress0/bv/fuzz02.delta01.smt18
19 files changed, 503 insertions, 87 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 5d7c5ea74..bc071f7f6 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 "theory/decision_attributes.h"
#include "util/ite_removal.h"
#include "util/output.h"
diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h
index 335e6279e..20743cba1 100644
--- a/src/decision/decision_mode.h
+++ b/src/decision/decision_mode.h
@@ -46,6 +46,15 @@ enum DecisionMode {
};/* enum DecisionMode */
+
+/** Enumeration of combining functions for computing internal weights */
+enum DecisionWeightInternal {
+ DECISION_WEIGHT_INTERNAL_OFF,
+ DECISION_WEIGHT_INTERNAL_MAX,
+ DECISION_WEIGHT_INTERNAL_SUM,
+ DECISION_WEIGHT_INTERNAL_USR1
+};/* enum DecisionInternalWeight */
+
}/* CVC4::decision namespace */
std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC;
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 28d26adb1..de49f6e0a 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -22,6 +22,7 @@
#include "expr/node_manager.h"
#include "expr/kind.h"
#include "theory/rewriter.h"
+#include "decision/options.h"
#include "util/ite_removal.h"
@@ -32,7 +33,9 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
context::Context *c):
ITEDecisionStrategy(de, c),
d_justified(c),
+ d_exploredThreshold(c),
d_prvsIndex(c, 0),
+ d_threshPrvsIndex(c, 0),
d_helfulness("decision::jh::helpfulness", 0),
d_giveup("decision::jh::giveup", 0),
d_timestat("decision::jh::time"),
@@ -41,7 +44,10 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
d_iteCache(uc),
d_visited(),
d_visitedComputeITE(),
- d_curDecision() {
+ d_curDecision(),
+ d_curThreshold(0),
+ d_childCache(uc),
+ d_weightCache(uc) {
StatisticsRegistry::registerStat(&d_helfulness);
StatisticsRegistry::registerStat(&d_giveup);
StatisticsRegistry::registerStat(&d_timestat);
@@ -54,11 +60,26 @@ JustificationHeuristic::~JustificationHeuristic() {
StatisticsRegistry::unregisterStat(&d_timestat);
}
-CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) {
- Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
+CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
+{
+ if(options::decisionThreshold() > 0) {
+ bool stopSearchTmp = false;
+ SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold());
+ if(lit != undefSatLiteral) {
+ Assert(stopSearchTmp == false);
+ return lit;
+ }
+ Assert(stopSearchTmp == true);
+ }
+ return getNextThresh(stopSearch, 0);
+}
+
+CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, DecisionWeight threshold) {
+ Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl;
TimerStat::CodeTimer codeTimer(d_timestat);
d_visited.clear();
+ d_curThreshold = threshold;
if(Trace.isOn("justified")) {
for(JustifiedSet::key_iterator i = d_justified.key_begin();
@@ -71,7 +92,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) {
}
}
- for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
+ for(unsigned i = getPrvsIndex(); i < d_assertions.size(); ++i) {
Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
// Sanity check: if it was false, aren't we inconsistent?
@@ -83,7 +104,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) {
litDecision = findSplitter(d_assertions[i], desiredVal);
if(litDecision != undefSatLiteral) {
- d_prvsIndex = i;
+ setPrvsIndex(i);
return litDecision;
}
}
@@ -104,12 +125,13 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) {
<< d_assertions[i] << std::endl;
}
}
- Assert(alljustified);
+ Assert(alljustified || d_curThreshold != 0);
#endif
// SAT solver can stop...
stopSearch = true;
- d_decisionEngine->setResult(SAT_VALUE_TRUE);
+ if(d_curThreshold == 0)
+ d_decisionEngine->setResult(SAT_VALUE_TRUE);
return prop::undefSatLiteral;
}
@@ -164,6 +186,8 @@ void JustificationHeuristic::addAssertions
d_iteAssertions[i->first] = assertions[i->second];
}
+
+ // Automatic weight computation
}
SatLiteral JustificationHeuristic::findSplitter(TNode node,
@@ -187,6 +211,139 @@ bool JustificationHeuristic::checkJustified(TNode n)
return d_justified.find(n) != d_justified.end();
}
+DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n)
+{
+ return
+ d_exploredThreshold.find(n) == d_exploredThreshold.end() ?
+ numeric_limits<DecisionWeight>::max() : d_exploredThreshold[n];
+}
+
+void JustificationHeuristic::setExploredThreshold(TNode n)
+{
+ d_exploredThreshold[n] = d_curThreshold;
+}
+
+int JustificationHeuristic::getPrvsIndex()
+{
+ if(d_curThreshold == 0)
+ return d_prvsIndex;
+ else
+ return d_threshPrvsIndex;
+}
+
+void JustificationHeuristic::setPrvsIndex(int prvsIndex)
+{
+ if(d_curThreshold == 0)
+ d_prvsIndex = prvsIndex;
+ else
+ d_threshPrvsIndex = prvsIndex;
+}
+
+DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satValue)
+{
+ Assert(satValue == SAT_VALUE_TRUE || satValue == SAT_VALUE_FALSE);
+ return getWeightPolarized(n, satValue == SAT_VALUE_TRUE);
+}
+
+DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity)
+{
+ if(options::decisionWeightInternal() != DECISION_WEIGHT_INTERNAL_USR1) {
+ return getWeight(n);
+ }
+
+ if(d_weightCache.find(n) == d_weightCache.end()) {
+ Kind k = n.getKind();
+ theory::TheoryId tId = theory::kindToTheoryId(k);
+ DecisionWeight dW1, dW2;
+ if(tId != theory::THEORY_BOOL) {
+ dW1 = dW2 = getWeight(n);
+ } else {
+
+ if(k == kind::OR) {
+ dW1 = numeric_limits<DecisionWeight>::max(), dW2 = 0;
+ for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
+ dW1 = min(dW1, getWeightPolarized(*i, true));
+ dW2 = max(dW2, getWeightPolarized(*i, false));
+ }
+ } else if(k == kind::AND) {
+ dW1 = 0, dW2 = numeric_limits<DecisionWeight>::max();
+ for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
+ dW1 = max(dW1, getWeightPolarized(*i, true));
+ dW2 = min(dW2, getWeightPolarized(*i, false));
+ }
+ } else if(k == kind::IMPLIES) {
+ dW1 = min(getWeightPolarized(n[0], false),
+ getWeightPolarized(n[1], true));
+ dW2 = max(getWeightPolarized(n[0], true),
+ getWeightPolarized(n[1], false));
+ } else if(k == kind::NOT) {
+ dW1 = getWeightPolarized(n[0], false);
+ dW2 = getWeightPolarized(n[0], true);
+ } else {
+ dW1 = 0;
+ for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
+ dW1 = max(dW1, getWeightPolarized(*i, true));
+ dW1 = max(dW1, getWeightPolarized(*i, false));
+ }
+ dW2 = dW1;
+ }
+
+ }
+ d_weightCache[n] = make_pair(dW1, dW2);
+ }
+ return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second;
+}
+
+DecisionWeight JustificationHeuristic::getWeight(TNode n) {
+ if(!n.hasAttribute(theory::DecisionWeightAttr()) ) {
+
+ DecisionWeightInternal combiningFn =
+ options::decisionWeightInternal();
+
+ if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) {
+
+ if(options::decisionRandomWeight() != 0) {
+ n.setAttribute(theory::DecisionWeightAttr(), rand() % options::decisionRandomWeight());
+ }
+
+ } else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) {
+
+ DecisionWeight dW = 0;
+ for(TNode::iterator i=n.begin(); i != n.end(); ++i)
+ dW = max(dW, getWeight(*i));
+ n.setAttribute(theory::DecisionWeightAttr(), dW);
+
+ } else if(combiningFn == DECISION_WEIGHT_INTERNAL_SUM ||
+ combiningFn == DECISION_WEIGHT_INTERNAL_USR1) {
+ DecisionWeight dW = 0;
+ for(TNode::iterator i=n.begin(); i != n.end(); ++i)
+ dW = max(dW, getWeight(*i));
+ n.setAttribute(theory::DecisionWeightAttr(), dW);
+
+ } else {
+ Unreachable();
+ }
+
+ }
+ return n.getAttribute(theory::DecisionWeightAttr());
+}
+
+typedef vector<TNode> ChildList;
+TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
+ if(options::decisionUseWeight()) {
+ // TODO: Optimize storing & access
+ if(d_childCache.find(n) == d_childCache.end()) {
+ ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end());
+ std::sort(list0.begin(), list0.end(), JustificationHeuristic::myCompareClass(this,false));
+ std::sort(list1.begin(), list1.end(), JustificationHeuristic::myCompareClass(this,true));
+ d_childCache[n] = make_pair(list0, list1);
+ }
+ return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i];
+ } else {
+ return n[i];
+ }
+}
+
SatValue JustificationHeuristic::tryGetSatValue(Node n)
{
Debug("decision") << " " << n << " has sat value " << " ";
@@ -233,8 +390,8 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l)
}
}
-bool JustificationHeuristic::findSplitterRec(TNode node,
- SatValue desiredVal)
+JustificationHeuristic::SearchResult
+JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
{
/**
* Main idea
@@ -258,7 +415,12 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
/* Base case */
if (checkJustified(node)) {
Debug("decision::jh") << " justified, returning" << std::endl;
- return false;
+ return NO_SPLITTER;
+ }
+ if (getExploredThreshold(node) < d_curThreshold) {
+ Debug("decision::jh") << " explored, returning" << std::endl;
+ Assert(d_curThreshold != 0);
+ return DONT_KNOW;
}
#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
@@ -298,23 +460,25 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
if(tId != theory::THEORY_BOOL) {
// if node has embedded ites, resolve that first
- if(handleEmbeddedITEs(node))
- return true;
+ if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
if(litVal != SAT_VALUE_UNKNOWN) {
setJustified(node);
- return false;
+ return NO_SPLITTER;
}
else {
Assert(d_decisionEngine->hasSatLiteral(node));
- SatVariable v =
+ if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold)
+ return DONT_KNOW;
+ SatVariable v =
d_decisionEngine->getSatLiteral(node).getSatVariable();
d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
- return true;
+ return FOUND_SPLITTER;
}
}
- bool ret = false;
+ SearchResult ret = NO_SPLITTER;
switch (k) {
case kind::CONST_BOOLEAN:
@@ -365,65 +529,108 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
break;
}//end of switch(k)
- if(ret == false) {
- Assert(litPresent == false || litVal == desiredVal,
+ if(ret == DONT_KNOW) {
+ setExploredThreshold(node);
+ }
+
+ if(ret == NO_SPLITTER) {
+ Assert( litPresent == false || litVal == desiredVal,
"Output should be justified");
setJustified(node);
}
return ret;
}/* findRecSplit method */
-bool JustificationHeuristic::handleAndOrEasy(TNode node,
- SatValue desiredVal)
+JustificationHeuristic::SearchResult
+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;
+ for(int i = 0; i < numChildren; ++i) {
+ TNode curNode = getChildByWeight(node, i, desiredVal);
+ if ( tryGetSatValue(curNode) != desiredValInverted ) {
+ SearchResult ret = findSplitterRec(curNode, desiredVal);
+ if(ret != DONT_KNOW)
+ return ret;
+ }
+ }
+ Assert(d_curThreshold != 0, "handleAndOrEasy: No controlling input found");
+ return DONT_KNOW;
}
-bool JustificationHeuristic::handleAndOrHard(TNode node,
+JustificationHeuristic::SearchResult 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 noSplitter = true;
+ for(int i = 0; i < numChildren; ++i) {
+ TNode curNode = getChildByWeight(node, i, desiredVal);
+ SearchResult ret = findSplitterRec(curNode, desiredVal);
+ if (ret == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
+ noSplitter = noSplitter && (ret == NO_SPLITTER);
+ }
+ return noSplitter ? NO_SPLITTER : DONT_KNOW;
}
-bool JustificationHeuristic::handleBinaryEasy(TNode node1,
+JustificationHeuristic::SearchResult 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;
+ if(options::decisionUseWeight() &&
+ getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
+ swap(node1, node2);
+ swap(desiredVal1, desiredVal2);
+ }
+
+ if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) {
+ SearchResult ret = findSplitterRec(node1, desiredVal1);
+ if(ret != DONT_KNOW)
+ return ret;
+ }
+ if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) {
+ SearchResult ret = findSplitterRec(node2, desiredVal2);
+ if(ret != DONT_KNOW)
+ return ret;
+ }
+ Assert(d_curThreshold != 0, "handleBinaryEasy: No controlling input found");
+ return DONT_KNOW;
}
-bool JustificationHeuristic::handleBinaryHard(TNode node1,
+JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TNode node1,
SatValue desiredVal1,
TNode node2,
SatValue desiredVal2)
{
- if( findSplitterRec(node1, desiredVal1) )
- return true;
- return findSplitterRec(node2, desiredVal2);
+ if(options::decisionUseWeight() &&
+ getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
+ swap(node1, node2);
+ swap(desiredVal1, desiredVal2);
+ }
+
+ bool noSplitter = true;
+ SearchResult ret;
+
+ ret = findSplitterRec(node1, desiredVal1);
+ if (ret == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
+ noSplitter &= (ret == NO_SPLITTER);
+
+ ret = findSplitterRec(node2, desiredVal2);
+ if (ret == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
+ noSplitter &= (ret == NO_SPLITTER);
+
+ return noSplitter ? NO_SPLITTER : DONT_KNOW;
}
-bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
+JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
{
Debug("decision::jh") << " handleITE (" << node << ", "
<< desiredVal << std::endl;
@@ -431,48 +638,59 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
//[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;
+ SatValue trueChildVal = tryGetSatValue(node[1]);
+ SatValue falseChildVal = tryGetSatValue(node[2]);
+ SatValue ifDesiredVal;
+
+ if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) {
+ ifDesiredVal = SAT_VALUE_TRUE;
+ } else if(trueChildVal == invertValue(desiredVal) ||
+ falseChildVal == desiredVal ||
+ (options::decisionUseWeight() &&
+ getWeightPolarized(node[1], true) > getWeightPolarized(node[2], false))
+ ) {
+ ifDesiredVal = SAT_VALUE_FALSE;
+ } else {
+ ifDesiredVal = SAT_VALUE_TRUE;
+ }
+
+ if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
- Assert(false, "No controlling input found (6)");
+ Assert(d_curThreshold != 0, "No controlling input found (6)");
+ return DONT_KNOW;
} else {
// Try to justify 'if'
- if(findSplitterRec(node[0], ifVal)) return true;
+ if(findSplitterRec(node[0], ifVal) == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
// 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;
+ if( findSplitterRec(node[ch], desiredVal) == FOUND_SPLITTER ) {
+ return FOUND_SPLITTER;
}
+
+ return NO_SPLITTER;
}// else (...ifVal...)
- return false;
}
-bool JustificationHeuristic::handleEmbeddedITEs(TNode node)
+JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node)
{
const IteList l = getITEs(node);
Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+ bool noSplitter = true;
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;
+ SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE);
+ if (ret == FOUND_SPLITTER)
+ return FOUND_SPLITTER;
+ noSplitter = noSplitter && (ret == NO_SPLITTER);
d_visited.erase((*i).first);
}
}
- return false;
+ return noSplitter ? NO_SPLITTER : DONT_KNOW;
}
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 503f6c2af..01458d9ea 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -37,14 +37,23 @@ namespace CVC4 {
namespace decision {
class JustificationHeuristic : public ITEDecisionStrategy {
+ // TRUE FALSE MEH
+ enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
+
typedef std::vector<pair<TNode,TNode> > IteList;
typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
+ typedef std::vector<TNode> ChildList;
+ typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
+ typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache;
// being 'justified' is monotonic with respect to decisions
typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
JustifiedSet d_justified;
+ typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold;
+ ExploredThreshold d_exploredThreshold;
context::CDO<unsigned> d_prvsIndex;
+ context::CDO<unsigned> d_threshPrvsIndex;
IntStat d_helfulness;
IntStat d_giveup;
@@ -80,6 +89,26 @@ class JustificationHeuristic : public ITEDecisionStrategy {
/** current decision for the recursive call */
SatLiteral d_curDecision;
+ /** current threshold for the recursive call */
+ DecisionWeight d_curThreshold;
+
+ /** child cache */
+ ChildCache d_childCache;
+
+ /** computed polarized weight cache */
+ WeightCache d_weightCache;
+
+
+ class myCompareClass {
+ JustificationHeuristic* d_jh;
+ bool d_b;
+ public:
+ myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {};
+ bool operator() (TNode n1, TNode n2) {
+ return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b);
+ }
+ };
+
public:
JustificationHeuristic(CVC4::DecisionEngine* de,
context::UserContext *uc,
@@ -94,17 +123,30 @@ public:
IteSkolemMap iteSkolemMap);
private:
+ /* getNext with an option to specify threshold */
+ prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
+
SatLiteral findSplitter(TNode node, SatValue desiredVal);
/**
* Do all the hard work.
*/
- bool findSplitterRec(TNode node, SatValue value);
+ SearchResult findSplitterRec(TNode node, SatValue value);
/* Helper functions */
void setJustified(TNode);
bool checkJustified(TNode);
-
+ DecisionWeight getExploredThreshold(TNode);
+ void setExploredThreshold(TNode);
+ void setPrvsIndex(int);
+ int getPrvsIndex();
+ DecisionWeight getWeightPolarized(TNode n, bool polarity);
+ DecisionWeight getWeightPolarized(TNode n, SatValue);
+ static DecisionWeight getWeight(TNode);
+ bool compareByWeightFalse(TNode, TNode);
+ bool compareByWeightTrue(TNode, TNode);
+ TNode getChildByWeight(TNode n, int i, bool polarity);
+
/* If literal exists corresponding to the node return
that. Otherwise an UNKNOWN */
SatValue tryGetSatValue(Node n);
@@ -115,14 +157,14 @@ 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,
+ SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
+ SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
+ SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1,
TNode node2, SatValue desiredVal2);
- bool handleBinaryHard(TNode node1, SatValue desiredVal1,
+ SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
TNode node2, SatValue desiredVal2);
- bool handleITE(TNode node, SatValue desiredVal);
- bool handleEmbeddedITEs(TNode node);
+ SearchResult handleITE(TNode node, SatValue desiredVal);
+ SearchResult handleEmbeddedITEs(TNode node);
};/* class JustificationHeuristic */
}/* namespace decision */
diff --git a/src/decision/options b/src/decision/options
index 7e457f125..b86577e7b 100644
--- a/src/decision/options
+++ b/src/decision/options
@@ -20,4 +20,16 @@ option decisionMustRelevancy bool
# only use DE to determine when to stop, not to make decisions
option decisionStopOnly bool
+expert-option decisionThreshold --decision-threshold=N decision::DecisionWeight :default 0 :include "theory/decision_attributes.h"
+ ignore all nodes greater than threshold in first attempt to pick decision
+
+expert-option decisionUseWeight --decision-use-weight bool :default false
+ use the weight nodes (locally, by looking at children) to direct recursive search
+
+expert-option decisionRandomWeight --decision-random-weight=N int :default 0
+ assign random weights to nodes between 0 and N-1 (0: disable)
+
+expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::decision::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "decision/options_handlers.h"
+ computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)
+
endmodule
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index 1d4321614..05d975ef1 100644
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -107,6 +107,19 @@ inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEn
}
}
+inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "off")
+ return DECISION_WEIGHT_INTERNAL_OFF;
+ else if(optarg == "max")
+ return DECISION_WEIGHT_INTERNAL_MAX;
+ else if(optarg == "sum")
+ return DECISION_WEIGHT_INTERNAL_SUM;
+ else if(optarg == "usr1")
+ return DECISION_WEIGHT_INTERNAL_USR1;
+ else
+ throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
+}
+
}/* CVC4::decision namespace */
}/* CVC4 namespace */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c7f1780b6..6196ca357 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -458,9 +458,8 @@ Lit Solver::pickBranchLit()
}
#endif /* CVC4_REPLAY */
- // Theory/DE requests
- bool stopSearch = false;
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+ // Theory requests
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
while (nextLit != lit_Undef) {
if(value(var(nextLit)) == l_Undef) {
Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
@@ -469,12 +468,21 @@ Lit Solver::pickBranchLit()
} else {
Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
}
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
}
+ Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
+
+ // DE requests
+ bool stopSearch = false;
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
if(stopSearch) {
return lit_Undef;
}
- Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
+ if(nextLit != lit_Undef) {
+ Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value");
+ decisions++;
+ return nextLit;
+ }
Var next = var_Undef;
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index a6908ff52..c9f19b42e 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -79,15 +79,12 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
d_queue.push(literalNode);
}
-SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
+SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
TNode n = d_theoryEngine->getNextDecisionRequest();
- if(not n.isNull()) {
- return d_cnfStream->getLiteral(n);
- }
+ return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
+}
- // If theory doesn't give us a deicsion ask the decision engine. It
- // may return in undefSatLiteral in which case the sat solver uses
- // whatever default heuristic it has.
+SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
Assert(d_decisionEngine != NULL);
Assert(stopSearch != true);
SatLiteral ret = d_decisionEngine->getNext(stopSearch);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 5f1ea0e23..7b0aa2058 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -93,7 +93,9 @@ public:
void enqueueTheoryLiteral(const SatLiteral& l);
- SatLiteral getNextDecisionRequest(bool& stopSearch);
+ SatLiteral getNextTheoryDecisionRequest();
+
+ SatLiteral getNextDecisionEngineRequest(bool& stopSearch);
bool theoryNeedCheck() const;
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index ad62ade38..8579012ab 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -108,6 +108,13 @@ void Bitblaster::bbAtom(TNode node) {
}
}
+uint64_t Bitblaster::computeAtomWeight(TNode node) {
+ node = node.getKind() == kind::NOT? node[0] : node;
+
+ Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
+ uint64_t size = utils::numNodes(atom_bb);
+ return size;
+}
void Bitblaster::bbTerm(TNode node, Bits& bits) {
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 2c52a2670..c122c407d 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -165,6 +165,7 @@ public:
}
bool isSharedTerm(TNode node);
+ uint64_t computeAtomWeight(TNode node);
private:
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 997244c40..2308f36a3 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -19,6 +19,8 @@
#include "theory/bv/theory_bv_utils.h"
#include "theory/bv/bitblaster.h"
#include "theory/bv/options.h"
+#include "theory/decision_attributes.h"
+#include "decision/options.h"
using namespace std;
using namespace CVC4;
@@ -58,7 +60,12 @@ void BitblastSolver::preRegister(TNode node) {
if (options::bitvectorEagerBitblast()) {
d_bitblaster->bbAtom(node);
} else {
+ CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
d_bitblastQueue.push_back(node);
+ if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
+ !node.hasAttribute(theory::DecisionWeightAttr())) {
+ node.setAttribute(theory::DecisionWeightAttr(), d_bitblaster->computeAtomWeight(node));
+ }
}
}
}
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 433223308..c597cb083 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -78,13 +78,15 @@ TheoryBV::Statistics::Statistics():
d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
d_solveTimer("theory::bv::solveTimer"),
d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
- d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0)
+ d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
+ d_weightComputationTimer("theory::bv::weightComputationTimer")
{
StatisticsRegistry::registerStat(&d_avgConflictSize);
StatisticsRegistry::registerStat(&d_solveSubstitutions);
StatisticsRegistry::registerStat(&d_solveTimer);
StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
+ StatisticsRegistry::registerStat(&d_weightComputationTimer);
}
TheoryBV::Statistics::~Statistics() {
@@ -93,6 +95,7 @@ TheoryBV::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_solveTimer);
StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
+ StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
}
@@ -205,6 +208,7 @@ void TheoryBV::propagate(Effort e) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
// temporary fix for incremental bit-blasting
if (d_valuation.isSatLiteral(literal)) {
+ Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
ok = d_out->propagate(literal);
}
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8b184f972..481493e13 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -78,6 +78,7 @@ private:
TimerStat d_solveTimer;
IntStat d_numCallsToCheckFullEffort;
IntStat d_numCallsToCheckStandardEffort;
+ TimerStat d_weightComputationTimer;
Statistics();
~Statistics();
};
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dffdf10df..174df03ab 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -23,7 +23,7 @@
#include <vector>
#include <sstream>
#include "expr/node_manager.h"
-
+#include "theory/decision_attributes.h"
namespace CVC4 {
@@ -493,6 +493,26 @@ inline T gcd(T a, T b) {
}
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
+inline uint64_t numNodesAux(TNode node, TNodeSet& seen) {
+ if (seen.find(node) != seen.end())
+ return 0;
+
+ uint64_t size = 1;
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ size += numNodesAux(node[i], seen);
+ }
+ seen.insert(node);
+ return size;
+}
+
+inline uint64_t numNodes(TNode node) {
+ TNodeSet seen;
+ uint64_t size = numNodesAux(node, seen);
+ return size;
+}
+
}
}
}
diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h
new file mode 100644
index 000000000..204362a2a
--- /dev/null
+++ b/src/theory/decision_attributes.h
@@ -0,0 +1,36 @@
+/********************* */
+/*! \file decision_attributes.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewriter attributes
+ **
+ ** Rewriter attributes.
+ **/
+
+#ifndef __CVC4__THEORY__DECISION_ATRRIBUTES
+#define __CVC4__THEORY__DECISION_ATRRIBUTES
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace decision {
+typedef uint64_t DecisionWeight;
+}
+namespace theory {
+namespace attr {
+ struct DecisionWeightTag {};
+}/* CVC4::theory::attr namespace */
+
+typedef expr::Attribute<attr::DecisionWeightTag, decision::DecisionWeight> DecisionWeightAttr;
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DECISION_ATRRIBUTES */
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 5d3fe371e..dbd9547a9 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -20,6 +20,7 @@ MAKEFLAGS = -k
# Regression tests for SMT inputs
SMT_TESTS = \
fuzz01.smt \
+ fuzz02.delta01.smt \
fuzz02.smt \
fuzz03.smt \
fuzz04.smt \
diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2
new file mode 100644
index 000000000..1feb32c7f
--- /dev/null
+++ b/test/regress/regress0/bv/decision-weight00.smt2
@@ -0,0 +1,19 @@
+(set-option :produce-models true)
+(set-logic QF_BV)
+(set-info :source |
+ Patrice Godefroid, SAGE (systematic dynamic test generation)
+ For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun x () (_ BitVec 32))
+(declare-fun y () (_ BitVec 32))
+(declare-fun z () (_ BitVec 4))
+(assert (or
+ (= x (bvmul x y))
+ (and (= x y)
+ (not (= ((_ extract 2 2) x) ((_ extract 2 2) z))))
+ ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/fuzz02.delta01.smt b/test/regress/regress0/bv/fuzz02.delta01.smt
new file mode 100644
index 000000000..1ef924ef1
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz02.delta01.smt
@@ -0,0 +1,18 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v2 BitVec[9]))
+:status unsat
+:formula
+(let (?n1 bv0[2])
+(let (?n2 bv0[6])
+(flet ($n3 (bvult v2 v2))
+(let (?n4 bv1[1])
+(let (?n5 bv0[1])
+(let (?n6 (ite $n3 ?n4 ?n5))
+(let (?n7 (concat ?n2 ?n6))
+(let (?n8 bv0[7])
+(let (?n9 (bvcomp ?n7 ?n8))
+(let (?n10 (zero_extend[1] ?n9))
+(flet ($n11 (= ?n1 ?n10))
+$n11
+))))))))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback