12#define OPTIONS \
13 OPTION (ands, 1, 0, 1, "extract and eliminate and gates") \
14 OPTION (backbone, 1, 0, 2, "binary clause backbone (2=eager)") \
15 OPTION (backboneeffort, 20, 0, 1e5, "effort in per mille") \
16 OPTION (backbonemaxrounds, 1e3, 1, INT_MAX, "maximum backbone rounds") \
17 OPTION (backbonerounds, 100, 1, INT_MAX, "backbone rounds limit") \
18 OPTION (bigbigfraction, 990, 0, 1000, "big binary clause fraction per mille") \
19 OPTION (bump, 1, 0, 1, "enable variable bumping") \
20 OPTION (bumpreasons, 1, 0, 1, "bump reason side literals too") \
21 OPTION (bumpreasonslimit, 10, 1, INT_MAX, "relative reason literals limit") \
22 OPTION (bumpreasonsrate, 10, 1, INT_MAX, "decision rate limit") \
23 DBGOPT (check, 2, 0, 2, "check model (1) and derived clauses (2)") \
24 OPTION (chrono, 1, 0, 1, "allow chronological backtracking") \
25 OPTION (chronolevels, 100, 0, INT_MAX, "maximum jumped over levels") \
26 OPTION (compact, 1, 0, 1, "enable compacting garbage collection") \
27 OPTION (compactlim, 10, 0, 100, "compact inactive limit (in percent)") \
28 OPTION (congruence, 1, 0, 1, "congruence closure on extracted gates") \
29 OPTION (congruenceandarity, 1000000, 2, 50000000, "AND gate arity limit") \
30 OPTION (congruenceands, 1, 0, 1, "extract AND gates for congruence closure") \
31 OPTION (congruencebinaries, 1, 0, 1, "extract certain binary clauses") \
32 OPTION (congruenceites, 1, 0, 1, "extract ITE gates for congruence closure") \
33 OPTION (congruenceonce, 0, 0, 1, "congruence closure only initially") \
34 OPTION (congruencexorarity, 4, 2, 20, "congruence XOR gate arity limit") \
35 OPTION (congruencexorcounts, 2, 1, INT_MAX, "XOR counting rounds") \
36 OPTION (congruencexors, 1, 0, 1, "extract XOR gates for congruence closure") \
37 OPTION (decay, 50, 1, 200, "per mille scores decay") \
38 OPTION (definitioncores, 2, 1, 100, "how many cores") \
39 OPTION (definitions, 1, 0, 1, "extract general definitions") \
40 OPTION (definitionticks, 1e6, 0, INT_MAX, "kitten ticks limits") \
41 OPTION (defraglim, 75, 50, 100, "usable defragmentation limit in percent") \
42 OPTION (defragsize, 1 << 18, 10, INT_MAX, "size defragmentation limit") \
43 OPTION (eagersubsume, 4, 0, 4, "eagerly subsume previous learned clauses") \
44 OPTION (eliminate, 1, 0, 1, "bounded variable elimination BVE") \
45 OPTION (eliminatebound, 16, 0, 1 << 13, "maximum elimination bound") \
46 OPTION (eliminateclslim, 100, 1, INT_MAX, "elimination clause size limit") \
47 OPTION (eliminateeffort, 100, 0, 2e3, "effort in per mille") \
48 OPTION (eliminateinit, 500, 0, INT_MAX, "initial elimination interval") \
49 OPTION (eliminateint, 500, 10, INT_MAX, "base elimination interval") \
50 OPTION (eliminateocclim, 2e3, 0, INT_MAX, "elimination occurrence limit") \
51 OPTION (eliminaterounds, 2, 1, 1e4, "elimination rounds limit") \
52 OPTION (emafast, 33, 10, 1e6, "fast exponential moving average window") \
53 OPTION (emaslow, 1e5, 100, 1e6, "slow exponential moving average window") \
54 EMBOPT (embedded, 1, 0, 1, "parse and apply embedded options") \
55 OPTION (equivalences, 1, 0, 1, "extract and eliminate equivalence gates") \
56 OPTION (extract, 1, 0, 1, "extract gates in variable elimination") \
57 OPTION (factor, 1, 0, 1, "bounded variable addition") \
58 OPTION (factorcandrounds, 2, 0, INT_MAX, "candidates reduction rounds") \
59 OPTION (factoreffort, 50, 0, 1e6, "bounded variable effort in per mille") \
60 OPTION (factorhops, 3, 1, 10, "structural factoring heuristic hops") \
61 OPTION (factoriniticks, 700, 1, 1000000, "initial ticks ticks in millions") \
62 OPTION (factorsize, 5, 2, INT_MAX, "bounded variable addition clause size") \
63 OPTION (factorstructural, 0, 0, 1, "structural bounded variable addition") \
64 OPTION (fastel, 1, 0, 1, "initial fast variable elimination") \
65 OPTION (fastelclslim, 100, 1, INT_MAX, "fast elimination clause length limit") \
66 OPTION (fastelim, 8, 1, 1000, "fast elimination resolvents limit") \
67 OPTION (fasteloccs, 100, 1, 1000, "fast elimination occurrence limit") \
68 OPTION (fastelrounds, 4, 1, 1000, "fast elimination rounds") \
69 OPTION (fastelsub, 1, 0, 1, "forward subsuming fast variable elimination") \
70 OPTION (flushproof, 0, 0, 1, "flush proof lines immediately") \
71 OPTION (focusedtiers, 1, 0, 1, "always used focused mode tiers") \
72 OPTION (forcephase, 0, 0, 1, "force initial phase") \
73 OPTION (forward, 1, 0, 1, "forward subsumption in BVE") \
74 OPTION (forwardeffort, 100, 0, 1e6, "effort in per mille") \
75 OPTION (ifthenelse, 1, 0, 1, "extract and eliminate if-then-else gates") \
76 OPTION (incremental, 0, 0, 1, "enable incremental solving") \
77 OPTION (jumpreasons, 1, 0, 1, "jump binary reasons") \
78 LOGOPT (log, 0, 0, 5, "logging level (1=on,2=more,3=check,4/5=mem)") \
79 OPTION (lucky, 1, 0, 1, "try some lucky assignments") \
80 OPTION (luckyearly, 1, 0, 1, "lucky assignments before preprocessing") \
81 OPTION (luckylate, 1, 0, 1, "lucky assignments after preprocessing") \
82 OPTION (mineffort, 10, 0, INT_MAX, "minimum absolute effort in millions") \
83 OPTION (minimize, 1, 0, 1, "learned clause minimization") \
84 OPTION (minimizedepth, 1e3, 1, 1e6, "minimization depth") \
85 OPTION (minimizeticks, 1, 0, 1, "count ticks in minimize and shrink") \
86 OPTION (modeinit, 1e3, 10, 1e8, "initial focused conflicts limit") \
87 OPTION (modeint, 1e3, 10, 1e8, "focused conflicts interval") \
88 OPTION (otfs, 1, 0, 1, "on-the-fly strengthening") \
89 OPTION (phase, 1, 0, 1, "initial decision phase") \
90 OPTION (phasesaving, 1, 0, 1, "enable phase saving") \
91 OPTION (preprocess, 1, 0, 1, "initial preprocessing") \
92 OPTION (preprocessbackbone, 1, 0, 1, "backbone preprocessing") \
93 OPTION (preprocesscongruence, 1, 0, 1, "congruence preprocessing") \
94 OPTION (preprocessfactor, 1, 0, 1, "variable addition preprocessing") \
95 OPTION (preprocessprobe, 1, 0, 1, "probing preprocessing") \
96 OPTION (preprocessrounds, 1, 1, INT_MAX, "initial preprocessing rounds") \
97 OPTION (preprocessweep, 1, 0, 1, "sweep preprocessing") \
98 OPTION (probe, 1, 0, 1, "enable probing") \
99 OPTION (probeinit, 100, 0, INT_MAX, "initial probing interval") \
100 OPTION (probeint, 100, 2, INT_MAX, "probing interval") \
101 OPTION (proberounds, 2, 1, INT_MAX, "probing rounds") \
102 NQTOPT (profile, 2, 0, 4, "profile level") \
103 OPTION (promote, 1, 0, 1, "promote clauses") \
104 NQTOPT (quiet, 0, 0, 1, "disable all messages") \
105 OPTION (randec, 1, 0, 1, "random decisions") \
106 OPTION (randecfocused, 1, 0, 1, "random decisions in focused mode") \
107 OPTION (randecinit, 500, 0, INT_MAX, "random decisions interval") \
108 OPTION (randecint, 500, 0, INT_MAX, "initial random decisions interval") \
109 OPTION (randeclength, 10, 1, INT_MAX, "random conflicts length") \
110 OPTION (randecstable, 0, 0, 1, "random decisions in stable mode") \
111 OPTION (reduce, 1, 0, 1, "learned clause reduction") \
112 OPTION (reducehigh, 900, 0, 1000, "high reduce fraction per mille") \
113 OPTION (reduceinit, 1e3, 2, 1e5, "initial reduce interval") \
114 OPTION (reduceint, 1e3, 2, 1e5, "base reduce interval") \
115 OPTION (reducelow, 500, 0, 1000, "low reduce fraction per mille") \
116 OPTION (reluctant, 1, 0, 1, "stable reluctant doubling restarting") \
117 OPTION (reluctantint, 1 << 10, 2, 1 << 15, "reluctant interval") \
118 OPTION (reluctantlim, 1 << 20, 0, 1 << 30, "reluctant limit (0=unlimited)") \
119 OPTION (reorder, 2, 0, 2, "reorder decisions (1=stable-mode-only)") \
120 OPTION (reorderinit, 1e4, 0, 1e5, "initial reorder interval") \
121 OPTION (reorderint, 1e4, 1, 1e5, "base reorder interval") \
122 OPTION (reordermaxsize, 100, 2, 256, "reorder maximum clause size") \
123 OPTION (rephase, 1, 0, 1, "reinitialization of decision phases") \
124 OPTION (rephaseinit, 1e3, 10, 1e5, "initial rephase interval") \
125 OPTION (rephaseint, 1e3, 10, 1e5, "base rephase interval") \
126 OPTION (restart, 1, 0, 1, "enable restarts") \
127 OPTION (restartint, RESTARTINT_DEFAULT, 1, 1e4, "base restart interval") \
128 OPTION (restartmargin, 10, 0, 25, "fast/slow margin in percent") \
129 OPTION (restartreusetrail, 1, 0, 1, "restarts tries to reuse trail") \
130 OPTION (seed, 0, 0, INT_MAX, "random seed") \
131 OPTION (shrink, 3, 0, 3, "learned clauses (1=bin,2=lrg,3=rec)") \
132 OPTION (simplify, 1, 0, 1, "enable probing and elimination") \
133 OPTION (smallclauses, 1e5, 0, INT_MAX, "small clauses limit") \
134 OPTION (stable, STABLE_DEFAULT, 0, 2, "enable stable search mode") \
135 NQTOPT (statistics, 0, 0, 1, "print complete statistics") \
136 OPTION (substitute, 1, 0, 1, "equivalent literal substitution") \
137 OPTION (substituteeffort, 10, 1, 1e3, "effort in per mille") \
138 OPTION (substituterounds, 2, 1, 100, "maximum substitution rounds") \
139 OPTION (subsumeclslim, 1e3, 1, INT_MAX, "subsumption clause size limit") \
140 OPTION (subsumeocclim, 1e3, 0, INT_MAX, "subsumption occurrence limit") \
141 OPTION (sweep, 1, 0, 1, "enable SAT sweeping") \
142 OPTION (sweepclauses, 1024, 0, INT_MAX, "environment clauses") \
143 OPTION (sweepcomplete, 0, 0, 1, "run SAT sweeping until completion") \
144 OPTION (sweepdepth, 2, 0, INT_MAX, "environment depth") \
145 OPTION (sweepeffort, 100, 0, 1e4, "effort in per mille") \
146 OPTION (sweepfliprounds, 1, 0, INT_MAX, "flipping rounds") \
147 OPTION (sweepmaxclauses, 32768, 2, INT_MAX, "maximum environment clauses") \
148 OPTION (sweepmaxdepth, 3, 1, INT_MAX, "maximum environment depth") \
149 OPTION (sweepmaxvars, 8192, 2, INT_MAX, "maximum environment variables") \
150 OPTION (sweeprand, 0, 0, 1, "randomize sweeping environment") \
151 OPTION (sweepvars, 256, 0, INT_MAX, "environment variables") \
152 OPTION (target, TARGET_DEFAULT, 0, 2, "target phases (1=stable,2=focused)") \
153 OPTION (tier1, 2, 1, 100, "learned clause tier one glue limit") \
154 OPTION (tier1relative, 500, 0, 1000, "relative tier one glue limit") \
155 OPTION (tier2, 6, 1, 1e3, "learned clause tier two glue limit") \
156 OPTION (tier2relative, 900, 0, 1000, "relative tier two glue limit") \
157 OPTION (transitive, 1, 0, 1, "transitive reduction of binary clauses") \
158 OPTION (transitiveeffort, 20, 0, 2e3, "effort in per mille") \
159 OPTION (transitivekeep, 1, 0, 1, "keep transitivity candidates") \
160 OPTION (tumble, 1, 0, 1, "tumbled external indices order") \
161 NQTOPT (verbose, 0, 0, 3, "verbosity level") \
162 OPTION (vivify, 1, 0, 1, "vivify clauses") \
163 OPTION (vivifyeffort, 100, 0, 1e3, "effort in per mille") \
164 OPTION (vivifyfocusedtiers, 1, 0, 1, "use focused tier limits") \
165 OPTION (vivifyirr, 3, 0, 100, "relative irredundant effort") \
166 OPTION (vivifysort, 1, 0, 1, "sort vivification candidates") \
167 OPTION (vivifytier1, 3, 0, 100, "relative tier1 effort") \
168 OPTION (vivifytier2, 3, 0, 100, "relative tier2 effort") \
169 OPTION (vivifytier3, 1, 0, 100, "relative tier3 effort") \
170 OPTION (walkeffort, 50, 0, 1e6, "effort in per mille") \
171 OPTION (walkinitially, 0, 0, 1, "initial local search") \
172 OPTION (warmup, 1, 0, 1, "initialize phases by unit propagation")
