blob: 5ad691e622928032275e98d6f57fa35ac7892a90 (
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
|
id = "PROP"
name = "SAT layer"
header = "options/prop_options.h"
[[option]]
name = "satRandomFreq"
smt_name = "random-frequency"
category = "regular"
long = "random-freq=P"
type = "double"
default = "0.0"
predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
read_only = true
help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)"
[[option]]
name = "satRandomSeed"
smt_name = "random-seed"
category = "regular"
long = "random-seed=S"
type = "uint32_t"
default = "0"
help = "sets the random seed for the sat solver"
[[option]]
name = "satVarDecay"
category = "regular"
type = "double"
default = "0.95"
predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
help = "variable activity decay factor for Minisat"
[[option]]
name = "satClauseDecay"
category = "regular"
type = "double"
default = "0.999"
predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
help = "clause activity decay factor for Minisat"
[[option]]
name = "satRestartFirst"
category = "regular"
long = "restart-int-base=N"
type = "unsigned"
default = "25"
read_only = true
help = "sets the base restart interval for the sat solver (N=25 by default)"
[[option]]
name = "satRestartInc"
category = "regular"
long = "restart-int-inc=F"
type = "double"
default = "3.0"
predicates = ["doubleGreaterOrEqual0"]
read_only = true
help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"
[[option]]
name = "sat_refine_conflicts"
category = "regular"
long = "refine-conflicts"
type = "bool"
default = "false"
read_only = true
help = "refine theory conflict clauses (default false)"
[[option]]
name = "minisatUseElim"
category = "regular"
long = "minisat-elimination"
type = "bool"
default = "true"
help = "use Minisat elimination"
[[option]]
name = "minisatDumpDimacs"
category = "regular"
long = "minisat-dump-dimacs"
type = "bool"
default = "false"
read_only = true
help = "instead of solving minisat dumps the asserted clauses in Dimacs format"
|
