diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-23 17:56:19 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-23 17:56:19 +0000 |
commit | 5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3 (patch) | |
tree | a3fe0f00ae5d5cd087b23c885c8b170ceb07b919 /src/util | |
parent | 04e81f6d12cad8f2519aa6c94adee52aadd71ec3 (diff) |
Merge from decision branch -- partially working justification heuristic
Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
unknown and smtEngine queries DE to get the answer
relevant stat: smt::resultSource
* there are known bugs
Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A
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; |