diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-12 19:41:28 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 20:00:55 -0400 |
commit | b480438b3d39000cfac88eac12922a23f9fccbea (patch) | |
tree | ab310d8512298a733f8e2d8f4805d06ee126208e /src | |
parent | 6106f021745ffc7ebc068f762a196140deb9d48d (diff) |
Fix to bug 497: make justification heuristic's ITE cache context-dependent.
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/decision_engine.cpp | 2 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 4 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 25 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 6 |
4 files changed, 19 insertions, 18 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 08a3e49d0..98294f92b 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -29,7 +29,7 @@ using namespace std; namespace CVC4 { DecisionEngine::DecisionEngine(context::Context *sc, - context::Context *uc) : + context::UserContext *uc) : d_enabledStrategies(), d_needIteSkolemMap(), d_relevancyStrategy(NULL), diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index ea16cec16..859443d00 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -50,7 +50,7 @@ class DecisionEngine { DPLLSatSolverInterface* d_satSolver; context::Context* d_satContext; - context::Context* d_userContext; + context::UserContext* d_userContext; // Does decision engine know the answer? context::CDO<SatValue> d_result; @@ -64,7 +64,7 @@ public: // Necessary functions /** Constructor */ - DecisionEngine(context::Context *sc, context::Context *uc); + DecisionEngine(context::Context *sc, context::UserContext *uc); /** Destructor, currently does nothing */ ~DecisionEngine() { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 0b63dfbe1..b77d3ba6b 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -28,7 +28,7 @@ using namespace CVC4; JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, - context::Context *uc, + context::UserContext *uc, context::Context *c): ITEDecisionStrategy(de, c), d_justified(c), @@ -38,7 +38,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_timestat("decision::jh::time"), d_assertions(uc), d_iteAssertions(uc), - d_iteCache(), + d_iteCache(uc), d_visited(), d_visitedComputeITE(), d_curDecision() { @@ -199,19 +199,20 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n) }//end of else } -const JustificationHeuristic::IteList& +JustificationHeuristic::IteList JustificationHeuristic::getITEs(TNode n) { IteCache::iterator it = d_iteCache.find(n); if(it != d_iteCache.end()) { - return it->second; + return (*it).second; } else { // Compute the list of ITEs // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = IteList(); d_visitedComputeITE.clear(); - computeITEs(n, d_iteCache[n]); - return d_iteCache[n]; + IteList ilist; + computeITEs(n, ilist); + d_iteCache.insert(n, ilist); + return ilist; } } @@ -462,15 +463,15 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) bool JustificationHeuristic::handleEmbeddedITEs(TNode node) { - const IteList& l = getITEs(node); + const IteList l = getITEs(node); Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl; for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { - if(d_visited.find(i->first) == d_visited.end()) { - d_visited.insert(i->first); - if(findSplitterRec(i->second, SAT_VALUE_TRUE)) + if(d_visited.find((*i).first) == d_visited.end()) { + d_visited.insert((*i).first); + if(findSplitterRec((*i).second, SAT_VALUE_TRUE)) return true; - d_visited.erase(i->first); + d_visited.erase((*i).first); } } return false; diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 91c21d981..d8f9a15a8 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -38,7 +38,7 @@ namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector<pair<TNode,TNode> > IteList; - typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; + typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache; typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; // being 'justified' is monotonic with respect to decisions @@ -82,7 +82,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { SatLiteral d_curDecision; public: JustificationHeuristic(CVC4::DecisionEngine* de, - context::Context *uc, + context::UserContext *uc, context::Context *c); ~JustificationHeuristic(); @@ -110,7 +110,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const JustificationHeuristic::IteList& getITEs(TNode n); + JustificationHeuristic::IteList getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); |