diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/options_handlers.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/options_handlers.h')
-rw-r--r-- | src/theory/arith/options_handlers.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h index 1e2ab379a..899a3a7c6 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -51,16 +51,16 @@ This decides on kind of propagation arithmetic attempts to do during the search. +both\n\ "; -static const std::string heuristicPivotRulesHelp = "\ -This decides on the rule used by simplex during heuristic rounds\n\ +static const std::string errorSelectionRulesHelp = "\ +This decides on the rule used by simplex during hueristic rounds\n\ for deciding the next basic variable to select.\n\ Heuristic 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\ ++varord\n\ + The variable order\n\ "; inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { @@ -99,15 +99,15 @@ inline ArithPropagationMode stringToArithPropagationMode(std::string option, std } } -inline ArithHeuristicPivotRule stringToArithHeuristicPivotRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { +inline ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "min") { - return MINIMUM; - } else if(optarg == "min-break-ties") { - return BREAK_TIES; + return MINIMUM_AMOUNT; + } else if(optarg == "varord") { + return VAR_ORDER; } else if(optarg == "max") { - return MAXIMUM; + return MAXIMUM_AMOUNT; } else if(optarg == "help") { - puts(heuristicPivotRulesHelp.c_str()); + puts(errorSelectionRulesHelp.c_str()); exit(1); } else { throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") + |