summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/Makefile.am5
-rw-r--r--src/decision/decision_engine.cpp22
-rw-r--r--src/decision/decision_mode.cpp40
-rw-r--r--src/decision/decision_mode.h57
-rw-r--r--src/decision/decision_strategy.h13
-rw-r--r--src/decision/options23
-rw-r--r--src/decision/options_handlers.h112
-rw-r--r--src/decision/relevancy.cpp6
-rw-r--r--src/decision/relevancy.h26
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback