From: Kshitij Bansal Date: Tue, 4 Dec 2012 21:41:51 +0000 (+0000) Subject: * Add support for --decision=justification + incremental (bug 437) X-Git-Tag: cvc5-1.0.0~7482 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7efd777609f7fbc20701402ad949971cbc251f8f;p=cvc5.git * Add support for --decision=justification + incremental (bug 437) - Fix a destruction order issue this triggered in DE (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 22c70eb6d..9e8add752 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -33,7 +33,7 @@ DecisionEngine::DecisionEngine(context::Context *sc, d_enabledStrategies(), d_needIteSkolemMap(), d_relevancyStrategy(NULL), - d_assertions(), + d_assertions(uc), d_cnfStream(NULL), d_satSolver(NULL), d_satContext(sc), @@ -50,18 +50,6 @@ void DecisionEngine::init() d_engineState = 1; Trace("decision-init") << "DecisionEngine::init()" << std::endl; - if(options::incrementalSolving()) { - if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) { - if(options::decisionMode.wasSetByUser()) { - Warning() << "Ignorning decision option since using incremental mode (currently not supported together)" - << std::endl; - } else { - Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)" - << std::endl; - } - } - return; - } Trace("decision-init") << " * options->decisionMode: " << options::decisionMode() << std:: endl; Trace("decision-init") << " * options->decisionStopOnly: " @@ -70,11 +58,16 @@ void DecisionEngine::init() if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { } if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) { ITEDecisionStrategy* ds = - new decision::JustificationHeuristic(this, d_satContext); + new decision::JustificationHeuristic(this, d_userContext, d_satContext); enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) { + if(options::incrementalSolving()) { + Warning() << "Relevancy decision heuristic and incremental not supported together" + << std::endl; + return; // Currently not supported with incremental + } RelevancyStrategy* ds = new decision::Relevancy(this, d_satContext); enableStrategy(ds); @@ -137,7 +130,7 @@ void DecisionEngine::addAssertions(const vector &assertions, // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; - d_assertions.reserve(assertions.size()); + // d_assertions.reserve(assertions.size()); for(unsigned i = 0; i < assertions.size(); ++i) d_assertions.push_back(assertions[i]); diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 4d354af2a..ea16cec16 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -42,7 +42,8 @@ class DecisionEngine { vector d_needIteSkolemMap; RelevancyStrategy* d_relevancyStrategy; - vector d_assertions; + typedef context::CDList AssertionsList; + AssertionsList d_assertions; // PropEngine* d_propEngine; CnfStream* d_cnfStream; @@ -55,7 +56,7 @@ class DecisionEngine { context::CDO d_result; // Disable creating decision engine without required parameters - DecisionEngine() : d_result(NULL) {} + DecisionEngine(); // init/shutdown state unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown @@ -68,8 +69,6 @@ public: /** Destructor, currently does nothing */ ~DecisionEngine() { Trace("decision") << "Destroying decision engine" << std::endl; - for(unsigned i = 0; i < d_enabledStrategies.size(); ++i) - delete d_enabledStrategies[i]; } // void setPropEngine(PropEngine* pe) { @@ -99,14 +98,15 @@ public: /** * This is called by SmtEngine, at shutdown time, just before * destruction. It is important because there are destruction - * ordering issues between some parts of the system. For now, - * there's nothing to do here in the DecisionEngine. + * ordering issues between some parts of the system. */ void shutdown() { Assert(d_engineState == 1); d_engineState = 2; Trace("decision") << "Shutting down decision engine" << std::endl; + for(unsigned i = 0; i < d_enabledStrategies.size(); ++i) + delete d_enabledStrategies[i]; } // Interface for External World to use our services @@ -191,7 +191,7 @@ public: /** * Get the assertions. Strategies are notified when these are available. */ - const vector& getAssertions() { + AssertionsList& getAssertions() { return d_assertions; } diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ba8ab91b7..494da72bf 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -73,7 +73,7 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l) for(unsigned i=0; isecond)); + l.push_back(make_pair(n[i], (*it2).second)); Assert(n[i].getNumChildren() == 0); } computeITEs(n[i], l); @@ -98,6 +98,15 @@ bool JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal, SatLiteral* litDecision) { + /** + * Main idea + * + * Given a boolean formula "node", the goal is to try to make it + * evaluate to "desiredVal" (true/false). for instance if "node" is a AND + * formula we want to make it evaluate to true, we'd like one of the + * children to be true. this is done recursively. + */ + Trace("jh-findSplitterRec") << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a3b05b1bb..adccc0d55 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -27,6 +27,8 @@ #include "decision_strategy.h" #include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "prop/sat_solver_types.h" @@ -44,7 +46,7 @@ public: class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector > IteList; typedef hash_map IteCache; - typedef hash_map SkolemMap; + typedef context::CDHashMap SkolemMap; // being 'justified' is monotonic with respect to decisions typedef context::CDHashSet JustifiedSet; @@ -59,7 +61,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { * A copy of the assertions that need to be justified * directly. Doesn't have ones introduced during during ITE-removal. */ - std::vector d_assertions; + context::CDList d_assertions; //TNode is fine since decisionEngine has them too /** map from ite-rewrite skolem to a boolean-ite assertion */ @@ -77,13 +79,17 @@ class JustificationHeuristic : public ITEDecisionStrategy { */ hash_set d_visited; public: - JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c): + 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_timestat("decision::jh::time"), + d_assertions(uc), + d_iteAssertions(uc) { StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_giveup); StatisticsRegistry::registerStat(&d_timestat); @@ -91,6 +97,7 @@ public: } ~JustificationHeuristic() { StatisticsRegistry::unregisterStat(&d_helfulness); + StatisticsRegistry::unregisterStat(&d_giveup); StatisticsRegistry::unregisterStat(&d_timestat); } prop::SatLiteral getNext(bool &stopSearch) {