decision_engine.cpp \
decision_strategy.h \
justification_heuristic.h \
- justification_heuristic.cpp
+ justification_heuristic.cpp \
+ relevancy.h \
+ relevancy.cpp
#include "decision/decision_engine.h"
#include "decision/justification_heuristic.h"
+#include "decision/relevancy.h"
#include "expr/node.h"
#include "util/options.h"
context::Context *uc) :
d_enabledStrategies(),
d_needIteSkolemMap(),
+ d_relevancyStrategy(NULL),
d_assertions(),
d_cnfStream(NULL),
d_satSolver(NULL),
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)
}
+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
// 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;
vector <DecisionStrategy* > d_enabledStrategies;
vector <ITEDecisionStrategy* > d_needIteSkolemMap;
+ RelevancyStrategy* d_relevancyStrategy;
vector <Node> d_assertions;
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 "
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 */
// 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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
** \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
int runCvc4(int argc, char* argv[], Options& options) {
+ // Timer statistic
+ TimerStat s_totalTime("totalTime");
+ s_totalTime.start();
+
// For the signal handlers' benefit
pOptions = &options;
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+ // Timer statistic
+ RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
+
+ // Filename statistics
ReferenceStat< const char* > s_statFilename("filename", filename);
RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
ReferenceStat< Result > s_statSatResult("sat/unsat", result);
RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
+ s_totalTime.stop();
+
if(options.statistics) {
pStatistics->flushInformation(*options.err);
}
}
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
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;
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]);
+ }
}
if (next == lit_Undef) {
// New variable decision:
- decisions++;
next = pickBranchLit();
if (next == lit_Undef) {
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::Lit>& minisat_clause) {
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;
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::Lit>& minisat_clause);
static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
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));
** \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
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.
*/
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 */
bool isDecisionEngineDone();
+ bool isDecisionRelevant(SatVariable var);
+
+ SatValue getDecisionPolarity(SatVariable var);
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
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
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();
}
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();
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(): "
{
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) {
# 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),
simplificationModeSetByUser(false),
decisionMode(DECISION_STRATEGY_INTERNAL),
decisionModeSetByUser(false),
+ decisionOptions(DecisionOptions(defaultDecOpt)),
doStaticLearning(true),
doITESimp(false),
doITESimpSetByUser(false),
{
}
+
static const string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:\n\
--version | -V identify this CVC4 binary\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\
\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 = "\
LAZY_DEFINITION_EXPANSION,
SIMPLIFICATION_MODE,
DECISION_MODE,
+ DECISION_BUDGET,
NO_STATIC_LEARNING,
ITE_SIMP,
NO_ITE_SIMP,
{ "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 },
} 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);
}
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;
/**
* 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;
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)
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
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 \
projects / cvc5.git / commitdiff