在一对文件（options.hpp和options.cpp）运行控制参数统一初始化并设置动态增长规律；
1 #ifndef _options_hpp_INCLUDED
2 #define _options_hpp_INCLUDED
3
4 /*------------------------------------------------------------------------*/
5
6 // In order to add a new option, simply add a new line below. Make sure that
7 // options are sorted correctly (with '!}sort -k 2' in 'vi'). Otherwise
8 // initializing the options will trigger an internal error. For the model
9 // based tester 'mobical' the policy is that options which become redundant
10 // because another one is disabled (set to zero) should have the name of the
11 // latter as prefix. The 'O' column determines the options which are
12 // target to 'optimize' them ('-O[1-3]'). A zero value in the 'O' column
13 // means that this option is not optimized. A value of '1' results in
14 // optimizing its value exponentially with exponent base '2', and a value
15 // of '2' uses base '10'. The 'P' column determines simplification
16 // options (disabled with '--plain') and 'R' which values can be reset.
17
18 // clang-format off
19
20 #define OPTIONS \
21 \
22 /* NAME DEFAULT, LO, HI,O,P,R, USAGE */ \
23 \
24 OPTION( arena, 1, 0, 1,0,0,1, "allocate clauses in arena") \
25 OPTION( arenacompact, 1, 0, 1,0,0,1, "keep clauses compact") \
26 OPTION( arenasort, 1, 0, 1,0,0,1, "sort clauses in arena") \
27 OPTION( arenatype, 3, 1, 3,0,0,1, "1=clause, 2=var, 3=queue") \
28 OPTION( binary, 1, 0, 1,0,0,1, "use binary proof format") \
29 OPTION( block, 0, 0, 1,0,1,1, "blocked clause elimination") \
30 OPTION( blockmaxclslim, 1e5, 1,2e9,2,0,1, "maximum clause size") \
31 OPTION( blockminclslim, 2, 2,2e9,0,0,1, "minimum clause size") \
32 OPTION( blockocclim, 1e2, 1,2e9,2,0,1, "occurrence limit") \
33 OPTION( bump, 1, 0, 1,0,0,1, "bump variables") \
34 OPTION( bumpreason, 1, 0, 1,0,0,1, "bump reason literals too") \
35 OPTION( bumpreasondepth, 1, 1, 3,0,0,1, "bump reason depth") \
36 OPTION( check, 0, 0, 1,0,0,0, "enable internal checking") \
37 OPTION( checkassumptions, 1, 0, 1,0,0,0, "check assumptions satisfied") \
38 OPTION( checkconstraint, 1, 0, 1,0,0,0, "check constraint satisfied") \
39 OPTION( checkfailed, 1, 0, 1,0,0,0, "check failed literals form core") \
40 OPTION( checkfrozen, 0, 0, 1,0,0,0, "check all frozen semantics") \
41 OPTION( checkproof, 3, 0, 3,0,0,0, "1=drat, 2=lrat, 3=both") \
42 OPTION( checkwitness, 1, 0, 1,0,0,0, "check witness internally") \
43 OPTION( chrono, 1, 0, 2,0,0,1, "chronological backtracking") \
44 OPTION( chronoalways, 0, 0, 1,0,0,1, "force always chronological") \
45 OPTION( chronolevelim, 1e2, 0,2e9,0,0,1, "chronological level limit") \
46 OPTION( chronoreusetrail, 1, 0, 1,0,0,1, "reuse trail chronologically") \
47 OPTION( compact, 1, 0, 1,0,1,1, "compact internal variables") \
48 OPTION( compactint, 2e3, 1,2e9,0,0,1, "compacting interval") \
49 OPTION( compactlim, 1e2, 0,1e3,0,0,1, "inactive limit per mille") \
50 OPTION( compactmin, 1e2, 1,2e9,0,0,1, "minimum inactive limit") \
51 OPTION( condition, 0, 0, 1,0,0,1, "globally blocked clause elim") \
52 OPTION( conditionint, 1e4, 1,2e9,0,0,1, "initial conflict interval") \
53 OPTION( conditionmaxeff, 1e7, 0,2e9,1,0,1, "maximum condition efficiency") \
54 OPTION( conditionmaxrat, 100, 1,2e9,1,0,1, "maximum clause variable ratio") \
55 OPTION( conditionmineff, 1e6, 0,2e9,1,0,1, "minimum condition efficiency") \
56 OPTION( conditionreleff, 100, 1,1e5,0,0,1, "relative efficiency per mille") \
57 OPTION( cover, 0, 0, 1,0,1,1, "covered clause elimination") \
58 OPTION( covermaxclslim, 1e5, 1,2e9,2,0,1, "maximum clause size") \
59 OPTION( covermaxeff, 1e8, 0,2e9,1,0,1, "maximum cover efficiency") \
60 OPTION( coverminclslim, 2, 2,2e9,0,0,1, "minimum clause size") \
61 OPTION( covermineff, 1e6, 0,2e9,1,0,1, "minimum cover efficiency") \
62 OPTION( coverreleff, 4, 1,1e5,1,0,1, "relative efficiency per mille") \
63 OPTION( decompose, 1, 0, 1,0,1,1, "decompose BIG in SCCs and ELS") \
64 OPTION( decomposerounds, 2, 1, 16,1,0,1, "number of decompose rounds") \
65 OPTION( deduplicate, 1, 0, 1,0,1,1, "remove duplicated binaries") \
66 OPTION( eagersubsume, 1, 0, 1,0,0,1, "subsume recently learned") \
67 OPTION( eagersubsumelim, 20, 1,1e3,0,0,1, "limit on subsumed candidates") \
68 OPTION( elim, 1, 0, 1,0,1,1, "bounded variable elimination") \
69 OPTION( elimands, 1, 0, 1,0,0,1, "find AND gates") \
70 OPTION( elimaxeff, 2e9, 0,2e9,1,0,1, "maximum elimination efficiency") \
71 OPTION( elimbackward, 1, 0, 1,0,0,1, "eager backward subsumption") \
72 OPTION( elimboundmax, 16, -1,2e6,1,0,1, "maximum elimination bound") \
73 OPTION( elimboundmin, 0, -1,2e6,0,0,1, "minimum elimination bound") \
74 OPTION( elimclslim, 1e2, 2,2e9,2,0,1, "resolvent size limit") \
75 OPTION( elimequivs, 1, 0, 1,0,0,1, "find equivalence gates") \
76 OPTION( elimineff, 1e7, 0,2e9,1,0,1, "minimum elimination efficiency") \
77 OPTION( elimint, 2e3, 1,2e9,0,0,1, "elimination interval") \
78 OPTION( elimites, 1, 0, 1,0,0,1, "find if-then-else gates") \
79 OPTION( elimlimited, 1, 0, 1,0,0,1, "limit resolutions") \
80 OPTION( elimocclim, 1e2, 0,2e9,2,0,1, "occurrence limit") \
81 OPTION( elimprod, 1, 0,1e4,0,0,1, "elim score product weight") \
82 OPTION( elimreleff, 1e3, 1,1e5,1,0,1, "relative efficiency per mille") \
83 OPTION( elimrounds, 2, 1,512,1,0,1, "usual number of rounds") \
84 OPTION( elimsubst, 1, 0, 1,0,0,1, "elimination by substitution") \
85 OPTION( elimsum, 1, 0,1e4,0,0,1, "elimination score sum weight") \
86 OPTION( elimxorlim, 5, 2, 27,1,0,1, "maximum XOR size") \
87 OPTION( elimxors, 1, 0, 1,0,0,1, "find XOR gates") \
88 OPTION( emagluefast, 33, 1,2e9,0,0,1, "window fast glue") \
89 OPTION( emaglueslow, 1e5, 1,2e9,0,0,1, "window slow glue") \
90 OPTION( emajump, 1e5, 1,2e9,0,0,1, "window back-jump level") \
91 OPTION( emalevel, 1e5, 1,2e9,0,0,1, "window back-track level") \
92 OPTION( emasize, 1e5, 1,2e9,0,0,1, "window learned clause size") \
93 OPTION( ematrailfast, 1e2, 1,2e9,0,0,1, "window fast trail") \
94 OPTION( ematrailslow, 1e5, 1,2e9,0,0,1, "window slow trail") \
95 OPTION( externallrat, 0, 0, 1,0,0,1, "external lrat") \
96 OPTION( flush, 0, 0, 1,0,0,1, "flush redundant clauses") \
97 OPTION( flushfactor, 3, 1,1e3,0,0,1, "interval increase") \
98 OPTION( flushint, 1e5, 1,2e9,0,0,1, "initial limit") \
99 OPTION( forcephase, 0, 0, 1,0,0,1, "always use initial phase") \
100 OPTION( frat, 0, 0, 2,0,0,1, "1=frat(lrat), 2=frat(drat)") \
101 OPTION( idrup, 0, 0, 1,0,0,1, "incremental proof format") \
102 OPTION( ilb, 1, 0, 1,0,0,1, "ILB (incremental lazy backtrack)") \
103 OPTION( ilbassumptions, 1, 0, 1,0,0,1, "trail reuse for assumptions (ILB-like)") \
104 OPTION( inprocessing, 1, 0, 1,0,0,1, "enable inprocessing") \
105 OPTION( instantiate, 0, 0, 1,0,1,1, "variable instantiation") \
106 OPTION( instantiateclslim, 3, 2,2e9,0,0,1, "minimum clause size") \
107 OPTION( instantiateocclim, 1, 1,2e9,2,0,1, "maximum occurrence limit") \
108 OPTION( instantiateonce, 1, 0, 1,0,0,1, "instantiate each clause once") \
109 LOGOPT( log, 0, 0, 1,0,0,0, "enable logging") \
110 LOGOPT( logsort, 0, 0, 1,0,0,0, "sort logged clauses") \
111 OPTION( lrat, 0, 0, 1,0,0,1, "use LRAT proof format") \
112 OPTION( lucky, 1, 0, 1,0,0,1, "search for lucky phases") \
113 OPTION( minimize, 1, 0, 1,0,0,1, "minimize learned clauses") \
114 OPTION( minimizedepth, 1e3, 0,1e3,0,0,1, "minimization depth") \
115 OPTION( otfs, 1, 0, 1,0,0,1, "on-the-fly self subsumption") \
116 OPTION( phase, 1, 0, 1,0,0,1, "initial phase") \
117 OPTION( probe, 1, 0, 1,0,1,1, "failed literal probing" ) \
118 OPTION( probehbr, 1, 0, 1,0,0,1, "learn hyper binary clauses") \
119 OPTION( probeint, 5e3, 1,2e9,0,0,1, "probing interval" ) \
120 OPTION( probemaxeff, 1e8, 0,2e9,1,0,1, "maximum probing efficiency") \
121 OPTION( probemineff, 1e6, 0,2e9,1,0,1, "minimum probing efficiency") \
122 OPTION( probereleff, 20, 1,1e5,1,0,1, "relative efficiency per mille") \
123 OPTION( proberounds, 1, 1, 16,1,0,1, "probing rounds" ) \
124 OPTION( profile, 2, 0, 4,0,0,0, "profiling level") \
125 QUTOPT( quiet, 0, 0, 1,0,0,0, "disable all messages") \
126 OPTION( radixsortlim, 800, 0,2e9,0,0,1, "radix sort limit") \
127 OPTION( realtime, 0, 0, 1,0,0,0, "real instead of process time") \
128 OPTION( reduce, 1, 0, 1,0,0,1, "reduce useless clauses") \
129 OPTION( reduceint, 300, 10,1e6,0,0,1, "reduce interval") \
130 OPTION( reducetarget, 75, 10,1e2,0,0,1, "reduce fraction in percent") \
131 OPTION( reducetier1glue, 2, 1,2e9,0,0,1, "glue of kept learned clauses") \
132 OPTION( reducetier2glue, 6, 1,2e9,0,0,1, "glue of tier two clauses") \
133 OPTION( reluctant, 1024, 0,2e9,0,0,1, "reluctant doubling period") \
134 OPTION( reluctantmax,1048576, 0,2e9,0,0,1, "reluctant doubling period") \
135 OPTION( rephase, 1, 0, 1,0,0,1, "enable resetting phase") \
136 OPTION( rephaseint, 1e3, 1,2e9,0,0,1, "rephase interval") \
137 OPTION( report,reportdefault, 0, 1,0,0,1, "enable reporting") \
138 OPTION( reportall, 0, 0, 1,0,0,1, "report even if not successful") \
139 OPTION( reportsolve, 0, 0, 1,0,0,1, "use solving not process time") \
140 OPTION( restart, 1, 0, 1,0,0,1, "enable restarts") \
141 OPTION( restartint, 2, 1,2e9,0,0,1, "restart interval") \
142 OPTION( restartmargin, 10, 0,1e2,0,0,1, "slow fast margin in percent") \
143 OPTION( restartreusetrail, 1, 0, 1,0,0,1, "enable trail reuse") \
144 OPTION( restoreall, 0, 0, 2,0,0,1, "restore all clauses (2=really)") \
145 OPTION( restoreflush, 0, 0, 1,0,0,1, "remove satisfied clauses") \
146 OPTION( reverse, 0, 0, 1,0,0,1, "reverse variable ordering") \
147 OPTION( score, 1, 0, 1,0,0,1, "use EVSIDS scores") \
148 OPTION( scorefactor, 950,500,1e3,0,0,1, "score factor per mille") \
149 OPTION( seed, 0, 0,2e9,0,0,1, "random seed") \
150 OPTION( shrink, 3, 0, 3,0,0,1, "shrink conflict clause") \
151 OPTION( shrinkreap, 1, 0, 1,0,0,1, "use a reap for shrinking") \
152 OPTION( shuffle, 0, 0, 1,0,0,1, "shuffle variables") \
153 OPTION( shufflequeue, 1, 0, 1,0,0,1, "shuffle variable queue") \
154 OPTION( shufflerandom, 0, 0, 1,0,0,1, "not reverse but random") \
155 OPTION( shufflescores, 1, 0, 1,0,0,1, "shuffle variable scores") \
156 OPTION( stabilize, 1, 0, 1,0,0,1, "enable stabilizing phases") \
157 OPTION( stabilizefactor, 200,101,2e9,0,0,1, "phase increase in percent") \
158 OPTION( stabilizeint, 1e3, 1,2e9,0,0,1, "stabilizing interval") \
159 OPTION( stabilizemaxint, 2e9, 1,2e9,0,0,1, "maximum stabilizing phase") \
160 OPTION( stabilizeonly, 0, 0, 1,0,0,1, "only stabilizing phases") \
161 OPTION( stats, 0, 0, 1,0,0,1, "print all statistics at the end of the run") \
162 OPTION( subsume, 1, 0, 1,0,1,1, "enable clause subsumption") \
163 OPTION( subsumebinlim, 1e4, 0,2e9,1,0,1, "watch list length limit") \
164 OPTION( subsumeclslim, 1e2, 0,2e9,2,0,1, "clause length limit") \
165 OPTION( subsumeint, 1e4, 1,2e9,0,0,1, "subsume interval") \
166 OPTION( subsumelimited, 1, 0, 1,0,0,1, "limit subsumption checks") \
167 OPTION( subsumemaxeff, 1e8, 0,2e9,1,0,1, "maximum subsuming efficiency") \
168 OPTION( subsumemineff, 1e6, 0,2e9,1,0,1, "minimum subsuming efficiency") \
169 OPTION( subsumeocclim, 1e2, 0,2e9,1,0,1, "watch list length limit") \
170 OPTION( subsumereleff, 1e3, 1,1e5,1,0,1, "relative efficiency per mille") \
171 OPTION( subsumestr, 1, 0, 1,0,0,1, "strengthen during subsume") \
172 OPTION( target, 1, 0, 2,0,0,1, "target phases (1=stable only)") \
173 OPTION( terminateint, 10, 0,1e4,0,0,1, "termination check interval") \
174 OPTION( ternary, 1, 0, 1,0,1,1, "hyper ternary resolution") \
175 OPTION( ternarymaxadd, 1e3, 0,1e4,1,0,1, "max clauses added in percent") \
176 OPTION( ternarymaxeff, 1e8, 0,2e9,1,0,1, "ternary maximum efficiency") \
177 OPTION( ternarymineff, 1e6, 1,2e9,1,0,1, "minimum ternary efficiency") \
178 OPTION( ternaryocclim, 1e2, 1,2e9,2,0,1, "ternary occurrence limit") \
179 OPTION( ternaryreleff, 10, 1,1e5,1,0,1, "relative efficiency per mille") \
180 OPTION( ternaryrounds, 2, 1, 16,1,0,1, "maximum ternary rounds") \
181 OPTION( transred, 1, 0, 1,0,1,1, "transitive reduction of BIG") \
182 OPTION( transredmaxeff, 1e8, 0,2e9,1,0,1, "maximum efficiency") \
183 OPTION( transredmineff, 1e6, 0,2e9,1,0,1, "minimum efficiency") \
184 OPTION( transredreleff, 1e2, 1,1e5,1,0,1, "relative efficiency per mille") \
185 QUTOPT( verbose, 0, 0, 3,0,0,0, "more verbose messages") \
186 OPTION( veripb, 0, 0, 4,0,0,1, "odd=checkdeletions, > 2=drat") \
187 OPTION( vivify, 1, 0, 1,0,1,1, "vivification") \
188 OPTION( vivifyinst, 1, 0, 1,0,0,1, "instantiate last literal when vivify") \
189 OPTION( vivifymaxeff, 2e7, 0,2e9,1,0,1, "maximum efficiency") \
190 OPTION( vivifymineff, 2e4, 0,2e9,1,0,1, "minimum efficiency") \
191 OPTION( vivifyonce, 0, 0, 2,0,0,1, "vivify once: 1=red, 2=red+irr") \
192 OPTION( vivifyredeff, 75, 0,1e3,1,0,1, "redundant efficiency per mille") \
193 OPTION( vivifyreleff, 20, 1,1e5,1,0,1, "relative efficiency per mille") \
194 OPTION( walk, 1, 0, 1,0,0,1, "enable random walks") \
195 OPTION( walkmaxeff, 1e7, 0,2e9,1,0,1, "maximum efficiency") \
196 OPTION( walkmineff, 1e5, 0,1e7,1,0,1, "minimum efficiency") \
197 OPTION( walknonstable, 1, 0, 1,0,0,1, "walk in non-stabilizing phase") \
198 OPTION( walkredundant, 0, 0, 1,0,0,1, "walk redundant clauses too") \
199 OPTION( walkreleff, 20, 1,1e5,1,0,1, "relative efficiency per mille") \
200
201 // Note, keep an empty line right before this line because of the last '\'!
202 // Also keep those single spaces after 'OPTION(' for proper sorting.
203
204 // clang-format on
205
206 /*------------------------------------------------------------------------*/
207
208 // Some of the 'OPTION' macros above should only be included if certain
209 // compile time options are enabled. This has the effect, that for instance
210 // if 'LOGGING' is defined, and thus logging code is included, then also the
211 // 'log' option is defined. Otherwise the 'log' option is not included.
212
213 #ifdef LOGGING
214 #define LOGOPT OPTION
215 #else
216 #define LOGOPT(...) /**/
217 #endif
218
219 #ifdef QUIET
220 #define QUTOPT(...) /**/
221 #else
222 #define QUTOPT OPTION
223 #endif
224
225 /*------------------------------------------------------------------------*/
226
227 namespace CaDiCaL {
228
229 struct Internal;
230
231 /*------------------------------------------------------------------------*/
232
233 class Options;
234
235 struct Option {
236 const char *name;
237 int def, lo, hi;
238 int optimizable;
239 bool preprocessing;
240 const char *description;
241 int &val (Options *);
242 };
243
244 /*------------------------------------------------------------------------*/
245
246 // Produce a compile time constant for the number of options.
247
248 static const size_t number_of_options =
249 #define OPTION(N, V, L, H, O, P, R, D) 1 +
250 OPTIONS
251 #undef OPTION
252 + 0;
253
254 /*------------------------------------------------------------------------*/
255
256 class Options {
257
258 Internal *internal;
259
260 void set (Option *, int val); // Force to [lo,hi] interval.
261
262 friend struct Option;
263 static Option table[];
264
265 static void initialize_from_environment (int &val, const char *name,
266 const int L, const int H);
267
268 friend Config;
269
270 void reset_default_values ();
271 void disable_preprocessing ();
272
273 public:
274 // For library usage we disable reporting by default while for the stand
275 // alone SAT solver we enable it by default. This default value has to
276 // be set before the constructor of 'Options' is called (which in turn is
277 // called from the constructor of 'Solver'). If we would simply overwrite
278 // its initial value while initializing the stand alone solver, we will
279 // get that change of the default value (from 'false' to 'true') shown
280 // during calls to 'print ()', which is confusing to the user.
281 //
282 static int reportdefault;
283
284 Options (Internal *);
285
286 // Makes options directly accessible, e.g., for instance declares the
287 // member 'int restart' here. This will give fast access to option values
288 // internally in the solver and thus can also be used in tight loops.
289 //
290 private:
291 int __start_of_options__; // Used by 'val' below.
292 public:
293 #define OPTION(N, V, L, H, O, P, R, D) \
294 int N; // Access option values by name.
295 OPTIONS
296 #undef OPTION
297
298 // It would be more elegant to use an anonymous 'struct' of the actual
299 // option values overlayed with an 'int values[number_of_options]' array
300 // but that is not proper ISO C++ and produces a warning. Instead we use
301 // the following construction which relies on '__start_of_options__' and
302 // that the following options are really allocated directly after it.
303 //
304 inline int &val (size_t idx) {
305 assert (idx < number_of_options);
306 return (&__start_of_options__ + 1)[idx];
307 }
308
309 // With the following function we can get rather fast access to the option
310 // limits, the default value and the description. The code uses binary
311 // search over the sorted option 'table'. This static data is shared
312 // among different instances of the solver. The actual current option
313 // values are here in the 'Options' class. They can be accessed by the
314 // offset of the static options using 'Option::val' if you have an
315 // 'Option' or to have even faster access directly by the member function
316 // (the 'N' above, e.g., 'restart').
317 //
318 static Option *has (const char *name);
319
320 bool set (const char *name, int); // Explicit version.
321 int get (const char *name); // Get current value.
322
323 void print (); // Print current values in command line form
324 static void usage (); // Print usage message for all options.
325
326 void optimize (int val); // increase some limits (val=0..31)
327
328 static bool is_preprocessing_option (const char *name);
329
330 // Parse long option argument
331 //
332 // --<name>
333 // --<name>=<val>
334 // --no-<name>
335 //
336 // where '<val>' is as in 'parse_option_value'. If parsing succeeds,
337 // 'true' is returned and the string will be set to the name of the
338 // option. Additionally the parsed value is set (last argument).
339 //
340 static bool parse_long_option (const char *, string &, int &);
341
342 // Iterating options.
343
344 typedef Option *iterator;
345 typedef const Option *const_iterator;
346
347 static iterator begin () { return table; }
348 static iterator end () { return table + number_of_options; }
349
350 void copy (Options &other) const; // Copy 'this' into 'other'.
351 };
352
353 inline int &Option::val (Options *opts) {
354 assert (Options::table <= this &&
355 this < Options::table + number_of_options);
356 return opts->val (this - Options::table);
357 }
358
359 } // namespace CaDiCaL
360
361 #endif
options.hpp
|
|
1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
5 /*------------------------------------------------------------------------*/
6
7 // By default, e.g., for library usage, the 'opts.report' value is zero
8 // ('false') but can be set to '1' by the stand alone solver. Using here
9 // a static default value avoids that the stand alone solver reports that
10 // '--report=1' is different from the default in 'print ()' below.
11 //
12 int Options::reportdefault;
13
14 /*------------------------------------------------------------------------*/
15
16 // The order of initializations of static objects is undefined and thus we
17 // can not assume that this table is already initialized if a solver and
18 // thus the constructor of 'Options' is called. Therefore we just have to
19 // reinitialize this table in every call to 'Options::Options'. This does
20 // not produce a data race even for parallel initialization since the
21 // same values are written by all threads under the assumption that the
22 // 'reportdefault' is set before any solver is initialized. We do have to
23 // perform this static initialization though, since 'has' is static and does
24 // not require that the 'Options' constructor was called.
25
26 Option Options::table[] = {
27 #define OPTION(N, V, L, H, O, P, R, D) \
28 {#N, (int) V, (int) L, (int) H, (int) O, (bool) P, D},
29 OPTIONS
30 #undef OPTION
31 };
32
33 /*------------------------------------------------------------------------*/
34
35 // Binary search in 'table', which requires option names to be sorted, which
36 // in turned is checked at start-up in 'Options::Options'.
37
38 Option *Options::has (const char *name) {
39 size_t l = 0, r = number_of_options;
40 while (l < r) {
41 size_t m = l + (r - l) / 2;
42 Option *res = &table[m];
43 int tmp = strcmp (name, res->name);
44 if (!tmp)
45 return res;
46 if (tmp < 0)
47 r = m;
48 if (tmp > 0)
49 l = m + 1;
50 }
51 return 0;
52 }
53
54 /*------------------------------------------------------------------------*/
55
56 bool Options::parse_long_option (const char *arg, string &name, int &val) {
57 if (arg[0] != '-' || arg[1] != '-')
58 return false;
59 const bool has_no_prefix =
60 (arg[2] == 'n' && arg[3] == 'o' && arg[4] == '-');
61 const size_t offset = has_no_prefix ? 5 : 2;
62 name = arg + offset;
63 const size_t pos = name.find_first_of ('=');
64 if (pos != string::npos)
65 name[pos] = 0;
66 if (!Options::has (name.c_str ()))
67 return false;
68 if (pos == string::npos)
69 val = !has_no_prefix;
70 else {
71 const char *val_str = name.c_str () + pos + 1;
72 if (!parse_int_str (val_str, val))
73 return false;
74 }
75 return true;
76 }
77
78 /*------------------------------------------------------------------------*/
79
80 void Options::initialize_from_environment (int &val, const char *name,
81 const int L, const int H) {
82 char key[80], *q;
83 const char *p;
84 assert (strlen (name) + strlen ("CADICAL_") + 1 < sizeof (key));
85 for (p = "CADICAL_", q = key; *p; p++)
86 *q++ = *p;
87 for (p = name; *p; p++)
88 *q++ = toupper (*p);
89 assert (q < key + sizeof (key));
90 *q = 0;
91 const char *val_str = getenv (key);
92 if (!val_str)
93 return;
94 if (!parse_int_str (val_str, val))
95 return;
96 if (val < L)
97 val = L;
98 if (val > H)
99 val = H;
100 }
101
102 // Initialize all the options to their default value 'V'.
103
104 Options::Options (Internal *s) : internal (s) {
105 assert (number_of_options == sizeof Options::table / sizeof (Option));
106
107 // First initialize them according to defaults in 'options.hpp'.
108 //
109 const char *prev = "";
110 size_t i = 0;
111 #define OPTION(N, V, L, H, O, P, R, D) \
112 do { \
113 if ((L) > (V)) \
114 FATAL ("'" #N "' default '" #V "' " \
115 "lower minimum '" #L "' in 'options.hpp'"); \
116 if ((H) < (V)) \
117 FATAL ("'" #N "' default '" #V "' " \
118 "larger maximum '" #H "' in 'options.hpp'"); \
119 if (strcmp (prev, #N) > 0) \
120 FATAL ("'%s' ordered before '" #N "' in 'options.hpp'", prev); \
121 N = (int) (V); \
122 assert (&val (i) == &N); \
123 /* The order of initializing static data is undefined and thus */ \
124 /* it might be the case that the 'table' is not initialized yet. */ \
125 /* Thus this construction just reinitializes the table too even */ \
126 /* though it might not be necessary. */ \
127 assert (!table[i].name || !strcmp (table[i].name, #N)); \
128 table[i] = {#N, (int) (V), (int) (L), (int) (H), \
129 (int) (O), (bool) (P), D}; \
130 prev = #N; \
131 i++; \
132 } while (0);
133 OPTIONS
134 #undef OPTION
135
136 // Check consistency in debugging mode.
137 //
138 #ifndef NDEBUG
139 assert (i == number_of_options);
140 assert (!has ("aaaaa"));
141 assert (!has ("non-existing-option"));
142 assert (!has ("zzzzz"));
143 #endif
144
145 // Now overwrite default options with environment values.
146 //
147 #define OPTION(N, V, L, H, O, P, R, D) \
148 initialize_from_environment (N, #N, L, H);
149 OPTIONS
150 #undef OPTION
151 }
152
153 /*------------------------------------------------------------------------*/
154
155 void Options::set (Option *o, int new_val) {
156 assert (o);
157 int &val = o->val (this), old_val = val;
158 if (old_val == new_val) {
159 LOG ("keeping value '%d' of option '%s'", old_val, o->name);
160 return;
161 }
162 if (new_val < o->lo) {
163 LOG ("bounding '%d' to lower limit '%d' for option '%s'", new_val,
164 o->lo, o->name);
165 new_val = o->lo;
166 }
167 if (new_val > o->hi) {
168 LOG ("bounding '%d' to upper limit '%d' for option '%s'", new_val,
169 o->hi, o->name);
170 new_val = o->hi;
171 }
172 val = new_val;
173 LOG ("set option 'set (\"%s\", %d)' from '%d'", o->name, new_val,
174 old_val);
175 }
176
177 // Explicit option value setting.
178
179 bool Options::set (const char *name, int val) {
180 Option *o = has (name);
181 if (!o)
182 return false;
183 set (o, val);
184 return true;
185 }
186
187 int Options::get (const char *name) {
188 Option *o = has (name);
189 return o ? o->val (this) : 0;
190 }
191
192 /*------------------------------------------------------------------------*/
193
194 void Options::print () {
195 unsigned different = 0;
196 #ifdef QUIET
197 const bool verbose = false;
198 #endif
199 char buffer[256];
200 // We prefer the macro iteration here since '[VLH]' might be '1e9' etc.
201 #define OPTION(N, V, L, H, O, P, R, D) \
202 if (N != (V)) \
203 different++; \
204 if (verbose || N != (V)) { \
205 if ((L) == 0 && (H) == 1) { \
206 snprintf (buffer, sizeof buffer, "--" #N "=%s", \
207 (N ? "true" : "false")); \
208 MSG (" %s%-30s%s (%s default %s'%s'%s)", \
209 ((N == (V)) ? "" : tout.bright_yellow_code ()), buffer, \
210 ((N == (V)) ? "" : tout.normal_code ()), \
211 ((N == (V)) ? "same as" : "different from"), \
212 ((N == (V)) ? tout.green_code () : tout.yellow_code ()), \
213 (bool) (V) ? "true" : "false", tout.normal_code ()); \
214 } else { \
215 snprintf (buffer, sizeof buffer, "--" #N "=%d", N); \
216 MSG (" %s%-30s%s (%s default %s'" #V "'%s)", \
217 ((N == (V)) ? "" : tout.bright_yellow_code ()), buffer, \
218 ((N == (V)) ? "" : tout.normal_code ()), \
219 ((N == (V)) ? "same as" : "different from"), \
220 ((N == (V)) ? tout.green_code () : tout.yellow_code ()), \
221 tout.normal_code ()); \
222 } \
223 }
224 OPTIONS
225 #undef OPTION
226 if (!different)
227 MSG ("all options are set to their default value");
228 }
229
230 /*------------------------------------------------------------------------*/
231
232 void Options::usage () {
233 // We prefer the macro iteration here since '[VLH]' might be '1e9' etc.
234 #define OPTION(N, V, L, H, O, P, R, D) \
235 if ((L) == 0 && (H) == 1) \
236 printf (" %-26s " D " [%s]\n", "--" #N "=bool", \
237 (bool) (V) ? "true" : "false"); \
238 else \
239 printf (" %-26s " D " [" #V "]\n", "--" #N "=" #L ".." #H);
240 OPTIONS
241 #undef OPTION
242 }
243
244 /*------------------------------------------------------------------------*/
245
246 void Options::optimize (int val) {
247
248 if (val < 0) {
249 LOG ("ignoring negative optimization mode '%d'", val);
250 return;
251 }
252
253 const int max_val = 31;
254 if (val > max_val) {
255 LOG ("optimization argument '%d' reduced to '%d'", val, max_val);
256 val = max_val;
257 }
258
259 int64_t factor2 = 1;
260 for (int i = 0; i < val && factor2 <= INT_MAX; i++)
261 factor2 *= 2;
262
263 int64_t factor10 = 1;
264 for (int i = 0; i < val && factor10 <= INT_MAX; i++)
265 factor10 *= 10;
266
267 unsigned increased = 0;
268 #define OPTION(N, V, L, H, O, P, R, D) \
269 do { \
270 if (!(O)) \
271 break; \
272 const int64_t factor = ((O) == 1 ? factor2 : factor10); \
273 int64_t new_val = factor * (int64_t) (V); \
274 if (new_val > (H)) \
275 new_val = (H); \
276 if (new_val == (int) (V)) \
277 break; \
278 LOG ("optimization mode '%d' for '%s' " \
279 "gives '%" PRId64 "' instead of '%d", \
280 val, #N, new_val, (int) (V)); \
281 assert (new_val <= INT_MAX); \
282 N = (int) new_val; \
283 increased++; \
284 } while (0);
285 OPTIONS
286 #undef OPTION
287 if (increased)
288 MSG ("optimization mode '-O%d' increased %u limits", val, increased);
289 }
290
291 /*------------------------------------------------------------------------*/
292
293 void Options::disable_preprocessing () {
294 size_t count = 0;
295 #define OPTION(N, V, L, H, O, P, R, D) \
296 do { \
297 if (!(P)) \
298 break; \
299 if (!(N)) \
300 break; \
301 assert ((L) == 0); \
302 assert ((H) == 1); \
303 LOG ("plain mode disables '%s'", #N); \
304 count++; \
305 N = 0; \
306 } while (0);
307 OPTIONS
308 #undef OPTION
309 LOG ("forced plain mode disabled %zd preprocessing options", count);
310 #ifndef LOGGING
311 (void) count;
312 #endif
313 }
314
315 bool Options::is_preprocessing_option (const char *name) {
316 Option *o = has (name);
317 return o ? o->preprocessing : false;
318 }
319
320 /*------------------------------------------------------------------------*/
321
322 void Options::reset_default_values () {
323 size_t count = 0;
324 #define OPTION(N, V, L, H, O, P, R, D) \
325 do { \
326 if (!(R)) \
327 break; \
328 if (N == (V)) \
329 break; \
330 LOG ("resetting option '%s' to default %s", #N, #V); \
331 count++; \
332 N = (int) (V); \
333 } while (0);
334 OPTIONS
335 #undef OPTION
336 LOG ("reset %zd options to their default values", count);
337 #ifndef LOGGING
338 (void) count;
339 #endif
340 }
341
342 /*------------------------------------------------------------------------*/
343
344 void Options::copy (Options &other) const {
345 #ifdef LOGGING
346 Internal *internal = other.internal;
347 #endif
348 #define OPTION(N, V, L, H, O, P, R, D) \
349 if ((N) == (int) (V)) \
350 LOG ("keeping non default option '--%s=%s'", #N, #V); \
351 else if ((N) != (int) (V)) { \
352 LOG ("overwriting default option by '--%s=%d'", #N, N); \
353 other.N = N; \
354 }
355 OPTIONS
356 #undef OPTION
357 }
358
359 } // namespace CaDiCaL
options.cpp
|
在各个模块中被使用。
|
1. 重启采用reuse trail —— opts.restartreusetrail设置为真。 在restart.cpp中被使用。 //restart.cpp
int Internal::reuse_trail () {
const int trivial_decisions =
assumptions.size ()
// Plus 1 if the constraint is satisfied via implications of
// assumptions and a pseudo-decision level was introduced
+ !control[assumptions.size () + 1].decision;
if (!opts.restartreusetrail)
return trivial_decisions;
int decision = next_decision_variable ();
assert (1 <= decision);
int res = trivial_decisions;
if (use_scores ()) {
while (
res < level && control[res + 1].decision &&
score_smaller (this) (decision, abs (control[res + 1].decision))) {
assert (control[res + 1].decision);
res++;
}
} else {
int64_t limit = bumped (decision);
while (res < level && control[res + 1].decision &&
bumped (control[res + 1].decision) > limit) {
assert (control[res + 1].decision);
res++;
}
}
int reused = res - trivial_decisions;
if (reused > 0) {
stats.reused++;
stats.reusedlevels += reused;
if (stable)
stats.reusedstable++;
}
return res;
}
|
|
|
2. 重启后设置下次冲突次数界限，用以触发下一次重启 —— opts.restartint 为restart interval。 1 void Internal::restart () {
2 START (restart);
3 stats.restarts++;
4 stats.restartlevels += level;
5 if (stable)
6 stats.restartstable++;
7 LOG ("restart %" PRId64 "", stats.restarts);
8 backtrack (reuse_trail ());
9
10 lim.restart = stats.conflicts + opts.restartint;
11 LOG ("new restart limit at %" PRId64 " conflicts", lim.restart);
12
13 report ('R', 2);
14 STOP (restart);
15 }
|
|
标签：2e9,OPTION,val,int,Options,数据结构,cadical,options,运行 From： https://www.cnblogs.com/yuweng1689/p/18224706