From: Kshitij Bansal Date: Sat, 16 Jun 2012 22:44:20 +0000 (+0000) Subject: This is an attempt to fix the bug in the justification heuristic. The X-Git-Tag: cvc5-1.0.0~7991 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a45b80a981a875cb560876dee2eb7bfa9db1e08;p=cvc5.git This is an attempt to fix the bug in the justification heuristic. The other minor change is removing dependency of header file in theory_engine.h It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a wrong answer for QF_AUFLIA -- it is currently unclear what is the cause of this bug, could be sharing. Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of course, those for which the answer was wrong earlier; and also perhaps one or two off-cases) The issue was with how the infinite loop in justification stuff was prevented. To keep it short, I skip what was wrong earlier, and this is what is done now: * whenever an atomic formula is seen, a list of pairs of is created for each skolem occuring in the atom. * we iterate over this list, doing the following: check if skolem is marked as visited. if not, mark visited, recurse, when back unmark. I lied, I will tell you what was being done earlier was -- 1. the check for not being visited was being done in each recursive call, not just for atoms. 2. The AssertionCorrespondingToIteSkolem was being used to check if something is visited and not IteSkolemVariable. I don't know if this makes any difference, but anyhow, I think this is cleaner & clearer, so I keep this. --- diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 93ff65e6d..065d40a9a 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -96,16 +96,18 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n) void JustificationHeuristic::computeITEs(TNode n, IteList &l) { - Debug("jh-ite") << " computeITEs( " << n << ", &l)\n"; + Trace("jh-ite") << " computeITEs( " << n << ", &l)\n"; for(unsigned i=0; isecond); + if(it2 != d_iteAssertions.end()) { + l.push_back(make_pair(n[i], it2->second)); + Assert(n[i].getNumChildren() == 0); + } computeITEs(n[i], l); } } -const IteList& JustificationHeuristic::getITEs(TNode n) +const JustificationHeuristic::IteList& JustificationHeuristic::getITEs(TNode n) { IteCache::iterator it = d_iteCache.find(n); if(it != d_iteCache.end()) { @@ -113,7 +115,7 @@ const IteList& JustificationHeuristic::getITEs(TNode n) } else { // Compute the list of ITEs // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = vector(); + d_iteCache[n] = IteList(); computeITEs(n, d_iteCache[n]); return d_iteCache[n]; } @@ -123,7 +125,7 @@ bool JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal, SatLiteral* litDecision) { - Trace("decision") + Trace("jh-findSplitterRec") << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; @@ -136,36 +138,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node, if(Debug.isOn("decision")) { if(checkJustified(node)) Debug("decision") << " justified, returning" << std::endl; - if(d_visited.find(node) != d_visited.end()) - Debug("decision") << " visited, returning" << std::endl; } /* Base case */ - if (checkJustified(node)) + if (checkJustified(node)) { return false; - if(d_visited.find(node) != d_visited.end()) { - - if(tryGetSatValue(node) != SAT_VALUE_UNKNOWN) { - setJustified(node); - return false; - } 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; - return true; - } - } -#if defined CVC4_ASSERTIONS || defined CVC4_TRACING +#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG // 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(Debug.isOn("decision")) { if(!litPresent) { - Trace("decision") << "no sat literal for this node" << std::endl; + Debug("decision") << "no sat literal for this node" << std::endl; } } //Assert(litPresent); -- fails @@ -186,10 +172,10 @@ bool JustificationHeuristic::findSplitterRec(TNode node, 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; + 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; /** * If not in theory of booleans, and not a "boolean" EQUAL (IFF), @@ -202,73 +188,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node, // if node has embedded ites -- which currently happens iff it got // replaced during ite removal -- then try to resolve that first const IteList& l = getITEs(node); - Debug("jh-ite") << " ite size = " << l.size() << std::endl; - d_visited.insert(node); - for(unsigned i = 0; i < l.size(); ++i) { - Debug("jh-ite") << " i = " << i - << " l[i] = " << l[i] << std::endl; - if (checkJustified(l[i])) continue; - - // Assert(l[i].getKind() == kind::ITE, "Expected ITE"); - if(l[i].getKind() != kind::ITE) { - //this might happen because of repeatSimp - Debug("jh-ite") << " not an ite, must have got repeatSimp-ed" - << std::endl; - findSplitterRec(l[i], SAT_VALUE_TRUE, litDecision); - continue; - } - - SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable -#ifdef CVC4_ASSERTIONS - bool litPresent = d_decisionEngine->hasSatLiteral(l[i]); -#endif - - // Handle the ITE to catch the case when a variable is its own - // fanin - SatValue ifVal = tryGetSatValue(l[i][0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - // are we better off trying false? if not, try true - SatValue ifDesiredVal = - (tryGetSatValue(l[i][2]) == desiredVal || - tryGetSatValue(l[i][1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) { - return true; - } - - // Handle special case when if node itself is visited. Decide - // on it. - if(d_visited.find(l[i][0]) != d_visited.end()) { - Assert(d_decisionEngine->hasSatLiteral(l[i][0])); - SatVariable v = d_decisionEngine->getSatLiteral(l[i][0]).getSatVariable(); - *litDecision = SatLiteral(v, ifDesiredVal != SAT_VALUE_TRUE ); + 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; - } - - Assert(false, "No controlling input found (1)"); + Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl; + d_visited.erase(i->first); } else { - - // Try to justify 'if' - if (findSplitterRec(l[i][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(l[i][ch]); - if( d_visited.find(l[i]) == d_visited.end() - && (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) - && findSplitterRec(l[i][ch], desiredVal, litDecision) ) { - return true; - } + Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl; } - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(l[i]); } - d_visited.erase(node); if(litVal != SAT_VALUE_UNKNOWN) { setJustified(node); diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 6c470e6df..1dc7a85d7 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -34,8 +34,6 @@ namespace CVC4 { namespace decision { -typedef std::vector IteList; - class GiveUpException : public Exception { public: GiveUpException() : @@ -44,11 +42,13 @@ public: };/* class GiveUpException */ class JustificationHeuristic : public ITEDecisionStrategy { + typedef std::vector > IteList; typedef hash_map IteCache; typedef hash_map SkolemMap; // being 'justified' is monotonic with respect to decisions - context::CDHashSet d_justified; + typedef context::CDHashSet JustifiedSet; + JustifiedSet d_justified; context::CDO d_prvsIndex; IntStat d_helfulness; @@ -99,8 +99,19 @@ public: 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") <<"{ "<first) << " maps to " + 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]; @@ -175,7 +186,7 @@ private: return prop::undefSatLiteral; } if(ret == true) { - Trace("decision") << "Yippee!!" << std::endl; + Debug("decision") << "Yippee!!" << std::endl; //d_prvsIndex = i; ++d_helfulness; return litDecision; @@ -199,7 +210,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const IteList& getITEs(TNode n); + const JustificationHeuristic::IteList& getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index c5e1f7fbc..f73337c8f 100644 --- a/src/decision/relevancy.cpp +++ b/src/decision/relevancy.cpp @@ -68,7 +68,7 @@ void Relevancy::computeITEs(TNode n, IteList &l) } } -const IteList& Relevancy::getITEs(TNode n) +const Relevancy::IteList& Relevancy::getITEs(TNode n) { IteCache::iterator it = d_iteCache.find(n); if(it != d_iteCache.end()) { diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index 3a33a5cb8..f45ce2e8f 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -46,8 +46,6 @@ namespace CVC4 { namespace decision { -typedef std::vector IteList; - class RelGiveUpException : public Exception { public: RelGiveUpException() : @@ -56,6 +54,7 @@ public: };/* class GiveUpException */ class Relevancy : public RelevancyStrategy { + typedef std::vector IteList; typedef hash_map IteCache; typedef hash_map SkolemMap; typedef hash_map PolarityCache; @@ -139,6 +138,10 @@ public: d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0), d_curDecision(NULL) { + Warning() << "There are known bugs in this Relevancy code which we know" + << "how to fix (but haven't yet)." << std::endl + << "Please bug kshitij if you wish to use." << std::endl; + StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_polqueries); StatisticsRegistry::registerStat(&d_polhelp); @@ -350,7 +353,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const IteList& getITEs(TNode n); + const Relevancy::IteList& getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2bdf7b71f..5e8d71198 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1267,7 +1267,7 @@ bool SmtEnginePrivate::simplifyAssertions() d_assertionsToCheck.swap(d_assertionsToPreprocess); } - Debug("smt") << "POST nonClasualSimplify" << std::endl; + Trace("smt") << "POST nonClasualSimplify" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1283,7 +1283,7 @@ bool SmtEnginePrivate::simplifyAssertions() } } - Debug("smt") << "POST theoryPP" << std::endl; + Trace("smt") << "POST theoryPP" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1292,7 +1292,7 @@ bool SmtEnginePrivate::simplifyAssertions() simpITE(); } - Debug("smt") << "POST iteSimp" << std::endl; + Trace("smt") << "POST iteSimp" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1301,7 +1301,7 @@ bool SmtEnginePrivate::simplifyAssertions() unconstrainedSimp(); } - Debug("smt") << "POST unconstraintedSimp" << std::endl; + Trace("smt") << "POST unconstraintedSimp" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1313,7 +1313,7 @@ bool SmtEnginePrivate::simplifyAssertions() if(!noConflict) return false; } - Debug("smt") << "POST repeatSimp" << std::endl; + Trace("smt") << "POST repeatSimp" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1480,7 +1480,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; + Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0c0d65d74..92e4b17df 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,6 +19,8 @@ #include #include +#include "decision/decision_engine.h" + #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2440a2e53..0452d13aa 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -25,7 +25,6 @@ #include #include -#include "decision/decision_engine.h" #include "expr/node.h" #include "expr/command.h" #include "prop/prop_engine.h" @@ -76,6 +75,8 @@ namespace theory { class Instantiator; }/* CVC4::theory namespace */ +class DecisionEngine; + /** * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various