decision_engine.cpp \
decision_strategy.h \
justification_heuristic.h \
- justification_heuristic.cpp \
- relevancy.h \
- relevancy.cpp
+ justification_heuristic.cpp
EXTRA_DIST = \
options_handlers.h
#include "decision/decision_engine.h"
#include "decision/justification_heuristic.h"
-#include "decision/relevancy.h"
#include "expr/node.h"
#include "decision/options.h"
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;
- }
}
}
}
-
-
-
-
-
-
-
void DecisionEngine::addAssertions(const vector<Node> &assertions)
{
Assert(false); // doing this so that we revisit what to do
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 */
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
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") {
} 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);
}
}
-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;
+++ /dev/null
-/********************* */
-/*! \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; i<n.getNumChildren(); ++i) {
- SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
- if(it2 != d_iteAssertions.end())
- l.push_back(it2->second);
- 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<TNode>();
- 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<bool>() == false || desiredVal == SAT_VALUE_TRUE);
- Assert(node.getConst<bool>() == 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
+++ /dev/null
-/********************* */
-/*! \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<TNode> IteList;
- typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
- typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
- typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
-
- // being 'justified' is monotonic with respect to decisions
- context::CDHashSet<Node, NodeHashFunction> d_justified;
- context::CDO<unsigned> 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<TNode> 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<TNode,TNodeHashFunction> 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<TNode,int,TNodeHashFunction> d_maxRelevancy;
- context::CDHashMap<TNode,int,TNodeHashFunction> 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="<<i<<"]: "
- << d_assertions[i] << std::endl;
- }
- }
- Assert(alljustified);
-#endif
-
- // SAT solver can stop...
- stopSearch = true;
- d_decisionEngine->setResult(SAT_VALUE_TRUE);
- return prop::undefSatLiteral;
- }
-
- void addAssertions(const std::vector<Node> &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 */
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));
projects / cvc5.git / commitdiff