diff options
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 116 |
1 files changed, 7 insertions, 109 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 4be436351..91c21d981 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -83,120 +83,18 @@ class JustificationHeuristic : public ITEDecisionStrategy { public: JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *uc, - context::Context *c): - ITEDecisionStrategy(de, c), - d_justified(c), - d_prvsIndex(c, 0), - d_helfulness("decision::jh::helpfulness", 0), - d_giveup("decision::jh::giveup", 0), - d_timestat("decision::jh::time"), - d_assertions(uc), - d_iteAssertions(uc), - d_iteCache(), - d_visited(), - d_visitedComputeITE(), - d_curDecision() { - StatisticsRegistry::registerStat(&d_helfulness); - StatisticsRegistry::registerStat(&d_giveup); - StatisticsRegistry::registerStat(&d_timestat); - Trace("decision") << "Justification heuristic enabled" << std::endl; - } - ~JustificationHeuristic() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_giveup); - StatisticsRegistry::unregisterStat(&d_timestat); - } - prop::SatLiteral getNext(bool &stopSearch) { - Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; - TimerStat::CodeTimer codeTimer(d_timestat); - - d_visited.clear(); - - if(Trace.isOn("justified")) { - for(JustifiedSet::key_iterator i = d_justified.key_begin(); - i != d_justified.key_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) { - Debug("decision") << "---" << std::endl << 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; - - litDecision = findSplitter(d_assertions[i], desiredVal); - - if(litDecision != undefSatLiteral) { - d_prvsIndex = i; - return litDecision; - } - } - - Trace("decision") << "jh: Nothing to split on " << std::endl; - -#if 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; - } + context::Context *c); + + ~JustificationHeuristic(); + + prop::SatLiteral getNext(bool &stopSearch); void addAssertions(const std::vector<Node> &assertions, unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { - Trace("decision") - << "JustificationHeuristic::addAssertions()" - << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd - << std::endl; - - // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) - d_assertions.push_back(assertions[i]); - - // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - 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]; - } - } + IteSkolemMap iteSkolemMap); private: - SatLiteral findSplitter(TNode node, SatValue desiredVal) - { - d_curDecision = undefSatLiteral; - if(findSplitterRec(node, desiredVal)) { - ++d_helfulness; - } - return d_curDecision; - } + SatLiteral findSplitter(TNode node, SatValue desiredVal); /** * Do all the hard work. |