diff options
Diffstat (limited to 'src/decision/options')
| -rw-r--r-- | src/decision/options | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/decision/options b/src/decision/options new file mode 100644 index 000000000..7e457f125 --- /dev/null +++ b/src/decision/options @@ -0,0 +1,23 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DECISION "decision/options.h" Decision heuristics + +# When/whether to use any decision strategies +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 + +endmodule |