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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-02-20.
Revision History:
--*/
#pragma once
#include "ast/static_features.h"
#include "params/dyn_ack_params.h"
#include "params/qi_params.h"
#include "params/theory_arith_params.h"
#include "params/theory_array_params.h"
#include "params/theory_bv_params.h"
#include "params/theory_seq_params.h"
#include "params/theory_pb_params.h"
#include "params/theory_datatype_params.h"
#include "params/preprocessor_params.h"
#include "params/context_params.h"
enum phase_selection {
PS_ALWAYS_FALSE,
PS_ALWAYS_TRUE,
PS_CACHING,
PS_CACHING_CONSERVATIVE,
PS_CACHING_CONSERVATIVE2, // similar to the previous one, but alternated default config from time to time.
PS_RANDOM,
PS_OCCURRENCE,
PS_THEORY
};
enum restart_strategy {
RS_GEOMETRIC,
RS_IN_OUT_GEOMETRIC,
RS_LUBY,
RS_FIXED,
RS_ARITHMETIC
};
enum lemma_gc_strategy {
LGC_FIXED,
LGC_GEOMETRIC,
LGC_AT_RESTART,
LGC_NONE
};
enum initial_activity {
IA_ZERO, // initialized with 0
IA_RANDOM_WHEN_SEARCHING, // random when searching
IA_RANDOM // always random
};
enum case_split_strategy {
CS_ACTIVITY, // case split based on activity
CS_ACTIVITY_DELAY_NEW, // case split based on activity but delay new case splits created during the search
CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
CS_RELEVANCY, // case split based on relevancy
CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
CS_RELEVANCY_GOAL, // based on relevancy and the current goal
CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
};
struct smt_params : public preprocessor_params,
public dyn_ack_params,
public qi_params,
public theory_arith_params,
public theory_array_params,
public theory_bv_params,
public theory_seq_params,
public theory_pb_params,
public theory_datatype_params {
bool m_display_proof = false;
bool m_display_dot_proof = false;
bool m_display_unsat_core = false;
bool m_check_proof = false;
bool m_eq_propagation = true;
bool m_binary_clause_opt = true;
unsigned m_relevancy_lvl = 2;
bool m_relevancy_lemma = false;
unsigned m_random_seed = 0;
double m_random_var_freq = 0.01;
double m_inv_decay = 1.052;
unsigned m_clause_decay = 1;
initial_activity m_random_initial_activity = initial_activity::IA_RANDOM_WHEN_SEARCHING;
phase_selection m_phase_selection = phase_selection::PS_CACHING_CONSERVATIVE;
unsigned m_phase_caching_on = 700;
unsigned m_phase_caching_off = 100;
bool m_minimize_lemmas = true;
unsigned m_max_conflicts = UINT_MAX;
unsigned m_restart_max;
unsigned m_cube_depth = 1;
unsigned m_threads = 1;
unsigned m_threads_max_conflicts = UINT_MAX;
unsigned m_threads_cube_frequency = 2;
bool m_simplify_clauses = true;
unsigned m_tick = 1000;
bool m_display_features = false;
bool m_new_core2th_eq = true;
bool m_ematching = true;
bool m_ho_matching = false;
unsigned m_ho_matching_bound = 10000;
bool m_term_enumeration = true;
bool m_induction = false;
bool m_clause_proof = false;
symbol m_proof_log;
bool m_sls_enable = false;
bool m_sls_parallel = true;
// -----------------------------------
//
// Case split strategy
//
// -----------------------------------
case_split_strategy m_case_split_strategy = case_split_strategy::CS_ACTIVITY_DELAY_NEW;
unsigned m_rel_case_split_order = 0;
bool m_lookahead_diseq = false;
bool m_theory_case_split = false;
bool m_theory_aware_branching = false;
// -----------------------------------
//
// Delay units...
//
// -----------------------------------
bool m_delay_units = false;
unsigned m_delay_units_threshold = 32;
// -----------------------------------
//
// Conflict resolution
//
// -----------------------------------
bool m_theory_resolve = false;
// -----------------------------------
//
// Restart
//
// -----------------------------------
restart_strategy m_restart_strategy = restart_strategy::RS_IN_OUT_GEOMETRIC;
unsigned m_restart_initial = 100;
double m_restart_factor = 1.1;
bool m_restart_adaptive = true;
double m_agility_factor = 0.9999;
double m_restart_agility_threshold = 0.18;
// -----------------------------------
//
// Lemma garbage collection
//
// -----------------------------------
lemma_gc_strategy m_lemma_gc_strategy = lemma_gc_strategy::LGC_FIXED;
bool m_lemma_gc_half = false;
unsigned m_recent_lemmas_size = 100;
unsigned m_lemma_gc_initial = 5000;
double m_lemma_gc_factor = 1.1;
unsigned m_new_old_ratio = 16; //!< the ratio of new and old clauses.
unsigned m_new_clause_activity = 10;
unsigned m_old_clause_activity = 500;
unsigned m_new_clause_relevancy = 45; //!< Max. number of unassigned literals to be considered relevant.
unsigned m_old_clause_relevancy = 6; //!< Max. number of unassigned literals to be considered relevant.
double m_inv_clause_decay = 1; //!< clause activity decay
// -----------------------------------
//
// User propagator configuration
//
// -----------------------------------
bool m_up_persist_clauses = false;
// -----------------------------------
//
// SMT-LIB (debug) pretty printer
//
// -----------------------------------
bool m_axioms2files = false;
bool m_lemmas2console = false;
bool m_instantiations2console = false;
symbol m_logic = symbol::null;
// -----------------------------------
//
// Statistics for Profiling
//
// -----------------------------------
bool m_profile_res_sub = false;
bool m_display_bool_var2expr = false;
bool m_display_ll_bool_var2expr = false;
// -----------------------------------
//
// Model generation
//
// -----------------------------------
bool m_model = true;
bool m_model_on_timeout = false;
bool m_model_on_final_check = false;
// -----------------------------------
//
// Progress sampling
//
// -----------------------------------
unsigned m_progress_sampling_freq = 0;
// -----------------------------------
//
// Debugging goodies
//
// -----------------------------------
bool m_core_validate = false;
// -----------------------------------
//
// From front_end_params
//
// -----------------------------------
bool m_preprocess = true; // temporary hack for disabling all preprocessing..
bool m_user_theory_preprocess_axioms = false;
bool m_user_theory_persist_axioms = false;
bool m_at_labels_cex = false; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels = false; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt = false;
bool m_auto_config = true;
// -----------------------------------
//
// Spacer hacking
//
// -----------------------------------
bool m_dump_benchmarks;
double m_dump_min_time;
bool m_dump_recheck;
// -----------------------------------
//
// Solver selection
//
// -----------------------------------
symbol m_string_solver;
smt_params(params_ref const & p = params_ref()):
m_string_solver(symbol("auto")){
updt_local_params(p);
}
void updt_local_params(params_ref const & p);
void updt_params(params_ref const & p);
void updt_params(context_params const & p);
void display(std::ostream & out) const;
void validate_string_solver(symbol const& s) const;
void setup_QF_UF();
void setup_QF_RDL();
void setup_QF_RDL(static_features & st);
void setup_QF_IDL();
void setup_QF_IDL(static_features & st);
void setup_QF_LRA();
void setup_QF_LRA(static_features const& st);
void setup_QF_LIA();
void setup_QF_LIA(static_features const& st);
void setup_QF_UFIDL();
void setup_QF_UFLIA();
void setup_QF_UFLRA();
void setup_QF_BV();
void setup_QF_AUFBV();
void setup_QF_AX();
void setup_QF_AX(static_features const& st);
void setup_QF_AUFLIA();
void setup_QF_AUFLIA(static_features const& st);
void setup_AUFLIA(bool simple_array);
void setup_AUFLIA(static_features const & st);
void setup_AUFLIRA(bool simple_array);
void setup_LRA();
};