diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 2 | ||||
-rw-r--r-- | src/util/options.h | 17 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index b6a306ee0..0bd02f308 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -80,6 +80,8 @@ Options::Options() : printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), simplificationModeSetByUser(false), + decisionMode(DECISION_STRATEGY_INTERNAL), + decisionModeSetByUser(false), doStaticLearning(true), interactive(false), interactiveSetByUser(false), 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; |