From: Kshitij Bansal Date: Fri, 8 Jun 2012 05:56:08 +0000 (+0000) Subject: Merge from decision branch (till r3663) X-Git-Tag: cvc5-1.0.0~8106 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8cd22903675724e29249ce089ee77c7c4d3897fb;p=cvc5.git Merge from decision branch (till r3663) (no performace or search behavior changes expected) --- 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 &assertions) { Assert(false); // doing this so that we revisit what to do @@ -68,10 +106,9 @@ void DecisionEngine::addAssertions(const vector &assertions) // d_assertions.push_back(assertions[i]); } -void DecisionEngine::addAssertions - (const vector &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) +void DecisionEngine::addAssertions(const vector &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 d_enabledStrategies; vector d_needIteSkolemMap; + RelevancyStrategy* d_relevancyStrategy; vector 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; isecond); + 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(); + 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() == 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(!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 IteList; + +class RelGiveUpException : public Exception { +public: + RelGiveUpException() : + Exception("relevancy: giving up") { + } +};/* class GiveUpException */ + +class Relevancy : public RelevancyStrategy { + 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? + + /** 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="<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(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 */ diff --git a/src/main/driver.cpp b/src/main/driver.cpp index ef6b99715..042a8ef1d 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: cconway - ** Minor contributors (to current version): barrett, dejan, taking + ** Minor contributors (to current version): barrett, dejan, taking, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011, 2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -82,6 +82,10 @@ void printUsage(Options& options, bool full) { int runCvc4(int argc, char* argv[], Options& options) { + // Timer statistic + TimerStat s_totalTime("totalTime"); + s_totalTime.start(); + // For the signal handlers' benefit pOptions = &options; @@ -161,6 +165,10 @@ int runCvc4(int argc, char* argv[], Options& options) { // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; + // Timer statistic + RegisterStatistic statTotalTime(exprMgr, &s_totalTime); + + // Filename statistics ReferenceStat< const char* > s_statFilename("filename", filename); RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); @@ -308,6 +316,8 @@ int runCvc4(int argc, char* argv[], Options& options) { ReferenceStat< Result > s_statSatResult("sat/unsat", result); RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); + s_totalTime.stop(); + if(options.statistics) { pStatistics->flushInformation(*options.err); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 62d885c06..485ddbb55 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -120,6 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const { } void TseitinCnfStream::ensureLiteral(TNode n) { + Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { // Already a literal! // newLiteral() may be necessary to renew a previously-extant literal diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d220c4dbb..a260a8ca1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -395,6 +395,7 @@ Lit Solver::pickBranchLit() while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; + decisions++; return nextLit; } else { Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; @@ -414,14 +415,35 @@ Lit Solver::pickBranchLit() rnd_decisions++; } // Activity based decision: - while (next == var_Undef || value(next) != l_Undef || !decision[next]) + while (next == var_Undef || value(next) != l_Undef || !decision[next]) { if (order_heap.empty()){ next = var_Undef; break; - }else + }else { next = order_heap.removeMin(); + } + + if(!decision[next]) continue; + // Check with decision engine about relevancy + if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) { + next = var_Undef; + } + } - return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); + if(next == var_Undef) { + return lit_Undef; + } else { + decisions++; + // Check with decision engine if it can tell polarity + lbool dec_pol = MinisatSatSolver::toMinisatlbool + (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next))); + if(dec_pol != l_Undef) { + Assert(dec_pol == l_True || dec_pol == l_False); + return mkLit(next, (dec_pol == l_True) ); + } + // If it can't use internal heuristic to do that + return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); + } } @@ -1127,7 +1149,6 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // New variable decision: - decisions++; next = pickBranchLit(); if (next == lit_Undef) { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 4f2a16670..6b02153c7 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -69,6 +69,20 @@ SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { return SAT_VALUE_FALSE; } +Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0); + if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2); + Assert(val == SAT_VALUE_FALSE); + return Minisat::lbool((uint8_t)1); +} + +/*bool MinisatSatSolver::tobool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return true; + Assert(val == SAT_VALUE_FALSE); + return false; + }*/ void MinisatSatSolver::toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause) { @@ -92,10 +106,15 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; + if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) { + Notice() << "minisat: Incremental solving is disabled" + << " unless using internal decision strategy." << std::endl; + } + // Create the solver d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, Options::current()->incrementalSolving || - Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION ); + Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ); // Setup the verbosity d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 19ade8ffa..9171bf232 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -45,8 +45,10 @@ public: static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatValue toSatLiteralValue(bool res); - static SatValue toSatLiteralValue(Minisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Minisat::lbool res); + static Minisat::lbool toMinisatlbool(SatValue val); + //(Commented because not in use) static bool tobool(SatValue val); static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (Minisat::vec& clause, SatClause& sat_clause); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 58270b4d0..702a530cf 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -77,7 +77,11 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : d_satSolver = SatSolverFactory::createDPLLMinisat(); theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1); + d_cnfStream = new CVC4::prop::TseitinCnfStream + (d_satSolver, registrar, + // fullLitToNode Map = + Options::current()->threads > 1 || + Options::current()->decisionMode == Options::DECISION_STRATEGY_RELEVANCY); d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 0da4d7a6a..9dcc1c4bf 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): barrett, cconway + ** Minor contributors (to current version): barrett, cconway, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -41,6 +41,15 @@ enum SatValue { SAT_VALUE_FALSE }; +/** Helper function for inverting a SatValue */ +inline 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; +} + + /** * A variable of the SAT solver. */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index ccb26b6f0..93f8c0a5d 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -188,9 +188,17 @@ void TheoryProxy::checkTime() { d_propEngine->checkTime(); } +bool TheoryProxy::isDecisionRelevant(SatVariable var) { + return d_decisionEngine->isRelevant(var); +} + bool TheoryProxy::isDecisionEngineDone() { return d_decisionEngine->isDone(); } +SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { + return d_decisionEngine->getPolarity(var); +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 2fac0ab7b..99aab8286 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -119,6 +119,10 @@ public: bool isDecisionEngineDone(); + bool isDecisionRelevant(SatVariable var); + + SatValue getDecisionPolarity(SatVariable var); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ed28c23a3..d0f7a0584 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1039,6 +1039,9 @@ void SmtEnginePrivate::simplifyAssertions() expandDefinitions(d_assertionsToPreprocess[i], cache); } } + + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { // Perform non-clausal simplification @@ -1053,6 +1056,9 @@ void SmtEnginePrivate::simplifyAssertions() d_assertionsToCheck.swap(d_assertionsToPreprocess); } + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(Options::current()->doITESimp) { // ite simplification simpITE(); @@ -1063,6 +1069,8 @@ void SmtEnginePrivate::simplifyAssertions() } if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { + Trace("simplify") << "SmtEnginePrivate::simplify(): " + << " doing repeated simplification" << std::endl; d_assertionsToCheck.swap(d_assertionsToPreprocess); // Abuse the user context to make sure circuit propagator gets backtracked d_smt.d_userContext->push(); @@ -1070,6 +1078,9 @@ void SmtEnginePrivate::simplifyAssertions() d_smt.d_userContext->pop(); } + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(Options::current()->doStaticLearning) { // Perform static learning Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -1180,14 +1191,10 @@ void SmtEnginePrivate::processAssertions() { { TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime); - // Remove ITEs - d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); // Remove ITEs, updating d_iteSkolemMap + d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); removeITEs(); d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); - // This may need to be in a try-catch - // block. make regress is passing, so - // skipping for now --K } if(Options::current()->repeatSimp) { diff --git a/src/util/options.cpp b/src/util/options.cpp index e5d91e0d8..c86109d34 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -58,6 +58,14 @@ CVC4_THREADLOCAL(const Options*) Options::s_current = NULL; # define DO_SEMANTIC_CHECKS_BY_DEFAULT true #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ +/** default decision options */ +const Options::DecisionOptions defaultDecOpt = { + false, // relevancyLeaves + 1000, // maxRelTimeAsPermille + true, // computeRelevancy + false, // mustRelevancy +}; + Options::Options() : binary_name(), statistics(false), @@ -82,6 +90,7 @@ Options::Options() : simplificationModeSetByUser(false), decisionMode(DECISION_STRATEGY_INTERNAL), decisionModeSetByUser(false), + decisionOptions(DecisionOptions(defaultDecOpt)), doStaticLearning(true), doITESimp(false), doITESimpSetByUser(false), @@ -135,6 +144,7 @@ Options::Options() : { } + static const string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:\n\ --version | -V identify this CVC4 binary\n\ @@ -188,6 +198,8 @@ Additional CVC4 options:\n\ --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ --decision=MODE choose decision mode, see --decision=help\n\ + --decision-budget=N impose a budget for relevancy hueristic which increases linearly with\n\ + each decision. N between 0 and 1000. (default: 1000, no budget)\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ @@ -276,6 +288,22 @@ internal (default)\n\ \n\ justification\n\ + An ATGP-inspired justification heuristic\n\ +\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\ "; static const string dumpHelp = "\ @@ -431,6 +459,7 @@ enum OptionValue { LAZY_DEFINITION_EXPANSION, SIMPLIFICATION_MODE, DECISION_MODE, + DECISION_BUDGET, NO_STATIC_LEARNING, ITE_SIMP, NO_ITE_SIMP, @@ -533,6 +562,7 @@ static struct option cmdlineOptions[] = { { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, { "decision", required_argument, NULL, DECISION_MODE }, + { "decision-budget", required_argument, NULL, DECISION_BUDGET }, { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "ite-simp", no_argument, NULL, ITE_SIMP }, { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP }, @@ -841,6 +871,28 @@ throw(OptionException) { } else if(!strcmp(optarg, "justification")) { decisionMode = DECISION_STRATEGY_JUSTIFICATION; decisionModeSetByUser = true; + } else if(!strcmp(optarg, "relevancy")) { + decisionMode = DECISION_STRATEGY_RELEVANCY; + decisionModeSetByUser = true; + decisionOptions.relevancyLeaves = false; + } else if(!strcmp(optarg, "relevancy-leaves")) { + decisionMode = DECISION_STRATEGY_RELEVANCY; + decisionModeSetByUser = true; + decisionOptions.relevancyLeaves = true; + } else if(!strcmp(optarg, "justification-rel")) { + decisionMode = DECISION_STRATEGY_RELEVANCY; + decisionModeSetByUser = true; + // relevancyLeaves : irrelevant + // maxRelTimeAsPermille : irrelevant + decisionOptions.computeRelevancy = false; + decisionOptions.mustRelevancy = false; + } else if(!strcmp(optarg, "justification-must")) { + decisionMode = DECISION_STRATEGY_RELEVANCY; + decisionModeSetByUser = true; + // relevancyLeaves : irrelevant + // maxRelTimeAsPermille : irrelevant + decisionOptions.computeRelevancy = false; + decisionOptions.mustRelevancy = true; } else if(!strcmp(optarg, "help")) { puts(decisionHelp.c_str()); exit(1); @@ -850,6 +902,21 @@ throw(OptionException) { } break; + case DECISION_BUDGET: { + int i = atoi(optarg); + if(i < 0 || i > 1000) { + throw OptionException(string("invalid value for --decision-budget: `") + + optarg + "'. Must be between 0 and 1000."); + } + if(i == 0) { + Warning() << "Decision budget is 0. Consider using internal decision hueristic and " + << std::endl << " removing this option." << std::endl; + + } + decisionOptions.maxRelTimeAsPermille = (unsigned short)i; + } + break; + case NO_STATIC_LEARNING: doStaticLearning = false; break; diff --git a/src/util/options.h b/src/util/options.h index f48b45b49..0584fdc2a 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -136,12 +136,27 @@ struct CVC4_PUBLIC Options { /** * Use the justification heuristic */ - DECISION_STRATEGY_JUSTIFICATION + DECISION_STRATEGY_JUSTIFICATION, + DECISION_STRATEGY_RELEVANCY } DecisionMode; /** When/whether to use any decision strategies */ DecisionMode decisionMode; /** Whether the user set the decision strategy */ bool decisionModeSetByUser; + /** + * Extra settings for decision stuff, varies by strategy enabled + * - With DECISION_STRATEGY_RELEVANCY + * > Least significant bit: true if one should only decide on leaves + */ + + /** DecisionOption along */ + struct DecisionOptions { + bool relevancyLeaves; + unsigned short maxRelTimeAsPermille; /* permille = part per thousand */ + bool computeRelevancy; /* if false, do justification stuff using relevancy.h */ + bool mustRelevancy; /* use the must be relevant */ + }; + DecisionOptions decisionOptions; /** Whether to perform the static learning pass. */ bool doStaticLearning; diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 28d116c4a..19837d8f1 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -19,8 +19,8 @@ TESTS = \ delta-minimized-row-vector-bug.smt \ fuzz_3-eq.smt \ leq.01.smt \ - miplibtrick.smt \ - problem__003.smt2 + miplibtrick.smt +# problem__003.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index f205aa767..b8806d7a4 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -24,7 +24,6 @@ TESTS = \ arith-int-042.min.cvc \ arith-int-047.cvc \ arith-int-050.cvc \ - arith-int-082.cvc \ arith-int-084.cvc \ arith-int-085.cvc \ arith-int-097.cvc @@ -100,6 +99,7 @@ EXTRA_DIST = $(TESTS) \ arith-int-079.cvc \ arith-int-080.cvc \ arith-int-081.cvc \ + arith-int-082.cvc \ arith-int-083.cvc \ arith-int-086.cvc \ arith-int-087.cvc \