diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/Makefile.am | 5 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 22 | ||||
-rw-r--r-- | src/decision/decision_mode.cpp | 40 | ||||
-rw-r--r-- | src/decision/decision_mode.h | 57 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 13 | ||||
-rw-r--r-- | src/decision/options | 23 | ||||
-rw-r--r-- | src/decision/options_handlers.h | 112 | ||||
-rw-r--r-- | src/decision/relevancy.cpp | 6 | ||||
-rw-r--r-- | src/decision/relevancy.h | 26 |
9 files changed, 269 insertions, 35 deletions
diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am index 4f454e9bf..5f62568ee 100644 --- a/src/decision/Makefile.am +++ b/src/decision/Makefile.am @@ -6,6 +6,8 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libdecision.la libdecision_la_SOURCES = \ + decision_mode.h \ + decision_mode.cpp \ decision_engine.h \ decision_engine.cpp \ decision_strategy.h \ @@ -13,3 +15,6 @@ libdecision_la_SOURCES = \ justification_heuristic.cpp \ relevancy.h \ relevancy.cpp + +EXTRA_DIST = \ + options_handlers.h diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index b42f69b7f..2832a9577 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -21,7 +21,10 @@ #include "decision/relevancy.h" #include "expr/node.h" -#include "util/options.h" +#include "decision/options.h" +#include "decision/decision_mode.h" + +#include "smt/options.h" using namespace std; @@ -49,24 +52,23 @@ void DecisionEngine::init() d_engineState = 1; Trace("decision-init") << "DecisionEngine::init()" << std::endl; - const Options* options = Options::current(); - if(options->incrementalSolving) return; + if(options::incrementalSolving()) return; Trace("decision-init") << " * options->decisionMode: " - << options->decisionMode << std:: endl; - Trace("decision-init") << " * options->decisionOptions.stopOnly: " - << ((options->decisionOptions).stopOnly) << std::endl; + << options::decisionMode() << std:: endl; + Trace("decision-init") << " * options->decisionStopOnly: " + << options::decisionStopOnly() << std::endl; - if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } - if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { + if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { } + if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) { ITEDecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext); enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } - if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) { + if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) { RelevancyStrategy* ds = - new decision::Relevancy(this, d_satContext, options->decisionOptions); + new decision::Relevancy(this, d_satContext); enableStrategy(ds); d_needIteSkolemMap.push_back(ds); d_relevancyStrategy = ds; diff --git a/src/decision/decision_mode.cpp b/src/decision/decision_mode.cpp new file mode 100644 index 000000000..c4bb58b93 --- /dev/null +++ b/src/decision/decision_mode.cpp @@ -0,0 +1,40 @@ +/********************* */ +/*! \file decision_mode.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "decision/decision_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) { + switch(mode) { + case decision::DECISION_STRATEGY_INTERNAL: + out << "DECISION_STRATEGY_INTERNAL"; + break; + case decision::DECISION_STRATEGY_JUSTIFICATION: + out << "DECISION_STRATEGY_JUSTIFICATION"; + break; + default: + out << "DecisionMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ + diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h new file mode 100644 index 000000000..f6dba32ea --- /dev/null +++ b/src/decision/decision_mode.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file decision_mode.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SMT__DECISION_MODE_H +#define __CVC4__SMT__DECISION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace decision { + +/** Enumeration of decision strategies */ +enum DecisionMode { + + /** + * Decision engine doesn't do anything. Use sat solver's internal + * heuristics + */ + DECISION_STRATEGY_INTERNAL, + + /** + * Use the justification heuristic + */ + DECISION_STRATEGY_JUSTIFICATION, + + /** + * Use may-relevancy. + */ + DECISION_STRATEGY_RELEVANCY + +};/* enum DecisionMode */ + +}/* CVC4::decision namespace */ + +std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__DECISION_MODE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index ee7d340c4..dd6c7f548 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -27,8 +27,8 @@ namespace CVC4 { class DecisionEngine; namespace context { -class Context; -} + class Context; +}/* CVC4::context namespace */ namespace decision { @@ -47,7 +47,7 @@ public: virtual bool needIteSkolemMap() { return false; } virtual void notifyAssertionsAvailable() { return; } -}; +};/* class DecisionStrategy */ class ITEDecisionStrategy : public DecisionStrategy { public: @@ -61,7 +61,7 @@ public: virtual void addAssertions(const std::vector<Node> &assertions, unsigned assertionsEnd, IteSkolemMap iteSkolemMap) = 0; -}; +};/* class ITEDecisionStrategy */ class RelevancyStrategy : public ITEDecisionStrategy { public: @@ -71,10 +71,9 @@ public: virtual bool isRelevant(TNode n) = 0; virtual prop::SatValue getPolarity(TNode n) = 0; -}; +};/* class RelevancyStrategy */ - -}/* decision namespace */ +}/* CVC4::decision namespace */ }/* CVC4 namespace */ #endif /* __CVC4__DECISION__DECISION_STRATEGY_H */ diff --git a/src/decision/options b/src/decision/options new file mode 100644 index 000000000..7e457f125 --- /dev/null +++ b/src/decision/options @@ -0,0 +1,23 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DECISION "decision/options.h" Decision heuristics + +# When/whether to use any decision strategies +option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h" + choose decision mode, see --decision=help + +option decisionRelevancyLeaves bool +# permille = part per thousand +option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h" + impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget) +# if false, do justification stuff using relevancy.h +option decisionComputeRelevancy bool +# use the must be relevant +option decisionMustRelevancy bool +# only use DE to determine when to stop, not to make decisions +option decisionStopOnly bool + +endmodule diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h new file mode 100644 index 000000000..e9f227043 --- /dev/null +++ b/src/decision/options_handlers.h @@ -0,0 +1,112 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Custom handlers and predicates for DecisionEngine options + ** + ** Custom handlers and predicates for DecisionEngine options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__DECISION__OPTIONS_HANDLERS_H +#define __CVC4__DECISION__OPTIONS_HANDLERS_H + +#include "decision/decision_mode.h" +#include "main/options.h" + +namespace CVC4 { +namespace decision { + +static const std::string decisionModeHelp = "\ +Decision modes currently supported by the --decision option:\n\ +\n\ +internal (default)\n\ ++ Use the internal decision hueristics of the SAT solver\n\ +\n\ +justification\n\ ++ An ATGP-inspired justification heuristic\n\ +\n\ +justification-stoponly\n\ ++ Use the justification heuristic only to stop early, not for decisions\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\ +"; + +inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + options::decisionRelevancyLeaves.set(false); + options::decisionMaxRelTimeAsPermille.set(1000); + options::decisionComputeRelevancy.set(true); + options::decisionMustRelevancy.set(false); + options::decisionStopOnly.set(false); + + if(optarg == "internal") { + return DECISION_STRATEGY_INTERNAL; + } else if(optarg == "justification") { + return DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "justification-stoponly") { + options::decisionStopOnly.set(true); + return DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "relevancy") { + options::decisionRelevancyLeaves.set(false); + return DECISION_STRATEGY_RELEVANCY; + } else if(optarg == "relevancy-leaves") { + options::decisionRelevancyLeaves.set(true); + Trace("options") << "version is " << options::version() << std::endl; + return DECISION_STRATEGY_RELEVANCY; + } else if(optarg == "justification-rel") { + // relevancyLeaves : irrelevant + // maxRelTimeAsPermille : irrelevant + options::decisionComputeRelevancy.set(false); + options::decisionMustRelevancy.set(false); + return DECISION_STRATEGY_RELEVANCY; + } else if(optarg == "justification-must") { + // relevancyLeaves : irrelevant + // maxRelTimeAsPermille : irrelevant + options::decisionComputeRelevancy.set(false); + options::decisionMustRelevancy.set(true); + return DECISION_STRATEGY_RELEVANCY; + } else if(optarg == "help") { + puts(decisionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --decision: `") + + optarg + "'. Try --decision help."); + } +} + +inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) { + if(budget == 0) { + Warning() << "Decision budget is 0. Consider using internal decision heuristic and " + << std::endl << " removing this option." << std::endl; + + } +} + +}/* CVC4::decision namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__OPTIONS_HANDLERS_H */ diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index d0d44f606..fe5bdcc20 100644 --- a/src/decision/relevancy.cpp +++ b/src/decision/relevancy.cpp @@ -34,7 +34,7 @@ void Relevancy::setJustified(TNode n) { Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; d_justified.insert(n); - if(d_opt.computeRelevancy) { + if(options::decisionComputeRelevancy()) { d_relevancy[n] = d_maxRelevancy[n]; updateRelevancy(n); } @@ -117,7 +117,7 @@ bool Relevancy::findSplitterRec(TNode node, if(d_polarityCache.find(node) == d_polarityCache.end()) { d_polarityCache[node] = desiredVal; } else { - Assert(d_multipleBacktrace || d_opt.computeRelevancy); + Assert(d_multipleBacktrace || options::decisionComputeRelevancy()); return true; } @@ -289,7 +289,7 @@ bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) { bool ret = false; for(int i = 0; i < n; ++i) { if (findSplitterRec(node[i], desiredVal)) { - if(!d_opt.computeRelevancy) + if(!options::decisionComputeRelevancy()) return true; else ret = true; diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index f45ce2e8f..a529b974e 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -35,12 +35,12 @@ #include "decision_engine.h" #include "decision_strategy.h" +#include "decision/options.h" #include "context/cdhashset.h" #include "context/cdhashmap.h" #include "expr/node.h" #include "prop/sat_solver_types.h" -#include "util/options.h" namespace CVC4 { @@ -109,9 +109,6 @@ class Relevancy : public RelevancyStrategy { 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; @@ -121,7 +118,7 @@ class Relevancy : public RelevancyStrategy { /** current decision for the recursive call */ SatLiteral* d_curDecision; public: - Relevancy(CVC4::DecisionEngine* de, context::Context *c, const Options::DecisionOptions &decOpt): + Relevancy(CVC4::DecisionEngine* de, context::Context *c): RelevancyStrategy(de, c), d_justified(c), d_prvsIndex(c, 0), @@ -132,10 +129,9 @@ public: d_expense("decision::rel::expense", 0), d_timestat("decision::rel::time"), d_relevancy(c), - d_multipleBacktrace(decOpt.computeRelevancy), + d_multipleBacktrace(options::decisionComputeRelevancy()), // d_computeRelevancy(decOpt.computeRelevancy), - d_opt(decOpt), - d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0), + d_maxTimeAsPercentageOfTotalTime(options::decisionMaxRelTimeAsPermille()*1.0/10.0), d_curDecision(NULL) { Warning() << "There are known bugs in this Relevancy code which we know" @@ -149,11 +145,11 @@ public: StatisticsRegistry::registerStat(&d_expense); StatisticsRegistry::registerStat(&d_timestat); Trace("decision") << "relevancy enabled with" << std::endl; - Trace("decision") << " * computeRelevancy: " << (d_opt.computeRelevancy ? "on" : "off") + Trace("decision") << " * computeRelevancy: " << (options::decisionComputeRelevancy() ? "on" : "off") << std::endl; - Trace("decision") << " * relevancyLeaves: " << (d_opt.relevancyLeaves ? "on" : "off") + Trace("decision") << " * relevancyLeaves: " << (options::decisionRelevancyLeaves() ? "on" : "off") << std::endl; - Trace("decision") << " * mustRelevancy [unimplemented]: " << (d_opt.mustRelevancy ? "on" : "off") + Trace("decision") << " * mustRelevancy [unimplemented]: " << (options::decisionMustRelevancy() ? "on" : "off") << std::endl; } ~Relevancy() { @@ -189,13 +185,13 @@ public: SatValue desiredVal = SAT_VALUE_TRUE; SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal); - if(!d_opt.computeRelevancy && litDecision != undefSatLiteral) { + if(!options::decisionComputeRelevancy() && litDecision != undefSatLiteral) { d_prvsIndex = i; return litDecision; } } - if(d_opt.computeRelevancy) return undefSatLiteral; + if(options::decisionComputeRelevancy()) return undefSatLiteral; Trace("decision") << "jh: Nothing to split on " << std::endl; @@ -244,7 +240,7 @@ public: for(unsigned i = 0; i < assertionsEnd; ++i) { d_assertions.push_back(assertions[i]); d_visited.clear(); - if(d_opt.computeRelevancy) increaseMaxRelevancy(assertions[i]); + if(options::decisionComputeRelevancy()) increaseMaxRelevancy(assertions[i]); d_visited.clear(); } @@ -267,7 +263,7 @@ public: return true; } - if(d_opt.relevancyLeaves && !isAtomicFormula(n)) { + if(options::decisionRelevancyLeaves() && !isAtomicFormula(n)) { Trace("decision") << "no [not a leaf]" << std::endl; return false; } |