summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/decision_attributes.h36
-rw-r--r--src/decision/decision_engine.cpp11
-rw-r--r--src/decision/decision_engine.h6
-rw-r--r--src/decision/decision_mode.cpp38
-rw-r--r--src/decision/decision_mode.h64
-rw-r--r--src/decision/decision_strategy.h2
-rw-r--r--src/decision/justification_heuristic.cpp21
-rw-r--r--src/decision/justification_heuristic.h9
-rw-r--r--src/decision/options27
-rw-r--r--src/decision/options_handlers.h76
10 files changed, 59 insertions, 231 deletions
diff --git a/src/decision/decision_attributes.h b/src/decision/decision_attributes.h
new file mode 100644
index 000000000..03229ac84
--- /dev/null
+++ b/src/decision/decision_attributes.h
@@ -0,0 +1,36 @@
+/********************* */
+/*! \file decision_attributes.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewriter attributes
+ **
+ ** Rewriter attributes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__DECISION__DECISION_ATTRIBUTES_H
+#define __CVC4__DECISION__DECISION_ATTRIBUTES_H
+
+#include "options/decision_weight.h"
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace decision {
+namespace attr {
+ struct DecisionWeightTag {};
+}/* CVC4::decision::attr namespace */
+
+typedef expr::Attribute<attr::DecisionWeightTag, DecisionWeight> DecisionWeightAttr;
+
+}/* CVC4::decision namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__DECISION_ATTRIBUTES_H */
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index d7d463d79..12400a3b1 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -13,15 +13,14 @@
**
** Decision engine
**/
-
#include "decision/decision_engine.h"
-#include "decision/justification_heuristic.h"
+#include "decision/decision_attributes.h"
+#include "decision/justification_heuristic.h"
#include "expr/node.h"
-#include "decision/options.h"
-#include "decision/decision_mode.h"
-
-#include "smt/options.h"
+#include "options/decision_mode.h"
+#include "options/decision_options.h"
+#include "options/smt_options.h"
using namespace std;
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index ffcf2db63..7f1b7fbe2 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -21,16 +21,14 @@
#include <vector>
+#include "base/output.h"
#include "decision/decision_strategy.h"
-
#include "expr/node.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/sat_solver_types.h"
-#include "theory/decision_attributes.h"
-#include "util/ite_removal.h"
-#include "util/output.h"
#include "smt/smt_engine_scope.h"
+#include "smt_util/ite_removal.h"
using namespace std;
using namespace CVC4::prop;
diff --git a/src/decision/decision_mode.cpp b/src/decision/decision_mode.cpp
deleted file mode 100644
index 912089179..000000000
--- a/src/decision/decision_mode.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-/********************* */
-/*! \file decision_mode.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** 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
deleted file mode 100644
index fb01c587b..000000000
--- a/src/decision/decision_mode.h
+++ /dev/null
@@ -1,64 +0,0 @@
-/********************* */
-/*! \file decision_mode.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** 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 */
-
-
-/** Enumeration of combining functions for computing internal weights */
-enum DecisionWeightInternal {
- DECISION_WEIGHT_INTERNAL_OFF,
- DECISION_WEIGHT_INTERNAL_MAX,
- DECISION_WEIGHT_INTERNAL_SUM,
- DECISION_WEIGHT_INTERNAL_USR1
-};/* enum DecisionInternalWeight */
-
-}/* 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 94db110c2..210628afc 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -20,7 +20,7 @@
#define __CVC4__DECISION__DECISION_STRATEGY_H
#include "prop/sat_solver_types.h"
-#include "util/ite_removal.h"
+#include "smt_util/ite_removal.h"
namespace CVC4 {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 082f3cdbf..68c7379ce 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -16,17 +16,16 @@
**
** It needs access to the simplified but non-clausal formula.
**/
-
#include "justification_heuristic.h"
-#include "expr/node_manager.h"
#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "options/decision_options.h"
#include "theory/rewriter.h"
-#include "decision/options.h"
-#include "util/ite_removal.h"
+#include "smt_util/ite_removal.h"
-using namespace CVC4;
+namespace CVC4 {
JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
context::UserContext *uc,
@@ -297,7 +296,7 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
}
DecisionWeight JustificationHeuristic::getWeight(TNode n) {
- if(!n.hasAttribute(theory::DecisionWeightAttr()) ) {
+ if(!n.hasAttribute(DecisionWeightAttr()) ) {
DecisionWeightInternal combiningFn =
options::decisionWeightInternal();
@@ -305,7 +304,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) {
if(options::decisionRandomWeight() != 0) {
- n.setAttribute(theory::DecisionWeightAttr(), rand() % options::decisionRandomWeight());
+ n.setAttribute(DecisionWeightAttr(), rand() % options::decisionRandomWeight());
}
} else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) {
@@ -313,21 +312,21 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
DecisionWeight dW = 0;
for(TNode::iterator i=n.begin(); i != n.end(); ++i)
dW = max(dW, getWeight(*i));
- n.setAttribute(theory::DecisionWeightAttr(), dW);
+ n.setAttribute(DecisionWeightAttr(), dW);
} else if(combiningFn == DECISION_WEIGHT_INTERNAL_SUM ||
combiningFn == DECISION_WEIGHT_INTERNAL_USR1) {
DecisionWeight dW = 0;
for(TNode::iterator i=n.begin(); i != n.end(); ++i)
dW = max(dW, getWeight(*i));
- n.setAttribute(theory::DecisionWeightAttr(), dW);
+ n.setAttribute(DecisionWeightAttr(), dW);
} else {
Unreachable();
}
}
- return n.getAttribute(theory::DecisionWeightAttr());
+ return n.getAttribute(DecisionWeightAttr());
}
typedef vector<TNode> ChildList;
@@ -711,3 +710,5 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(
}
return noSplitter ? NO_SPLITTER : DONT_KNOW;
}
+
+} /* namespace CVC4 */
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index e1ed431d1..5b0deca1b 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -23,17 +23,16 @@
#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
-#include "decision_engine.h"
-#include "decision_strategy.h"
-
+#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
-#include "context/cdhashmap.h"
+#include "decision/decision_attributes.h"
+#include "decision/decision_engine.h"
+#include "decision/decision_strategy.h"
#include "expr/node.h"
#include "prop/sat_solver_types.h"
namespace CVC4 {
-
namespace decision {
class JustificationHeuristic : public ITEDecisionStrategy {
diff --git a/src/decision/options b/src/decision/options
deleted file mode 100644
index 1f0b137cb..000000000
--- a/src/decision/options
+++ /dev/null
@@ -1,27 +0,0 @@
-#
-# 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=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
-
-# only use DE to determine when to stop, not to make decisions
-option decisionStopOnly bool
-
-expert-option decisionThreshold --decision-threshold=N decision::DecisionWeight :default 0 :include "theory/decision_attributes.h"
- ignore all nodes greater than threshold in first attempt to pick decision
-
-expert-option decisionUseWeight --decision-use-weight bool :default false
- use the weight nodes (locally, by looking at children) to direct recursive search
-
-expert-option decisionRandomWeight --decision-random-weight=N int :default 0
- assign random weights to nodes between 0 and N-1 (0: disable)
-
-expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::decision::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "decision/options_handlers.h"
- computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)
-
-endmodule
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
deleted file mode 100644
index 723fb243c..000000000
--- a/src/decision/options_handlers.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/********************* */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** 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 heuristics 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\
-";
-
-inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- 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 == "help") {
- puts(decisionModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --decision: `") +
- optarg + "'. Try --decision help.");
- }
-}
-
-inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "off")
- return DECISION_WEIGHT_INTERNAL_OFF;
- else if(optarg == "max")
- return DECISION_WEIGHT_INTERNAL_MAX;
- else if(optarg == "sum")
- return DECISION_WEIGHT_INTERNAL_SUM;
- else if(optarg == "usr1")
- return DECISION_WEIGHT_INTERNAL_USR1;
- else
- throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
-}
-
-}/* CVC4::decision namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__DECISION__OPTIONS_HANDLERS_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback