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 * RECORD TO STORE SEARCH OPTIONS/SETTINGS 21 */ 22 23 #ifndef __SEARCH_PARAMETERS_H 24 #define __SEARCH_PARAMETERS_H 25 26 27 #include <stdbool.h> 28 #include <stdint.h> 29 30 #include "yices_types.h" 31 32 33 /* 34 * Possible branching heuristics: 35 * - determine whether to assign the decision literal to true or false 36 */ 37 typedef enum { 38 BRANCHING_DEFAULT, // use internal smt_core cache 39 BRANCHING_NEGATIVE, // branch l := false 40 BRANCHING_POSITIVE, // branch l := true 41 BRANCHING_THEORY, // defer to the theory solver 42 BRANCHING_TH_NEG, // defer to theory solver for atoms, branch l := false otherwise 43 BRANCHING_TH_POS, // defer to theory solver for atoms, branch l := true otherwise 44 } branch_t; 45 46 #define NUM_BRANCHING_MODES 6 47 48 49 struct param_s { 50 /* 51 * Restart heuristic: similar to PICOSAT or MINISAT 52 * 53 * If fast_restart is true: PICOSAT-style heuristic 54 * - inner restarts based on c_threshold 55 * - outer restarts based on d_threshold 56 * 57 * If fast_restart is false: MINISAT-style restarts 58 * - c_threshold and c_factor are used 59 * - d_threshold and d_threshold are ignored 60 * - to get periodic restart set c_factor = 1.0 61 * 62 * HACK to select a Luby-style restart: 63 * - set fast_restart to true and c_factor to 0.0 64 * - then c_threshold defines the base period 65 * - d_threshold and d_factor are ignored 66 */ 67 bool fast_restart; 68 uint32_t c_threshold; // initial value of c_threshold 69 uint32_t d_threshold; // initial value of d_threshold 70 double c_factor; // increase factor for next c_threshold 71 double d_factor; // increase factor for next d_threshold 72 73 /* 74 * Clause-deletion heuristic 75 * - initial reduce_threshold is max(r_threshold, num_prob_clauses * r_fraction) 76 * - increase by r_factor on every outer restart provided reduce was called in that loop 77 */ 78 uint32_t r_threshold; 79 double r_fraction; 80 double r_factor; 81 82 /* 83 * SMT Core parameters: 84 * - randomness and var_decay are used by the branching heuristic 85 * the default branching mode uses the cached polarity in smt_core. 86 * - clause_decay influence clause deletion 87 * - random seed 88 * 89 * SMT Core caching of theory lemmas: 90 * - if cache_tclauses is true, then the core internally turns 91 * some theory lemmas into learned clauses 92 * - for the core, a theory lemma is either a conflict reported by 93 * the theory solver or a theory implication 94 * - a theory implication is considered for caching if it's involved 95 * in a conflict resolution 96 * - parameter tclause_size controls the lemma size: only theory lemmas 97 * of size <= tclause_size are turned into learned clauses 98 */ 99 double var_decay; // decay factor for variable activity 100 float randomness; // probability of a random pick in select_unassigned_literal 101 uint32_t random_seed; 102 branch_t branching; // branching heuristic 103 float clause_decay; // decay factor for learned-clause activity 104 bool cache_tclauses; 105 uint32_t tclause_size; 106 107 /* 108 * EGRAPH PARAMETERS 109 * 110 * Control of the Ackermann lemmas 111 * - use_dyn_ack: if true, the dynamic ackermann heuristic is enabled for 112 * non-boolean terms 113 * - use_bool_dyn_ack: if true, the dynamic ackermann heuristic is enabled 114 * for boolean terms 115 * - use_optimistic_fcheck: if true, model reconciliation is used 116 * in final_check 117 * 118 * Limits to stop the Ackermann trick if too many lemmas are generated 119 * - max_ackermann: limit for the non-boolean version 120 * - max_boolackermann: limit for the boolean version 121 * 122 * The Ackermann clauses may require the construction of new equality 123 * terms that were not present in the context. This is controlled by 124 * the egraph's quota on auxiliary equalities. The quota is initialized 125 * to max(aux_eq_ratio * n, aux_eq_quota) where n is the total 126 * number of terms in the initial egraph. 127 * 128 * Thresholds for generation of Ackermann lemma: no effect unless 129 * use_dyn_ack or use_bool_dyn_ack is true. 130 * 131 * Control of interface equality generation: set a limit on 132 * the number of interface equalities created per round. 133 */ 134 bool use_dyn_ack; 135 bool use_bool_dyn_ack; 136 bool use_optimistic_fcheck; 137 uint32_t max_ackermann; 138 uint32_t max_boolackermann; 139 uint32_t aux_eq_quota; 140 double aux_eq_ratio; 141 uint16_t dyn_ack_threshold; 142 uint16_t dyn_bool_ack_threshold; 143 uint32_t max_interface_eqs; 144 145 146 /* 147 * SIMPLEX PARAMETERS 148 * - simplex_prop: if true enable propagation via propagation table 149 * - adjust_simplex_model: if true, enable adjustment in 150 * reconciliation of the egraph and simplex models 151 * - integer_check: if true, periodically call the integer solver 152 * - max_prop_row_size: limit on the size of the propagation rows 153 * - bland_threshold: threshold that triggers switching to Bland's rule 154 * - integer_check_period: how often the integer solver is called 155 */ 156 bool use_simplex_prop; 157 bool adjust_simplex_model; 158 bool integer_check; 159 uint32_t max_prop_row_size; 160 uint32_t bland_threshold; 161 int32_t integer_check_period; 162 163 /* 164 * ARRAY SOLVER PARAMETERS 165 * - max_update_conflicts: limit on the number of update axioms generated 166 * per call to final_check 167 * - max_extensionality: limit on the number of extensionality axioms 168 * generated per call to reconcile_model 169 */ 170 uint32_t max_update_conflicts; 171 uint32_t max_extensionality; 172 173 }; 174 175 176 177 /************************ 178 * PARAMETER RECORDS * 179 ***********************/ 180 181 /* 182 * Initialize params with default values 183 */ 184 extern void init_params_to_defaults(param_t *parameters); 185 186 187 /* 188 * Get a pointer to an internal record (set to defaults) 189 */ 190 extern const param_t *get_default_params(void); 191 192 193 /* 194 * Set a field in the parameter record 195 * - key = field name 196 * - value = value for that field 197 * 198 * Return code: 199 * -1 if the key is not recognized 200 * -2 if the value is not recognized 201 * -3 if the value is not valid for the key 202 * 0 otherwise 203 */ 204 extern int32_t params_set_field(param_t *parameters, const char *key, const char *value); 205 206 207 /* 208 * To synchronize with set-random-seed/get-random-seed 209 */ 210 extern uint32_t params_default_random_seed(void); 211 212 213 #endif /* __SEARCH_PARAMETERS_H */ 214