diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/options.cpp | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 0bd02f308..4e8bc375b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -172,6 +172,7 @@ Additional CVC4 options:\n\ --print-expr-types print types with variables when printing exprs\n\ --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ + --decision=MODE choose decision mode, see --decision=help\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ @@ -225,6 +226,16 @@ none\n\ + do not perform nonclausal simplification\n\ "; +static const string decisionHelp = "\ +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\ +"; + static const string dumpHelp = "\ Dump modes currently supported by the --dump option:\n\ \n\ @@ -338,6 +349,7 @@ enum OptionValue { UF_THEORY, LAZY_DEFINITION_EXPANSION, SIMPLIFICATION_MODE, + DECISION_MODE, NO_STATIC_LEARNING, INTERACTIVE, NO_INTERACTIVE, @@ -426,6 +438,7 @@ static struct option cmdlineOptions[] = { { "uf" , required_argument, NULL, UF_THEORY }, { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, + { "decision", required_argument, NULL, DECISION_MODE }, { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, @@ -696,6 +709,22 @@ throw(OptionException) { } break; + case DECISION_MODE: + if(!strcmp(optarg, "internal")) { + decisionMode = DECISION_STRATEGY_INTERNAL; + decisionModeSetByUser = true; + } else if(!strcmp(optarg, "justification")) { + decisionMode = DECISION_STRATEGY_JUSTIFICATION; + decisionModeSetByUser = true; + } else if(!strcmp(optarg, "help")) { + puts(decisionHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --decision: `") + + optarg + "'. Try --decision help."); + } + break; + case NO_STATIC_LEARNING: doStaticLearning = false; break; |