diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_attributes.h | 36 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 11 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 6 | ||||
-rw-r--r-- | src/decision/decision_mode.cpp | 38 | ||||
-rw-r--r-- | src/decision/decision_mode.h | 64 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 2 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 21 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 9 | ||||
-rw-r--r-- | src/decision/options | 27 | ||||
-rw-r--r-- | src/decision/options_handlers.h | 76 |
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 */ |