summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h17
1 files changed, 17 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
index c7fbcd896..6205c7543 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -126,6 +126,23 @@ struct CVC4_PUBLIC Options {
/** Whether the user set the nonclausal simplification mode. */
bool simplificationModeSetByUser;
+ /** Enumeration of decision strategies */
+ typedef enum {
+ /**
+ * Decision engine doesn't do anything. Use sat solver's internal
+ * heuristics
+ */
+ DECISION_STRATEGY_INTERNAL,
+ /**
+ * Use the justification heuristic
+ */
+ DECISION_STRATEGY_JUSTIFICATION
+ } DecisionMode;
+ /** When/whether to use any decision strategies */
+ DecisionMode decisionMode;
+ /** Whether the user set the decision strategy */
+ bool decisionModeSetByUser;
+
/** Whether to perform the static learning pass. */
bool doStaticLearning;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback