diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
commit | 52c5c282f47448856e0dec8a7d4e5de612a8dcc3 (patch) | |
tree | b6eac07d1c91aeab8fbfa4d6bd03981939614e77 /src/util/options.cpp | |
parent | 6ce8f5cc5d7767d5ff9e74bc08d3c8a364ad8bf1 (diff) |
This commit merges in the branch arithmetic/cprop.
Diffstat (limited to 'src/util/options.cpp')
-rw-r--r-- | src/util/options.cpp | 207 |
1 files changed, 154 insertions, 53 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index e41959da2..a510f35f8 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -101,21 +101,22 @@ Options::Options() : replayFilename(""), replayStream(NULL), replayLog(NULL), - arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value satVarDecay(0.95), satClauseDecay(0.999), satRestartFirst(25), satRestartInc(3.0), - pivotRule(MINIMUM), + arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS), + arithPropagationMode(BOTH_PROP), + arithPivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), - ufSymmetryBreaker(false), - ufSymmetryBreakerSetByUser(false), - dioSolver(true), + arithDioSolver(true), arithRewriteEq(false), arithRewriteEqSetByUser(false), + ufSymmetryBreaker(false), + ufSymmetryBreakerSetByUser(false), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -134,8 +135,10 @@ static const string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:\n\ --version | -V identify this CVC4 binary\n\ --help | -h full command line reference\n\ - --lang | -L force input language (default is `auto'; see --lang help)\n\ - --output-lang force output language (default is `auto'; see --lang help)\n\ + --lang | -L force input language\n\ + (default is `auto'; see --lang help)\n\ + --output-lang force output language\n\ + (default is `auto'; see --lang help)\n\ --verbose | -v increase verbosity (may be repeated)\n\ --quiet | -q decrease verbosity (may be repeated)\n\ --stats give statistics on exit\n\ @@ -165,7 +168,8 @@ Additional CVC4 options:\n\ --mmap memory map file input\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ --lazy-type-checking type check expressions only when necessary (default)\n\ - --eager-type-checking type check expressions immediately on creation (debug builds only)\n\ + --eager-type-checking type check expressions immediately on creation\n\ + (debug builds only)\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ @@ -185,18 +189,35 @@ Additional CVC4 options:\n\ --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ - --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ - --pivot-threshold=N sets the number of heuristic pivots per variable per simplex instance\n\ - --prop-row-length=N sets the maximum row length to be used in propagation\n\ - --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ + SAT:\n\ + --random-freq=P frequency of random decisions in the sat solver\n\ + (P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ - --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ - --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ - --disable-arithmetic-propagation turns on arithmetic propagation\n\ - --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ + --restart-int-base=I sets the base restart interval for the sat solver\n\ + (I=25 by default)\n\ + --restart-int-inc=F restart interval increase factor for the sat solver\n\ + (F=3.0 by default)\n\ + ARITHMETIC:\n\ + --arith-presolve-lemmas=MODE determines which lemmas to add before solving\n\ + (default is 'all', see --arith-presolve-lemmas=help)\n\ + --arith-prop=MODE turns on arithmetic propagation\n\ + (default is 'old', see --arith-prop=help)\n\ + --pivot-rule=RULE change the pivot rule for the basic variable\n\ + (default is 'min', see --pivot-rule help)\n\ + --pivot-threshold=N sets the number of pivots using --pivot-rule\n\ + per basic variable per simplex instance before\n\ + using variable order\n\ + --prop-row-length=N sets the maximum row length to be used in propagation\n\ + --disable-dio-solver turns off Linear Diophantine Equation solver \n\ + (Griggio, JSAT 2012)\n\ + --enable-arith-rewrite-equalities turns on the preprocessing rewrite\n\ + turning equalities into a conjunction of inequalities.\n \ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite\n\ + turning equalities into a conjunction of inequalities.\n \ + UF:\n\ + --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\ + CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ - --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ - --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ @@ -315,6 +336,44 @@ pipe to perform on-line checking. The --dump-to option can be used to dump\n\ to a file.\n\ "; +static const string arithPresolveLemmasHelp = "\ +Presolve lemmas are generated before SAT search begins using the relationship\n\ +of constant terms and polynomials.\n\ +Modes currently supported by the --arith-presolve-lemmas option:\n\ ++ none \n\ ++ ineqs \n\ + Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ ++ eqs \n\ + Outputs lemmas of the general forms\n\ + (= p c) implies (<= p d) for c < d, or\n\ + (= p c) implies (not (= p d)) for c != d.\n\ ++ all \n\ + A combination of inequalities and equalities.\n\ +"; + +static const string propagationModeHelp = "\ +This decides on kind of propagation arithmetic attempts to do during the search.\n\ ++ none\n\ ++ unate\n\ + use constraints to do unate propagation\n\ ++ bi (Bounds Inference)\n\ + infers bounds on basic variables using the upper and lower bounds of the\n\ + non-basic variables in the tableau.\n\ ++both\n\ +"; + +static const string pivotRulesHelp = "\ +This decides on the rule used by simplex during hueristic rounds\n\ +for deciding the next basic variable to select.\n\ +Pivot rules available:\n\ ++min\n\ + The minimum abs() value of the variable's violation of its bound. (default)\n\ ++min-break-ties\n\ + The minimum violation with ties broken by variable order (total)\n\ ++max\n\ + The maximum violation the bound\n\ +"; + string Options::getDescription() const { return optionsDescription; } @@ -341,7 +400,8 @@ void Options::printLanguageHelp(std::ostream& out) { * any collision. */ enum OptionValue { - SMTCOMP = 256, /* avoid clashing with char options */ + OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */ + SMTCOMP, STATS, SEGV_NOSPIN, OUTPUT_LANGUAGE, @@ -377,13 +437,14 @@ enum OptionValue { EAGER_TYPE_CHECKING, REPLAY, REPLAY_LOG, - PIVOT_RULE, PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, SAT_RESTART_FIRST, SAT_RESTART_INC, - ARITHMETIC_PROPAGATION, + ARITHMETIC_UNATE_LEMMA_MODE, + ARITHMETIC_PROPAGATION_MODE, + ARITHMETIC_PIVOT_RULE, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, @@ -401,7 +462,8 @@ enum OptionValue { BITVECTOR_EAGER_BITBLAST, BITVECTOR_SHARE_LEMMAS, BITVECTOR_EAGER_FULLCHECK, - SAT_REFINE_CONFLICTS + SAT_REFINE_CONFLICTS, + OPTION_VALUE_END };/* enum OptionValue */ /** @@ -475,15 +537,16 @@ static struct option cmdlineOptions[] = { { "incremental", no_argument , NULL, 'i' }, { "replay" , required_argument, NULL, REPLAY }, { "replay-log" , required_argument, NULL, REPLAY_LOG }, - { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, - { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD }, - { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, { "print-winner", no_argument , NULL, PRINT_WINNER }, - { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, + { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE }, + { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE }, + { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE }, + { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD }, + { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES }, { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES }, @@ -878,24 +941,6 @@ throw(OptionException) { #endif /* CVC4_REPLAY */ break; - case ARITHMETIC_PROPAGATION: - arithPropagation = false; - break; - - case ARITHMETIC_DIO_SOLVER: - dioSolver = false; - break; - - case ENABLE_ARITHMETIC_REWRITE_EQUALITIES: - arithRewriteEq = true; - arithRewriteEqSetByUser = true; - break; - - case DISABLE_ARITHMETIC_REWRITE_EQUALITIES: - arithRewriteEq = false; - arithRewriteEqSetByUser = true; - break; - case ENABLE_SYMMETRY_BREAKER: ufSymmetryBreaker = true; ufSymmetryBreakerSetByUser = true; @@ -993,21 +1038,62 @@ throw(OptionException) { } break; - case PIVOT_RULE: + case ARITHMETIC_UNATE_LEMMA_MODE: + if(!strcmp(optarg, "all")) { + arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "none")) { + arithUnateLemmaMode = NO_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "ineqs")) { + arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "eqs")) { + arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "help")) { + puts(arithPresolveLemmasHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --arith-presolve-lemmas: `") + + optarg + "'. Try --arith-presolve-lemmas=help."); + } + break; + + case ARITHMETIC_PROPAGATION_MODE: + if(!strcmp(optarg, "none")) { + arithPropagationMode = NO_PROP; + break; + } else if(!strcmp(optarg, "unate")) { + arithPropagationMode = UNATE_PROP; + break; + } else if(!strcmp(optarg, "bi")) { + arithPropagationMode = BOUND_INFERENCE_PROP; + break; + } else if(!strcmp(optarg, "both")) { + arithPropagationMode = BOTH_PROP; + break; + } else if(!strcmp(optarg, "help")) { + puts(propagationModeHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --arith-prop: `") + + optarg + "'. Try --arith-prop help."); + } + break; + + case ARITHMETIC_PIVOT_RULE: if(!strcmp(optarg, "min")) { - pivotRule = MINIMUM; + arithPivotRule = MINIMUM; break; } else if(!strcmp(optarg, "min-break-ties")) { - pivotRule = BREAK_TIES; + arithPivotRule = BREAK_TIES; break; } else if(!strcmp(optarg, "max")) { - pivotRule = MAXIMUM; + arithPivotRule = MAXIMUM; break; } else if(!strcmp(optarg, "help")) { - printf("Pivot rules available:\n"); - printf("min\n"); - printf("min-break-ties\n"); - printf("max\n"); + puts(pivotRulesHelp.c_str()); exit(1); } else { throw OptionException(string("unknown option for --pivot-rule: `") + @@ -1023,6 +1109,20 @@ throw(OptionException) { arithPropagateMaxLength = atoi(optarg); break; + case ARITHMETIC_DIO_SOLVER: + arithDioSolver = false; + break; + + case ENABLE_ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = true; + arithRewriteEqSetByUser = true; + break; + + case DISABLE_ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = false; + arithRewriteEqSetByUser = true; + break; + case SHOW_DEBUG_TAGS: if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { printf("available tags:"); @@ -1121,7 +1221,8 @@ throw(OptionException) { case ':': // This can be a long or short option, and the way to get at the name of it is different. - if(optopt == 0) { // was a long option + if(optopt == 0 || // was a long option + (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); } else { // was a short option throw OptionException(string("option `-") + char(optopt) + "' missing its required argument"); |