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 * DATA STRUCTURES FOR THE SIMPLEX SOLVER
21 *
22 * Version 2: simplified to attempt to get close to Yices 1 solver
23 * - removed all equality atoms (x == b): they are always
24 * rewritten as (and (x <= b) (x >= b))
25 * - generate binary lemmas all the time (not optional)
26 * - removed "derived bounds". All theory propagations are direct
27 * assertions of a literal in the core.
28 * - added support for turning propagations into lemmas.
29 * - removed trichotomy lemmas/cache
30 *
31 * Version 3: 2008/11/03
32 * - put back the derived bounds and more general forms of bound
33 * propagation.
34 * - added diophantine subsolver
35 * - put back the trichotomy cache. It's now used for interfacing
36 * with the egraph.
37 */
38
39 /*
40 * Simplex solver:
41 * - a global set of linear equalities A X = 0
42 * where A is a matrix and X is the vector of variables
43 * - all atoms are of the form (x <= b) or (x >= b) where
44 * x is a variable and b is a rational constant.
45 * - strict inequalities are encoded using "extended rational":
46 * an extended rational is of the form (b + c \delta) where b and c
47 * are rationals and \delta is infinitesimal.
48 *
49 * Variable table: (cf. arith_vartable):
50 * - each variable x is stored in the simplex's variable table
51 * - the table maps x to a descriptor
52 * - variable 0 is always the constant (const_idx = 0)
53 * its descriptor is the rational 1/1 (kind = AVAR_CONST)
54 * - for all other variables, we use only two kinds of descriptors
55 * either x is a free variable (kind = AVAR_FREE)
56 * or x has a polynomial definition (kind = AVAR_POLY)
57 * We convert any rational constant to a constant polynomial before
58 * adding it to the variable table (i.e., we don't use kind = AVAR_CONST).
59 *
60 * Variable substitutions: if x's definition is a simple polynomial of
61 * the form (c + b.y) then the solver always replace x by c + b.y
62 * (rather than adding the row c - x + b.y = 0 to the matrix).
63 *
64 * Matrix/tableau:
65 * - We use a two-stage approach to building the constraints A X = 0.
66 * - The constraint matrix is built during formula internalization.
67 * It contains two types of rows:
68 * - variable definitions: rows of the form (x - p) == 0,
69 * where x := p is an entry in the variable table and p is not a
70 * simple polynomial
71 * - top-level assertions: rows of the form (p == 0) when p == 0
72 * is asserted at the toplevel
73 * - The matrix is simplified and the tableau is constructed
74 * when start_search is called.
75 *
76 * The solver maintains:
77 * - a variable assignment that maps X to extended rationals
78 * - a queue/stack of asserted or derived constraints
79 * - each constraint in the queue is either (x <= u) or (x >= l)
80 * where u and l are extended rationals
81 * - each constraint has an explanation
82 *
83 * For each variable x, we keep track of the current lower and upper bounds for x
84 *
85 */
86
87 /*
88 * Processing of assertions/bounds
89 * -------------------------------
90 * There are two stacks: a stack of assertions and a constraint (or bound) stack.
91 * Assertions are arithmetic atoms or negation of arithmetic atoms. Each assertion
92 * is identified by the atom id and a polarity bit (1 for negation).
93 * Assertions are pushed onto the assertion stack when the core calls
94 * simplex_assert_atom(.., l) where l is a literal. The bound stack maintains the
95 * current lower and upper bound on each variable.
96 *
97 * Then simplex_propagate does the following operations:
98 *
99 * 1) Process_assertions: visit all assertions on the assertion stack
100 * - if an assertion i conflicts with an existing bound then a conflict is reported,
101 * and simplex_propagate exits.
102 * (Example: i is (x >= a) and current upper bound on x is smaller than a.)
103 * - if an assertion i is redundant, it's skipped.
104 * (Example: i is (x >= a) and current lower bound on x is larger than or equal to a).
105 * - otherwise, a new bound for x is pushed onto the bound stack.
106 *
107 * 2) If process_assertions does not detect a conflict, update the variable assignment:
108 * Visit all the constraints added to the bound-stack during process_assertions.
109 * Update the assignment to ensure that all non-basic variables are within their bounds,
110 * collect the basic variables that are not within their bounds.
111 *
112 * 3) Check feasibility using simplex.
113 *
114 * 4) Optional: search for implied bounds (simplex-propagation)
115 * If no conflict is found by step 1 or 3:
116 * - add more bounds to the bound stacks (implied bounds).
117 * - if integer variables are present, theory propagation may detect
118 * conflicts or invalidate the current assignment (i.e.. val[x] no longer
119 * between lb[x] and ub[x] because the bounds are strengthened).
120 * - if theory_propagation does not find a conflict but the current assignment is
121 * invalid, attempt to correct it: make sure all non-basic variables are within
122 * their bounds then call make_feasible again.
123 *
124 * 5) Find implied literals and propagate them to the core.
125 * If no conflict is found in steps 1, 3, or 4: process all the new bounds on the
126 * bound stack, and assign all literals implied by these bounds in the core.
127 */
128
129
130 #ifndef __SIMPLEX_TYPES_H
131 #define __SIMPLEX_TYPES_H
132
133 #include <stdint.h>
134 #include <stdbool.h>
135 #include <setjmp.h>
136
137 #include "context/context_types.h"
138 #include "solvers/cdcl/gates_manager.h"
139 #include "solvers/cdcl/smt_core.h"
140 #include "solvers/egraph/diseq_stacks.h"
141 #include "solvers/egraph/egraph.h"
142 #include "solvers/egraph/egraph_assertion_queues.h"
143 #include "solvers/simplex/arith_atomtable.h"
144 #include "solvers/simplex/arith_vartable.h"
145 #include "solvers/simplex/diophantine_systems.h"
146 #include "solvers/simplex/matrices.h"
147 #include "solvers/simplex/offset_equalities.h"
148 #include "terms/extended_rationals.h"
149 #include "terms/poly_buffer.h"
150 #include "terms/polynomials.h"
151 #include "terms/rationals.h"
152 #include "utils/arena.h"
153 #include "utils/bitvectors.h"
154 #include "utils/cache.h"
155 #include "utils/int_heap.h"
156 #include "utils/int_vectors.h"
157 #include "utils/ptr_vectors.h"
158
159
160 /*******************
161 * BOUND STACK *
162 ******************/
163
164 /*
165 * Each element i in the stack is a constraint of the form (x <= u) or (x >= l)
166 * - x is an arithmetic variable stored in bstack->var[i]
167 * - u or l is an extended rational (of the form a + b\delta) stored in bstack->bound[i]
168 * - each constraint has an 8bit tag that defines what it is and how it was derived:
169 * - lower order bit = 0 means it's a lower bound (x >= l)
170 * lower order bit = 1 means it's an upper bound (x <= u)
171 * - the next two lower bits define how to explain the bound:
172 * axiom --> no explanation
173 * assertion --> explanation is a literal l
174 * derived/strengthened --> explanation is an array of literals
175 * equality propagation from the egraph --> the explanation is a pair
176 * of variables (v[0], v[1])
177 * new egraph explanation --> explanation is a pointer to a triple
178 * (v[0], v[1], id) where id is an egraph edge index
179 *
180 * - bit 7 of the tag is used as a mark when generating explanations
181 * - for backtracking, pre[i] stores the previous constraint of the same type,
182 * on the same variable.
183 *
184 * For each variable x, we maintain a list of lower and upper bounds on x:
185 * - lower_index[x] = -1 if x has no lower bound
186 * lower_index[x] = index k of the current lower bound on x in the stack otherwise
187 * then pre[k] = index of the previous lower on x, and so forth
188 * - upper_index[x]: same thing for upper bounds on x
189 *
190 * Other components:
191 * - top = top of the stack
192 * - prop_ptr = index of the first constraint to check for theory propagation
193 * (bounds of index prop_ptr to top-1 have not been visited)
194 * - fix_ptr = index of the first constraint to check for updating the assignment.
195 * - size = size of all subarrays
196 */
197
198 // Explanation: either a literal or a pointer or a pair of variables
199 typedef union arith_expl_u {
200 literal_t lit;
201 void *ptr;
202 thvar_t v[2];
203 } arith_expl_t;
204
205 typedef struct arith_bstack_s {
206 xrational_t *bound;
207 thvar_t *var;
208 arith_expl_t *expl;
209 int32_t *pre;
210 uint8_t *tag;
211
212 uint32_t top;
213 uint32_t prop_ptr;
214 uint32_t fix_ptr;
215 uint32_t size;
216 } arith_bstack_t;
217
218
219 // New: explanation triple from the egraph
220 typedef struct egraph_expl_triple_s {
221 thvar_t var[2];
222 int32_t id;
223 } egraph_expl_triple_t;
224
225
226 /*
227 * Default/maximal sizes
228 */
229 #define DEF_ARITH_BSTACK_SIZE 100
230 #define MAX_ARITH_BSTACK_SIZE (UINT32_MAX/sizeof(xrational_t))
231
232
233 /*
234 * Tags and marks
235 */
236 typedef enum arith_cnstr_type {
237 ATYPE_LB = 0, // lower bound
238 ATYPE_UB = 1, // upper bound
239 } arith_cnstr_type_t;
240
241 typedef enum arith_cnstr_expl {
242 AEXPL_AXIOM,
243 AEXPL_ASSERTION,
244 AEXPL_DERIVED,
245 AEXPL_EGRAPHEQ,
246 } arith_cnstr_expl_t;
247
248
249 #define ARITH_CNSTR_TYPE_MASK ((uint8_t) 0x1)
250 #define ARITH_CNSTR_TAG_MASK ((uint8_t) 0x6)
251 #define ARITH_CNSTR_MARK_MASK ((uint8_t) 0x80)
252
253
254
255 // construct an 8bit tag (we need a macro here because it's used in constant definitions below)
256 #define mk_arith_tag(e, t) ((uint8_t)(((e)<<1)|(t)))
257
mk_arith_lb_tag(arith_cnstr_expl_t e)258 static inline uint8_t mk_arith_lb_tag(arith_cnstr_expl_t e) {
259 return mk_arith_tag(e, ATYPE_LB);
260 }
261
mk_arith_ub_tag(arith_cnstr_expl_t e)262 static inline uint8_t mk_arith_ub_tag(arith_cnstr_expl_t e) {
263 return mk_arith_tag(e, ATYPE_UB);
264 }
265
266
267 // check the mark
arith_tag_mark(uint8_t tag)268 static inline bool arith_tag_mark(uint8_t tag) {
269 return (tag & ARITH_CNSTR_MARK_MASK) != 0;
270 }
271
272
273 // extract components
arith_tag_get_expl(uint8_t tag)274 static inline arith_cnstr_expl_t arith_tag_get_expl(uint8_t tag) {
275 return (arith_cnstr_expl_t)((tag & ARITH_CNSTR_TAG_MASK) >> 1);
276 }
277
arith_tag_get_type(uint8_t tag)278 static inline arith_cnstr_type_t arith_tag_get_type(uint8_t tag) {
279 return (arith_cnstr_type_t) (tag & ARITH_CNSTR_TYPE_MASK);
280 }
281
282 // type + explanation
arith_tag(uint8_t tag)283 static inline uint8_t arith_tag(uint8_t tag) {
284 return (uint8_t) (tag & (ARITH_CNSTR_TAG_MASK|ARITH_CNSTR_TYPE_MASK));
285 }
286
287
288
289 /*
290 * All combinations
291 */
292 #define ARITH_AXIOM_LB mk_arith_tag(AEXPL_AXIOM, ATYPE_LB)
293 #define ARITH_AXIOM_UB mk_arith_tag(AEXPL_AXIOM, ATYPE_UB)
294 #define ARITH_ASSERTED_LB mk_arith_tag(AEXPL_ASSERTION, ATYPE_LB)
295 #define ARITH_ASSERTED_UB mk_arith_tag(AEXPL_ASSERTION, ATYPE_UB)
296 #define ARITH_DERIVED_LB mk_arith_tag(AEXPL_DERIVED, ATYPE_LB)
297 #define ARITH_DERIVED_UB mk_arith_tag(AEXPL_DERIVED, ATYPE_UB)
298 #define ARITH_EGRAPHEQ_LB mk_arith_tag(AEXPL_EGRAPHEQ, ATYPE_LB)
299 #define ARITH_EGRAPHEQ_UB mk_arith_tag(AEXPL_EGRAPHEQ, ATYPE_UB)
300
301
302
303
304
305
306 /****************************
307 * ASSERTIONS STACK/QUEUE *
308 ***************************/
309
310 /*
311 * Asserted atoms (from the core) are stored into a queue/stack
312 * before being processed by simplex_propagate.
313 * - each assertion is a 32bit integer than consists of an
314 * atom id + a sign bit
315 * - the atom id, is an atom index in the atom table
316 * (that fits in 28 bits since there are at most UINT32_MAX/16 atoms)
317 * The sign bit is the low-order bit of the assertion code:
318 * - sign bit = 0 means atom asserted true
319 * - sign bit = 1 means atom asserted false
320 *
321 * Any atom that's in the queue is also marked in the atom table (this
322 * is used for theory propagation). Atoms are unmarked during
323 * backtracking.
324 *
325 * Other components:
326 * - size = size of the stack
327 * - top = top of the stack = end of the queue
328 * - prop_ptr = first assertion to process = start of the queue
329 * the queue is the set of assertions in data[prop_ptr ... top-1]
330 */
331 typedef struct arith_astack_s {
332 uint32_t size;
333 uint32_t top;
334 uint32_t prop_ptr;
335 int32_t *data;
336 } arith_astack_t;
337
338
339 #define DEF_ARITH_ASTACK_SIZE 100
340 #define MAX_ARITH_ASTACK_SIZE (UINT32_MAX/4)
341
342
343
344
345 /****************
346 * UNDO STACK *
347 ***************/
348
349 /*
350 * On entry to each decision level k we store:
351 * - the number of asserted bounds (i.e., arith_stack.top)
352 * - the number of asserted atoms (i.e., arith_queue.top)
353 *
354 * At level 0: n_bounds = 0, n_assertions = 0
355 */
356 typedef struct arith_undo_record_s {
357 uint32_t n_bounds;
358 uint32_t n_assertions;
359 } arith_undo_record_t;
360
361 typedef struct arith_undo_stack_s {
362 uint32_t size;
363 uint32_t top;
364 arith_undo_record_t *data;
365 } arith_undo_stack_t;
366
367 #define DEF_ARITH_UNDO_STACK_SIZE 100
368 #define MAX_ARITH_UNDO_STACK_SIZE (UINT32_MAX/sizeof(arith_undo_record_t))
369
370
371
372
373
374 /********************
375 * PUSH/POP STACK *
376 *******************/
377
378 /*
379 * The constraint matrix is modified (destructively) on every simplex_start_search
380 * To support push/pop and multiple checks, we must keep enough information to
381 * restore the matrix to what it was before the previous 'start_search'.
382 *
383 * The matrix contains two types of rows:
384 * - rows of the form (p == 0) added on calls to assert_eq_axiom
385 * - rows of the form (x - q = 0) where x is a variable and q is a polynomial.
386 * The polynomial q is x's definition obtained from the variable table.
387 *
388 * We don't add the row (x - q = 0) if q is simple. Currently
389 * simple means that q is of the form (k + a.y) for two constants k and a.
390 * For such polynomials, we replace x by q eagerly, everywhere x is referenced.
391 * (and x is a trivial variable).
392 *
393 * To restore the matrix to its old state:
394 * - we keep a copy of all polynomials p_1, ..., p_k that form the first type of
395 * rows. These polynomials are stored in vector simplex->saved_rows.
396 * - we reconstruct the rows (x - q = 0) for all the non-trivial variables.
397 */
398
399 /*
400 * On entry to a new base level, we save
401 * - the number of variables and atoms
402 * - the size of the saved row vector
403 * - the current propagation pointer for both assertion_queue and bound stack
404 */
405 typedef struct arith_trail_s {
406 uint32_t nvars;
407 uint32_t natoms;
408 uint32_t nsaved_rows;
409 uint32_t bound_ptr;
410 uint32_t assertion_ptr;
411 } arith_trail_t;
412
413 typedef struct arith_trail_stack_s {
414 uint32_t size;
415 uint32_t top;
416 arith_trail_t *data;
417 } arith_trail_stack_t;
418
419
420 #define DEF_SIMPLEX_TRAIL_SIZE 20
421 #define MAX_SIMPLEX_TRAIL_SIZE (UINT32_MAX/sizeof(arith_trail_t))
422
423
424
425
426 /********************************
427 * THEORY PROPAGATION OBJECTS *
428 *******************************/
429
430 /*
431 * When a simplex solver propagate a literal l (via a call to propagate_literal)
432 * it uses an propagation object as antecedent for l. The propagation object
433 * stores enough information to construct an explanation for l when requested.
434 * The explanation for l must be a vector of literals (l_1 ... l_n) such that
435 * "(and l_1 ... l_n) implies l" holds.
436 *
437 * Currently, there are two types of propagation objects, corresponding to two
438 * propagation rules:
439 *
440 * 1) simplex propagation:
441 * a bound k implies l (e.g., bound k is (x >= 2) and l is the atom (x >= 1))
442 * The propagation object stores k in that case.
443 *
444 * 2) egraph disequalities:
445 * If x1 and x2 are attached to terms t1 and t2 in the egraph, then
446 * the egraph will assert (x1 != x2) in simplex when (t1 != t2) holds in
447 * the egraph. To deal with (x1 != x2), the simplex will create
448 * a simplex variable y = x1 - x2 and two atoms (y >= 0) and (y <= 0).
449 * Then it will add a trichotomy clause to the core:
450 * (or (eq t1 t2) (not (y >= 0)) (not (y <= 0)))
451 * and the simplex solver may have to propagate (not (eq t1 t2)) to the core.
452 * The propagation object stores x1 and x2 in that case + a hint.
453 *
454 * The propagation objects starts with a tag that identifies the
455 * propagation rule.
456 *
457 * NOTE: APROP_EGRAPH_DISEQ is not used anymore.
458 */
459 typedef enum aprop_tag {
460 APROP_BOUND, // ordinary simplex propagation
461 APROP_EGRAPH_DISEQ, // propagation for egraph disequality
462 } aprop_tag_t;
463
464 typedef struct aprop_header_s {
465 aprop_tag_t tag;
466 } aprop_header_t;
467
468 // simplex propagation object
469 typedef struct aprop_s {
470 aprop_tag_t tag;
471 int32_t bound;
472 } aprop_t;
473
474 // egraph disequality propagation object
475 typedef struct aprop_egraph_diseq_s {
476 aprop_tag_t tag;
477 diseq_pre_expl_t d;
478 } aprop_egraph_diseq_t;
479
480
481
482
483 /*****************************************
484 * PROPAGATION USING OFFSET EQUALITIES *
485 ****************************************/
486
487 /*
488 * To propagate equalities to the egraph:
489 * - we use offset_manager as an auxiliary solver
490 * - for every theory variable x, we mark x as relevant
491 * if its definition is suitable for offset equality:
492 * (i.e., x's definition must be of the form x := y - z
493 * so that we can propagate y == z + a when we detect a <= x <= a)
494 * - to detect frozen variables, we keep a propagation pointer
495 * (an index in the simplex's bound stack).
496 *
497 * To build explanations:
498 * - aux = vector of frozen variables
499 * - expl_queue = queue of constraint indices used to convert aux
500 * into a th_explanation_t object.
501 * - we need a separate expl_queue than the one in the egraph
502 * because simplex_expand_th_explanation may be called
503 * within simplex_build_explanation
504 */
505 typedef struct eq_propagator_s {
506 offset_manager_t mngr;
507 byte_t *relevant; // one bit per variable
508 uint32_t nvars; // number of variables
509 uint32_t size; // size of vector 'relevant' (number of bits)
510 uint32_t prop_ptr; // propagation pointer
511
512 ivector_t aux; // for explanations
513 ivector_t expl_queue; // also for explanations
514 rational_t q_aux;
515 } eq_propagator_t;
516
517
518 #define DEF_EQPROP_SIZE 128
519
520
521
522 /******************
523 * CACHED DATA *
524 *****************/
525
526 /*
527 * If the simplex solver is connected to an egraph, trichotomy clauses
528 * may be generated dynamically. If t1 and t2 are two egraph terms,
529 * with respective theory variables x1 and x2 (both in the simplex), then the
530 * trichotomy clauses is the axiom:
531 * (t1 == t2) or (x1 < x2) or (x2 < x1)
532 * Internally, this is encoded via an auxiliary variable y and a constant k
533 * such that y - k = (x1 - x2) or y - k = (x2 - x1). The axiom is then
534 * (t1 == t2) or (not (y >= k)) or (not (y <= k))
535 *
536 * To avoid generating the same axiom several time, we keep track
537 * of which trichotomy clauses have been generated in an internal cache.
538 * For each clause, the cache stores a record [TRICHOTOMY_LEMMA, t1, t2]
539 * (modulo reordering to ensure t1 < t2). Note: we can't use l in the cache
540 * because (t1 == t2) may the false literal (fixed a bug by changing that).
541 *
542 * Each cache record needs a tag + a non-zero flag. To differentiate from the tags
543 * used in the egraph cache, we use 2 here.
544 */
545 typedef enum arith_lemma_tag {
546 TRICHOTOMY_LEMMA = 2,
547 } arith_lemma_tag_t;
548
549 typedef enum arith_lemma_flag {
550 ACTIVE_ARITH_LEMMA = 1,
551 } arith_lemma_flag_t;
552
553
554
555
556
557
558 /*********************
559 * BOUND COLLECTOR *
560 ********************/
561
562 /*
563 * When we adjust the model (in reconcile model), we try to shift the
564 * current value of a non-basic variable x by some delta, then adjust
565 * the value of all basic variables that depend on x. We want this
566 * shift to preserve feasibility (without requiring any pivoting)
567 *
568 * To do this, we compute an interval of values for delta that maintains
569 * feasibility and we also need a rational D that defines which deltas
570 * maintain integer feasibility. All these components are stored in
571 * the following record.
572 *
573 * - lb and ub are lower and upper bounds
574 * - has_lb is true if lb is valid, otherwise, there's no lower bound
575 * - has_ub is true if ub is valid, otherwise, there's no upper bound
576 * - period is a rational number, if it's not zero then the allowed
577 * shifts on x must be multiple of period. (If it's zero, the allowed
578 * shifts on x can be anything).
579 *
580 * Two more components are used for sampling
581 * - k_min = smallest integer k such that lb <= k period
582 * (i.e., k_min = ceil(lb/period))
583 * - k_max = largest integer k such that k period <= ub
584 * (i.e., k_max = floor(ub/period))
585 */
586 typedef struct interval_s {
587 bool has_lb;
588 bool has_ub;
589 xrational_t lb;
590 xrational_t ub;
591 rational_t period;
592 int32_t k_min;
593 int32_t k_max;
594 } interval_t;
595
596
597
598 /****************
599 * STATISTICS *
600 ***************/
601
602 /*
603 * Search + problem size
604 */
605 typedef struct simplex_stats_s {
606 // problem size
607 uint32_t num_init_vars; // number of variables/columns in initial matrix
608 uint32_t num_init_rows; // number of rows in the initial matrix
609 uint32_t num_atoms; // number of atoms (initially)
610
611 // simplification data
612 uint32_t num_elim_candidates;
613 uint32_t num_elim_rows;
614 uint32_t num_simpl_fvars; // number of fixed variable after simplification
615 uint32_t num_simpl_rows; // number of rows in the simplified matrix
616 uint32_t num_fixed_vars; // number of fixed variables after tableau construction
617
618 // more problem size data
619 uint32_t num_rows; // number of rows in the tableau after simplification
620 uint32_t num_end_rows; // number of rows in the final tableau
621 uint32_t num_end_atoms; // number of atoms at the end
622
623 // lemmas and propagation
624 uint32_t num_binary_lemmas; // simple lemmas
625 uint32_t num_prop_lemmas; // lemmas from theory propagation
626 uint32_t num_props; // theory propagations
627 uint32_t num_bound_props; // bound propagations
628 uint32_t num_prop_expl; // propagations involved in a conflict
629
630 // interface + trichotomy lemmas
631 uint32_t num_interface_lemmas;
632 uint32_t num_reduced_inter_lemmas;
633 uint32_t num_tricho_lemmas;
634 uint32_t num_reduced_tricho;
635
636 // search statistics
637 uint32_t num_make_feasible; // calls to make_feasible
638 uint32_t num_pivots; // pivoting steps
639 uint32_t num_blands; // number of activations of bland's rule
640 uint32_t num_conflicts;
641
642 // stats on integer arithmetic solver
643 uint32_t num_make_intfeasible; // calls to make_integer_feasible
644 uint32_t num_bound_conflicts; // unsat by ordinary bound strengthening
645 uint32_t num_bound_recheck_conflicts; // unsat by bound strengthening + recheck
646 uint32_t num_itest_conflicts; // unsat by the integrality test
647 uint32_t num_itest_bound_conflicts; // unsat by itest bound strengthening
648 uint32_t num_itest_recheck_conflicts; // unsat by itest bounds + recheck
649 uint32_t num_dioph_checks; // number of calls to dsolver_check
650 uint32_t num_dioph_gcd_conflicts; // failed GCD tests in dsolver
651 uint32_t num_dioph_conflicts; // number of dsolver unsat
652 uint32_t num_dioph_bound_conflicts; // unset by dioph bound strengthening
653 uint32_t num_dioph_recheck_conflicts; // unsat after dioph bounds + recheck
654
655 uint32_t num_branch_atoms; // new branch&bound atoms created
656 uint32_t num_gomory_cuts; // number of Gomory cuts
657
658 } simplex_stats_t;
659
660
661
662
663
664 /********************
665 * SIMPLEX SOLVER *
666 *******************/
667
668 typedef struct simplex_solver_s {
669 /*
670 * Attached smt core + gate manager + egraph
671 * (egraph may be NULL)
672 */
673 smt_core_t *core;
674 gate_manager_t *gate_manager;
675 egraph_t *egraph;
676
677 /*
678 * Base level and decision level
679 */
680 uint32_t base_level;
681 uint32_t decision_level;
682
683 /*
684 * Unsat flag: set to true if the asserted axioms are inconsistent
685 */
686 bool unsat_before_search;
687
688 /*
689 * Options: each option is a single bit in the 32-bit word
690 */
691 uint32_t options;
692
693 /*
694 * Interrupt flag: set to true to stop pivoting
695 */
696 bool interrupted;
697
698 /*
699 * Pivoting parameters
700 */
701 bool use_blands_rule; // true if Bland's rule is active
702 uint32_t bland_threshold; // number of repeat entering variable
703
704 /*
705 * Parameters for propagation
706 */
707 uint32_t prop_row_size; // max size of rows considered for propagation
708 int32_t last_conflict_row; // last row where a conflict was found
709 bool recheck; // true if make_feasible must be called after propagation
710
711 /*
712 * Pseudo-random number generator
713 */
714 uint32_t prng;
715
716 /*
717 * Flag and parameter for integer arithmetic
718 */
719 bool integer_solving;
720 bool enable_dfeas;
721 int32_t check_counter;
722 int32_t check_period;
723 bvar_t last_branch_atom;
724
725 /*
726 * Optional subsolver for integer arithmetic: allocated when needed
727 */
728 dsolver_t *dsolver;
729
730 /*
731 * Optional cache for trichotomy lemmas: allocated when needed
732 */
733 cache_t *cache;
734
735 /*
736 * Statistics
737 */
738 simplex_stats_t stats;
739
740 /*
741 * Table of variables and atoms + pointer to the variable manager
742 * for all input polynomials
743 */
744 arith_atomtable_t atbl;
745 arith_vartable_t vtbl;
746
747 /*
748 * Propagation data structure: defined elsewhere
749 */
750 void *propagator;
751
752 /*
753 * Propagator for the egraph: optional
754 */
755 eq_propagator_t *eqprop;
756
757 /*
758 * Matrix/tableau
759 * - tableau_ready is true if the matrix is in tableau form
760 * and the variables have an initial assignment
761 * - matrix_ready is true if the matrix contains all the
762 * constraints asserted so far
763 * - save_rows is true if the top-level rows must be saved (i.e.,
764 * if the context supports push/pop or multiple checks).
765 *
766 * The flags are set as follows to support push/pop/multicheck:
767 * - initially, the matrix is empty:
768 * tableau_ready = false
769 * matrix_ready = true
770 * - in start_search, the matrix is converted to a tableau:
771 * so after start_search,
772 * tableau_ready = true
773 * matrix_ready = false
774 * - after pop, the tableau is emptied:
775 * tableau_ready = false
776 * matrix_ready keeps its current value
777 * - in start_internalization, we restore the constraint matrix
778 * and reset the tableau if needed:
779 * tableau_ready = false
780 * matrix_ready = true
781 */
782 matrix_t matrix;
783 bool tableau_ready;
784 bool matrix_ready;
785 bool save_rows;
786
787 /*
788 * Heap to store the basic-variables whose current assignment
789 * does not satisfy the bounds
790 */
791 int_heap_t infeasible_vars;
792
793 /*
794 * Bounds + assertions
795 */
796 arith_bstack_t bstack;
797 arith_astack_t assertion_queue;
798
799 /*
800 * Queue of egraph assertions + disequalities received from
801 * the egraph (disequalities are stored in a stack)
802 */
803 eassertion_queue_t egraph_queue;
804
805 /*
806 * Undo stack
807 */
808 arith_undo_stack_t stack;
809
810 /*
811 * Push/pop stack + saved rows
812 */
813 arith_trail_stack_t trail_stack;
814 pvector_t saved_rows;
815
816 /*
817 * Result of matrix simplification
818 * - a triangular matrix + a variable assignment
819 */
820 elim_matrix_t elim;
821 fvar_vector_t fvars;
822
823 /*
824 * Auxiliary buffers and data structures
825 */
826 poly_buffer_t buffer;
827 rational_t constant;
828 rational_t aux;
829 rational_t gcd;
830 xrational_t bound;
831 xrational_t delta;
832 xrational_t xq0; // general purpose buffer
833
834 ivector_t expl_vector; // vector of literals for conflicts/explanations
835 ivector_t expl_queue; // vector used as a queue for building explanations
836 ivector_t expl_aux; // to collect explanations from the egraph
837 ivector_t aux_vector; // general-purpose vector
838 ivector_t aux_vector2; // another one
839 ivector_t rows_to_process; // rows for propagation
840
841 arena_t arena; // store explanations of implied atoms
842
843
844 /*
845 * Model construction support
846 * - value[x] = rational value of x
847 * - epsilon is a positive rational
848 * - if val[x] = a + b delta as an extended rational, then the rational value
849 * for a variable x is a + b * epsilon.
850 * - factor is an auxiliary rational used for computing epsilon
851 * - dprng is used by a pseudo-random number generator (for adjust model)
852 */
853 rational_t *value;
854 rational_t epsilon;
855 rational_t factor;
856 double dprng;
857
858 /*
859 * Jump buffer for exception handling during internalization
860 */
861 jmp_buf *env;
862 } simplex_solver_t;
863
864
865 /*
866 * Initial size of the explanation vector/queue
867 */
868 #define DEF_ARITH_EXPL_VECTOR_SIZE 20
869
870
871 /*
872 * Initial size of the vector of rows to process
873 */
874 #define DEF_PROCESS_ROW_VECTOR_SIZE 20
875
876
877
878 /*
879 * Option flags
880 * - each mask selects a bit in the option word
881 * - bit = 1 means option enabled, 0 means disabled
882 *
883 * Current options
884 * - EAGER_LEMMAS: when an atom on x is created, all binary lemmas
885 * relating it to other atoms on x are added to the clause set.
886 * - PROPAGATION: enable propagation via rows
887 * - ICHECK: enable periodic integer checking
888 * - ADJUST_MODEL: attempt to modify the variable assignment to
889 * make the simplex model consistent with the egraph (as much as possible).
890 * - EQPROP: enable propagation of equalities to the egraph
891 *
892 * Bland's rule threshold: based on the count of repeat
893 * leaving variable. The counter is incremented whenever
894 * a variable x leaves the basic for at least the second time.
895 * When the counter becomes >= threshold, then Bland's rule
896 * is activated to ensure termination.
897 *
898 * Propagation row size = maximal size of rows considered for propagation.
899 */
900 #define SIMPLEX_EAGER_LEMMAS 0x1
901 #define SIMPLEX_PROPAGATION 0x2
902 #define SIMPLEX_ICHECK 0x4
903 #define SIMPLEX_ADJUST_MODEL 0x8
904 #define SIMPLEX_EQPROP 0x10
905
906 #define SIMPLEX_DISABLE_ALL_OPTIONS 0x0
907
908 #define SIMPLEX_DEFAULT_BLAND_THRESHOLD 1000
909 #define SIMPLEX_DEFAULT_PROP_ROW_SIZE 30
910 #define SIMPLEX_DEFAULT_CHECK_PERIOD 99999999
911
912 // default options
913 #define SIMPLEX_DEFAULT_OPTIONS (SIMPLEX_DISABLE_ALL_OPTIONS)
914
915
916 #endif /* __SIMPLEX_TYPES_H */
917