blob: abb27ac9f7b7e158c7e5218deb608ca55b4486e8 (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
id = "DECISION"
name = "Decision Heuristics"
[[option]]
name = "decisionMode"
alias = ["decision-mode"]
category = "regular"
long = "decision=MODE"
type = "DecisionMode"
default = "INTERNAL"
help = "choose decision mode, see --decision=help"
help_mode = "Decision modes."
[[option.mode.INTERNAL]]
name = "internal"
help = "Use the internal decision heuristics of the SAT solver."
[[option.mode.JUSTIFICATION]]
name = "justification"
help = "An ATGP-inspired justification heuristic."
[[option.mode.STOPONLY]]
name = "stoponly"
help = "Use the justification heuristic only to stop early, not for decisions."
[[option.mode.JUSTIFICATION_OLD]]
name = "justification-old"
help = "Older implementation of an ATGP-inspired justification heuristic."
[[option.mode.STOPONLY_OLD]]
name = "stoponly-old"
help = "Use the old implementation of justification heuristic only to stop early, not for decisions."
[[option]]
name = "decisionThreshold"
category = "expert"
long = "decision-threshold=N"
type = "cvc5::decision::DecisionWeight"
default = "0"
includes = ["options/decision_weight.h"]
help = "ignore all nodes greater than threshold in first attempt to pick decision"
[[option]]
name = "decisionUseWeight"
category = "expert"
long = "decision-use-weight"
type = "bool"
default = "false"
help = "use the weight nodes (locally, by looking at children) to direct recursive search"
[[option]]
name = "decisionRandomWeight"
category = "expert"
long = "decision-random-weight=N"
type = "int"
default = "0"
help = "assign random weights to nodes between 0 and N-1 (0: disable)"
[[option]]
name = "decisionWeightInternal"
category = "expert"
long = "decision-weight-internal=HOW"
type = "DecisionWeightInternal"
default = "OFF"
help = "compute weights of internal nodes using children: off, max, sum, usr1"
help_mode = "Decision weight internal mode."
[[option.mode.OFF]]
name = "off"
[[option.mode.MAX]]
name = "max"
[[option.mode.SUM]]
name = "sum"
[[option.mode.USR1]]
name = "usr1"
[[option]]
name = "jhSkolemMode"
category = "expert"
long = "jh-skolem=MODE"
type = "JutificationSkolemMode"
default = "FIRST"
help = "policy for when to satisfy skolem definitions in justification heuristic"
help_mode = "Policy for when to satisfy skolem definitions in justification heuristic"
[[option.mode.FIRST]]
name = "first"
help = "satisfy pending relevant skolem definitions before input assertions"
[[option.mode.LAST]]
name = "last"
help = "satisfy pending relevant skolem definitions after input assertions"
[[option]]
name = "jhRlvOrder"
category = "expert"
long = "jh-rlv-order"
type = "bool"
default = "false"
help = "maintain activity-based ordering for decision justification heuristic"
[[option]]
name = "jhSkolemRlvMode"
category = "expert"
long = "jh-skolem-rlv=MODE"
type = "JutificationSkolemRlvMode"
default = "ASSERT"
help = "policy for when to consider skolem definitions relevant in justification heuristic"
help_mode = "Policy for when to consider skolem definitions relevant in justification heuristic"
[[option.mode.ASSERT]]
name = "assert"
help = "skolems are relevant when they occur in an asserted literal"
[[option.mode.ALWAYS]]
name = "always"
help = "skolems are always relevant"
|
