diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/Makefile.am | 4 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 45 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 10 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 11 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 6 | ||||
-rw-r--r-- | src/decision/relevancy.cpp | 376 | ||||
-rw-r--r-- | src/decision/relevancy.h | 423 |
7 files changed, 864 insertions, 11 deletions
diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am index c399cbf71..4f454e9bf 100644 --- a/src/decision/Makefile.am +++ b/src/decision/Makefile.am @@ -10,4 +10,6 @@ libdecision_la_SOURCES = \ decision_engine.cpp \ decision_strategy.h \ justification_heuristic.h \ - justification_heuristic.cpp + justification_heuristic.cpp \ + relevancy.h \ + relevancy.cpp diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 1afe835fb..b1ecabf81 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -18,6 +18,7 @@ #include "decision/decision_engine.h" #include "decision/justification_heuristic.h" +#include "decision/relevancy.h" #include "expr/node.h" #include "util/options.h" @@ -30,6 +31,7 @@ namespace CVC4 { context::Context *uc) : d_enabledStrategies(), d_needIteSkolemMap(), + d_relevancyStrategy(NULL), d_assertions(), d_cnfStream(NULL), d_satSolver(NULL), @@ -49,6 +51,13 @@ namespace CVC4 { enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } + if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) { + RelevancyStrategy* ds = + new decision::Relevancy(this, d_satContext, options->decisionOptions); + enableStrategy(ds); + d_needIteSkolemMap.push_back(ds); + d_relevancyStrategy = ds; + } } void DecisionEngine::enableStrategy(DecisionStrategy* ds) @@ -57,6 +66,35 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds) } +bool DecisionEngine::isRelevant(SatVariable var) +{ + Debug("decision") << "isRelevant(" << var <<")" << std::endl; + if(d_relevancyStrategy != NULL) { + //Assert(d_cnfStream->hasNode(var)); + return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) ); + } else { + return true; + } +} + +SatValue DecisionEngine::getPolarity(SatVariable var) +{ + Debug("decision") << "getPolariry(" << var <<")" << std::endl; + if(d_relevancyStrategy != NULL) { + Assert(isRelevant(var)); + return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) ); + } else { + return SAT_VALUE_UNKNOWN; + } +} + + + + + + + + void DecisionEngine::addAssertions(const vector<Node> &assertions) { Assert(false); // doing this so that we revisit what to do @@ -68,10 +106,9 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions) // d_assertions.push_back(assertions[i]); } -void DecisionEngine::addAssertions - (const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) +void DecisionEngine::addAssertions(const vector<Node> &assertions, + unsigned assertionsEnd, + IteSkolemMap iteSkolemMap) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 545ae1770..fb6f673d9 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -40,6 +40,7 @@ class DecisionEngine { vector <DecisionStrategy* > d_enabledStrategies; vector <ITEDecisionStrategy* > d_needIteSkolemMap; + RelevancyStrategy* d_relevancyStrategy; vector <Node> d_assertions; @@ -107,6 +108,15 @@ public: return ret; } + /** Is a sat variable relevant */ + bool isRelevant(SatVariable var); + + /** + * Try to get tell SAT solver what polarity to try for a + * decision. Return SAT_VALUE_UNKNOWN if it can't help + */ + SatValue getPolarity(SatVariable var); + /** Is the DecisionEngine in a state where it has solved everything? */ bool isDone() { Trace("decision") << "DecisionEngine::isDone() returning " diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 6ee583ec2..ee7d340c4 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -63,6 +63,17 @@ public: IteSkolemMap iteSkolemMap) = 0; }; +class RelevancyStrategy : public ITEDecisionStrategy { +public: + RelevancyStrategy(DecisionEngine* de, context::Context *c) : + ITEDecisionStrategy(de, c) { + } + + virtual bool isRelevant(TNode n) = 0; + virtual prop::SatValue getPolarity(TNode n) = 0; +}; + + }/* decision namespace */ }/* CVC4 namespace */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index c859e5d07..68c11295f 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -68,12 +68,6 @@ CVC3 code <----> this code // Local helper functions for just this file -SatValue invertValue(SatValue v) -{ - if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; - else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; - else return SAT_VALUE_TRUE; -} // JustificationHeuristic stuff diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp new file mode 100644 index 000000000..c5e1f7fbc --- /dev/null +++ b/src/decision/relevancy.cpp @@ -0,0 +1,376 @@ +/********************* */ +/*! \file relevancy.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 + +void Relevancy::setJustified(TNode n) +{ + Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; + d_justified.insert(n); + if(d_opt.computeRelevancy) { + 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 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 || d_opt.computeRelevancy); + 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 voilated"); + + /* 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(!d_opt.computeRelevancy) + 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 new file mode 100644 index 000000000..93fb3c999 --- /dev/null +++ b/src/decision/relevancy.h @@ -0,0 +1,423 @@ +/********************* */ +/*! \file relevancy.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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. + **/ + +#ifndef __CVC4__DECISION__RELEVANCY +#define __CVC4__DECISION__RELEVANCY + +#include "decision_engine.h" +#include "decision_strategy.h" + +#include "context/cdhashset.h" +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "prop/sat_solver_types.h" +#include "util/options.h" + +namespace CVC4 { + +namespace decision { + +typedef std::vector<TNode> IteList; + +class RelGiveUpException : public Exception { +public: + RelGiveUpException() : + Exception("relevancy: giving up") { + } +};/* class GiveUpException */ + +class Relevancy : public RelevancyStrategy { + 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<TNode,TNodeHashFunction> 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? + + /** Only leaves can be relevant */ + Options::DecisionOptions d_opt; // may be we shouldn't be caching them? + + static const double secondsPerDecision = 0.001; + static const double secondsPerExpense = 1e-7; + static const double EPS = 1e-9; + /** 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, const Options::DecisionOptions &decOpt): + 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(decOpt.computeRelevancy), + // d_computeRelevancy(decOpt.computeRelevancy), + d_opt(decOpt), + d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0), + d_curDecision(NULL) + { + 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: " << (d_opt.computeRelevancy ? "on" : "off") + << std::endl; + Trace("decision") << " * relevancyLeaves: " << (d_opt.relevancyLeaves ? "on" : "off") + << std::endl; + Trace("decision") << " * mustRelevancy [unimplemented]: " << (d_opt.mustRelevancy ? "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(!d_opt.computeRelevancy && litDecision != undefSatLiteral) { + d_prvsIndex = i; + return litDecision; + } + } + + if(d_opt.computeRelevancy) 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(d_opt.computeRelevancy) 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 + Warning() << "isRelevant: WARNING: didn't find node when we should had" << std::endl; + // Warning() doesn't work for some reason + cout << "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(d_opt.relevancyLeaves && !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 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 */ |