diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-04-26 20:30:41 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-05-08 19:34:15 -0400 |
| commit | b53423bcec060d5a49ee2df4d1da55ed289de1d2 (patch) | |
| tree | dc8b9a06b7dd3f4221112b93b03c8810cbc9e7dc /src/decision/options | |
| parent | 75d3b086d2cbcb4508446e405e0599788a3a25a5 (diff) | |
rm decision/relevancy
Diffstat (limited to 'src/decision/options')
| -rw-r--r-- | src/decision/options | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/decision/options b/src/decision/options index b86577e7b..5f89e9611 100644 --- a/src/decision/options +++ b/src/decision/options @@ -9,14 +9,6 @@ module DECISION "decision/options.h" Decision heuristics option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h" choose decision mode, see --decision=help -option decisionRelevancyLeaves bool -# permille = part per thousand -option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h" - impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget) -# if false, do justification stuff using relevancy.h -option decisionComputeRelevancy bool -# use the must be relevant -option decisionMustRelevancy bool # only use DE to determine when to stop, not to make decisions option decisionStopOnly bool |