blob: 7e457f125394b60381ef75ee92163fd3573fbc8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
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
|
