diff options
-rw-r--r-- | src/decision/justification_heuristic.cpp | 119 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 25 | ||||
-rw-r--r-- | src/decision/relevancy.cpp | 2 | ||||
-rw-r--r-- | src/decision/relevancy.h | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 3 |
7 files changed, 61 insertions, 111 deletions
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; i<n.getNumChildren(); ++i) { SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); - if(it2 != d_iteAssertions.end()) - l.push_back(it2->second); + 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<TNode>(); + 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<TNode> IteList; - class GiveUpException : public Exception { public: GiveUpException() : @@ -44,11 +42,13 @@ public: };/* 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; // being 'justified' is monotonic with respect to decisions - context::CDHashSet<TNode,TNodeHashFunction> d_justified; + typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet; + JustifiedSet d_justified; context::CDO<unsigned> 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") <<"{ "<<l<<"}" << n <<": "<<v << std::endl; + } + } + for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { - Trace("decision") << d_assertions[i] << std::endl; + Debug("decision") << d_assertions[i] << std::endl; // Sanity check: if it was false, aren't we inconsistent? Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); @@ -153,7 +164,7 @@ public: // Save mapping between ite skolems and ite assertions for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Debug("jh-ite") << " jh-ite: " << (i->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<TNode> IteList; - class RelGiveUpException : public Exception { public: RelGiveUpException() : @@ -56,6 +54,7 @@ public: };/* class GiveUpException */ class Relevancy : public RelevancyStrategy { + typedef std::vector<TNode> IteList; typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap; typedef hash_map<TNode,SatValue,TNodeHashFunction> 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 <vector> #include <list> +#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 <vector> #include <utility> -#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 |