From b53423bcec060d5a49ee2df4d1da55ed289de1d2 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 26 Apr 2013 20:30:41 -0400 Subject: [PATCH] rm decision/relevancy --- src/decision/Makefile.am | 4 +- src/decision/decision_engine.cpp | 31 --- src/decision/options | 8 - src/decision/options_handlers.h | 50 ---- src/decision/relevancy.cpp | 379 ---------------------------- src/decision/relevancy.h | 421 ------------------------------- src/prop/prop_engine.cpp | 3 +- 7 files changed, 3 insertions(+), 893 deletions(-) delete mode 100644 src/decision/relevancy.cpp delete mode 100644 src/decision/relevancy.h diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am index 6d49c6301..f75a17a69 100644 --- a/src/decision/Makefile.am +++ b/src/decision/Makefile.am @@ -12,9 +12,7 @@ libdecision_la_SOURCES = \ decision_engine.cpp \ decision_strategy.h \ justification_heuristic.h \ - justification_heuristic.cpp \ - relevancy.h \ - relevancy.cpp + justification_heuristic.cpp EXTRA_DIST = \ options_handlers.h diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index f634a28d9..073a3ff6b 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -16,7 +16,6 @@ #include "decision/decision_engine.h" #include "decision/justification_heuristic.h" -#include "decision/relevancy.h" #include "expr/node.h" #include "decision/options.h" @@ -62,18 +61,6 @@ void DecisionEngine::init() 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); - d_needIteSkolemMap.push_back(ds); - d_relevancyStrategy = ds; - } } @@ -112,13 +99,6 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } - - - - - - - void DecisionEngine::addAssertions(const vector &assertions) { Assert(false); // doing this so that we revisit what to do @@ -146,15 +126,4 @@ void DecisionEngine::addAssertions(const vector &assertions, addAssertions(assertions, assertionsEnd, iteSkolemMap); } -// void DecisionEngine::addAssertion(Node n) -// { -// d_result = SAT_VALUE_UNKNOWN; -// if(needIteSkolemMap()) { -// d_assertions.push_back(n); -// } -// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) -// d_needIteSkolemMap[i]->notifyAssertionsAvailable(); -// } - - }/* CVC4 namespace */ diff --git a/src/decision/options b/src/decision/options index b86577e7b..5f89e9611 100644 --- a/src/decision/options +++ b/src/decision/options @@ -9,14 +9,6 @@ module DECISION "decision/options.h" Decision heuristics option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h" choose decision mode, see --decision=help -option decisionRelevancyLeaves bool -# permille = part per thousand -option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h" - impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget) -# if false, do justification stuff using relevancy.h -option decisionComputeRelevancy bool -# use the must be relevant -option decisionMustRelevancy bool # only use DE to determine when to stop, not to make decisions option decisionStopOnly bool diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index 05d975ef1..44a623970 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -37,31 +37,8 @@ justification\n\ justification-stoponly\n\ + Use the justification heuristic only to stop early, not for decisions\n\ "; -/** Under-development options, commenting out from help for the release */ -/* -\n\ -relevancy\n\ -+ Under development may-relevancy\n\ -\n\ -relevancy-leaves\n\ -+ May-relevancy, but decide only on leaves\n\ -\n\ -Developer modes:\n\ -\n\ -justification-rel\n\ -+ Use the relevancy code to do the justification stuff\n\ -+ (This should do exact same thing as justification)\n\ -\n\ -justification-must\n\ -+ Start deciding on literals close to root instead of those\n\ -+ near leaves (don't expect it to work well) [Unimplemented]\n\ -";*/ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - options::decisionRelevancyLeaves.set(false); - options::decisionMaxRelTimeAsPermille.set(1000); - options::decisionComputeRelevancy.set(true); - options::decisionMustRelevancy.set(false); options::decisionStopOnly.set(false); if(optarg == "internal") { @@ -71,25 +48,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, } else if(optarg == "justification-stoponly") { options::decisionStopOnly.set(true); return DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "relevancy") { - options::decisionRelevancyLeaves.set(false); - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "relevancy-leaves") { - options::decisionRelevancyLeaves.set(true); - Trace("options") << "version is " << options::version() << std::endl; - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "justification-rel") { - // relevancyLeaves : irrelevant - // maxRelTimeAsPermille : irrelevant - options::decisionComputeRelevancy.set(false); - options::decisionMustRelevancy.set(false); - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "justification-must") { - // relevancyLeaves : irrelevant - // maxRelTimeAsPermille : irrelevant - options::decisionComputeRelevancy.set(false); - options::decisionMustRelevancy.set(true); - return DECISION_STRATEGY_RELEVANCY; } else if(optarg == "help") { puts(decisionModeHelp.c_str()); exit(1); @@ -99,14 +57,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, } } -inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) { - if(budget == 0) { - Warning() << "Decision budget is 0. Consider using internal decision heuristic and " - << std::endl << " removing this option." << std::endl; - - } -} - inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "off") return DECISION_WEIGHT_INTERNAL_OFF; diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp deleted file mode 100644 index f83e238d4..000000000 --- a/src/decision/relevancy.cpp +++ /dev/null @@ -1,379 +0,0 @@ -/********************* */ -/*! \file relevancy.cpp - ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Justification heuristic for decision making - ** - ** A ATGP-inspired justification-based decision heuristic. See - ** [insert reference] for more details. This code is, or not, based - ** on the CVC3 implementation of the same heuristic -- note below. - ** - ** It needs access to the simplified but non-clausal formula. - **/ -/*****************************************************************************/ - -#include "relevancy.h" - -#include "expr/node_manager.h" -#include "expr/kind.h" -#include "theory/rewriter.h" -#include "util/ite_removal.h" - -// Relevancy stuff - -const double Relevancy::secondsPerDecision = 0.001; -const double Relevancy::secondsPerExpense = 1e-7; -const double Relevancy::EPS = 1e-9; - - -void Relevancy::setJustified(TNode n) -{ - Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; - d_justified.insert(n); - if(options::decisionComputeRelevancy()) { - d_relevancy[n] = d_maxRelevancy[n]; - updateRelevancy(n); - } -} - -bool Relevancy::checkJustified(TNode n) -{ - return d_justified.find(n) != d_justified.end(); -} - -SatValue Relevancy::tryGetSatValue(Node n) -{ - Debug("decision") << " " << n << " has sat value " << " "; - if(d_decisionEngine->hasSatLiteral(n) ) { - Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl; - return d_decisionEngine->getSatValue(n); - } else { - Debug("decision") << "NO SAT LITERAL" << std::endl; - return SAT_VALUE_UNKNOWN; - }//end of else -} - -void Relevancy::computeITEs(TNode n, IteList &l) -{ - Debug("jh-ite") << " computeITEs( " << n << ", &l)\n"; - for(unsigned i=0; isecond); - computeITEs(n[i], l); - } -} - -const Relevancy::IteList& Relevancy::getITEs(TNode n) -{ - IteCache::iterator it = d_iteCache.find(n); - if(it != d_iteCache.end()) { - return it->second; - } else { - // Compute the list of ITEs - // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = vector(); - computeITEs(n, d_iteCache[n]); - return d_iteCache[n]; - } -} - -bool Relevancy::findSplitterRec(TNode node, - SatValue desiredVal) -{ - Trace("decision") - << "findSplitterRec([" << node.getId() << "]" << node << ", " - << desiredVal << ", .. )" << std::endl; - - ++d_expense; - - /* Handle NOT as a special case */ - while (node.getKind() == kind::NOT) { - desiredVal = invertValue(desiredVal); - node = node[0]; - } - - /* Avoid infinite loops */ - if(d_visited.find(node) != d_visited.end()) { - Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl; - Assert(false); - Assert(node.getKind() == kind::ITE); - return false; - } - - /* Base case */ - if(checkJustified(node)) { - return false; - } - - /** - * If we have already explored the subtree for some desiredVal, we - * skip this and continue exploring the rest - */ - if(d_polarityCache.find(node) == d_polarityCache.end()) { - d_polarityCache[node] = desiredVal; - } else { - Assert(d_multipleBacktrace || options::decisionComputeRelevancy()); - return true; - } - - d_visited.insert(node); - -#if defined CVC4_ASSERTIONS || defined CVC4_TRACING - // 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(!litPresent) { - Trace("decision") << "no sat literal for this node" << std::endl; - } - } - //Assert(litPresent); -- fails -#endif - - // Get value of sat literal for the node, if there is one - SatValue litVal = tryGetSatValue(node); - - /* You'd better know what you want */ - Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); - - /* Good luck, hope you can get what you want */ - Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - "invariant violated"); - - /* What type of node is this */ - Kind k = node.getKind(); - 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; - - /** - * If not in theory of booleans, and not a "boolean" EQUAL (IFF), - * then check if this is something to split-on. - */ - if(tId != theory::THEORY_BOOL - // && !(k == kind::EQUAL && node[0].getType().isBoolean()) - ) { - - // 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; - for(unsigned i = 0; i < l.size(); ++i) { - Assert(l[i].getKind() == kind::ITE, "Expected ITE"); - Debug("jh-ite") << " i = " << i - << " l[i] = " << l[i] << std::endl; - if(d_visited.find(node) != d_visited.end() ) continue; - if(findSplitterRec(l[i], SAT_VALUE_TRUE)) { - d_visited.erase(node); - return true; - } - } - Debug("jh-ite") << " ite done " << l.size() << std::endl; - - if(litVal != SAT_VALUE_UNKNOWN) { - d_visited.erase(node); - setJustified(node); - return false; - } else { - /* if(not d_decisionEngine->hasSatLiteral(node)) - throw GiveUpException(); */ - Assert(d_decisionEngine->hasSatLiteral(node)); - SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - Trace("decision") << "decision " << *d_curDecision << std::endl; - Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; - d_visited.erase(node); - return true; - } - } - - bool ret = false; - SatValue flipCaseVal = SAT_VALUE_FALSE; - switch (k) { - - case kind::CONST_BOOLEAN: - Assert(node.getConst() == false || desiredVal == SAT_VALUE_TRUE); - Assert(node.getConst() == true || desiredVal == SAT_VALUE_FALSE); - break; - - case kind::AND: - if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE); - else ret = handleOrFalse(node, SAT_VALUE_TRUE); - break; - - case kind::OR: - if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE); - else ret = handleOrTrue(node, SAT_VALUE_TRUE); - break; - - case kind::IMPLIES: - Assert(node.getNumChildren() == 2, "Expected 2 fanins"); - if (desiredVal == SAT_VALUE_FALSE) { - ret = findSplitterRec(node[0], SAT_VALUE_TRUE); - if(ret) break; - ret = findSplitterRec(node[1], SAT_VALUE_FALSE); - break; - } - else { - if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) { - ret = findSplitterRec(node[0], SAT_VALUE_FALSE); - //if(!ret || !d_multipleBacktrace) - break; - } - if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) { - ret = findSplitterRec(node[1], SAT_VALUE_TRUE); - break; - } - Assert(d_multipleBacktrace, "No controlling input found (3)"); - } - break; - - case kind::XOR: - flipCaseVal = SAT_VALUE_TRUE; - case kind::IFF: { - SatValue val = tryGetSatValue(node[0]); - if (val != SAT_VALUE_UNKNOWN) { - ret = findSplitterRec(node[0], val); - if (ret) break; - if (desiredVal == flipCaseVal) val = invertValue(val); - ret = findSplitterRec(node[1], val); - } - else { - val = tryGetSatValue(node[1]); - if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE; - if (desiredVal == flipCaseVal) val = invertValue(val); - ret = findSplitterRec(node[0], val); - if(ret) break; - Assert(false, "Unable to find controlling input (4)"); - } - break; - } - - case kind::ITE: - ret = handleITE(node, desiredVal); - break; - - default: - Assert(false, "Unexpected Boolean operator"); - break; - }//end of switch(k) - - d_visited.erase(node); - if(ret == false) { - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - } - return ret; - - Unreachable(); -}/* findRecSplit method */ - -bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) { - Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", " - << desiredVal << std::endl; - - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); - - int n = node.getNumChildren(); - bool ret = false; - for(int i = 0; i < n; ++i) { - if (findSplitterRec(node[i], desiredVal)) { - if(!options::decisionComputeRelevancy()) - return true; - else - ret = true; - } - } - return ret; -} - -bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) { - Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", " - << desiredVal << std::endl; - - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); - - int n = node.getNumChildren(); - SatValue desiredValInverted = invertValue(desiredVal); - for(int i = 0; i < n; ++i) { - if ( tryGetSatValue(node[i]) != desiredValInverted ) { - // PRE RELEVANCY return findSplitterRec(node[i], desiredVal); - bool ret = findSplitterRec(node[i], desiredVal); - if(ret) { - // Splitter could be found... so can't justify this node - if(!d_multipleBacktrace) - return true; - } - else { - // Splitter couldn't be found... should be justified - return false; - } - } - } - // Multiple backtrace is on, so must have reached here because - // everything had splitter - if(d_multipleBacktrace) return true; - - if(Debug.isOn("jh-findSplitterRec")) { - Debug("jh-findSplitterRec") << " * ** " << std::endl; - Debug("jh-findSplitterRec") << node.getKind() << " " - << node << std::endl; - for(unsigned i = 0; i < node.getNumChildren(); ++i) - Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i]) - << std::endl; - Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node) - << std::endl; - } - Assert(false, "No controlling input found"); - return false; -} - -bool Relevancy::handleITE(TNode node, SatValue desiredVal) -{ - Debug("jh-findSplitterRec") << " handleITE (" << node << ", " - << desiredVal << std::endl; - - //[0]: if, [1]: then, [2]: else - SatValue ifVal = tryGetSatValue(node[0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - - // are we better off trying false? if not, try true - SatValue ifDesiredVal = - (tryGetSatValue(node[2]) == desiredVal || - tryGetSatValue(node[1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(node[0], ifDesiredVal)) return true; - - Assert(false, "No controlling input found (6)"); - } else { - - // Try to justify 'if' - if(findSplitterRec(node[0], ifVal)) 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(node[ch]); - if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) && - findSplitterRec(node[ch], desiredVal) ) { - return true; - } - }// else (...ifVal...) - return false; -}//handleITE diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h deleted file mode 100644 index fd16eb0cc..000000000 --- a/src/decision/relevancy.h +++ /dev/null @@ -1,421 +0,0 @@ -/********************* */ -/*! \file relevancy.h - ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Justification heuristic for decision making - ** - ** A ATGP-inspired justification-based decision heuristic. See - ** [insert reference] for more details. This code is, or not, based - ** on the CVC3 implementation of the same heuristic. - ** - ** It needs access to the simplified but non-clausal formula. - ** - ** Relevancy - ** --------- - ** - ** This class also currently computes the may-relevancy of a node - ** - ** A node is may-relevant if there is a path from the root of the - ** formula to the node such that no node on the path is justified. As - ** contrapositive, a node is not relevant (with the may-notion) if all - ** path from the root to the node go through a justified node. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__DECISION__RELEVANCY -#define __CVC4__DECISION__RELEVANCY - -#include "decision_engine.h" -#include "decision_strategy.h" -#include "decision/options.h" - -#include "context/cdhashset.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "prop/sat_solver_types.h" - -namespace CVC4 { - -namespace decision { - -class RelGiveUpException : public Exception { -public: - RelGiveUpException() : - Exception("relevancy: giving up") { - } -};/* class GiveUpException */ - -class Relevancy : public RelevancyStrategy { - typedef std::vector IteList; - typedef hash_map IteCache; - typedef hash_map SkolemMap; - typedef hash_map PolarityCache; - - // being 'justified' is monotonic with respect to decisions - context::CDHashSet d_justified; - context::CDO d_prvsIndex; - - IntStat d_helfulness; - IntStat d_polqueries; - IntStat d_polhelp; - IntStat d_giveup; - IntStat d_expense; /* Total number of nodes considered over - all calls to the findSplitter function */ - TimerStat d_timestat; - - /** - * A copy of the assertions that need to be justified - * directly. Doesn't have ones introduced during during ITE-removal. - */ - std::vector d_assertions; - //TNode is fine since decisionEngine has them too - - /** map from ite-rewrite skolem to a boolean-ite assertion */ - SkolemMap d_iteAssertions; - // 'key' being TNode is fine since if a skolem didn't exist anywhere, - // we won't look it up. as for 'value', same reason as d_assertions - - /** Cache for ITE skolems present in a atomic formula */ - IteCache d_iteCache; - - /** - * This is used to prevent infinite loop when trying to find a - * splitter. Can happen when exploring assertion corresponding to a - * term-ITE. - */ - hash_set d_visited; - - /** - * May-relevancy of a node is an integer. For a node n, it becomes - * irrelevant when d_maxRelevancy[n] = d_relevancy[n] - */ - hash_map d_maxRelevancy; - context::CDHashMap d_relevancy; - PolarityCache d_polarityCache; - - /** **** * * *** * * OPTIONS *** * * ** * * **** */ - - /** - * do we do "multiple-backtrace" to try to justify a node - */ - bool d_multipleBacktrace; - //bool d_computeRelevancy; // are we in a mode where we compute relevancy? - - static const double secondsPerDecision; - static const double secondsPerExpense; - static const double EPS; - - /** Maximum time this algorithm should spent as part of whole algorithm */ - double d_maxTimeAsPercentageOfTotalTime; - - /** current decision for the recursive call */ - SatLiteral* d_curDecision; -public: - Relevancy(CVC4::DecisionEngine* de, context::Context *c): - RelevancyStrategy(de, c), - d_justified(c), - d_prvsIndex(c, 0), - d_helfulness("decision::rel::preventedDecisions", 0), - d_polqueries("decision::rel::polarityQueries", 0), - d_polhelp("decision::rel::polarityHelp", 0), - d_giveup("decision::rel::giveup", 0), - d_expense("decision::rel::expense", 0), - d_timestat("decision::rel::time"), - d_relevancy(c), - d_multipleBacktrace(options::decisionComputeRelevancy()), - // d_computeRelevancy(decOpt.computeRelevancy), - d_maxTimeAsPercentageOfTotalTime(options::decisionMaxRelTimeAsPermille()*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); - StatisticsRegistry::registerStat(&d_giveup); - StatisticsRegistry::registerStat(&d_expense); - StatisticsRegistry::registerStat(&d_timestat); - Trace("decision") << "relevancy enabled with" << std::endl; - Trace("decision") << " * computeRelevancy: " << (options::decisionComputeRelevancy() ? "on" : "off") - << std::endl; - Trace("decision") << " * relevancyLeaves: " << (options::decisionRelevancyLeaves() ? "on" : "off") - << std::endl; - Trace("decision") << " * mustRelevancy [unimplemented]: " << (options::decisionMustRelevancy() ? "on" : "off") - << std::endl; - } - ~Relevancy() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_polqueries); - StatisticsRegistry::unregisterStat(&d_polhelp); - StatisticsRegistry::unregisterStat(&d_giveup); - StatisticsRegistry::unregisterStat(&d_expense); - StatisticsRegistry::unregisterStat(&d_timestat); - } - prop::SatLiteral getNext(bool &stopSearch) { - Debug("decision") << std::endl; - Trace("decision") << "Relevancy::getNext()" << std::endl; - TimerStat::CodeTimer codeTimer(d_timestat); - - if( d_maxTimeAsPercentageOfTotalTime < 100.0 - EPS && - double(d_polqueries.getData())*secondsPerDecision < - d_maxTimeAsPercentageOfTotalTime*double(d_expense.getData())*secondsPerExpense - ) { - ++d_giveup; - return undefSatLiteral; - } - - d_visited.clear(); - d_polarityCache.clear(); - - for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { - Trace("decision") << 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 = findSplitter(d_assertions[i], desiredVal); - - if(!options::decisionComputeRelevancy() && litDecision != undefSatLiteral) { - d_prvsIndex = i; - return litDecision; - } - } - - if(options::decisionComputeRelevancy()) return undefSatLiteral; - - Trace("decision") << "jh: Nothing to split on " << std::endl; - -#if defined CVC4_ASSERTIONS || 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="<setResult(SAT_VALUE_TRUE); - return prop::undefSatLiteral; - } - - void addAssertions(const std::vector &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { - Trace("decision") - << "Relevancy::addAssertions()" - << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd - << std::endl; - - // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - Assert(i->second >= assertionsEnd && i->second < assertions.size()); - Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to " - << assertions[(i->second)] << std::endl; - d_iteAssertions[i->first] = assertions[i->second]; - } - - // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) { - d_assertions.push_back(assertions[i]); - d_visited.clear(); - if(options::decisionComputeRelevancy()) increaseMaxRelevancy(assertions[i]); - d_visited.clear(); - } - - } - - bool isRelevant(TNode n) { - Trace("decision") << "isRelevant(" << n << "): "; - - if(Debug.isOn("decision")) { - if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) { - // we are becuase of not getting information about literals - // created using newLiteral command... need to figure how to - // handle that - Message() << "isRelevant: WARNING: didn't find node when we should had" << std::endl; - } - } - - if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) { - Trace("decision") << "yes [not found in db]" << std::endl; - return true; - } - - if(options::decisionRelevancyLeaves() && !isAtomicFormula(n)) { - Trace("decision") << "no [not a leaf]" << std::endl; - return false; - } - - Trace("decision") << (d_maxRelevancy[n] == d_relevancy[n] ? "no":"yes") - << std::endl; - - Debug("decision") << " maxRel: " << (d_maxRelevancy[n] ) - << " rel: " << d_relevancy[n].get() << std::endl; - // Assert(d_maxRelevancy.find(n) != d_maxRelevancy.end()); - Assert(0 <= d_relevancy[n] && d_relevancy[n] <= d_maxRelevancy[n]); - - if(d_maxRelevancy[n] == d_relevancy[n]) { - ++d_helfulness; // preventedDecisions - return false; - } else { - return true; - } - } - - SatValue getPolarity(TNode n) { - Trace("decision") << "getPolarity([" << n.getId() << "]" << n << "): "; - Assert(n.getKind() != kind::NOT); - ++d_polqueries; - PolarityCache::iterator it = d_polarityCache.find(n); - if(it == d_polarityCache.end()) { - Trace("decision") << "don't know" << std::endl; - return SAT_VALUE_UNKNOWN; - } else { - ++d_polhelp; - Trace("decision") << it->second << std::endl; - return it->second; - } - } - - /* Compute justified */ - /*bool computeJustified() { - - }*/ -private: - SatLiteral findSplitter(TNode node, SatValue desiredVal) - { - bool ret; - SatLiteral litDecision; - try { - // init - d_curDecision = &litDecision; - - // solve - ret = findSplitterRec(node, desiredVal); - - // post - d_curDecision = NULL; - }catch(RelGiveUpException &e) { - return prop::undefSatLiteral; - } - if(ret == true) { - Trace("decision") << "Yippee!!" << std::endl; - return litDecision; - } else { - return undefSatLiteral; - } - } - - /** - * Do all the hardwork. - * Return 'true' if the node cannot be justfied, 'false' it it can be. - * Sets 'd_curDecision' if unable to justify (depending on the mode) - * If 'd_computeRelevancy' is on does multiple backtrace - */ - bool findSplitterRec(TNode node, SatValue value); - // Functions to make findSplitterRec modular... - bool handleOrFalse(TNode node, SatValue desiredVal); - bool handleOrTrue(TNode node, SatValue desiredVal); - bool handleITE(TNode node, SatValue desiredVal); - - /* Helper functions */ - void setJustified(TNode); - bool checkJustified(TNode); - - /* If literal exists corresponding to the node return - that. Otherwise an UNKNOWN */ - SatValue tryGetSatValue(Node n); - - /* Get list of all term-ITEs for the atomic formula v */ - const Relevancy::IteList& getITEs(TNode n); - - /* Compute all term-ITEs in a node recursively */ - void computeITEs(TNode n, IteList &l); - - /* Checks whether something is an atomic formula or not */ - bool isAtomicFormula(TNode n) { - return theory::kindToTheoryId(n.getKind()) != theory::THEORY_BOOL; - } - - /** Recursively increase relevancies */ - void updateRelevancy(TNode n) { - if(d_visited.find(n) != d_visited.end()) return; - - Assert(d_relevancy[n] <= d_maxRelevancy[n]); - - if(d_relevancy[n] != d_maxRelevancy[n]) - return; - - d_visited.insert(n); - if(isAtomicFormula(n)) { - const IteList& l = getITEs(n); - for(unsigned i = 0; i < l.size(); ++i) { - if(d_visited.find(l[i]) == d_visited.end()) continue; - d_relevancy[l[i]] = d_relevancy[l[i]] + 1; - updateRelevancy(l[i]); - } - } else { - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - if(d_visited.find(n[i]) == d_visited.end()) continue; - d_relevancy[n[i]] = d_relevancy[n[i]] + 1; - updateRelevancy(n[i]); - } - } - d_visited.erase(n); - } - - /* */ - void increaseMaxRelevancy(TNode n) { - - Debug("decision") - << "increaseMaxRelevancy([" << n.getId() << "]" << n << ")" - << std::endl; - - d_maxRelevancy[n]++; - - // don't update children multiple times - if(d_visited.find(n) != d_visited.end()) return; - - d_visited.insert(n); - // Part to make the recursive call - if(isAtomicFormula(n)) { - const IteList& l = getITEs(n); - for(unsigned i = 0; i < l.size(); ++i) - if(d_visited.find(l[i]) == d_visited.end()) - increaseMaxRelevancy(l[i]); - } else { - for(unsigned i = 0; i < n.getNumChildren(); ++i) - increaseMaxRelevancy(n[i]); - } //else (...atomic formula...) - } - -};/* class Relevancy */ - -}/* namespace decision */ - -}/* namespace CVC4 */ - -#endif /* __CVC4__DECISION__RELEVANCY */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5d6356a5b..a169d31e6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -83,7 +83,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext userContext, // fullLitToNode Map = options::threads() > 1 || - options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY); + options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY + ); d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); -- 2.30.2