blob: b86577e7bb8b9c27cef4e7f86a5f3f4b627419f2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
#
# 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
expert-option decisionThreshold --decision-threshold=N decision::DecisionWeight :default 0 :include "theory/decision_attributes.h"
ignore all nodes greater than threshold in first attempt to pick decision
expert-option decisionUseWeight --decision-use-weight bool :default false
use the weight nodes (locally, by looking at children) to direct recursive search
expert-option decisionRandomWeight --decision-random-weight=N int :default 0
assign random weights to nodes between 0 and N-1 (0: disable)
expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::decision::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "decision/options_handlers.h"
computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)
endmodule
|
