1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * THE SEARCH PARAMETERS/OPTIONS USED BY THE SOLVER
21 */
22
23 #include <float.h>
24 #include <assert.h>
25
26 #include "api/search_parameters.h"
27 #include "solvers/funs/fun_solver.h"
28 #include "solvers/simplex/simplex.h"
29 #include "utils/string_utils.h"
30
31
32
33 /*******************************
34 * DEFAULT SEARCH PARAMETERS *
35 ******************************/
36
37 /*
38 * Default restart parameters for SMT solving
39 * Minisat-like behavior
40 */
41 #define DEFAULT_FAST_RESTART false
42 #define DEFAULT_C_THRESHOLD 100
43 #define DEFAULT_D_THRESHOLD 100
44 #define DEFAULT_C_FACTOR 1.5
45 #define DEFAULT_D_FACTOR 1.5
46
47 /*
48 * Restart parameters if option --fast-restarts is set
49 */
50 #define FAST_RESTART_C_THRESHOLD 100
51 #define FAST_RESTART_D_THRESHOLD 100
52 #define FAST_RESTART_C_FACTOR 1.1
53 #define FAST_RESTART_D_FACTOR 1.1
54
55 /*
56 * Default clause deletion parameters
57 */
58 #define DEFAULT_R_THRESHOLD 1000
59 #define DEFAULT_R_FRACTION 0.25
60 #define DEFAULT_R_FACTOR 1.05
61
62
63 /*
64 * The default SMT parameters are copied from smt_core.h
65 * - VAR_DECAY_FACTOR = 0.95
66 * - VAR_RANDOM_FACTOR = 0.02
67 * - CLAUSE_DECAY_FACTOR = 0.999
68 * - clause caching is disabled
69 */
70 #define DEFAULT_VAR_DECAY VAR_DECAY_FACTOR
71 #define DEFAULT_RANDOMNESS VAR_RANDOM_FACTOR
72 #define DEFAULT_CLAUSE_DECAY CLAUSE_DECAY_FACTOR
73 #define DEFAULT_CACHE_TCLAUSES false
74 #define DEFAULT_TCLAUSE_SIZE 0
75
76
77 /*
78 * Default random seed as in smt_core.d
79 */
80 #define DEFAULT_RANDOM_SEED 0xabcdef98
81
82 /*
83 * Default branching = the smt_core default
84 */
85 #define DEFAULT_BRANCHING BRANCHING_DEFAULT
86
87 /*
88 * The default EGRAPH parameters are defined in egraph_types.h
89 * - DEFAULT_MAX_ACKERMANN = 1000
90 * - DEFAULT_MAX_BOOLACKERMANN = 600000
91 * - DEFAULT_AUX_EQ_QUOTA = 100
92 * - DEFAULT_ACKERMANN_THRESHOLD = 8
93 * - DEFAULT_BOOLACK_THRESHOLD = 8
94 * - DEFAULT_MAX_INTERFACE_EQS = 200
95 *
96 * The dynamic ackermann heuristic is disabled for both
97 * boolean and non-boolean terms.
98 */
99 #define DEFAULT_USE_DYN_ACK false
100 #define DEFAULT_USE_BOOL_DYN_ACK false
101 #define DEFAULT_USE_OPTIMISTIC_FCHECK true
102 #define DEFAULT_AUX_EQ_RATIO 0.3
103
104
105 /*
106 * Default SIMPLEX parameters defined in simplex_types.h
107 * - SIMPLEX_DEFAULT_BLAND_THRESHOLD = 1000
108 * - SIMPLEX_DEFAULT_PROP_ROW_SIZE = 30
109 * - SIMPLEX_DEFAULT_CHECK_PERIOD = infinity
110 * - propagation is disabled by default
111 * - model adjustment is also disabled
112 * - integer check is disabled too
113 */
114 #define DEFAULT_SIMPLEX_PROP_FLAG false
115 #define DEFAULT_SIMPLEX_ADJUST_FLAG false
116 #define DEFAULT_SIMPLEX_ICHECK_FLAG false
117
118 /*
119 * Default parameters for the array solver (defined in fun_solver.h
120 * - MAX_UPDATE_CONFLICTS = 20
121 * - MAX_EXTENSIONALITY = 1
122 */
123
124
125 /*
126 * All default parameters
127 */
128 static const param_t default_settings = {
129 DEFAULT_FAST_RESTART,
130 DEFAULT_C_THRESHOLD,
131 DEFAULT_D_THRESHOLD,
132 DEFAULT_C_FACTOR,
133 DEFAULT_D_FACTOR,
134
135 DEFAULT_R_THRESHOLD,
136 DEFAULT_R_FRACTION,
137 DEFAULT_R_FACTOR,
138
139 DEFAULT_VAR_DECAY,
140 DEFAULT_RANDOMNESS,
141 DEFAULT_RANDOM_SEED,
142 DEFAULT_BRANCHING,
143 DEFAULT_CLAUSE_DECAY,
144 DEFAULT_CACHE_TCLAUSES,
145 DEFAULT_TCLAUSE_SIZE,
146
147 DEFAULT_USE_DYN_ACK,
148 DEFAULT_USE_BOOL_DYN_ACK,
149 DEFAULT_USE_OPTIMISTIC_FCHECK,
150 DEFAULT_MAX_ACKERMANN,
151 DEFAULT_MAX_BOOLACKERMANN,
152 DEFAULT_AUX_EQ_QUOTA,
153 DEFAULT_AUX_EQ_RATIO,
154 DEFAULT_ACKERMANN_THRESHOLD,
155 DEFAULT_BOOLACK_THRESHOLD,
156 DEFAULT_MAX_INTERFACE_EQS,
157
158 DEFAULT_SIMPLEX_PROP_FLAG,
159 DEFAULT_SIMPLEX_ADJUST_FLAG,
160 DEFAULT_SIMPLEX_ICHECK_FLAG,
161 SIMPLEX_DEFAULT_PROP_ROW_SIZE,
162 SIMPLEX_DEFAULT_BLAND_THRESHOLD,
163 SIMPLEX_DEFAULT_CHECK_PERIOD,
164
165 DEFAULT_MAX_UPDATE_CONFLICTS,
166 DEFAULT_MAX_EXTENSIONALITY,
167 };
168
169
170
171 /*************************************
172 * GLOBAL TABLES: PARAMETER NAMES *
173 ************************************/
174
175 /*
176 * Search parameters and options can be set individually.
177 *
178 * We use an integer code to identify the parameters + a table of
179 * parameter names in lexicographic order. Each parameter
180 * is described in context.h
181 */
182 typedef enum param_key {
183 // restart parameters
184 PARAM_FAST_RESTART,
185 PARAM_C_THRESHOLD,
186 PARAM_D_THRESHOLD,
187 PARAM_C_FACTOR,
188 PARAM_D_FACTOR,
189 // clause deletion heuristic
190 PARAM_R_THRESHOLD,
191 PARAM_R_FRACTION,
192 PARAM_R_FACTOR,
193 // branching heuristic
194 PARAM_VAR_DECAY,
195 PARAM_RANDOMNESS,
196 PARAM_RANDOM_SEED,
197 PARAM_BRANCHING,
198 // learned clauses
199 PARAM_CLAUSE_DECAY,
200 PARAM_CACHE_TCLAUSES,
201 PARAM_TCLAUSE_SIZE,
202 // egraph parameters
203 PARAM_DYN_ACK,
204 PARAM_DYN_BOOL_ACK,
205 PARAM_OPTIMISTIC_FCHECK,
206 PARAM_MAX_ACK,
207 PARAM_MAX_BOOL_ACK,
208 PARAM_AUX_EQ_QUOTA,
209 PARAM_AUX_EQ_RATIO,
210 PARAM_DYN_ACK_THRESHOLD,
211 PARAM_DYN_BOOL_ACK_THRESHOLD,
212 PARAM_MAX_INTERFACE_EQS,
213 // simplex parameters
214 PARAM_SIMPLEX_PROP,
215 PARAM_SIMPLEX_ADJUST,
216 PARAM_SIMPLEX_ICHECK,
217 PARAM_PROP_THRESHOLD,
218 PARAM_BLAND_THRESHOLD,
219 PARAM_ICHECK_PERIOD,
220 // array solver
221 PARAM_MAX_UPDATE_CONFLICTS,
222 PARAM_MAX_EXTENSIONALITY,
223 } param_key_t;
224
225 #define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+1)
226
227 // parameter names in lexicographic ordering
228 static const char *const param_key_names[NUM_PARAM_KEYS] = {
229 "aux-eq-quota",
230 "aux-eq-ratio",
231 "bland-threshold",
232 "branching",
233 "c-factor",
234 "c-threshold",
235 "cache-tclauses",
236 "clause-decay",
237 "d-factor",
238 "d-threshold",
239 "dyn-ack",
240 "dyn-ack-threshold",
241 "dyn-bool-ack",
242 "dyn-bool-ack-threshold",
243 "fast-restarts",
244 "icheck",
245 "icheck-period",
246 "max-ack",
247 "max-bool-ack",
248 "max-extensionality",
249 "max-interface-eqs",
250 "max-update-conflicts",
251 "optimistic-final-check",
252 "prop-threshold",
253 "r-factor",
254 "r-fraction",
255 "r-threshold",
256 "random-seed",
257 "randomness",
258 "simplex-adjust",
259 "simplex-prop",
260 "tclause-size",
261 "var-decay",
262 };
263
264 // corresponding parameter codes in order
265 static const int32_t param_code[NUM_PARAM_KEYS] = {
266 PARAM_AUX_EQ_QUOTA,
267 PARAM_AUX_EQ_RATIO,
268 PARAM_BLAND_THRESHOLD,
269 PARAM_BRANCHING,
270 PARAM_C_FACTOR,
271 PARAM_C_THRESHOLD,
272 PARAM_CACHE_TCLAUSES,
273 PARAM_CLAUSE_DECAY,
274 PARAM_D_FACTOR,
275 PARAM_D_THRESHOLD,
276 PARAM_DYN_ACK,
277 PARAM_DYN_ACK_THRESHOLD,
278 PARAM_DYN_BOOL_ACK,
279 PARAM_DYN_BOOL_ACK_THRESHOLD,
280 PARAM_FAST_RESTART,
281 PARAM_SIMPLEX_ICHECK,
282 PARAM_ICHECK_PERIOD,
283 PARAM_MAX_ACK,
284 PARAM_MAX_BOOL_ACK,
285 PARAM_MAX_EXTENSIONALITY,
286 PARAM_MAX_INTERFACE_EQS,
287 PARAM_MAX_UPDATE_CONFLICTS,
288 PARAM_OPTIMISTIC_FCHECK,
289 PARAM_PROP_THRESHOLD,
290 PARAM_R_FACTOR,
291 PARAM_R_FRACTION,
292 PARAM_R_THRESHOLD,
293 PARAM_RANDOM_SEED,
294 PARAM_RANDOMNESS,
295 PARAM_SIMPLEX_ADJUST,
296 PARAM_SIMPLEX_PROP,
297 PARAM_TCLAUSE_SIZE,
298 PARAM_VAR_DECAY,
299 };
300
301
302
303 /*
304 * Names of each branching mode (in lexicographic order)
305 */
306 static const char * const branching_modes[NUM_BRANCHING_MODES] = {
307 "default",
308 "negative",
309 "positive",
310 "th-neg",
311 "th-pos",
312 "theory",
313 };
314
315 static const int32_t branching_code[NUM_BRANCHING_MODES] = {
316 BRANCHING_DEFAULT,
317 BRANCHING_NEGATIVE,
318 BRANCHING_POSITIVE,
319 BRANCHING_TH_NEG,
320 BRANCHING_TH_POS,
321 BRANCHING_THEORY,
322 };
323
324
325
326
327 /****************
328 * FUNCTIONS *
329 ***************/
330
331 /*
332 * Initialize params with a copy of default_settings
333 */
init_params_to_defaults(param_t * parameters)334 void init_params_to_defaults(param_t *parameters) {
335 *parameters = default_settings;
336 }
337
338
339 /*
340 * Return the default parameters
341 */
get_default_params(void)342 const param_t *get_default_params(void) {
343 return &default_settings;
344 }
345
346
347 /*
348 * Parse value as a boolean. Store the result in *v
349 * - return 0 if this works
350 * - return -2 otherwise
351 */
set_bool_param(const char * value,bool * v)352 static int32_t set_bool_param(const char *value, bool *v) {
353 int32_t k;
354
355 k = parse_as_boolean(value, v);
356 return (k == valid_boolean) ? 0 : -2;
357 }
358
359
360 /*
361 * Parse value as a branching mode. Store the result in *v
362 * - return 0 if this works
363 * - return -2 otherwise
364 */
set_branching_param(const char * value,branch_t * v)365 static int32_t set_branching_param(const char *value, branch_t *v) {
366 int32_t k;
367
368 k = parse_as_keyword(value, branching_modes, branching_code, NUM_BRANCHING_MODES);
369 assert(k >= 0 || k == -1);
370
371 if (k >= 0) {
372 assert(BRANCHING_DEFAULT <= k && k <= BRANCHING_TH_POS);
373 *v = (branch_t) k;
374 k = 0;
375 } else {
376 k = -2;
377 }
378
379 return k;
380 }
381
382
383 /*
384 * Parse val as a signed 32bit integer. Check whether
385 * the result is in the interval [low, high].
386 * - if so, store the result into *v and return 0
387 * - if val is not an integer, return -2
388 * - if the result is not in the interval, return -2
389 */
set_int32_param(const char * value,int32_t * v,int32_t low,int32_t high)390 static int32_t set_int32_param(const char *value, int32_t *v, int32_t low, int32_t high) {
391 integer_parse_code_t k;
392 int32_t aux;
393
394 k = parse_as_integer(value, &aux);
395 switch (k) {
396 case valid_integer:
397 if (low <= aux && aux <= high) {
398 *v = aux;
399 aux = 0;
400 } else {
401 aux = -2;
402 }
403 break;
404
405 case integer_overflow:
406 case invalid_integer:
407 default: // prevent GCC warning
408 aux = -2;
409 break;
410 }
411
412 return aux;
413 }
414
415
416 /*
417 * Parse value as an unsigned integer
418 * - no interval check
419 * - if val is not an unsigned integer, return -2
420 */
set_uint32_param(const char * value,uint32_t * v)421 static int32_t set_uint32_param(const char *value, uint32_t *v) {
422 integer_parse_code_t k;
423 int32_t code;
424
425 k = parse_as_uint(value, v);
426 switch (k) {
427 case valid_integer:
428 code = 0;
429 break;
430
431 case integer_overflow:
432 case invalid_integer:
433 default:
434 code = -2;
435 break;
436 }
437
438 return code;
439 }
440
441
442
443 /*
444 * Parse value as a double. Check whether
445 * the result is in the interval [low, high].
446 * - if so, store the result into *v and return 0
447 * - if the string can't be parse as a double, return -1
448 * - if the result is not in the interval, return -2
449 */
set_double_param(const char * value,double * v,double low,double high)450 static int32_t set_double_param(const char *value, double *v, double low, double high) {
451 double_parse_code_t k;
452 double aux;
453 int32_t result;
454
455 k = parse_as_double(value, &aux);
456 switch (k) {
457 case valid_double:
458 if (low <= aux && aux <= high) {
459 *v = aux;
460 result = 0;
461 } else {
462 result = -2;
463 }
464 break;
465
466 case double_overflow:
467 case invalid_double:
468 default: // prevent GCC warning
469 result = -1;
470 break;
471 }
472
473 return result;
474 }
475
476
477
478
479 /*
480 * Set a field in the parameter record.
481 * - key = field name
482 * - value = value for that field
483 *
484 * Return code:
485 * -1 if the key is not recognized
486 * -2 if the value is not recognized
487 * -3 if the value has the wrong type for the key
488 * 0 otherwise (i.e., success)
489 */
params_set_field(param_t * parameters,const char * key,const char * value)490 int32_t params_set_field(param_t *parameters, const char *key, const char *value) {
491 int32_t k, r;
492 int32_t z;
493 double x;
494
495 z = 0; // to prevent GCC warning
496
497 k = parse_as_keyword(key, param_key_names, param_code, NUM_PARAM_KEYS);
498 switch (k) {
499 case PARAM_FAST_RESTART:
500 r = set_bool_param(value, ¶meters->fast_restart);
501 break;
502
503 case PARAM_C_THRESHOLD:
504 r = set_int32_param(value, &z, 1, INT32_MAX);
505 if (r == 0) {
506 parameters->c_threshold = (uint32_t) z;
507 }
508 break;
509
510 case PARAM_D_THRESHOLD:
511 r = set_int32_param(value, &z, 1, INT32_MAX);
512 if (r == 0) {
513 parameters->d_threshold = (uint32_t) z;
514 }
515 break;
516
517 case PARAM_C_FACTOR:
518 r = set_double_param(value, ¶meters->c_factor, 1.0, DBL_MAX);
519 break;
520
521 case PARAM_D_FACTOR:
522 r = set_double_param(value, ¶meters->d_factor, 1.0, DBL_MAX);
523 break;
524
525 case PARAM_R_THRESHOLD:
526 r = set_int32_param(value, &z, 1, INT32_MAX);
527 if (r == 0) {
528 parameters->r_threshold = z;
529 }
530 break;
531
532 case PARAM_R_FRACTION:
533 r = set_double_param(value, ¶meters->r_fraction, 0.0, 1.0);
534 break;
535
536 case PARAM_R_FACTOR:
537 r = set_double_param(value, ¶meters->r_factor, 1.0, DBL_MAX);
538 break;
539
540 case PARAM_VAR_DECAY:
541 r = set_double_param(value, ¶meters->var_decay, 0.0, 1.0);
542 break;
543
544 case PARAM_RANDOMNESS:
545 r = set_double_param(value, &x, 0.0, 1.0);
546 if (r == 0) {
547 parameters->randomness = (float) x;
548 }
549 break;
550
551 case PARAM_RANDOM_SEED:
552 r = set_uint32_param(value, ¶meters->random_seed);
553 break;
554
555 case PARAM_BRANCHING:
556 r = set_branching_param(value, ¶meters->branching);
557 break;
558
559 case PARAM_CLAUSE_DECAY:
560 r = set_double_param(value, &x, 0.0, 1.0);
561 if (r == 0) {
562 parameters->clause_decay = (float) x;
563 }
564 break;
565
566 case PARAM_CACHE_TCLAUSES:
567 r = set_bool_param(value, ¶meters->cache_tclauses);
568 break;
569
570 case PARAM_TCLAUSE_SIZE:
571 r = set_int32_param(value, &z, 2, INT32_MAX);
572 if (r == 0) {
573 parameters->tclause_size = (uint32_t) z;
574 }
575 break;
576
577 case PARAM_DYN_ACK:
578 r = set_bool_param(value, ¶meters->use_dyn_ack);
579 break;
580
581 case PARAM_DYN_BOOL_ACK:
582 r = set_bool_param(value, ¶meters->use_bool_dyn_ack);
583 break;
584
585 case PARAM_OPTIMISTIC_FCHECK:
586 r = set_bool_param(value, ¶meters->use_optimistic_fcheck);
587 break;
588
589 case PARAM_MAX_ACK:
590 r = set_int32_param(value, &z, 1, INT32_MAX);
591 if (r == 0) {
592 parameters->max_ackermann = (uint32_t) z;
593 }
594 break;
595
596 case PARAM_MAX_BOOL_ACK:
597 r = set_int32_param(value, &z, 1, INT32_MAX);
598 if (r == 0) {
599 parameters->max_boolackermann = (uint32_t) z;
600 }
601 break;
602
603 case PARAM_AUX_EQ_QUOTA:
604 r = set_int32_param(value, &z, 1, INT32_MAX);
605 if (r == 0) {
606 parameters->aux_eq_quota = (uint32_t) z;
607 }
608 break;
609
610 case PARAM_AUX_EQ_RATIO:
611 r = set_double_param(value, &x, 0.0, (double) FLT_MAX);
612 if (r == 0) {
613 if (x > 0.0) {
614 parameters->aux_eq_ratio = (float) x;
615 } else {
616 r = -2;
617 }
618 }
619 break;
620
621 case PARAM_DYN_ACK_THRESHOLD:
622 r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);
623 if (r == 0) {
624 parameters->dyn_ack_threshold = (uint16_t) z;
625 }
626 break;
627
628
629 case PARAM_DYN_BOOL_ACK_THRESHOLD:
630 r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);
631 if (r == 0) {
632 parameters->dyn_bool_ack_threshold = (uint16_t) z;
633 }
634 break;
635
636 case PARAM_MAX_INTERFACE_EQS:
637 r = set_int32_param(value, &z, 1, INT32_MAX);
638 if (r == 0) {
639 parameters->max_interface_eqs = (uint32_t) z;
640 }
641 break;
642
643 case PARAM_SIMPLEX_PROP:
644 r = set_bool_param(value, ¶meters->use_simplex_prop);
645 break;
646
647 case PARAM_SIMPLEX_ADJUST:
648 r = set_bool_param(value, ¶meters->adjust_simplex_model);
649 break;
650
651 case PARAM_SIMPLEX_ICHECK:
652 r = set_bool_param(value, ¶meters->integer_check);
653 break;
654
655 case PARAM_PROP_THRESHOLD:
656 r = set_int32_param(value, &z, 0, INT32_MAX);
657 if (r == 0) {
658 parameters->max_prop_row_size = (uint32_t) z;
659 }
660 break;
661
662 case PARAM_BLAND_THRESHOLD:
663 r = set_int32_param(value, &z, 1, INT32_MAX);
664 if (r == 0) {
665 parameters->bland_threshold = (uint32_t) z;
666 }
667 break;
668
669 case PARAM_ICHECK_PERIOD:
670 r = set_int32_param(value, ¶meters->integer_check_period, 1, INT32_MAX);
671 break;
672
673 case PARAM_MAX_UPDATE_CONFLICTS:
674 r = set_int32_param(value, &z, 1, INT32_MAX);
675 if (r == 0) {
676 parameters->max_update_conflicts = (uint32_t) z;
677 }
678 break;
679
680 case PARAM_MAX_EXTENSIONALITY:
681 r = set_int32_param(value, &z, 1, INT32_MAX);
682 if (r == 0) {
683 parameters->max_extensionality = (uint32_t) z;
684 }
685 break;
686
687 default:
688 assert(k == -1);
689 r = -1;
690 break;
691 }
692
693 return r;
694 }
695
696
697 /*
698 * Utility function: so that yices and yices_smt2
699 * can keep a copy of the initial random seed
700 */
params_default_random_seed(void)701 uint32_t params_default_random_seed(void) {
702 return DEFAULT_RANDOM_SEED;
703 }
704