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 * DPLL(T) SOLVER
21 *
22 * An smt_core structure is parameterized by a theory-solver
23 * object. Operations that the theory solver must implement are
24 * accessed via function pointers.
25 *
26 * Atoms, explanations, and theory solver are treated abstractly by the smt_core.
27 * They are represented by generic (void *) pointers. The two lower-order bits
28 * of an explanation pointer must be 00 (aligned to a multiple of 4bytes).
29 *
30 * The core has support for
31 * - creation of boolean variables
32 * - attaching atoms to boolean variables
33 * - addition of clauses
34 * - push/pop/reset operations
35 * - boolean and theory propagation
36 * - assertion of implied literals and conflicts
37 * - conflict resolution and construction of learned clauses
38 * - optional deletion of newly created atoms on backtracking (to support
39 * solver that create many atoms on the fly).
40 * - restart
41 * - reduction of learned clause database
42 *
43 * Variables and clauses can be added on the fly, during the search.
44 *
45 * History: created January 10, 2008.
46 * Based on an earlier version (dpll.h and dpll.c) that was not sufficient.
47 */
48
49 #ifndef __SMT_CORE_H
50 #define __SMT_CORE_H
51
52 #include <stdint.h>
53 #include <stdbool.h>
54 #include <stddef.h>
55
56 #include "io/tracer.h"
57 #include "solvers/cdcl/smt_core_base_types.h"
58 #include "solvers/cdcl/gates_hash_table.h"
59 #include "utils/bitvectors.h"
60 #include "utils/int_vectors.h"
61
62 #include "yices_types.h"
63
64
65 // EXPERIMENTAL
66 #include "scratch/booleq_table.h"
67
68
69 /***********
70 * CLAUSES *
71 **********/
72
73 /*
74 * Clauses structure
75 * - two pointers to form lists of clauses for the watched literals
76 * - a clause is an array of literals terminated by an end marker
77 * (a negative number).
78 * - the first two literals stored in cl[0] and cl[1]
79 * are the watched literals.
80 * Learned clauses have the same components as a clause
81 * and an activity, i.e., a float used by the clause-deletion
82 * heuristic. (Because of alignment and padding, this wastes 32bits
83 * on a 64bit machine....)
84 *
85 * Linked lists:
86 * - a link lnk is a pointer to a clause cl
87 * the low-order bits of lnk encode whether the next link is
88 * in cl->link[0] or cl->link[1]
89 * - this is compatible with the tagged pointers used as antecedents.
90 *
91 * SPECIAL CODING: to distinguish between learned clauses and problem
92 * clauses, the end marker is different.
93 * - for problem clauses, end_marker = -1
94 * - for learned clauses, end_marker = -2
95 *
96 * These two end_markers always have an UNDEF_VALYE:
97 * - value[-1] = VAL_UNDEF_FALSE
98 * value[-2] = VAL_UNDEF_FALSE
99 *
100 * CLAUSE DELETION AND SIMPLIFICATION:
101 * - to mark a clause for deletion or to removed it from the watched lists,
102 * both cl[0] and cl[1] are replaced by their opposite (turned into negative numbers).
103 */
104
105 enum {
106 end_clause = -1, // end of problem clause
107 end_learned = -2, // end of learned clause
108 };
109
110 typedef struct clause_s clause_t;
111
112 typedef uintptr_t link_t;
113
114 struct clause_s {
115 link_t link[2];
116 literal_t cl[0];
117 };
118
119 typedef struct learned_clause_s {
120 float activity;
121 clause_t clause;
122 } learned_clause_t;
123
124
125 /*
126 * Tagging/untagging of link pointers
127 */
128 #define LINK_TAG ((uintptr_t) 0x1)
129 #define NULL_LINK ((link_t) 0)
130
mk_link(clause_t * c,uint32_t i)131 static inline link_t mk_link(clause_t *c, uint32_t i) {
132 assert((i & ~LINK_TAG) == 0 && (((uintptr_t) c) & LINK_TAG) == 0);
133 return (link_t)(((uintptr_t) c) | ((uintptr_t) i));
134 }
135
clause_of(link_t lnk)136 static inline clause_t *clause_of(link_t lnk) {
137 return (clause_t *)(lnk & ~LINK_TAG);
138 }
139
idx_of(link_t lnk)140 static inline uint32_t idx_of(link_t lnk) {
141 return (uint32_t)(lnk & LINK_TAG);
142 }
143
next_of(link_t lnk)144 static inline link_t next_of(link_t lnk) {
145 return clause_of(lnk)->link[idx_of(lnk)];
146 }
147
148
149 /*
150 * return a new link lnk0 such that
151 * - clause_of(lnk0) = c
152 * - idx_of(lnk0) = i
153 * - next_of(lnk0) = lnk
154 */
cons(uint32_t i,clause_t * c,link_t lnk)155 static inline link_t cons(uint32_t i, clause_t *c, link_t lnk) {
156 assert(i <= 1);
157 c->link[i] = lnk;
158 return mk_link(c, i);
159 }
160
161 /*
162 * If lnk points to a clause cl, then return
163 * a pointer to either cl->link[0] or cl->link[1], depending on
164 * the lower order bit of lnk.
165 */
cdr_ptr(link_t lnk)166 static inline link_t *cdr_ptr(link_t lnk) {
167 return clause_of(lnk)->link + idx_of(lnk);
168 }
169
170
171
172
173
174 /*********************************
175 * CLAUSE AND LITERAL VECTORS *
176 ********************************/
177
178 /*
179 * Vectors are arrays preceded by a hidden header
180 * - e.g., a literal vector v is a pointer to literals
181 * - the elements in the vectors are v[0] ... v[n-1]
182 * - the header specifies the capacity and current size of v
183 */
184 typedef struct clause_vector_s {
185 uint32_t capacity;
186 uint32_t size;
187 clause_t *data[0];
188 } clause_vector_t;
189
190 typedef struct literal_vector_s {
191 uint32_t capacity;
192 uint32_t size;
193 literal_t data[0];
194 } literal_vector_t;
195
196
197 /*
198 * Access to header of clause vector v
199 */
cv_header(clause_t ** v)200 static inline clause_vector_t *cv_header(clause_t **v) {
201 return (clause_vector_t *)(((char *)v) - offsetof(clause_vector_t, data));
202 }
203
get_cv_size(clause_t ** v)204 static inline uint32_t get_cv_size(clause_t **v) {
205 return cv_header(v)->size;
206 }
207
set_cv_size(clause_t ** v,uint32_t sz)208 static inline void set_cv_size(clause_t **v, uint32_t sz) {
209 cv_header(v)->size = sz;
210 }
211
get_cv_capacity(clause_t ** v)212 static inline uint32_t get_cv_capacity(clause_t **v) {
213 return cv_header(v)->capacity;
214 }
215
216
217 /*
218 * Header, size and capacity of a literal vector v
219 */
lv_header(literal_t * v)220 static inline literal_vector_t *lv_header(literal_t *v) {
221 return (literal_vector_t *)(((char *) v) - offsetof(literal_vector_t, data));
222 }
223
get_lv_size(literal_t * v)224 static inline uint32_t get_lv_size(literal_t *v) {
225 return lv_header(v)->size;
226 }
227
set_lv_size(literal_t * v,uint32_t sz)228 static inline void set_lv_size(literal_t *v, uint32_t sz) {
229 lv_header(v)->size = sz;
230 }
231
get_lv_capacity(literal_t * v)232 static inline uint32_t get_lv_capacity(literal_t *v) {
233 return lv_header(v)->capacity;
234 }
235
236
237
238 /*
239 * Default sizes and max sizes of vectors
240 */
241 #define DEF_CLAUSE_VECTOR_SIZE 100
242 #define MAX_CLAUSE_VECTOR_SIZE (((uint32_t)(UINT32_MAX-sizeof(clause_vector_t)))/8)
243
244 #define DEF_LITERAL_VECTOR_SIZE 10
245 #define DEF_LITERAL_BUFFER_SIZE 100
246 #define MAX_LITERAL_VECTOR_SIZE (((uint32_t)(UINT32_MAX-sizeof(literal_vector_t)))/4)
247
248
249
250 /**********************************
251 * ASSIGNMENT/PROPAGATION QUEUE *
252 *********************************/
253
254 /*
255 * Assignment stack/propagation queue
256 * - an array of literals (the literals assigned to true)
257 * - pointers: top of the stack
258 * - pointers for boolean and theory propagation
259 * - prop_ptr: beginning of the boolean propagation queue
260 * - theory_ptr: beginning of the theory propagation queue
261 * - literals in stack->lit[prop_ptr ... top-1] form the boolean propagation queue
262 * - literals in stack->lit[theory_ptr ... top-1] form the theory propagation queue
263 * - for each decision level, an index into the stack points
264 * to the literal decided or assigned at that level (for backtracking)
265 * - for level 0, level_index[0] = 0 = index of the first literal assigned
266 */
267 typedef struct {
268 literal_t *lit;
269 uint32_t top;
270 uint32_t prop_ptr;
271 uint32_t theory_ptr;
272 uint32_t *level_index;
273 uint32_t nlevels; // size of level_index array
274 } prop_stack_t;
275
276
277 /*
278 * Initial size of level_index
279 */
280 #define DEFAULT_NLEVELS 100
281
282
283
284
285 /******************
286 * ANTECEDENTS *
287 *****************/
288
289 /*
290 * Antecedent = reason for an implied literal.
291 * It's either a clause or a literal or a generic explanation.
292 * Antecedents are represented as tagged pointers with tag in the
293 * two low-order bits
294 * - tag = 00: clause with implied literal as cl[0]
295 * - tag = 01: clause with implied literal as cl[1]
296 * - tag = 10: literal
297 * - tag = 11: generic explanation from a theory solver
298 */
299 typedef uintptr_t antecedent_t;
300
301 enum {
302 clause0_tag = 0,
303 clause1_tag = 1,
304 literal_tag = 2,
305 generic_tag = 3,
306 };
307
antecedent_tag(antecedent_t a)308 static inline uint32_t antecedent_tag(antecedent_t a) {
309 return a & 0x3;
310 }
311
literal_antecedent(antecedent_t a)312 static inline literal_t literal_antecedent(antecedent_t a) {
313 return (literal_t) (((int32_t) a) >>2);
314 }
315
clause_antecedent(antecedent_t a)316 static inline clause_t *clause_antecedent(antecedent_t a) {
317 return (clause_t *) (a & ~((uintptr_t) 0x3));
318 }
319
320 // clause index: 0 or 1, low order bit of a
clause_index(antecedent_t a)321 static inline uint32_t clause_index(antecedent_t a) {
322 return (uint32_t) (a & 0x1);
323 }
324
generic_antecedent(antecedent_t a)325 static inline void *generic_antecedent(antecedent_t a) {
326 return (void *) (a & ~((uintptr_t) 0x3));
327 }
328
mk_literal_antecedent(literal_t l)329 static inline antecedent_t mk_literal_antecedent(literal_t l) {
330 return (((uintptr_t) l) << 2) | literal_tag;
331 }
332
mk_clause0_antecedent(clause_t * cl)333 static inline antecedent_t mk_clause0_antecedent(clause_t *cl) {
334 assert((((uintptr_t) cl) & 0x3) == 0);
335 return ((uintptr_t) cl) | clause0_tag;
336 }
337
mk_clause1_antecedent(clause_t * cl)338 static inline antecedent_t mk_clause1_antecedent(clause_t *cl) {
339 assert((((uintptr_t) cl) & 0x3) == 0);
340 return ((uintptr_t) cl) | clause1_tag;
341 }
342
mk_clause_antecedent(clause_t * cl,int32_t idx)343 static inline antecedent_t mk_clause_antecedent(clause_t *cl, int32_t idx) {
344 assert((((uintptr_t) cl) & 0x3) == 0);
345 return ((uintptr_t) cl) | (idx & 1);
346 }
347
mk_generic_antecedent(void * g)348 static inline antecedent_t mk_generic_antecedent(void *g) {
349 assert((((uintptr_t) g) & 0x3) == 0);
350 return ((uintptr_t) g) | generic_tag;
351 }
352
353
354 /*
355 * Macros to pack/unpack an integer into a void* pointer
356 * to be used as a generic explanation.
357 * - we can't use the default tag_i32/untag_i32 because we must
358 * keep the two lower bits 00
359 */
mk_i32_expl(int32_t x)360 static inline void *mk_i32_expl(int32_t x) {
361 return (void *) (((uintptr_t) ((uint32_t) x))<<2);
362 }
363
i32_of_expl(void * g)364 static inline int32_t i32_of_expl(void *g) {
365 return (int32_t) (((uintptr_t) g) >> 2);
366 }
367
368
369
370 /*******************
371 * VARIABLE HEAP *
372 ******************/
373
374 /*
375 * Heap: for activity-based variable selection heuristic
376 * - activity[x]: for every variable x between 0 and nvars - 1
377 * - indices -1 and -2 are used as sentinels:
378 * activity[-1] = DBL_MAX (higher than any activity)
379 * activity[-2] = -1.0 (lower than any variable activity)
380 * - heap_index[x]: for every variable x,
381 * heap_index[x] = i if x is in the heap and heap[i] = x
382 * or heap_index[x] = -1 if x is not in the heap
383 * - heap: array of nvars + 1 variables
384 * - heap_last: index of last element in the heap
385 * heap[0] = -1,
386 * for i=1 to heap_last, heap[i] = x for some variable x
387 * - act_inc: variable activity increment
388 * - inv_act_decay: inverse of variable activity decay (e.g., 1/0.95)
389 */
390 typedef struct var_heap_s {
391 uint32_t size;
392 double *activity;
393 bvar_t *heap;
394 int32_t *heap_index;
395 uint32_t heap_last;
396 double act_increment;
397 double inv_act_decay;
398 } var_heap_t;
399
400
401
402
403 /*****************
404 * TRAIL STACK *
405 ****************/
406
407 /*
408 * Push/pop stack:
409 * - for each base_level: we keep the number of variables and unit-clauses
410 * + the size of vectors binary_clauses and problem_clauses on entry to that level,
411 * + the propagation pointers at that point.
412 * - we store prop_ptr to support sequences such as
413 * assert unit clause l1;
414 * push;
415 * assert unit clause l2;
416 * search;
417 * pop;
418 * assert more clauses;
419 * search
420 * - on entry to the first search, no boolean propagation has been done yet, prop_ptr = 0
421 * - after pop, we need to restore prop_ptr to 0, otherwise anything implied by
422 * the unit clause l1 may be missed
423 */
424 typedef struct trail_s {
425 uint32_t nvars;
426 uint32_t nunits;
427 uint32_t nbins;
428 uint32_t nclauses;
429 uint32_t prop_ptr;
430 uint32_t theory_ptr;
431 } trail_t;
432
433 typedef struct trail_stack_s {
434 uint32_t size;
435 uint32_t top;
436 trail_t *data;
437 } trail_stack_t;
438
439 #define DEFAULT_DPLL_TRAIL_SIZE 20
440 #define MAX_DPLL_TRAIL_SIZE (UINT32_MAX/sizeof(trail_t))
441
442
443
444
445
446 /****************
447 * ATOM TABLE *
448 ***************/
449
450 /*
451 * The atom table maps boolean variables to atoms
452 *
453 * For every boolean variable v:
454 * - has_atom[v]: one bit = 1 if v has an associated atom, 0 otherwise
455 * - atom[v] = pointer to the atom attached to v (not initialized if has_atom[v] == 0)
456 * - size = size of array atom = number of bits in has_atom vector
457 *
458 * Using the extra bitvector has_atom improves performance
459 * if there are a lot of variables but few atoms.
460 *
461 * Initially, size is 0 and nothing is allocated.
462 * The table is extended if needed when attach_atom is called.
463 */
464 typedef struct atom_table_s {
465 byte_t *has_atom;
466 void **atom;
467 uint32_t size;
468 uint32_t natoms; // for statistics
469 } atom_table_t;
470
471
472 #define MAX_ATOM_TABLE_SIZE (UINT32_MAX/8)
473
474
475
476 /********************
477 * THEORY SOLVER *
478 *******************/
479
480 /*
481 * A theory solver must implement the following functions
482 *
483 * 1) void start_internalization(void *solver)
484 * - this is called to signal the solver that new assertions will
485 * be added at the base level
486 * - assert_atom/propagate may be called after this and before
487 * start_search to perform base-level simplifications.
488 *
489 * 2) void start_search(void *solver)
490 * - this is called when the search starts to enable solver to perform
491 * initializations and simplifications. If solver detects an inconsistency
492 * at this point, it must record it using record_theory_conflict (possibly
493 * with an empty conflict).
494 *
495 * 3) bool assert_atom(void *solver, void *atom, literal_t l)
496 * - this is called when literal l is assigned and var_of(l) has an atom attached.
497 * if l has positive sign, then atom is true
498 * if l has negative sign, then atom is false
499 * - the function must return false if a conflict is detected and
500 * record the conflict (as a conjunction of false literals) by
501 * calling record_theory_conflict
502 * - it must return true if no conflict is detected
503 *
504 * 4) bool propagate(void *solver)
505 * - this is called at the end of each propagation round to check whether
506 * all atoms asserted so far are consistent.
507 * - the function must return true if no conflict is detected
508 * - it must return false if a conflict is detected and record that conflict
509 *
510 * 5) fcheck_code_t final_check(void *solver)
511 * - this is called when smt_final_check is invoked (when all boolean
512 * variables are assigned)
513 * - final_check must return one of the following codes:
514 * FCHECK_CONTINUE: if more processing is required
515 * FCHECK_SAT: if the solver agrees that the problem is SAT
516 * FCHECK_UNKNOWN: if the solver is incomplete and cannot determine
517 * whether the problem is SAT
518 * - if the solver returns FCHECK_CONTINUE, it must have done one of
519 * the following things:
520 * - record a conflict (by calling record_theory_conflict)
521 * - create lemmas or atoms in the core
522 * - if the theory solver returns FCHECK_SAT or FCHECK_UNKNOWN, the search
523 * stops and the solver smt-core status is set to SAT or UNKNOWN.
524 *
525 * 6) void expand_explanation(void *solver, literal_t l, void *expl, ivector_t *v)
526 * - this is called during conflict resolution to deal with literals propagated
527 * by the theory solver.
528 * - solver can propagate literals by calling propagate_literal(core, l, expl)
529 * where l is a literal, expl is an abstract explanation object (void *)
530 * - if l is involved in conflict resolution later on, then expl must be expanded
531 * into a conjunction of literals l_1 ... l_n such that
532 * (l_1 and .... and l_n) implies l
533 * holds in the theory.
534 * - function expand_explanation(solver, l, expl, v) must perform the expansion
535 * l is an implied literal, with expl as generic antecedent.
536 * v is a vector to store the result
537 * the literals l1 ... l_n must be appended to vector v (without resetting v)
538 *
539 * 7) void increase_decision_level(void *solver)
540 * - this is called whenever a new decision level is entered, i.e., within
541 * any call to decide_literal(core, l)
542 * - the theory solver must keep track of this so that it can backtrack to the
543 * right point later on
544 *
545 * 8) void backtrack(void *solver, uint32_t back_level)
546 * - this is called whenever the core backtracks to back_level. The theory
547 * solver must undo all assertions made at decision levels > back_level.
548 *
549 * 9) literal_t select_polarity(void *solver, void *atom, literal_t l)
550 * - optional support for a solver-specific splitting heuristic:
551 * - l is a decision literal attached to a solver's atom.
552 * - the function must decide between setting l true or false
553 * - it must return either l (set l := true) or (not l) (set l := false)
554 *
555 * 10) void delete_atom(void *solver, void *atom)
556 * - this is called to inform solver that the core has removed a variable v
557 * with atom attached from its set of variables. This is intended to
558 * support a minimal form of garbage collection (stack based).
559 * - removal of variables occurs if a checkpoint has been set at a decision level k,
560 * and the core backtracks to a level <= k.
561 *
562 * 11) void end_atom_deletion(void *solver)
563 * - this is called when the core has finished deleting a group of atoms, to
564 * enable solver to take appropriate cleanup actions.
565 *
566 * 12) void push(void *solver)
567 * void pop(void *solver)
568 * void reset(void *solver)
569 *
570 * 13) void clear(void *solver)
571 * - new function added June 12, 2014. Whenever smt_clear is called
572 * the smt_core propagates it to the theory solver by calling this function.
573 * Smt_clear is called in a state where solver->status is SAT or UNKNOWN,
574 * the theory solver must restore its internal state to what it was on entry
575 * to the previous call to final_check (this should be used by the Egraph
576 * to remove all temporary equalities introduced during model reconciliation).
577 *
578 *
579 * Functions deleted_atom, end_deletion, push, pop, and reset are
580 * optional. The corresponding function pointer in theory_solver_t
581 * object may be set to NULL. This will work provided the features
582 * that require them are never used (i.e., "fire-and-forget" mode of
583 * operation, and no calls to checkpoint).
584 *
585 * The theory solver can propagate literal assignments to the core, and
586 * add clauses, atoms, and literals on the fly.
587 * - literal propagation is performed by calling propagate_literal(core, ...)
588 * this function can be called only from
589 * th->start_search
590 * th->propagate
591 * - on-the-fly literals, atoms, and lemmas can be created from within
592 * th->start_search
593 * th->propagate
594 * th->backtrack
595 * - it's not safe to call propagate_literal or to add clauses or literals
596 * within th->assert_atom
597 */
598
599 // Codes for final_check
600 typedef enum fcheck_code {
601 FCHECK_CONTINUE,
602 FCHECK_SAT,
603 FCHECK_UNKNOWN,
604 } fcheck_code_t;
605
606
607 // Signatures for all these functions
608 typedef void (*start_intern_fun_t)(void *solver);
609 typedef void (*start_fun_t)(void *solver);
610 typedef bool (*assert_fun_t)(void *solver, void *atom, literal_t l);
611 typedef bool (*propagate_fun_t)(void *solver);
612 typedef fcheck_code_t (*final_check_fun_t)(void *solver);
613 typedef void (*expand_expl_fun_t)(void *solver, literal_t l, void *expl, ivector_t *v);
614 typedef void (*increase_level_fun_t)(void *solver);
615 typedef void (*backtrack_fun_t)(void *solver, uint32_t back_level);
616 typedef literal_t (*select_pol_fun_t)(void *solver, void *atom, literal_t l);
617 typedef void (*del_atom_fun_t)(void *solver, void *atom);
618 typedef void (*end_del_fun_t)(void *solver);
619 typedef void (*push_fun_t)(void *solver);
620 typedef void (*pop_fun_t)(void *solver);
621 typedef void (*reset_fun_t)(void *solver);
622 typedef void (*clear_fun_t)(void *solver);
623
624
625 /*
626 * Solver descriptor: 2008/02/11: we now split it into
627 * - a control interface
628 * - an SMT-specific interface
629 *
630 * The control interface is generic and is also used for communication
631 * form the egraph to other theory solvers.
632 *
633 * The SMT-specific interface needs to be implemented only by solvers
634 * that can interface directly with the core. It includes the solver
635 * operations that have to do with atoms and explanations.
636 */
637 typedef struct th_ctrl_interface_s {
638 start_intern_fun_t start_internalization;
639 start_fun_t start_search;
640 propagate_fun_t propagate;
641 final_check_fun_t final_check;
642 increase_level_fun_t increase_decision_level;
643 backtrack_fun_t backtrack;
644 push_fun_t push;
645 pop_fun_t pop;
646 reset_fun_t reset;
647 clear_fun_t clear;
648 } th_ctrl_interface_t;
649
650 typedef struct th_smt_interface_s {
651 assert_fun_t assert_atom;
652 expand_expl_fun_t expand_explanation;
653 select_pol_fun_t select_polarity;
654 del_atom_fun_t delete_atom;
655 end_del_fun_t end_atom_deletion;
656 } th_smt_interface_t;
657
658
659
660
661 /*****************
662 * LEMMA QUEUE *
663 ****************/
664
665 /*
666 * By lemmas we mean clauses that are created on the fly by the theory solver.
667 * These new clauses may cause a conflict or require backtracking so they have
668 * to be processed and added carefully. To do this, we do not immediately add
669 * lemmas to the clause database but we copy them into an auxiliary queue, for
670 * processing when the theory solver returns.
671 *
672 * Each block in the queue is an array of literals. The content of this array
673 * is a set of lemmas separated by end markers (null_literal).
674 * - for a block b:
675 * b->data is an array of b->size literals
676 * the lemmas are stored in b->data[0 ... n-1] where n = b->ptr
677 *
678 * The queue itself is an array of blocks divided in three segments:
679 * - for 0 <= i < free_block: blocks currently in use (i.e., that contain lemmas)
680 * for 0 <= i < free_block-1, block[i] is full
681 * if free_block > 0 then i = free_block-1 = index of the current block
682 * where new lemmas are copied, if space is available
683 * - for free_block <= i < nblocks: allocated but unused blocks (all are empty).
684 * - for nblocks <= i < capacity: not allocated (block[i] is garbage/not a valid pointer).
685 */
686 typedef struct lemma_block_s {
687 uint32_t size; // size of data array
688 uint32_t ptr; // index of the first free element in data
689 literal_t data[0];
690 } lemma_block_t;
691
692 typedef struct lemma_queue_s {
693 uint32_t capacity; // size of block array
694 uint32_t nblocks; // number of non-null blocks
695 uint32_t free_block; // start of the free block segment
696 lemma_block_t **block;
697 } lemma_queue_t;
698
699
700 /*
701 * Default and max size of a block
702 */
703 #define DEF_LEMMA_BLOCK_SIZE 1000
704 #define MAX_LEMMA_BLOCK_SIZE (UINT32_MAX/4)
705
706 /*
707 * Max number of blocks in the queue
708 */
709 #define MAX_LEMMA_BLOCKS (UINT32_MAX/8)
710
711 /*
712 * Number of blocks for the first allocation
713 */
714 #define DEF_LEMMA_BLOCKS 4
715
716 /*
717 * Max number of empty blocks kept in the queue
718 * after it's reset
719 */
720 #define LEMMA_BLOCKS_TO_KEEP 4
721
722
723 /*****************
724 * CHECKPOINTS *
725 ****************/
726
727 /*
728 * THIS IS EXPERIMENTAL AND UNTESTED
729 *
730 * We use a stack-based mechanism for deleting irrelevant atoms,
731 * variables. and clauses constructed during the search. This is done
732 * via a stack of checkpoints. Each checkpoint records a decision
733 * level and the number of boolean variables on entry to that
734 * level. The garbage collection mechanism attempts to delete any new
735 * variables, atoms, and clauses created at levels > d when the solver
736 * backtracks to a lower decision level. Nothing is deleted if one or
737 * more atoms created at levels > d is now assigned at a level <= d,
738 * which may happen during conflict resolution. In such a case, the
739 * checkpoint is kept and deletion will be tried again later.
740 *
741 * This can be used as follows:
742 * - set a checkpoint before calling decide (current decision_level = d,
743 * current number of variables = n)
744 * - variables, atoms, and clauses can be created on-the-fly
745 * - when the solver backtracks to decision_level <= d, it removes all
746 * boolean variables created since the checkpoint was set. This restores
747 * the solver to n variables.
748 * - any clause that contain one of the deleted variables is also deleted
749 * - if a deleted variable is attached to an atom, then the theory solver
750 * is notified via the deleted_atom function
751 */
752
753 typedef struct checkpoint_s {
754 uint32_t dlevel;
755 uint32_t nvars;
756 } checkpoint_t;
757
758 typedef struct checkpoint_stack_s {
759 uint32_t size;
760 uint32_t top;
761 checkpoint_t *data;
762 } checkpoint_stack_t;
763
764
765 #define DEF_CHECKPOINT_STACK_SIZE 10
766 #define MAX_CHECKPOINT_STACK_SIZE (UINT32_MAX/sizeof(checkpoint_t))
767
768
769
770
771 /***********************
772 * STATISTICS RECORD *
773 **********************/
774
775 /*
776 * Search statistics
777 */
778 typedef struct dpll_stats_s {
779 uint32_t restarts; // number of restarts
780 uint32_t simplify_calls; // number of calls to simplify_clause_database
781 uint32_t reduce_calls; // number of calls to reduce_learned_clause_set
782 uint32_t remove_calls; // number of calls to remove_irrelevant_learned_clauses
783
784 uint64_t decisions; // number of decisions
785 uint64_t random_decisions; // number of random decisions
786 uint64_t propagations; // number of boolean propagations
787 uint64_t conflicts; // number of conflicts/backtrackings
788
789 uint32_t th_props; // number of theory propagation
790 uint32_t th_prop_lemmas; // number of propagation/explanation turned into clauses
791 uint32_t th_conflicts; // number of calls to record_conflict
792 uint32_t th_conflict_lemmas; // number of theory conflicts turned into clauses
793
794 uint64_t prob_literals; // number of literals in problem clauses
795 uint64_t learned_literals; // number of literals in learned clauses
796
797 uint64_t prob_clauses_deleted; // number of problem clauses deleted
798 uint64_t learned_clauses_deleted; // number of learned clauses deleted
799 uint64_t bin_clauses_deleted; // number of binary clauses deleted
800
801 uint64_t literals_before_simpl;
802 uint64_t subsumed_literals;
803 } dpll_stats_t;
804
805
806
807 /*********************
808 * SMT SOLVER CORE *
809 ********************/
810
811 /*
812 * Status: the codes are now defined in yices_types.h
813 * - idle is the initial status
814 * - addition of clauses may cause status to become unsat
815 * otherwise it remains idle until search starts.
816 * - status is switched to searching when search starts
817 * - the search can be interrupted, or it completes with
818 * status = SAT or UNSAT or UNKNOWN (unknown may be returned
819 * if the solver is incomplete and does not find an inconsistency)
820 * - if status is INTERRUPTED, SAT, or UNKNOWN, then push or clause
821 * addition returns status to idle.
822 * - if status is UNSAT, reset or pop must be called before any
823 * other operation. This also restores the state to idle.
824 */
825 #if 0
826 // this type is now imported from yices_types.h
827 typedef enum smt_status {
828 STATUS_IDLE,
829 STATUS_SEARCHING,
830 STATUS_UNKNOWN,
831 STATUS_SAT,
832 STATUS_UNSAT,
833 STATUS_INTERRUPTED,
834 STATUS_ERROR, // not used by the context operations/only by yices_api
835 } smt_status_t;
836 #endif
837
838 #define NUM_SMT_STATUSES (STATUS_ERROR+1)
839
840 /*
841 * Optional features: stored as bits in the solver option_flag
842 * - clean_interrupt: if this bit is set, the current state is saved
843 * on a call to start_search. This allows the solver to return
844 * to a clean state if stop_search() is called.
845 * - push_pop: if this bit is set, push and pop are supported, otherwise
846 * they are not.
847 * These options are set when the solver is created by giving a mode
848 * - INTERACTIVE enables both clean_interrupt and push_pop
849 * - PUHSPOP enables push_pop but disables clean_interrupt
850 * - BASIC disables clean_interrupt and push_pop
851 *
852 * Disabling push_pop and clean_interrupt results in more thorough clause
853 * simplification at the base_level, by ensuring base_level is always 0.
854 * This should improve performance.
855 */
856 typedef enum smt_mode {
857 SMT_MODE_BASIC,
858 SMT_MODE_PUSHPOP,
859 SMT_MODE_INTERACTIVE,
860 } smt_mode_t;
861
862 // bit masks
863 #define CLEAN_INTERRUPT_MASK (0x1)
864 #define PUSH_POP_MASK (0x2)
865
866
867 /*
868 * The clause database is divided into:
869 * - a vector of problem clauses
870 * - a vector of learned clauses
871 * unit and binary clauses are stored implicitly:
872 * - unit clauses are just literals in the assignment stack
873 * - binary clauses are stored in the binary watch vectors
874 *
875 * To support push/pop, we keep a copy of all binary clauses added at base_level>0.
876 *
877 * Propagation structures: for every literal l
878 * - bin[l] = literal vector for binary clauses
879 * - watch[l] = list of clauses where l is a watched literal
880 * (i.e., clauses where l occurs in position 0 or 1)
881 * - optional: end_watch[l] = pointer to the last element in the watch list of l
882 * end_watch is used if USE_END_WATCH is set a compilation time
883 *
884 * For every variable x between 0 and nb_vars - 1
885 * - antecedent[x]: antecedent type and value
886 * - level[x]: decision level (only meaningful if x is assigned)
887 * - mark[x]: 1 bit used in UIP computation
888 * - value[x] = current assignment
889 * value ranges from -1 to nbvars - 1 so that value[x] exists when x = null_bvar = -1
890 * value[-1] is always set to VAL_UNDEF_FALSE
891 *
892 * Assignment stack
893 *
894 * Variable heap
895 *
896 * Conflict data:
897 * - inconsistent is set to true when a conflict is detected
898 * - there are three types of conflicts:
899 * - a binary clause { l1, l2 } is false in the current assignment
900 * - a non-binary clause cl = { l1, ..., l_n } is false
901 * - the theory solver reports a conflict a = { l1, ..., l_n}
902 * - in all three cases, conflict points to an array of false literals,
903 * terminated by either end_clause/null_literal or end_learned.
904 * - false_clause and theory_conflict are set to indicate the conflict type.
905 * - for a binary clause:
906 * l1, l2, end_clause are copied into the auxiliary array conflict_buffer
907 * conflict points to conflict_buffer
908 * theory_conflict is false
909 * false_clause is NULL
910 * - for a non-binary clause conflict cl
911 * conflict points to cl->cl
912 * theory_conflict is false
913 * false_clause is set to cl
914 * - for a theory conflict a:
915 * conflict is set to a
916 * theory_conflict is true
917 * false_clause is NULL
918 *
919 * Theory-clause caching heuristics:
920 * - optionally, small theory conflicts and theory explanations can be turned
921 * into learned clauses (as a side effect of conflict resolution).
922 * - this feature is enabled by setting the flag theory_cache to true
923 * - if th_cache is true, th_cache_cl_size specifies which
924 * conflicts/explanations are considered (i.e., if they contain at most
925 * th_cache_cl_size literals, they are turned into clauses).
926 *
927 * Solving with assumptions:
928 * - we can optionally solve the problem under assumptions
929 * - the assumptions literals l_1 .... l_n
930 * - we store them in an assumptions array
931 * - we want to force the search tree to explore only the branches
932 * where l_1 ... l_n are all true
933 * - to do this, we force the n first decisions to be
934 * l_1 = true, ..., l_n = true.
935 * - there's a conflict when we can't make such a decision
936 * (i.e., l_i is forced to false by previous assumptions).
937 *
938 * We can then build an unsat core by keeping track of this l_i.
939 * We store it in core->bad_assumption. If there's no conflict,
940 * code->bad_assumption is null_literal.
941 */
942 typedef struct smt_core_s {
943 /* Theory solver */
944 void *th_solver; // pointer to the theory solver
945 th_ctrl_interface_t th_ctrl; // control functions
946 th_smt_interface_t th_smt; // SMT-specific operations
947 bool bool_only; // true means no theory propagation required
948
949 /* Status */
950 int32_t status;
951
952 /* Option flags */
953 uint32_t option_flag;
954
955 /* Problem size */
956 uint32_t nvars; // Number of variables
957 uint32_t nlits; // Number of literals = twice the number of variables
958 uint32_t vsize; // Size of the variable arrays (>= nb_vars)
959 uint32_t lsize; // Size of the literal arrays (>= nb_lits)
960
961 uint32_t nb_clauses; // Number of clauses with at least 3 literals (problem + learned clauses)
962 uint32_t nb_prob_clauses; // Number of (non-hidden) problem clauses
963 uint32_t nb_bin_clauses; // Number of binary clauses
964 uint32_t nb_unit_clauses; // Number of unit clauses
965
966 /* Counters for simplify DB */
967 uint32_t simplify_bottom; // stack top pointer after last simplify_clause_database
968 uint64_t simplify_props; // value of propagation counter at that point
969 uint64_t simplify_threshold; // number of propagations before simplify is enabled again
970
971 uint64_t aux_literals; // temporary counter used by simplify_clause
972 uint32_t aux_clauses; // temporary counter used by simplify_clause
973
974 /* Current decision level */
975 uint32_t decision_level;
976 uint32_t base_level; // Incremented on push/decremented on pop
977
978 /* Activity increments and decays for learned clauses */
979 float cla_inc; // Clause activity increment
980 float inv_cla_decay; // Inverse of clause decay (e.g., 1/0.999)
981
982 /* Randomness parameter */
983 uint32_t prng; // state of the pseudo random number generator
984 uint32_t scaled_random; // 0x1000000 * random_factor
985
986 /* Theory cache parameters */
987 bool th_cache_enabled; // true means caching enabled
988 uint32_t th_cache_cl_size; // max. size of cached clauses
989
990 /* Conflict data */
991 bool inconsistent;
992 bool theory_conflict;
993 literal_t conflict_buffer[4];
994 literal_t *conflict;
995 clause_t *false_clause;
996 uint32_t th_conflict_size; // number of literals in theory conflicts
997
998 /* Assumptions */
999 bool has_assumptions;
1000 uint32_t num_assumptions;
1001 uint32_t assumption_index;
1002 const literal_t *assumptions;
1003 literal_t bad_assumption;
1004
1005 /* Auxiliary buffers for conflict resolution */
1006 ivector_t buffer;
1007 ivector_t buffer2;
1008
1009 /* Buffer for expanding theory explanations */
1010 ivector_t explanation;
1011
1012 /* Clause database */
1013 clause_t **problem_clauses;
1014 clause_t **learned_clauses;
1015
1016 ivector_t binary_clauses; // Keeps a copy of binary clauses added at base_levels>0
1017
1018 /* Variable-indexed arrays (of size vsize) */
1019 uint8_t *value;
1020 antecedent_t *antecedent;
1021 uint32_t *level;
1022 byte_t *mark; // bitvector: for conflict resolution
1023
1024 /* Literal-indexed arrays (of size lsize) */
1025 literal_t **bin; // array of literal vectors
1026 link_t *watch; // array of watch lists
1027
1028 /* Stack/propagation queue */
1029 prop_stack_t stack;
1030
1031 /* Heap */
1032 var_heap_t heap;
1033
1034 /* Lemma queue */
1035 lemma_queue_t lemmas;
1036
1037 /* Statistics */
1038 dpll_stats_t stats;
1039
1040 /* Atom table */
1041 atom_table_t atoms;
1042
1043 /* Table of logical gates */
1044 gate_table_t gates;
1045
1046 /* Push/pop stack */
1047 trail_stack_t trail_stack;
1048
1049 /* Checkpoints */
1050 checkpoint_stack_t checkpoints;
1051 bool cp_flag; // set true when backtracking. false when checkpoints are added
1052
1053 /* EXPERIMENTAL (default to NULL) */
1054 booleq_table_t *etable;
1055
1056 /* Tracer object (default to NULL) */
1057 tracer_t *trace;
1058
1059 bool interrupt_push;
1060 } smt_core_t;
1061
1062
1063 /*
1064 * Initial size of buffer, buffer2, and explanation vectors
1065 */
1066 #define DEF_LBUFFER_SIZE 40
1067
1068
1069 /*
1070 * Default values for the clause/variable activity increment
1071 * - before smt_process returns, all activities are multiplied
1072 * by the decay factor
1073 * - when a variable or clause activity increases above the
1074 * activity threshold, then all activities are rescaled to
1075 * prevent overflow
1076 */
1077 #define VAR_DECAY_FACTOR 0.95
1078 #define VAR_ACTIVITY_THRESHOLD (1e100)
1079 #define INV_VAR_ACTIVITY_THRESHOLD (1e-100)
1080 #define INIT_VAR_ACTIVITY_INCREMENT 1.0
1081
1082 #define CLAUSE_DECAY_FACTOR (0.999F)
1083 #define CLAUSE_ACTIVITY_THRESHOLD (1e20F)
1084 #define INV_CLAUSE_ACTIVITY_THRESHOLD (1e-20F)
1085 #define INIT_CLAUSE_ACTIVITY_INCREMENT (1.0F)
1086
1087
1088 /*
1089 * Parameters for removing irrelevant learned clauses
1090 * (zchaff-style).
1091 */
1092 #define TAIL_RATIO 16
1093 #define HEAD_ACTIVITY 500
1094 #define TAIL_ACTIVITY 10
1095 #define HEAD_RELEVANCE 6
1096 #define TAIL_RELEVANCE 45
1097
1098
1099 /*
1100 * Default random_factor = 2% of decisions are random (more or less)
1101 * - the heuristic generates a random 24 bit integer
1102 * - if that number is <= random_factor * 2^24, then a random variable
1103 * is chosen
1104 * - so we store random_factor * 2^24 = random_factor * 0x1000000 in
1105 * the scaled_random field of an smt_core
1106 */
1107 #define VAR_RANDOM_FACTOR 0.02F
1108
1109 // mask to extract 24 bits out of an unsigned 32bit integer
1110 #define VAR_RANDOM_MASK ((uint32_t)0xFFFFFF)
1111 #define VAR_RANDOM_SCALE (VAR_RANDOM_MASK+1)
1112
1113
1114
1115
1116 /************************
1117 * GENERIC OPERATIONS *
1118 ***********************/
1119
1120 /*
1121 * Initialize an smt solver
1122 * - n = initial vsize = size of the variable-indexed arrays
1123 * - th = theory solver
1124 * - ctrl = descriptor of control functions for th
1125 * - smt = descriptor of the SMT functions for th
1126 * - mode = to select optional features
1127 * This creates the predefined "constant" variable and the true/false literals
1128 *
1129 * The clause and variable activity increments, and the randomness
1130 * parameters are set to their default values
1131 */
1132 extern void init_smt_core(smt_core_t *s, uint32_t n, void *th,
1133 th_ctrl_interface_t *ctrl, th_smt_interface_t *smt,
1134 smt_mode_t mode);
1135
1136
1137 /*
1138 * Set the bool_only flag (this an optimization for pure bitvector problems)
1139 * - if this flag is set, there's no theory propagation
1140 */
smt_core_set_bool_only(smt_core_t * s)1141 static inline void smt_core_set_bool_only(smt_core_t *s) {
1142 s->bool_only = true;
1143 }
1144
1145 /*
1146 * Replace the theory solver and interface descriptors
1147 * - this can used provided no atom/clause has been added yet
1148 */
1149 extern void smt_core_reset_thsolver(smt_core_t *s, void *th, th_ctrl_interface_t *ctrl,
1150 th_smt_interface_t *smt);
1151
1152
1153 /*
1154 * Delete: free all allocated memory
1155 */
1156 extern void delete_smt_core(smt_core_t *s);
1157
1158
1159 /*
1160 * Reset: remove all variables, atoms, and clauses
1161 * - also calls reset on the attached theory solver
1162 */
1163 extern void reset_smt_core(smt_core_t *s);
1164
1165
1166 /*
1167 * Attach a tracer object:
1168 * - s->trace must be NULL
1169 */
1170 extern void smt_core_set_trace(smt_core_t *s, tracer_t *tracer);
1171
1172
1173 /*
1174 * EXPERIMENTAL: create the etable
1175 */
1176 extern void smt_core_make_etable(smt_core_t *s);
1177
1178
1179 /*
1180 * EXPERIMENTAL: record l = (xor a b)
1181 * - call smt_core_make_etable first
1182 */
1183 extern void smt_core_record_xor_def(smt_core_t *s, literal_t l, literal_t a, literal_t b);
1184
1185
1186
1187 /*
1188 * Start a new base level
1189 * - keep track of the current set of variables, atoms, and clauses
1190 * - subsequent call to smt_pop restore s to that state
1191 * Push must not be called if a search is under way or if s has status UNSAT or INTERRUPTED
1192 * or if push_pop is disabled.
1193 *
1194 * If s->status is UNKNOWN or SAT, then the current boolean assignment is cleared
1195 * and s->status is reset to IDLE.
1196 */
1197 extern void smt_push(smt_core_t *s);
1198
1199
1200 /*
1201 * Restore to the saved state on top of the trail_stack
1202 * - remove all learned_clauses
1203 * - remove all clauses, variable, and atoms created at the current base_level
1204 * - reset status to IDLE
1205 * - must not be called if the trail_stack is empty (no push) or if
1206 * status is SEARCHING or INTERRUPTED
1207 */
1208 extern void smt_pop(smt_core_t *s);
1209
1210
1211 /*
1212 * Set the activity increment parameters
1213 * - decay_factor must be a floating point number between 0 and 1.0
1214 */
1215 extern void set_var_decay_factor(smt_core_t *s, double factor);
1216 extern void set_clause_decay_factor(smt_core_t *s, float factor);
1217
1218 /*
1219 * Set the randomness parameter used by the default variable
1220 * selection heuristic: random_factor must be a floating point
1221 * number between 0 and 1.0.
1222 */
1223 extern void set_randomness(smt_core_t *s, float random_factor);
1224
1225
1226 /*
1227 * Set the pseudo random number generator seed
1228 */
1229 extern void set_random_seed(smt_core_t *s, uint32_t seed);
1230
1231
1232 /*
1233 * Activate theory-clause caching
1234 * - cl_size = max size of clauses to be cached
1235 */
enable_theory_cache(smt_core_t * s,uint32_t cl_size)1236 static inline void enable_theory_cache(smt_core_t *s, uint32_t cl_size) {
1237 s->th_cache_enabled = true;
1238 s->th_cache_cl_size = cl_size;
1239 }
1240
1241 /*
1242 * Disable theory-clause caching
1243 */
disable_theory_cache(smt_core_t * s)1244 static inline void disable_theory_cache(smt_core_t *s) {
1245 s->th_cache_enabled = false;
1246 }
1247
1248
1249 /*
1250 * Read the current decision level
1251 */
smt_decision_level(smt_core_t * s)1252 static inline uint32_t smt_decision_level(smt_core_t *s) {
1253 return s->decision_level;
1254 }
1255
1256 /*
1257 * Read the current base level
1258 */
smt_base_level(smt_core_t * s)1259 static inline uint32_t smt_base_level(smt_core_t *s) {
1260 return s->base_level;
1261 }
1262
1263 /*
1264 * Read the status
1265 */
smt_status(smt_core_t * s)1266 static inline smt_status_t smt_status(smt_core_t *s) {
1267 return s->status;
1268 }
1269
1270 /*
1271 * Read the heuristic parameters
1272 */
var_decay_factor(smt_core_t * s)1273 static inline double var_decay_factor(smt_core_t *s) {
1274 return 1/s->heap.inv_act_decay;
1275 }
1276
clause_decay_factor(smt_core_t * s)1277 static inline double clause_decay_factor(smt_core_t *s) {
1278 return 1/s->inv_cla_decay;
1279 }
1280
randomness_factor(smt_core_t * s)1281 static inline double randomness_factor(smt_core_t *s) {
1282 return ((double) s->scaled_random)/ VAR_RANDOM_SCALE;
1283 }
1284
1285
1286
1287 /*
1288 * Read the search statistics
1289 */
num_restarts(smt_core_t * s)1290 static inline uint32_t num_restarts(smt_core_t *s) {
1291 return s->stats.restarts;
1292 }
1293
num_simplify_calls(smt_core_t * s)1294 static inline uint32_t num_simplify_calls(smt_core_t *s) {
1295 return s->stats.simplify_calls;
1296 }
1297
num_reduce_calls(smt_core_t * s)1298 static inline uint32_t num_reduce_calls(smt_core_t *s) {
1299 return s->stats.reduce_calls;
1300 }
1301
num_remove_calls(smt_core_t * s)1302 static inline uint32_t num_remove_calls(smt_core_t *s) {
1303 return s->stats.remove_calls;
1304 }
1305
num_decisions(smt_core_t * s)1306 static inline uint64_t num_decisions(smt_core_t *s) {
1307 return s->stats.decisions;
1308 }
1309
num_random_decisions(smt_core_t * s)1310 static inline uint64_t num_random_decisions(smt_core_t *s) {
1311 return s->stats.random_decisions;
1312 }
1313
num_propagations(smt_core_t * s)1314 static inline uint64_t num_propagations(smt_core_t *s) {
1315 return s->stats.propagations;
1316 }
1317
num_conflicts(smt_core_t * s)1318 static inline uint64_t num_conflicts(smt_core_t *s) {
1319 return s->stats.conflicts;
1320 }
1321
num_theory_conflicts(smt_core_t * s)1322 static inline uint32_t num_theory_conflicts(smt_core_t *s) {
1323 return s->stats.th_conflicts;
1324 }
1325
num_theory_propagations(smt_core_t * s)1326 static inline uint32_t num_theory_propagations(smt_core_t *s) {
1327 return s->stats.th_props;
1328 }
1329
1330
1331 /*
1332 * Read the size statistics
1333 */
num_vars(smt_core_t * s)1334 static inline uint32_t num_vars(smt_core_t *s) {
1335 return s->nvars;
1336 }
1337
num_atoms(smt_core_t * s)1338 static inline uint32_t num_atoms(smt_core_t *s) {
1339 return s->atoms.natoms;
1340 }
1341
num_literals(smt_core_t * s)1342 static inline uint32_t num_literals(smt_core_t *s) {
1343 return s->nlits;
1344 }
1345
num_prob_clauses(smt_core_t * s)1346 static inline uint32_t num_prob_clauses(smt_core_t *s) {
1347 return get_cv_size(s->problem_clauses);
1348 }
1349
num_prob_literals(smt_core_t * s)1350 static inline uint64_t num_prob_literals(smt_core_t *s) {
1351 return s->stats.prob_literals;
1352 }
1353
1354 // this is either 0 or 1
num_empty_clauses(smt_core_t * s)1355 static inline uint32_t num_empty_clauses(smt_core_t *s) {
1356 return s->inconsistent;
1357 }
1358
num_unit_clauses(smt_core_t * s)1359 static inline uint32_t num_unit_clauses(smt_core_t *s) {
1360 return s->nb_unit_clauses;
1361 }
1362
num_binary_clauses(smt_core_t * s)1363 static inline uint32_t num_binary_clauses(smt_core_t *s) {
1364 return s->nb_bin_clauses;
1365 }
1366
num_learned_clauses(smt_core_t * s)1367 static inline uint32_t num_learned_clauses(smt_core_t *s) {
1368 return get_cv_size(s->learned_clauses);
1369 }
1370
num_learned_literals(smt_core_t * s)1371 static inline uint64_t num_learned_literals(smt_core_t *s) {
1372 return s->stats.learned_literals;
1373 }
1374
1375 // all clauses
num_clauses(smt_core_t * s)1376 static inline uint32_t num_clauses(smt_core_t *s) {
1377 return num_empty_clauses(s) + num_unit_clauses(s) + num_binary_clauses(s) +
1378 num_prob_clauses(s) + num_learned_clauses(s);
1379 }
1380
1381 // average size of the learned clauses
1382 extern double avg_learned_clause_size(smt_core_t *core);
1383
1384
1385
1386
1387 /************************************
1388 * VARIABLES, LITERALS, AND ATOMS *
1389 ***********************************/
1390
1391 /*
1392 * Create a fresh variable and return its index
1393 * - the index is x = s->nvars
1394 *
1395 * Initialization:
1396 * - antecedent[x] = NULL
1397 * - level[x] not initialized
1398 * - mark[x] = 0
1399 * - polarity[x] = 0 (negative polarity preferred)
1400 * - activity[x] = 0 (in heap)
1401 *
1402 * For l=pos_lit(x) or neg_lit(x):
1403 * - value[l] = VAL_UNDEF
1404 * - bin[l] = NULL
1405 * - watch[l] = NULL
1406 */
1407 extern bvar_t create_boolean_variable(smt_core_t *s);
1408
1409 /*
1410 * Add n fresh boolean variables: the new indices are allocated starting
1411 * from s->nvars (i.e., if s->nvars == v before the call, the
1412 * new variables have indices v, v+1, ... v+n-1).
1413 */
1414 extern void add_boolean_variables(smt_core_t *s, uint32_t n);
1415
1416 /*
1417 * Attach atom a to boolean variable x
1418 * - x must not have an atom attached already
1419 */
1420 extern void attach_atom_to_bvar(smt_core_t *s, bvar_t x, void *atom);
1421
1422 /*
1423 * Remove atom attached to x (no effect if x doesn't have an atom)
1424 */
1425 extern void remove_bvar_atom(smt_core_t *s, bvar_t x);
1426
1427
1428 /*
1429 * Check whether x has an atom attached
1430 */
1431 extern bool bvar_has_atom(smt_core_t *s, bvar_t x);
1432
1433
1434 /*
1435 * Get the atom attached to x (NULL if x has no atom attached)
1436 */
1437 extern void *bvar_atom(smt_core_t *s, bvar_t x);
1438
1439
1440 /*
1441 * Faster than bvar_atom, but requires bvar_has_atom(s, x) to be true
1442 */
get_bvar_atom(smt_core_t * s,bvar_t x)1443 static inline void *get_bvar_atom(smt_core_t *s, bvar_t x) {
1444 assert(bvar_has_atom(s, x));
1445 return s->atoms.atom[x];
1446 }
1447
1448
1449 /*
1450 * Antecedent of x
1451 */
get_bvar_antecedent(smt_core_t * s,bvar_t x)1452 static inline antecedent_t get_bvar_antecedent(smt_core_t *s, bvar_t x) {
1453 assert(0 <= x && x < s->nvars);
1454 return s->antecedent[x];
1455 }
1456
1457
1458 /*
1459 * Set the initial activity of variable x.
1460 * This determines the initial variable ordering in the decision heuristics.
1461 * By default, all variables have the same initial activity, namely, 0.0
1462 */
1463 extern void set_bvar_activity(smt_core_t *s, bvar_t x, double a);
1464
1465 /*
1466 * Read variable current activity
1467 */
get_bvar_activity(smt_core_t * s,bvar_t x)1468 static inline double get_bvar_activity(smt_core_t *s, bvar_t x) {
1469 assert(0 <= x && x < s->nvars);
1470 return s->heap.activity[x];
1471 }
1472
1473
1474
1475 /*************************
1476 * MODEL CONSTRUCTION *
1477 ************************/
1478
1479 /*
1480 * Check whether variable x is assigned
1481 */
bvar_is_assigned(const smt_core_t * s,bvar_t x)1482 static inline bool bvar_is_assigned(const smt_core_t *s, bvar_t x) {
1483 assert(0 <= x && x < s->nvars);
1484 return bval_is_def(s->value[x]);
1485 }
1486
bvar_is_unassigned(const smt_core_t * s,bvar_t x)1487 static inline bool bvar_is_unassigned(const smt_core_t *s, bvar_t x) {
1488 assert(0 <= x && x < s->nvars);
1489 return bval_is_undef(s->value[x]);
1490 }
1491
1492 /*
1493 * Same thing for literal l
1494 */
literal_is_assigned(const smt_core_t * s,literal_t l)1495 static inline bool literal_is_assigned(const smt_core_t *s, literal_t l) {
1496 return bvar_is_assigned(s, var_of(l));
1497 }
1498
literal_is_unassigned(const smt_core_t * s,literal_t l)1499 static inline bool literal_is_unassigned(const smt_core_t *s, literal_t l) {
1500 return bvar_is_unassigned(s, var_of(l));
1501 }
1502
1503
1504 /*
1505 * Read the value assigned to variable x at the current decision level.
1506 * This can be used to build a model if s->status is SAT (or UNKNOWN).
1507 */
bvar_value(const smt_core_t * s,bvar_t x)1508 static inline bval_t bvar_value(const smt_core_t *s, bvar_t x) {
1509 assert(0 <= x && x < s->nvars);
1510 return s->value[x];
1511 }
1512
1513
1514 /*
1515 * Read the value assigned to a variable x at the base level
1516 * - if x is not assigned at the base level, this returns the
1517 * preferred value (either VAL_UNDEF_FALSE or VAL_UNDEF_TRUE)
1518 */
bvar_base_value(const smt_core_t * s,bvar_t x)1519 static inline bval_t bvar_base_value(const smt_core_t *s, bvar_t x) {
1520 bval_t v;
1521 assert(0 <= x && x < s->nvars);
1522 v = s->value[x];
1523 if (s->level[x] > s->base_level) {
1524 v &= 1; // clear bit 1, keep bit 0
1525 assert(bval_is_undef(v));
1526 }
1527 return v;
1528 }
1529
1530 /*
1531 * Get the polarity bit of x = low-order bit of value[x]
1532 * - if x is assigned, polarity = current value (0 means true, 1 means false)
1533 * - if x is unassigned, polarity = preferred value
1534 */
bvar_polarity(const smt_core_t * s,bvar_t x)1535 static inline uint32_t bvar_polarity(const smt_core_t *s, bvar_t x) {
1536 assert(0 <= x && x < s->nvars);
1537 return (uint32_t) (s->value[x] & 1);
1538 }
1539
1540
1541 /*
1542 * Read the value assigned to literal l at the current decision level
1543 * - let x var_of(l) then
1544 * - if sign_of(l) = 0, val(l) = val(x)
1545 * if sign_of(l) = 1, val(l) = opposite of val(x)
1546 * - returns VAL_UNDEF_TRUE or VAL_UNDEF_FALSE if no value is assigned.
1547 */
literal_value(const smt_core_t * s,literal_t l)1548 static inline bval_t literal_value(const smt_core_t *s, literal_t l) {
1549 assert(0 <= l && l < (int32_t) s->nlits);
1550 return s->value[var_of(l)] ^ sign_of_lit(l);
1551 }
1552
1553 /*
1554 * Read the value assigned to a literal l at the base level
1555 * - returns VAL_UNDEF_FALSE or VAL_UNDEF_TRUE if l is not assigned at that level
1556 */
literal_base_value(const smt_core_t * s,literal_t l)1557 static inline bval_t literal_base_value(const smt_core_t *s, literal_t l) {
1558 assert(0 <= l && l < s->nlits);
1559 return bvar_base_value(s, var_of(l)) ^ sign_of_lit(l);
1560 }
1561
1562
1563 /*
1564 * Get all true literals in the current assignment: copy them into vector v
1565 * - they are stored in chronological order
1566 * - the constant "true_literal" is not put in v
1567 */
1568 extern void collect_true_literals(smt_core_t *s, ivector_t *v);
1569
1570
1571 /*
1572 * Get the decision literals in the current assignment: copy them into vector v
1573 */
1574 extern void collect_decision_literals(smt_core_t *s, ivector_t *v);
1575
1576
1577 /*
1578 * Import a model from an external solver
1579 * - this sets the value of a boolean variable b
1580 */
1581 extern void set_bvar_value(smt_core_t *s, bvar_t x, bval_t val);
1582
1583 /*
1584 * Set the core status
1585 */
set_smt_status(smt_core_t * s,smt_status_t status)1586 static inline void set_smt_status(smt_core_t *s, smt_status_t status) {
1587 s->status = status;
1588 }
1589
1590 /*
1591 * Check whether the core is trivially SAT
1592 * - i.e., check whether there are no problem clauses
1593 */
1594 extern bool smt_trivially_sat(smt_core_t *s);
1595
1596 /*
1597 * Search for a satisfiable assignment.
1598 * - stop on the first conflict and return false
1599 * - return true if all Boolean variables are assigned.
1600 * Restrictions:
1601 * - s->status must be SEARCHING
1602 * - s must be purely Boolean.
1603 */
1604 extern bool smt_easy_sat(smt_core_t *s);
1605
1606
1607 /*********************
1608 * CLAUSE ADDITION *
1609 ********************/
1610
1611 /*
1612 * Clauses are simplified before being added:
1613 * - literals false at the base level are removed
1614 * - duplicate literals are removed
1615 * - a clause trivially true (either because it contains complementary
1616 * literals or a literal true at the base level) is ignored.
1617 *
1618 * The general form is add_clause(s, n, a) where a is an array of n literals.
1619 *
1620 * Special forms are provided for unit, binary, and ternary clauses (also
1621 * for the empty clause).
1622 *
1623 * Clauses can be added before the search, when s->status is STATUS_IDLE
1624 * or on-the-fly, when s->status is STATUS_SEARCHING.
1625 *
1626 * If s->status is SEARCHING and s->decision_level > s->base_level,
1627 * then the clause is a not added immediately, it's copied into the
1628 * lemma queue.
1629 */
1630 extern void add_empty_clause(smt_core_t *s);
1631 extern void add_unit_clause(smt_core_t *s, literal_t l);
1632 extern void add_binary_clause(smt_core_t *s, literal_t l1, literal_t l2);
1633 extern void add_ternary_clause(smt_core_t *s, literal_t l1, literal_t l2, literal_t l3);
1634
1635 extern void add_clause(smt_core_t *s, uint32_t n, literal_t *a);
1636
1637
1638 /******************************
1639 * ACCESS TO THE GATE TABLE *
1640 *****************************/
1641
get_gate_table(smt_core_t * s)1642 static inline gate_table_t *get_gate_table(smt_core_t *s) {
1643 return &s->gates;
1644 }
1645
1646
1647 /***********************
1648 * SEARCH PROCEDURES *
1649 **********************/
1650
1651 /*
1652 * Start a new round of assertions
1653 * - this is called before base_propagate or any other function
1654 * creating atoms, clauses, etc.
1655 * - this propagates to the theory solver.
1656 * - the current status must be IDLE and it remains IDLE.
1657 */
1658 extern void internalization_start(smt_core_t *s);
1659
1660
1661 /*
1662 * Propagation at the base-level:
1663 * - the current status must be IDLE
1664 * - this performs one round of propagation
1665 * Return true if no conflict is detected, false otherwise.
1666 * The status is updated to UNSAT if there's a conflict.
1667 * It remains IDLE otherwise.
1668 *
1669 * Warning: this is called before start_search.
1670 */
1671 extern bool base_propagate(smt_core_t *s);
1672
1673
1674 /*
1675 * Prepare for the search
1676 * - a = optional array of assumptions
1677 * - n = number of assumptions
1678 * - a[0 ... n-1] must all be valid literals in the core
1679 *
1680 * Effect:
1681 * - initialize variable heap
1682 * - store a pointer to the assumption array
1683 * - set status to SEARCHING
1684 * - reset the search statistics counters
1685 * - if clean_interrupt is enabled, save the current state to
1686 * enable cleanup after interrupt (this uses push)
1687 * The current status must be IDLE.
1688 */
1689 extern void start_search(smt_core_t *s, uint32_t n, const literal_t *a);
1690
1691
1692 /*
1693 * Stop the search:
1694 * - if s->status is SEARCHING, this sets status to INTERRUPTED
1695 * otherwise, this has no effect.
1696 * - this can be called from a signal handler to interrupt the solver
1697 * - if clean_interrupt is enabled, the state at start_search can be restored by
1698 * calling smt_cleanup
1699 */
1700 extern void stop_search(smt_core_t *s);
1701
1702
1703 /*
1704 * Perform a (branching) decision: assign l to true
1705 * - s->status must be SEARCHING
1706 * - l must be an unassigned literal
1707 * - the decision level is incremented and l is pushed on the
1708 * propagation stack with empty antecedent.
1709 */
1710 extern void decide_literal(smt_core_t *s, literal_t l);
1711
1712
1713 /*
1714 * Cause a restart: backtrack to the base_level
1715 * - s->status must be SEARCHING
1716 */
1717 extern void smt_restart(smt_core_t *s);
1718
1719
1720 /*
1721 * Variant of restart: attempt to reuse the assignment trail
1722 * - find the unassigned variable x of highest activity
1723 * - keep all current decisions that have a higher activity than x
1724 */
1725 extern void smt_partial_restart(smt_core_t *s);
1726
1727
1728 /*
1729 * Another variant of restart: attempt to reuse the assignment trail
1730 * - find the unassigned variable x of highest activity
1731 * - keep all current decision levels that have at least one
1732 * variable with a higher activity than x
1733 */
1734 extern void smt_partial_restart_var(smt_core_t *s);
1735
1736
1737 /*
1738 * Reduce the clause database by removing half the learned clauses
1739 * (the ones with lowest activities)
1740 */
1741 extern void reduce_clause_database(smt_core_t *s);
1742
1743
1744 /*
1745 * Reduce the clause database by remove large clauses with low activity
1746 * (complicated Zchaff/Berkmin-style heuristic)
1747 */
1748 extern void remove_irrelevant_learned_clauses(smt_core_t *s);
1749
1750
1751 /*
1752 * Set a checkpoint: this records the current decision_level and
1753 * number of variables.
1754 * - if the solver backtracks to this or a smaller decision level,
1755 * then all variables (and atoms) created after this checkpoints
1756 * are removed (well not quite!)
1757 * - any clause that contains a removed variable is also deleted
1758 */
1759 extern void smt_checkpoint(smt_core_t *s);
1760
1761
1762 /*
1763 * Main solving function: process until a stable state is reached
1764 * - a state with status UNSAT or INTERRUPTED is stable
1765 * - a state with status SEARCHING is stable if there's nothing
1766 * to propagate and no lemmas to process, and if there's no conflict
1767 * - from a stable state with status SEARCHING,
1768 * one can add lemmas and call process again
1769 * or select a decision literal and call process again
1770 * or close the state (mark it as SAT or UNKNOWN)
1771 *
1772 * smt_process executes the following code:
1773 *
1774 * repeat
1775 * if there's a conflict
1776 * try to resolve the conflict
1777 * if we can't resolve it
1778 * change status to UNSAT and exit
1779 * else
1780 * decay variable and clause activities
1781 * endif
1782 * elsif checkpoint-based garbage collection is possible
1783 * do the garbage collection
1784 * elsif lemmas are present then
1785 * integrate them to the clause database
1786 * else
1787 * perform boolean and theory propagation
1788 * if propagation finds no conflict and doesn't add lemmas
1789 * if decision_level == base_level
1790 * simplify the clause database
1791 * endif
1792 * exit the loop
1793 * endif
1794 * endif
1795 * end repeat
1796 *
1797 */
1798 extern void smt_process(smt_core_t *s);
1799
1800
1801 /*
1802 * Variant of smt_process with a conflict bound.
1803 *
1804 * After a conflict is resolved, this function checks whether the
1805 * total number of conflicts so far exceeds max_conflicts. If so
1806 * it exits.
1807 *
1808 * The returned value indicates whether this function exited in
1809 * a stable state or on an early exit:
1810 * - true means state state reached
1811 * - false means max_conflicts reached.
1812 *
1813 * If this function returns false, the caller can't assume that
1814 * it is safe to make a decision.
1815 */
1816 extern bool smt_bounded_process(smt_core_t *s, uint64_t max_conflicts);
1817
1818
1819 /*
1820 * Check for delayed theory solving:
1821 * - call the final_check function of the theory solver
1822 * - if the theory solver creates new variables or lemmas or report a conflict
1823 * then smt_process is called
1824 * - otherwise the core status is updated to SAT or UNKNOWN and the search
1825 * is done.
1826 */
1827 extern void smt_final_check(smt_core_t *s);
1828
1829
1830
1831 /*
1832 * Propagation function for the theory solver
1833 * - assign l to true with the given explanation as antecedent.
1834 * - l must not be assigned already.
1835 */
1836 extern void propagate_literal(smt_core_t *s, literal_t l, void *expl);
1837
1838
1839 /*
1840 * For the theory solver: record a conflict (a disjunction of literals is false)
1841 * - a must be an array of literals terminated by end_clause (which is
1842 * the same as null_literal).
1843 * - all literals in a must be false at the current decision level
1844 *
1845 * Warning: no copy is made. Array a should not be modified by the theory solver,
1846 * until the conflict is resolved.
1847 */
1848 extern void record_theory_conflict(smt_core_t *s, literal_t *a);
1849
1850 /*
1851 * Variants of record_theory_conflict
1852 */
1853 extern void record_empty_theory_conflict(smt_core_t *s);
1854 extern void record_unit_theory_conflict(smt_core_t *s, literal_t l);
1855 extern void record_binary_theory_conflict(smt_core_t *s, literal_t l1, literal_t l2);
1856 extern void record_ternary_theory_conflict(smt_core_t *s, literal_t l1, literal_t l2, literal_t l3);
1857
1858
1859 /*
1860 * Close the search: mark s as either SAT or UNKNOWN
1861 */
end_search_sat(smt_core_t * s)1862 static inline void end_search_sat(smt_core_t *s) {
1863 assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
1864 s->status = STATUS_SAT;
1865 }
1866
end_search_unknown(smt_core_t * s)1867 static inline void end_search_unknown(smt_core_t *s) {
1868 assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
1869 s->status = STATUS_UNKNOWN;
1870 }
1871
1872
1873 /*
1874 * If the search was interrupted, this function
1875 * restores s to what it was at the start of the search.
1876 * - remove all learned clauses and all the lemmas, variables, and atoms created
1877 * during the search.
1878 * - reset s->status to IDLE
1879 * - this must not be called if clean_interrupt is disabled.
1880 */
1881 extern void smt_cleanup(smt_core_t *s);
1882
1883
1884 /*
1885 * Clear assignment and enable addition of new clauses after a search.
1886 * - this can be called if s->status is UNKNOWN or SAT
1887 * - s->status is reset to STATUS_IDLE and the current boolean
1888 * assignment is cleared (i.e., we backtrack to the current base_level)
1889 */
1890 extern void smt_clear(smt_core_t *s);
1891
1892
1893 /*
1894 * Cleanup after the search returned unsat
1895 * - s->status must be UNSAT.
1896 * - if there are assumptions, this removes them and reset s->status
1897 * to STATUS_IDLE
1898 * - if clean_interrupt is enabled, this also restores s to its state
1899 * before the search: learned clauses are deleted, lemmas, variables
1900 * and atoms created during the search are deleted.
1901 * - if clean_interrupt is disabled and there are no assumptions,
1902 * this does nothing.
1903 *
1904 * On exit, s->status is either STATUS_UNSAT (if no assumptions
1905 * were removed) or STATUS_IDLE (if assumptions were removed).
1906 */
1907 extern void smt_clear_unsat(smt_core_t *s);
1908
1909
1910
1911 /*********************************
1912 * ASSUMPTIONS AND UNSAT CORES *
1913 ********************************/
1914
1915 /*
1916 * Get the next assumption for the current decision_level
1917 * - s->status mut be SEARCHING
1918 * - this scans the assumption array to search for an assumption
1919 * that is not already true.
1920 * - returns an assumption l or null_literal if all assumptions
1921 * are true (or if there are no assumptions)
1922 */
1923 extern literal_t get_next_assumption(smt_core_t *s);
1924
1925
1926 /*
1927 * Store l as a bad assumption:
1928 * - l must be false in s
1929 * - copy l in s->bad_assumption
1930 * - mark the context as unsat
1931 */
1932 extern void save_conflicting_assumption(smt_core_t *s, literal_t l);
1933
1934
1935 /*
1936 * Compute an unsat core:
1937 * - the core is stored as a list of literals in vector v:
1938 * (i.e., the conjunction of these literals is unsat in the current context)
1939 * - s->status must be UNSAT
1940 * - if there are no bad_assumption, an empty core is returned
1941 * - otherwise the core is build by resolving the bad_assumption's antecedents
1942 */
1943 extern void build_unsat_core(smt_core_t *s, ivector_t *v);
1944
1945
1946
1947 /**************************************
1948 * SUPPORT FOR BRANCHING HEURISTICS *
1949 *************************************/
1950
1951 /*
1952 * The default heuristic is based on variable activities +
1953 * randomization + the preferred polarity vector (picosat-style).
1954 *
1955 * The select...bvar functions can be used to implement other
1956 * heuristics.
1957 */
1958
1959 /*
1960 * Select an unassigned literal using the default decision heuristic:
1961 * - mix of activity based + randomization heuristic
1962 * - use the preferred polarity vector to decide between true/false
1963 * return null_literal if all variables are assigned.
1964 */
1965 extern literal_t select_unassigned_literal(smt_core_t *s);
1966
1967
1968 /*
1969 * Select the unassigned variable of highest activity
1970 * - return null_bvar if all variables are assigned
1971 */
1972 extern bvar_t select_most_active_bvar(smt_core_t *s);
1973
1974 /*
1975 * Randomly pick an unassigned variable (with uniform probability)
1976 * - return null_bvar if all variables are assigned.
1977 */
1978 extern bvar_t select_random_bvar(smt_core_t *s);
1979
1980 /*
1981 * Check whether all variables are assigned
1982 */
all_variables_assigned(smt_core_t * s)1983 static inline bool all_variables_assigned(smt_core_t *s) {
1984 assert(s->stack.top <= s->nvars);
1985 return s->nvars == s->stack.top;
1986 }
1987
1988 /*
1989 * Check whether all problem clauses (binary clauses + clauses with at
1990 * least three literals) are true in the current assignment.
1991 */
1992 extern bool all_clauses_true(smt_core_t *s);
1993
1994
1995 /****************************
1996 * UNCONSTRAINED VARIABLES *
1997 ***************************/
1998
1999 /*
2000 * Record to store the set of unconstrained variables:
2001 * - nvars = total number of variables
2002 * - free = array of booleans
2003 * - free[x] true means that x is unconstrained (i.e., does not occur
2004 * in any clause)
2005 */
2006 typedef struct free_bool_vars_s {
2007 uint8_t *free;
2008 uint32_t nvars;
2009 } free_bool_vars_t;
2010
2011 /*
2012 * Initialized fv structure:
2013 * - n = number of variables
2014 */
2015 extern void init_free_bool_vars(free_bool_vars_t *fv, uint32_t n);
2016
2017 /*
2018 * Delete fv
2019 */
2020 extern void delete_free_bool_vars(free_bool_vars_t *fv);
2021
2022 /*
2023 * Collect all the free variables in a solver s
2024 * - store them in fv
2025 * - fv must be initialized and large enough to store
2026 * all the variables of s
2027 */
2028 extern void collect_free_bool_vars(free_bool_vars_t *fv, const smt_core_t *s);
2029
2030
2031 #endif /* __SMT_CORE_H */
2032