1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "btorcore.h"
10
11 #include <limits.h>
12
13 #include "btorabort.h"
14 #ifndef NDEBUG
15 #include "btorchkfailed.h"
16 #include "btorchkmodel.h"
17 #endif
18 #include "btorclone.h"
19 #include "btorconfig.h"
20 #include "btordbg.h"
21 #include "btorexp.h"
22 #include "btorlog.h"
23 #include "btormodel.h"
24 #include "btoropt.h"
25 #include "btorrewrite.h"
26 #include "btorslvaigprop.h"
27 #include "btorslvfun.h"
28 #include "btorslvprop.h"
29 #include "btorslvquant.h"
30 #include "btorslvsls.h"
31 #include "btorsubst.h"
32 #include "preprocess/btorpreprocess.h"
33 #include "preprocess/btorvarsubst.h"
34 #include "utils/btorhashint.h"
35 #include "utils/btornodeiter.h"
36 #include "utils/btorutil.h"
37
38 /*------------------------------------------------------------------------*/
39
40 #define BTOR_INIT_UNIQUE_TABLE(mm, table) \
41 do \
42 { \
43 assert (mm); \
44 (table).size = 1; \
45 (table).num_elements = 0; \
46 BTOR_CNEW (mm, (table).chains); \
47 } while (0)
48
49 #define BTOR_RELEASE_UNIQUE_TABLE(mm, table) \
50 do \
51 { \
52 assert (mm); \
53 BTOR_DELETEN (mm, (table).chains, (table).size); \
54 } while (0)
55
56 #define BTOR_INIT_SORT_UNIQUE_TABLE(mm, table) \
57 do \
58 { \
59 BTOR_INIT_UNIQUE_TABLE (mm, table); \
60 table.mm = mm; \
61 BTOR_INIT_STACK (mm, table.id2sort); \
62 BTOR_PUSH_STACK (table.id2sort, 0); \
63 } while (0)
64
65 #define BTOR_RELEASE_SORT_UNIQUE_TABLE(mm, table) \
66 do \
67 { \
68 BTOR_RELEASE_UNIQUE_TABLE (mm, table); \
69 BTOR_RELEASE_STACK (table.id2sort); \
70 } while (0)
71
72 #define BTOR_COND_INVERT_AIG_NODE(exp, aig) \
73 ((BtorAIG *) (((uint32_t long int) (exp) &1ul) ^ ((uint32_t long int) (aig))))
74
75 #define BTOR_AIGVEC_NODE(btor, exp) \
76 (btor_node_is_inverted (exp) \
77 ? btor_aigvec_not ((btor)->avmgr, btor_node_real_addr (exp)->av) \
78 : btor_aigvec_copy ((btor)->avmgr, exp->av))
79
80 /*------------------------------------------------------------------------*/
81
82 static BtorAIG *exp_to_aig (Btor *, BtorNode *);
83
84 /*------------------------------------------------------------------------*/
85
86 enum BtorSubstCompKind
87 {
88 BTOR_SUBST_COMP_ULT_KIND,
89 BTOR_SUBST_COMP_ULTE_KIND,
90 BTOR_SUBST_COMP_UGT_KIND,
91 BTOR_SUBST_COMP_UGTE_KIND
92 };
93
94 typedef enum BtorSubstCompKind BtorSubstCompKind;
95
96 /*------------------------------------------------------------------------*/
97
98 void
btor_init_substitutions(Btor * btor)99 btor_init_substitutions (Btor *btor)
100 {
101 assert (btor);
102 assert (!btor->substitutions);
103
104 btor->substitutions =
105 btor_hashptr_table_new (btor->mm,
106 (BtorHashPtr) btor_node_hash_by_id,
107 (BtorCmpPtr) btor_node_compare_by_id);
108 }
109
110 void
btor_delete_substitutions(Btor * btor)111 btor_delete_substitutions (Btor *btor)
112 {
113 assert (btor);
114
115 if (!btor->substitutions) return;
116
117 BtorNode *cur;
118 BtorPtrHashTableIterator it;
119
120 btor_iter_hashptr_init (&it, btor->substitutions);
121 while (btor_iter_hashptr_has_next (&it))
122 {
123 btor_node_release (btor, (BtorNode *) it.bucket->data.as_ptr);
124 cur = btor_iter_hashptr_next (&it);
125 btor_node_release (btor, cur);
126 }
127
128 btor_hashptr_table_delete (btor->substitutions);
129 btor->substitutions = 0;
130 }
131
132 BtorNode *
btor_find_substitution(Btor * btor,BtorNode * exp)133 btor_find_substitution (Btor *btor, BtorNode *exp)
134 {
135 assert (btor);
136 assert (exp);
137
138 BtorNode *result = 0;
139 BtorPtrHashBucket *b;
140
141 if (!btor->substitutions) return 0;
142
143 while (1)
144 {
145 b = btor_hashptr_table_get (btor->substitutions, btor_node_real_addr (exp));
146 if (!b) break;
147 result = btor_node_cond_invert (exp, (BtorNode *) b->data.as_ptr);
148 exp = result;
149 }
150
151 return result;
152 }
153
154 #ifndef NDEBUG
155 static bool
substitution_cycle_check_dbg(Btor * btor,BtorNode * exp,BtorNode * subst)156 substitution_cycle_check_dbg (Btor *btor, BtorNode *exp, BtorNode *subst)
157 {
158 uint32_t i;
159 bool iscycle = false;
160 BtorMemMgr *mm;
161 BtorNode *cur;
162 BtorNodePtrStack visit;
163 BtorIntHashTable *cache;
164
165 mm = btor->mm;
166 exp = btor_node_real_addr (exp);
167 cache = btor_hashint_table_new (mm);
168
169 BTOR_INIT_STACK (mm, visit);
170 BTOR_PUSH_STACK (visit, subst);
171 while (!BTOR_EMPTY_STACK (visit))
172 {
173 cur = btor_node_real_addr (BTOR_POP_STACK (visit));
174
175 if (btor_hashint_table_contains (cache, cur->id)) continue;
176
177 if (cur == exp)
178 {
179 iscycle = true;
180 break;
181 }
182
183 btor_hashint_table_add (cache, cur->id);
184
185 for (i = 0; i < cur->arity; i++) BTOR_PUSH_STACK (visit, cur->e[i]);
186 }
187 BTOR_RELEASE_STACK (visit);
188 btor_hashint_table_delete (cache);
189 return !iscycle;
190 }
191 #endif
192
193 void
btor_insert_substitution(Btor * btor,BtorNode * exp,BtorNode * subst,bool update)194 btor_insert_substitution (Btor *btor,
195 BtorNode *exp,
196 BtorNode *subst,
197 bool update)
198 {
199 assert (btor);
200 assert (exp);
201 assert (subst);
202 assert (btor->substitutions);
203 assert (btor_node_get_sort_id (exp) == btor_node_get_sort_id (subst));
204 assert (!btor_node_is_simplified (exp));
205
206 BtorNode *simp;
207 BtorPtrHashBucket *b;
208 exp = btor_node_real_addr (exp);
209
210 if (exp == btor_node_real_addr (subst)) return;
211
212 assert (substitution_cycle_check_dbg (btor, exp, subst));
213
214 b = btor_hashptr_table_get (btor->substitutions, exp);
215 if (update && b)
216 {
217 assert (b->data.as_ptr);
218 /* release data of current bucket */
219 btor_node_release (btor, (BtorNode *) b->data.as_ptr);
220 btor_hashptr_table_remove (btor->substitutions, exp, 0, 0);
221 /* release key of current bucket */
222 btor_node_release (btor, exp);
223 }
224 else if (b)
225 {
226 assert ((BtorNode *) b->data.as_ptr == subst);
227 /* substitution already inserted */
228 return;
229 }
230
231 simp = btor_find_substitution (btor, subst);
232
233 if (simp) subst = simp;
234
235 assert (!btor_hashptr_table_get (btor->substitutions,
236 btor_node_real_addr (subst)));
237
238 if (exp == btor_node_real_addr (subst)) return;
239
240 btor_hashptr_table_add (btor->substitutions, btor_node_copy (btor, exp))
241 ->data.as_ptr = btor_node_copy (btor, subst);
242 }
243
244 /*------------------------------------------------------------------------*/
245
246 const char *
btor_version(const Btor * btor)247 btor_version (const Btor *btor)
248 {
249 assert (btor);
250 (void) btor;
251 return BTOR_VERSION;
252 }
253
254 const char *
btor_git_id(const Btor * btor)255 btor_git_id (const Btor *btor)
256 {
257 assert (btor);
258 (void) btor;
259 return BTOR_GIT_ID;
260 }
261
262 BtorAIGMgr *
btor_get_aig_mgr(const Btor * btor)263 btor_get_aig_mgr (const Btor *btor)
264 {
265 assert (btor);
266 return btor_aigvec_get_aig_mgr (btor->avmgr);
267 }
268
269 BtorSATMgr *
btor_get_sat_mgr(const Btor * btor)270 btor_get_sat_mgr (const Btor *btor)
271 {
272 assert (btor);
273 return btor_aig_get_sat_mgr (btor_get_aig_mgr (btor));
274 }
275
276 void
btor_reset_time(Btor * btor)277 btor_reset_time (Btor *btor)
278 {
279 assert (btor);
280 BTOR_CLR (&btor->time);
281 }
282
283 void
btor_reset_stats(Btor * btor)284 btor_reset_stats (Btor *btor)
285 {
286 assert (btor);
287 #ifndef NDEBUG
288 if (btor->stats.rw_rules_applied)
289 btor_hashptr_table_delete (btor->stats.rw_rules_applied);
290 #endif
291 BTOR_CLR (&btor->stats);
292 #ifndef NDEBUG
293 assert (!btor->stats.rw_rules_applied);
294 btor->stats.rw_rules_applied = btor_hashptr_table_new (
295 btor->mm, (BtorHashPtr) btor_hash_str, (BtorCmpPtr) strcmp);
296 #endif
297 }
298
299 static uint32_t
constraints_stats_changes(Btor * btor)300 constraints_stats_changes (Btor *btor)
301 {
302 uint32_t res;
303
304 if (btor->stats.oldconstraints.varsubst && !btor->varsubst_constraints->count)
305 return UINT32_MAX;
306
307 if (btor->stats.oldconstraints.embedded && !btor->embedded_constraints->count)
308 return UINT32_MAX;
309
310 if (btor->stats.oldconstraints.unsynthesized
311 && !btor->unsynthesized_constraints->count)
312 return UINT32_MAX;
313
314 res = btor->stats.oldconstraints.varsubst >= btor->varsubst_constraints->count
315 ? btor->stats.oldconstraints.varsubst
316 - btor->varsubst_constraints->count
317 : btor->varsubst_constraints->count
318 - btor->stats.oldconstraints.varsubst;
319 res +=
320 btor->stats.oldconstraints.embedded >= btor->embedded_constraints->count
321 ? btor->stats.oldconstraints.embedded
322 - btor->embedded_constraints->count
323 : btor->embedded_constraints->count
324 - btor->stats.oldconstraints.embedded;
325 res += btor->stats.oldconstraints.unsynthesized
326 >= btor->unsynthesized_constraints->count
327 ? btor->stats.oldconstraints.unsynthesized
328 - btor->unsynthesized_constraints->count
329 : btor->unsynthesized_constraints->count
330 - btor->stats.oldconstraints.unsynthesized;
331 res += btor->stats.oldconstraints.synthesized
332 >= btor->synthesized_constraints->count
333 ? btor->stats.oldconstraints.synthesized
334 - btor->synthesized_constraints->count
335 : btor->synthesized_constraints->count
336 - btor->stats.oldconstraints.synthesized;
337
338 return res;
339 }
340
341 static void
report_constraint_stats(Btor * btor,bool force)342 report_constraint_stats (Btor *btor, bool force)
343 {
344 uint32_t changes;
345
346 if (!force)
347 {
348 if (btor_opt_get (btor, BTOR_OPT_VERBOSITY) <= 0) return;
349
350 changes = constraints_stats_changes (btor);
351
352 if (btor_opt_get (btor, BTOR_OPT_VERBOSITY) == 1 && changes < 100000)
353 return;
354
355 if (btor_opt_get (btor, BTOR_OPT_VERBOSITY) == 2 && changes < 1000) return;
356
357 if (btor_opt_get (btor, BTOR_OPT_VERBOSITY) == 3 && changes < 10) return;
358
359 if (!changes) return;
360 }
361
362 BTOR_MSG (btor->msg,
363 1,
364 "%d/%d/%d/%d constraints %d/%d/%d/%d %.1f MB",
365 btor->stats.constraints.varsubst,
366 btor->stats.constraints.embedded,
367 btor->stats.constraints.unsynthesized,
368 btor->stats.constraints.synthesized,
369 btor->varsubst_constraints->count,
370 btor->embedded_constraints->count,
371 btor->unsynthesized_constraints->count,
372 btor->synthesized_constraints->count,
373 btor->mm->allocated / (double) (1 << 20));
374
375 btor->stats.oldconstraints.varsubst = btor->varsubst_constraints->count;
376 btor->stats.oldconstraints.embedded = btor->embedded_constraints->count;
377 btor->stats.oldconstraints.unsynthesized =
378 btor->unsynthesized_constraints->count;
379 btor->stats.oldconstraints.synthesized = btor->synthesized_constraints->count;
380 }
381
382 /* we do not count proxies */
383 static uint32_t
number_of_ops(Btor * btor)384 number_of_ops (Btor *btor)
385 {
386 int32_t i, result;
387 assert (btor);
388
389 result = 0;
390 for (i = 1; i < BTOR_NUM_OPS_NODE - 1; i++) result += btor->ops[i].cur;
391
392 return result;
393 }
394
395 #ifdef BTOR_TIME_STATISTICS
396 static double
percent(double a,double b)397 percent (double a, double b)
398 {
399 return b ? 100.0 * a / b : 0.0;
400 }
401 #endif
402
403 void
btor_print_stats(Btor * btor)404 btor_print_stats (Btor *btor)
405 {
406 uint32_t i, num_final_ops;
407 uint32_t verbosity;
408
409 if (!btor) return;
410
411 verbosity = btor_opt_get (btor, BTOR_OPT_VERBOSITY);
412
413 report_constraint_stats (btor, true);
414
415 BTOR_MSG (btor->msg, 1, "%u assumptions", btor->assumptions->count);
416
417 if (verbosity > 0)
418 {
419 BTOR_MSG (btor->msg, 1, "");
420 BTOR_MSG (btor->msg, 2, "%5d max rec. RW", btor->stats.max_rec_rw_calls);
421 BTOR_MSG (btor->msg,
422 2,
423 "%5lld number of expressions ever created",
424 btor->stats.expressions);
425 num_final_ops = number_of_ops (btor);
426 BTOR_MSG (btor->msg, 2, "%5d number of final expressions", num_final_ops);
427 assert (sizeof g_btor_op2str / sizeof *g_btor_op2str == BTOR_NUM_OPS_NODE);
428
429 BTOR_MSG (btor->msg,
430 1,
431 "%.2f MB allocated for nodes",
432 btor->stats.node_bytes_alloc / (double) (1 << 20));
433 if (num_final_ops > 0)
434 for (i = 1; i < BTOR_NUM_OPS_NODE - 1; i++)
435 if (btor->ops[i].cur || btor->ops[i].max)
436 BTOR_MSG (btor->msg,
437 2,
438 " %s: %d max %d",
439 g_btor_op2str[i],
440 btor->ops[i].cur,
441 btor->ops[i].max);
442 BTOR_MSG (btor->msg, 1, "");
443 }
444
445 if (btor_opt_get (btor, BTOR_OPT_UCOPT))
446 {
447 BTOR_MSG (
448 btor->msg, 1, "%5d unconstrained bv props", btor->stats.bv_uc_props);
449 BTOR_MSG (btor->msg,
450 1,
451 "%5d unconstrained array props",
452 btor->stats.fun_uc_props);
453 BTOR_MSG (btor->msg,
454 1,
455 "%5d unconstrained parameterized props",
456 btor->stats.param_uc_props);
457 }
458 BTOR_MSG (btor->msg,
459 1,
460 "%5d variable substitutions",
461 btor->stats.var_substitutions);
462 BTOR_MSG (btor->msg,
463 1,
464 "%5d uninterpreted function substitutions",
465 btor->stats.uf_substitutions);
466 BTOR_MSG (btor->msg,
467 1,
468 "%5d embedded constraint substitutions",
469 btor->stats.ec_substitutions);
470 BTOR_MSG (btor->msg,
471 1,
472 "%5d synthesized nodes rewritten",
473 btor->stats.rewrite_synth);
474
475 BTOR_MSG (btor->msg,
476 1,
477 "%5d linear constraint equations",
478 btor->stats.linear_equations);
479 BTOR_MSG (btor->msg,
480 1,
481 "%5d gaussian eliminations in linear equations",
482 btor->stats.gaussian_eliminations);
483 BTOR_MSG (btor->msg,
484 1,
485 "%5d eliminated sliced variables",
486 btor->stats.eliminated_slices);
487 BTOR_MSG (btor->msg,
488 1,
489 "%5d extracted skeleton constraints",
490 btor->stats.skeleton_constraints);
491 BTOR_MSG (
492 btor->msg, 1, "%5d and normalizations", btor->stats.ands_normalized);
493 BTOR_MSG (
494 btor->msg, 1, "%5d add normalizations", btor->stats.adds_normalized);
495 BTOR_MSG (
496 btor->msg, 1, "%5d mul normalizations", btor->stats.muls_normalized);
497 BTOR_MSG (btor->msg, 1, "%5lld lambdas merged", btor->stats.lambdas_merged);
498 BTOR_MSG (btor->msg,
499 1,
500 "%5d static apply propagations over lambdas",
501 btor->stats.prop_apply_lambda);
502 BTOR_MSG (btor->msg,
503 1,
504 "%5d static apply propagations over updates",
505 btor->stats.prop_apply_update);
506 BTOR_MSG (
507 btor->msg, 1, "%5lld beta reductions", btor->stats.beta_reduce_calls);
508 BTOR_MSG (btor->msg, 1, "%5lld clone calls", btor->stats.clone_calls);
509
510 BTOR_MSG (btor->msg, 1, "");
511 BTOR_MSG (btor->msg, 1, "rewrite rule cache");
512 BTOR_MSG (btor->msg, 1, " %lld cached (add) ", btor->rw_cache->num_add);
513 BTOR_MSG (btor->msg, 1, " %lld cached (get)", btor->rw_cache->num_get);
514 BTOR_MSG (btor->msg, 1, " %lld updated", btor->rw_cache->num_update);
515 BTOR_MSG (btor->msg, 1, " %lld removed (gc)", btor->rw_cache->num_remove);
516 BTOR_MSG (btor->msg,
517 1,
518 " %.2f MB cache",
519 (btor->rw_cache->cache->count * sizeof (BtorRwCacheTuple)
520 + btor->rw_cache->cache->count * sizeof (BtorPtrHashBucket)
521 + btor->rw_cache->cache->size * sizeof (BtorPtrHashBucket *))
522 / (double) (1 << 20));
523
524 #ifndef NDEBUG
525 BtorPtrHashTableIterator it;
526 char *rule;
527 int32_t num = 0;
528 BTOR_MSG (btor->msg, 1, "applied rewriting rules:");
529 if (btor->stats.rw_rules_applied->count == 0)
530 BTOR_MSG (btor->msg, 1, " none");
531 else
532 {
533 btor_iter_hashptr_init (&it, btor->stats.rw_rules_applied);
534 while (btor_iter_hashptr_has_next (&it))
535 {
536 num = it.bucket->data.as_int;
537 rule = btor_iter_hashptr_next (&it);
538 BTOR_MSG (btor->msg, 1, " %5d %s", num, rule);
539 }
540 }
541 #endif
542
543 BTOR_MSG (btor->msg, 1, "");
544 BTOR_MSG (btor->msg, 1, "bit blasting statistics:");
545 BTOR_MSG (btor->msg,
546 1,
547 " %7lld AIG vectors (%lld max)",
548 btor->avmgr ? btor->avmgr->cur_num_aigvecs : 0,
549 btor->avmgr ? btor->avmgr->max_num_aigvecs : 0);
550 BTOR_MSG (btor->msg,
551 1,
552 " %7lld AIG ANDs (%lld max)",
553 btor->avmgr ? btor->avmgr->amgr->cur_num_aigs : 0,
554 btor->avmgr ? btor->avmgr->amgr->max_num_aigs : 0);
555 BTOR_MSG (btor->msg,
556 1,
557 " %7lld AIG variables",
558 btor->avmgr ? btor->avmgr->amgr->max_num_aig_vars : 0);
559 BTOR_MSG (btor->msg,
560 1,
561 " %7lld CNF variables",
562 btor->avmgr ? btor->avmgr->amgr->num_cnf_vars : 0);
563 BTOR_MSG (btor->msg,
564 1,
565 " %7lld CNF clauses",
566 btor->avmgr ? btor->avmgr->amgr->num_cnf_clauses : 0);
567 BTOR_MSG (btor->msg,
568 1,
569 " %7lld CNF literals",
570 btor->avmgr ? btor->avmgr->amgr->num_cnf_literals : 0);
571
572 if (btor->slv) btor->slv->api.print_stats (btor->slv);
573
574 #ifdef BTOR_TIME_STATISTICS
575 BTOR_MSG (btor->msg, 1, "");
576 BTOR_MSG (btor->msg, 1, "%.2f seconds beta-reduction", btor->time.beta);
577 BTOR_MSG (btor->msg,
578 1,
579 "%.2f seconds synthesize expressions",
580 btor->time.synth_exp);
581 BTOR_MSG (btor->msg,
582 1,
583 "%.2f seconds determining failed assumptions",
584 btor->time.failed);
585 BTOR_MSG (btor->msg, 1, "%.2f seconds cloning", btor->time.cloning);
586 BTOR_MSG (btor->msg,
587 1,
588 "%.2f seconds substitute and rebuild",
589 btor->time.subst_rebuild);
590 if (btor_opt_get (btor, BTOR_OPT_MODEL_GEN))
591 BTOR_MSG (
592 btor->msg, 1, "%.2f seconds model generation", btor->time.model_gen);
593
594 BTOR_MSG (btor->msg, 1, "");
595 BTOR_MSG (btor->msg, 1, "%.2f seconds solving", btor->time.sat);
596 BTOR_MSG (
597 btor->msg, 1, " %.2f seconds rewriting engine", btor->time.simplify);
598 BTOR_MSG (btor->msg,
599 1,
600 " %.2f seconds variable substitution (%.0f%%)",
601 btor->time.subst,
602 percent (btor->time.subst, btor->time.simplify));
603 BTOR_MSG (btor->msg, 1, " %.2f seconds rewriting", btor->time.rewrite);
604 BTOR_MSG (
605 btor->msg, 1, " %.2f seconds occurrence check", btor->time.occurrence);
606
607 BTOR_MSG (btor->msg,
608 1,
609 " %.2f seconds embedded substitution (%.0f%%)",
610 btor->time.embedded,
611 percent (btor->time.embedded, btor->time.simplify));
612
613 if (btor_opt_get (btor, BTOR_OPT_ELIMINATE_SLICES))
614 BTOR_MSG (btor->msg,
615 1,
616 " %.2f seconds variable slicing (%.0f%%)",
617 btor->time.slicing,
618 percent (btor->time.slicing, btor->time.simplify));
619
620 #ifndef BTOR_DO_NOT_PROCESS_SKELETON
621 BTOR_MSG (btor->msg,
622 1,
623 " %.2f seconds skeleton preprocessing (%.0f%%)",
624 btor->time.skel,
625 percent (btor->time.skel, btor->time.simplify));
626 #endif
627
628 if (btor_opt_get (btor, BTOR_OPT_UCOPT))
629 BTOR_MSG (btor->msg,
630 1,
631 " %.2f seconds unconstrained optimization",
632 btor->time.ucopt);
633
634 if (btor_opt_get (btor, BTOR_OPT_EXTRACT_LAMBDAS))
635 BTOR_MSG (btor->msg,
636 1,
637 " %.2f seconds lambda extraction (%.0f%%)",
638 btor->time.extract,
639 percent (btor->time.extract, btor->time.simplify));
640
641 if (btor_opt_get (btor, BTOR_OPT_MERGE_LAMBDAS))
642 BTOR_MSG (btor->msg,
643 1,
644 " %.2f seconds lambda merging (%.0f%%)",
645 btor->time.merge,
646 percent (btor->time.merge, btor->time.simplify));
647
648 if (btor_opt_get (btor, BTOR_OPT_BETA_REDUCE))
649 BTOR_MSG (btor->msg,
650 1,
651 " %.2f seconds apply elimination (%.0f%%)",
652 btor->time.elimapplies,
653 percent (btor->time.elimapplies, btor->time.simplify));
654
655 if (btor_opt_get (btor, BTOR_OPT_ACKERMANN))
656 BTOR_MSG (btor->msg,
657 1,
658 " %.2f seconds ackermann constraints (%.0f%%)",
659 btor->time.ack,
660 percent (btor->time.ack, btor->time.simplify));
661
662 if (btor->slv) btor->slv->api.print_time_stats (btor->slv);
663 #endif
664
665 BTOR_MSG (btor->msg, 1, "");
666 BTOR_MSG (
667 btor->msg, 1, "%.1f MB", btor->mm->maxallocated / (double) (1 << 20));
668 }
669
670 Btor *
btor_new(void)671 btor_new (void)
672 {
673 BtorMemMgr *mm;
674 Btor *btor;
675
676 mm = btor_mem_mgr_new ();
677 BTOR_CNEW (mm, btor);
678
679 btor->mm = mm;
680 btor->msg = btor_msg_new (btor);
681 btor_set_msg_prefix (btor, "btor");
682
683 BTOR_INIT_UNIQUE_TABLE (mm, btor->nodes_unique_table);
684 BTOR_INIT_SORT_UNIQUE_TABLE (mm, btor->sorts_unique_table);
685 BTOR_INIT_STACK (btor->mm, btor->nodes_id_table);
686 BTOR_PUSH_STACK (btor->nodes_id_table, 0);
687 BTOR_INIT_STACK (btor->mm, btor->functions_with_model);
688 BTOR_INIT_STACK (btor->mm, btor->outputs);
689
690 btor_opt_init_opts (btor);
691
692 btor->avmgr = btor_aigvec_mgr_new (btor);
693
694 btor_rng_init (&btor->rng, btor_opt_get (btor, BTOR_OPT_SEED));
695
696 btor->bv_assignments = btor_ass_new_bv_list (mm);
697 btor->fun_assignments = btor_ass_new_fun_list (mm);
698
699 btor->symbols = btor_hashptr_table_new (
700 mm, (BtorHashPtr) btor_hash_str, (BtorCmpPtr) strcmp);
701 btor->node2symbol =
702 btor_hashptr_table_new (mm,
703 (BtorHashPtr) btor_node_hash_by_id,
704 (BtorCmpPtr) btor_node_compare_by_id);
705
706 btor->inputs = btor_hashptr_table_new (mm,
707 (BtorHashPtr) btor_node_hash_by_id,
708 (BtorCmpPtr) btor_node_compare_by_id);
709 btor->bv_vars = btor_hashptr_table_new (mm,
710 (BtorHashPtr) btor_node_hash_by_id,
711 (BtorCmpPtr) btor_node_compare_by_id);
712 btor->ufs = btor_hashptr_table_new (mm,
713 (BtorHashPtr) btor_node_hash_by_id,
714 (BtorCmpPtr) btor_node_compare_by_id);
715 btor->lambdas = btor_hashptr_table_new (mm,
716 (BtorHashPtr) btor_node_hash_by_id,
717 (BtorCmpPtr) btor_node_compare_by_id);
718 btor->quantifiers =
719 btor_hashptr_table_new (mm,
720 (BtorHashPtr) btor_node_hash_by_id,
721 (BtorCmpPtr) btor_node_compare_by_id);
722 btor->exists_vars =
723 btor_hashptr_table_new (mm,
724 (BtorHashPtr) btor_node_hash_by_id,
725 (BtorCmpPtr) btor_node_compare_by_id);
726 btor->forall_vars =
727 btor_hashptr_table_new (mm,
728 (BtorHashPtr) btor_node_hash_by_id,
729 (BtorCmpPtr) btor_node_compare_by_id);
730 btor->feqs = btor_hashptr_table_new (mm,
731 (BtorHashPtr) btor_node_hash_by_id,
732 (BtorCmpPtr) btor_node_compare_by_id);
733
734 btor->valid_assignments = 1;
735
736 btor->varsubst_constraints =
737 btor_hashptr_table_new (mm,
738 (BtorHashPtr) btor_node_hash_by_id,
739 (BtorCmpPtr) btor_node_compare_by_id);
740 btor->embedded_constraints =
741 btor_hashptr_table_new (mm,
742 (BtorHashPtr) btor_node_hash_by_id,
743 (BtorCmpPtr) btor_node_compare_by_id);
744 btor->unsynthesized_constraints =
745 btor_hashptr_table_new (mm,
746 (BtorHashPtr) btor_node_hash_by_id,
747 (BtorCmpPtr) btor_node_compare_by_id);
748 btor->synthesized_constraints =
749 btor_hashptr_table_new (mm,
750 (BtorHashPtr) btor_node_hash_by_id,
751 (BtorCmpPtr) btor_node_compare_by_id);
752 btor->assumptions =
753 btor_hashptr_table_new (mm,
754 (BtorHashPtr) btor_node_hash_by_id,
755 (BtorCmpPtr) btor_node_compare_by_id);
756 btor->orig_assumptions =
757 btor_hashptr_table_new (mm,
758 (BtorHashPtr) btor_node_hash_by_id,
759 (BtorCmpPtr) btor_node_compare_by_id);
760 BTOR_INIT_STACK (mm, btor->failed_assumptions);
761 btor->parameterized =
762 btor_hashptr_table_new (mm,
763 (BtorHashPtr) btor_node_hash_by_id,
764 (BtorCmpPtr) btor_node_compare_by_id);
765
766 BTOR_INIT_STACK (mm, btor->assertions);
767 BTOR_INIT_STACK (mm, btor->assertions_trail);
768 btor->assertions_cache = btor_hashint_table_new (mm);
769
770 #ifndef NDEBUG
771 btor->stats.rw_rules_applied = btor_hashptr_table_new (
772 mm, (BtorHashPtr) btor_hash_str, (BtorCmpPtr) strcmp);
773 #endif
774
775 btor->true_exp = btor_exp_true (btor);
776
777 BTOR_CNEW (mm, btor->rw_cache);
778 btor_rw_cache_init (btor->rw_cache, btor);
779
780 return btor;
781 }
782
783 static int32_t
terminate_aux_btor(void * btor)784 terminate_aux_btor (void *btor)
785 {
786 assert (btor);
787
788 int32_t res;
789 Btor *bt;
790
791 bt = (Btor *) btor;
792 if (!bt->cbs.term.fun) return 0;
793 if (bt->cbs.term.done) return 1;
794 res = ((int32_t (*) (void *)) bt->cbs.term.fun) (bt->cbs.term.state);
795 if (res) bt->cbs.term.done = res;
796 return res;
797 }
798
799 int32_t
btor_terminate(Btor * btor)800 btor_terminate (Btor *btor)
801 {
802 assert (btor);
803
804 if (btor->cbs.term.termfun) return btor->cbs.term.termfun (btor);
805 return 0;
806 }
807
808 void
btor_set_term(Btor * btor,int32_t (* fun)(void *),void * state)809 btor_set_term (Btor *btor, int32_t (*fun) (void *), void *state)
810 {
811 assert (btor);
812
813 BtorSATMgr *smgr;
814
815 btor->cbs.term.termfun = terminate_aux_btor;
816 btor->cbs.term.fun = fun;
817 btor->cbs.term.state = state;
818
819 smgr = btor_get_sat_mgr (btor);
820 btor_sat_mgr_set_term (smgr, terminate_aux_btor, btor);
821 }
822
823 static void
release_all_ext_exp_refs(Btor * btor)824 release_all_ext_exp_refs (Btor *btor)
825 {
826 assert (btor);
827
828 uint32_t i, cnt;
829 BtorNode *exp;
830
831 for (i = 1, cnt = BTOR_COUNT_STACK (btor->nodes_id_table); i <= cnt; i++)
832 {
833 if (!(exp = BTOR_PEEK_STACK (btor->nodes_id_table, cnt - i))) continue;
834 if (exp->ext_refs)
835 {
836 assert (exp->ext_refs <= exp->refs);
837 exp->refs = exp->refs - exp->ext_refs + 1;
838 btor->external_refs -= exp->ext_refs;
839 assert (exp->refs > 0);
840 exp->ext_refs = 0;
841 btor_node_release (btor, exp);
842 }
843 }
844 }
845
846 static void
release_all_ext_sort_refs(Btor * btor)847 release_all_ext_sort_refs (Btor *btor)
848 {
849 assert (btor);
850
851 uint32_t i, cnt;
852 BtorSort *sort;
853
854 cnt = BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort);
855 for (i = 1; i <= cnt; i++)
856 {
857 sort = BTOR_PEEK_STACK (btor->sorts_unique_table.id2sort, cnt - i);
858 if (!sort) continue;
859 assert (sort->refs);
860 assert (sort->ext_refs <= sort->refs);
861 sort->refs = sort->refs - sort->ext_refs + 1;
862 btor->external_refs -= sort->ext_refs;
863 assert (sort->refs > 0);
864 sort->ext_refs = 0;
865 btor_sort_release (btor, sort->id);
866 }
867 }
868
869 void
btor_release_all_ext_refs(Btor * btor)870 btor_release_all_ext_refs (Btor *btor)
871 {
872 release_all_ext_exp_refs (btor);
873 release_all_ext_sort_refs (btor);
874 }
875
876 void
btor_delete_varsubst_constraints(Btor * btor)877 btor_delete_varsubst_constraints (Btor *btor)
878 {
879 BtorPtrHashTableIterator it;
880 btor_iter_hashptr_init (&it, btor->varsubst_constraints);
881 while (btor_iter_hashptr_has_next (&it))
882 {
883 btor_node_release (btor, it.bucket->data.as_ptr);
884 btor_node_release (btor, btor_iter_hashptr_next (&it));
885 }
886 btor_hashptr_table_delete (btor->varsubst_constraints);
887 }
888
889 void
btor_delete(Btor * btor)890 btor_delete (Btor *btor)
891 {
892 assert (btor);
893
894 uint32_t i, cnt;
895 BtorNodePtrStack stack;
896 BtorMemMgr *mm;
897 BtorNode *exp;
898 BtorPtrHashTableIterator it;
899
900 mm = btor->mm;
901 btor_rng_delete (&btor->rng);
902
903 if (btor->slv) btor->slv->api.delet (btor->slv);
904
905 if (btor->parse_error_msg) btor_mem_freestr (mm, btor->parse_error_msg);
906
907 btor_ass_delete_bv_list (
908 btor->bv_assignments,
909 btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP)
910 || btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP_INTERNAL));
911 btor_ass_delete_fun_list (
912 btor->fun_assignments,
913 btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP)
914 || btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP_INTERNAL));
915
916 btor_delete_varsubst_constraints (btor);
917
918 btor_iter_hashptr_init (&it, btor->inputs);
919 btor_iter_hashptr_queue (&it, btor->embedded_constraints);
920 btor_iter_hashptr_queue (&it, btor->unsynthesized_constraints);
921 btor_iter_hashptr_queue (&it, btor->synthesized_constraints);
922 btor_iter_hashptr_queue (&it, btor->assumptions);
923 btor_iter_hashptr_queue (&it, btor->orig_assumptions);
924 while (btor_iter_hashptr_has_next (&it))
925 btor_node_release (btor, btor_iter_hashptr_next (&it));
926
927 btor_hashptr_table_delete (btor->inputs);
928 btor_hashptr_table_delete (btor->embedded_constraints);
929 btor_hashptr_table_delete (btor->unsynthesized_constraints);
930 btor_hashptr_table_delete (btor->synthesized_constraints);
931 btor_hashptr_table_delete (btor->assumptions);
932 btor_hashptr_table_delete (btor->orig_assumptions);
933 for (i = 0; i < BTOR_COUNT_STACK (btor->failed_assumptions); i++)
934 {
935 if (BTOR_PEEK_STACK (btor->failed_assumptions, i))
936 btor_node_release (btor, BTOR_PEEK_STACK (btor->failed_assumptions, i));
937 }
938 BTOR_RELEASE_STACK (btor->failed_assumptions);
939
940 for (i = 0; i < BTOR_COUNT_STACK (btor->assertions); i++)
941 btor_node_release (btor, BTOR_PEEK_STACK (btor->assertions, i));
942 BTOR_RELEASE_STACK (btor->assertions);
943 BTOR_RELEASE_STACK (btor->assertions_trail);
944 btor_hashint_table_delete (btor->assertions_cache);
945
946 btor_model_delete (btor);
947 btor_node_release (btor, btor->true_exp);
948
949 for (i = 0; i < BTOR_COUNT_STACK (btor->functions_with_model); i++)
950 btor_node_release (btor, BTOR_PEEK_STACK (btor->functions_with_model, i));
951 BTOR_RELEASE_STACK (btor->functions_with_model);
952
953 for (i = 0; i < BTOR_COUNT_STACK (btor->outputs); i++)
954 btor_node_release (btor, BTOR_PEEK_STACK (btor->outputs, i));
955 BTOR_RELEASE_STACK (btor->outputs);
956
957 BTOR_INIT_STACK (mm, stack);
958 /* copy lambdas and push onto stack since btor->lambdas does not hold a
959 * reference and they may get released if btor_node_lambda_delete_static_rho
960 * is called */
961 btor_iter_hashptr_init (&it, btor->lambdas);
962 while (btor_iter_hashptr_has_next (&it))
963 {
964 exp = btor_iter_hashptr_next (&it);
965 BTOR_PUSH_STACK (stack, btor_node_copy (btor, exp));
966 }
967 while (!BTOR_EMPTY_STACK (stack))
968 {
969 exp = BTOR_POP_STACK (stack);
970 btor_node_lambda_delete_static_rho (btor, exp);
971 btor_node_release (btor, exp);
972 }
973 BTOR_RELEASE_STACK (stack);
974
975 if (btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP) && btor->external_refs)
976 release_all_ext_exp_refs (btor);
977
978 if (btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP_INTERNAL))
979 {
980 cnt = BTOR_COUNT_STACK (btor->nodes_id_table);
981 for (i = 1; i <= cnt; i++)
982 {
983 exp = BTOR_PEEK_STACK (btor->nodes_id_table, cnt - i);
984 if (!exp) continue;
985 if (btor_node_is_simplified (exp)) exp->simplified = 0;
986 }
987 for (i = 1; i <= cnt; i++)
988 {
989 exp = BTOR_PEEK_STACK (btor->nodes_id_table, cnt - i);
990 if (!exp) continue;
991 assert (exp->refs);
992 exp->refs = 1;
993 btor->external_refs -= exp->ext_refs;
994 exp->ext_refs = 0;
995 btor_node_release (btor, exp);
996 assert (!BTOR_PEEK_STACK (btor->nodes_id_table, cnt - i));
997 }
998 }
999
1000 if (btor_opt_get (btor, BTOR_OPT_AUTO_CLEANUP) && btor->external_refs)
1001 release_all_ext_sort_refs (btor);
1002
1003 assert (getenv ("BTORLEAK") || btor->external_refs == 0);
1004
1005 #ifndef NDEBUG
1006 bool node_leak = false;
1007 BtorNode *cur;
1008 /* we need to check id_table here as not all nodes are in the unique table */
1009 for (i = 0; i < BTOR_COUNT_STACK (btor->nodes_id_table); i++)
1010 {
1011 cur = BTOR_PEEK_STACK (btor->nodes_id_table, i);
1012 if (cur)
1013 {
1014 BTORLOG (1,
1015 " unreleased node: %s (%d)",
1016 btor_util_node2string (cur),
1017 cur->refs);
1018 node_leak = true;
1019 }
1020 }
1021 assert (getenv ("BTORLEAK") || getenv ("BTORLEAKEXP") || !node_leak);
1022 #endif
1023 BTOR_RELEASE_UNIQUE_TABLE (mm, btor->nodes_unique_table);
1024 BTOR_RELEASE_STACK (btor->nodes_id_table);
1025
1026 assert (getenv ("BTORLEAK") || getenv ("BTORLEAKSORT")
1027 || btor->sorts_unique_table.num_elements == 0);
1028 BTOR_RELEASE_SORT_UNIQUE_TABLE (mm, btor->sorts_unique_table);
1029
1030 btor_hashptr_table_delete (btor->node2symbol);
1031 btor_iter_hashptr_init (&it, btor->symbols);
1032 while (btor_iter_hashptr_has_next (&it))
1033 btor_mem_freestr (btor->mm, (char *) btor_iter_hashptr_next (&it));
1034 btor_hashptr_table_delete (btor->symbols);
1035
1036 btor_hashptr_table_delete (btor->bv_vars);
1037 btor_hashptr_table_delete (btor->ufs);
1038 btor_hashptr_table_delete (btor->lambdas);
1039 btor_hashptr_table_delete (btor->quantifiers);
1040 assert (btor->exists_vars->count == 0);
1041 btor_hashptr_table_delete (btor->exists_vars);
1042 assert (btor->forall_vars->count == 0);
1043 btor_hashptr_table_delete (btor->forall_vars);
1044 btor_hashptr_table_delete (btor->feqs);
1045 btor_hashptr_table_delete (btor->parameterized);
1046 #ifndef NDEBUG
1047 btor_hashptr_table_delete (btor->stats.rw_rules_applied);
1048 #endif
1049
1050 if (btor->avmgr) btor_aigvec_mgr_delete (btor->avmgr);
1051 btor_opt_delete_opts (btor);
1052
1053 btor_rw_cache_delete (btor->rw_cache);
1054 BTOR_DELETE (mm, btor->rw_cache);
1055
1056 assert (btor->rec_rw_calls == 0);
1057 btor_msg_delete (btor->msg);
1058 BTOR_DELETE (mm, btor);
1059 btor_mem_mgr_delete (mm);
1060 }
1061
1062 void
btor_set_msg_prefix(Btor * btor,const char * prefix)1063 btor_set_msg_prefix (Btor *btor, const char *prefix)
1064 {
1065 assert (btor);
1066
1067 btor_mem_freestr (btor->mm, btor->msg->prefix);
1068 btor->msg->prefix =
1069 prefix ? btor_mem_strdup (btor->mm, prefix) : (char *) prefix;
1070 }
1071
1072 /* synthesizes unsynthesized constraints and updates constraints tables. */
1073 void
btor_process_unsynthesized_constraints(Btor * btor)1074 btor_process_unsynthesized_constraints (Btor *btor)
1075 {
1076 assert (btor);
1077 assert (!btor->inconsistent);
1078
1079 BtorPtrHashTable *uc, *sc;
1080 BtorPtrHashBucket *bucket;
1081 BtorNode *cur;
1082 BtorAIG *aig;
1083 BtorAIGMgr *amgr;
1084
1085 uc = btor->unsynthesized_constraints;
1086 sc = btor->synthesized_constraints;
1087 amgr = btor_get_aig_mgr (btor);
1088
1089 while (uc->count > 0)
1090 {
1091 bucket = uc->first;
1092 assert (bucket);
1093 cur = (BtorNode *) bucket->key;
1094
1095 #if 0
1096 #ifndef NDEBUG
1097 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 2)
1098 {
1099 BtorNode * real_cur = btor_node_real_addr (cur);
1100 if (btor_node_is_bv_eq (real_cur))
1101 {
1102 BtorNode * left = real_cur->e[0];
1103 BtorNode * right = real_cur->e[1];
1104 BtorNode * other;
1105
1106 if (btor_node_is_bv_const (left))
1107 other = right;
1108 else if (btor_node_is_bv_const (right))
1109 other = left;
1110 else
1111 other = 0;
1112
1113 // FIXME fails with symbolic lemmas (during beta-reduction
1114 // rewrite level is forced to 1, hence symbolic lemmas might
1115 // not be simplified as much as possible). possible solution:
1116 // use rewrite level > 1 for lemma generation.
1117 //if (other
1118 // && !btor_node_is_inverted (other)
1119 // && btor_node_is_bv_add (other))
1120 // {
1121 // assert (!btor_node_is_bv_const (other->e[0]));
1122 // assert (!btor_node_is_bv_const (other->e[1]));
1123 // }
1124 }
1125 }
1126 #endif
1127 #endif
1128
1129 if (!btor_hashptr_table_get (sc, cur))
1130 {
1131 aig = exp_to_aig (btor, cur);
1132 if (aig == BTOR_AIG_FALSE)
1133 {
1134 btor->found_constraint_false = true;
1135 break;
1136 }
1137 btor_aig_add_toplevel_to_sat (amgr, aig);
1138 btor_aig_release (amgr, aig);
1139 (void) btor_hashptr_table_add (sc, cur);
1140 btor_hashptr_table_remove (uc, cur, 0, 0);
1141
1142 btor->stats.constraints.synthesized++;
1143 report_constraint_stats (btor, false);
1144 }
1145 else
1146 {
1147 /* constraint is already in sc */
1148 btor_hashptr_table_remove (uc, cur, 0, 0);
1149 btor_node_release (btor, cur);
1150 }
1151 }
1152 }
1153
1154 void
btor_insert_unsynthesized_constraint(Btor * btor,BtorNode * exp)1155 btor_insert_unsynthesized_constraint (Btor *btor, BtorNode *exp)
1156 {
1157 assert (btor);
1158 assert (exp);
1159 assert (!btor_node_real_addr (exp)->parameterized);
1160
1161 BtorBitVector *bits;
1162 BtorPtrHashTable *uc;
1163
1164 if (btor_node_is_bv_const (exp))
1165 {
1166 bits = btor_node_bv_const_get_bits (exp);
1167 assert (btor_bv_get_width (bits) == 1);
1168 if ((btor_node_is_inverted (exp) && btor_bv_get_bit (bits, 0))
1169 || (!btor_node_is_inverted (exp) && !btor_bv_get_bit (bits, 0)))
1170 {
1171 btor->inconsistent = true;
1172 return;
1173 }
1174 /* we do not add true */
1175 assert ((btor_node_is_inverted (exp) && !btor_bv_get_bit (bits, 0))
1176 || (!btor_node_is_inverted (exp) && btor_bv_get_bit (bits, 0)));
1177 return;
1178 }
1179
1180 uc = btor->unsynthesized_constraints;
1181 if (!btor_hashptr_table_get (uc, exp))
1182 {
1183 (void) btor_hashptr_table_add (uc, btor_node_copy (btor, exp));
1184 btor_node_real_addr (exp)->constraint = 1;
1185 btor->stats.constraints.unsynthesized++;
1186 BTORLOG (
1187 1, "add unsynthesized constraint: %s", btor_util_node2string (exp));
1188 }
1189
1190 /* Insert into embedded constraint table if constraint has parents.
1191 * Expressions containing embedded constraints get rebuilt and the embedded
1192 * constraint is substituted by true/false. */
1193 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1
1194 && btor_node_real_addr (exp)->parents > 0
1195 && !btor_hashptr_table_get (btor->embedded_constraints, exp))
1196 {
1197 assert (!btor_node_is_bv_const (exp));
1198 (void) btor_hashptr_table_add (btor->embedded_constraints,
1199 btor_node_copy (btor, exp));
1200 btor->stats.constraints.embedded++;
1201 BTORLOG (1,
1202 "add embedded constraint: %s (%u parents)",
1203 btor_util_node2string (exp),
1204 btor_node_real_addr (exp)->parents);
1205 }
1206 }
1207
1208 static bool
constraint_is_inconsistent(Btor * btor,BtorNode * exp)1209 constraint_is_inconsistent (Btor *btor, BtorNode *exp)
1210 {
1211 assert (btor);
1212 assert (exp);
1213 // assert (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1);
1214 assert (btor_node_bv_get_width (btor, exp) == 1);
1215
1216 exp = btor_simplify_exp (btor, exp);
1217
1218 return btor_node_is_bv_const_zero (btor, exp)
1219 || btor_hashptr_table_get (btor->synthesized_constraints,
1220 btor_node_invert (exp))
1221 || btor_hashptr_table_get (btor->unsynthesized_constraints,
1222 btor_node_invert (exp));
1223 }
1224
1225 static void
insert_into_constraint_tables(Btor * btor,BtorNode * exp)1226 insert_into_constraint_tables (Btor *btor, BtorNode *exp)
1227 {
1228 if (constraint_is_inconsistent (btor, exp))
1229 {
1230 btor->inconsistent = true;
1231 }
1232 else
1233 {
1234 if (!btor_node_real_addr (exp)->constraint)
1235 {
1236 btor_insert_unsynthesized_constraint (btor, exp);
1237 }
1238 else
1239 {
1240 assert (btor_hashptr_table_get (btor->unsynthesized_constraints, exp)
1241 || btor_hashptr_table_get (btor->synthesized_constraints, exp));
1242 }
1243 }
1244 }
1245
1246 static void
insert_varsubst_constraint(Btor * btor,BtorNode * left,BtorNode * right)1247 insert_varsubst_constraint (Btor *btor, BtorNode *left, BtorNode *right)
1248 {
1249 assert (btor);
1250 assert (left);
1251 assert (right);
1252
1253 BtorNode *eq;
1254 BtorPtrHashTable *vsc;
1255 BtorPtrHashBucket *bucket;
1256
1257 vsc = btor->varsubst_constraints;
1258 bucket = btor_hashptr_table_get (vsc, left);
1259
1260 if (!bucket)
1261 {
1262 BTORLOG (1,
1263 "add variable substitution: %s -> %s",
1264 btor_util_node2string (left),
1265 btor_util_node2string (right));
1266
1267 btor_hashptr_table_add (vsc, btor_node_copy (btor, left))->data.as_ptr =
1268 btor_node_copy (btor, right);
1269
1270 btor->stats.constraints.varsubst++;
1271
1272 /* Always add varsubst contraints into unsynthesized/embedded contraints.
1273 * Otherwise, we get an inconsistent state if varsubst is disabled and
1274 * not all varsubst constraints have been processed. */
1275 eq = btor_exp_eq (btor, left, right);
1276 insert_into_constraint_tables (btor, eq);
1277 btor_node_release (btor, eq);
1278 }
1279 /* if v = t_1 is already in varsubst, we have to synthesize v = t_2 */
1280 else if (right != (BtorNode *) bucket->data.as_ptr)
1281 {
1282 eq = btor_exp_eq (btor, left, right);
1283 insert_into_constraint_tables (btor, eq);
1284 btor_node_release (btor, eq);
1285 }
1286 }
1287
1288 static BtorSubstCompKind
reverse_subst_comp_kind(Btor * btor,BtorSubstCompKind comp)1289 reverse_subst_comp_kind (Btor *btor, BtorSubstCompKind comp)
1290 {
1291 assert (btor);
1292 (void) btor;
1293 switch (comp)
1294 {
1295 case BTOR_SUBST_COMP_ULT_KIND: return BTOR_SUBST_COMP_UGT_KIND;
1296 case BTOR_SUBST_COMP_ULTE_KIND: return BTOR_SUBST_COMP_UGTE_KIND;
1297 case BTOR_SUBST_COMP_UGT_KIND: return BTOR_SUBST_COMP_ULT_KIND;
1298 default:
1299 assert (comp == BTOR_SUBST_COMP_UGTE_KIND);
1300 return BTOR_SUBST_COMP_ULTE_KIND;
1301 }
1302 }
1303
1304 /* check if left does not occur on the right side */
1305 static bool
occurrence_check(Btor * btor,BtorNode * left,BtorNode * right)1306 occurrence_check (Btor *btor, BtorNode *left, BtorNode *right)
1307 {
1308 assert (btor);
1309 assert (left);
1310 assert (right);
1311
1312 BtorNode *cur, *real_left;
1313 BtorNodePtrQueue queue;
1314 bool is_cyclic;
1315 uint32_t i;
1316 BtorMemMgr *mm;
1317 BtorIntHashTable *cache;
1318
1319 double start = btor_util_time_stamp ();
1320 is_cyclic = false;
1321 mm = btor->mm;
1322 cache = btor_hashint_table_new (mm);
1323 real_left = btor_node_real_addr (left);
1324 BTOR_INIT_QUEUE (mm, queue);
1325
1326 cur = btor_node_real_addr (right);
1327 goto OCCURRENCE_CHECK_ENTER_WITHOUT_POP;
1328
1329 do
1330 {
1331 cur = btor_node_real_addr (BTOR_DEQUEUE (queue));
1332 OCCURRENCE_CHECK_ENTER_WITHOUT_POP:
1333 assert (!btor_node_is_simplified (cur)
1334 || btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST));
1335 cur = btor_node_real_addr (btor_node_get_simplified (btor, cur));
1336
1337 if (real_left->id > cur->id) continue;
1338
1339 if (!btor_hashint_table_contains (cache, cur->id))
1340 {
1341 btor_hashint_table_add (cache, cur->id);
1342 if (cur == real_left)
1343 {
1344 is_cyclic = true;
1345 break;
1346 }
1347 for (i = 1; i <= cur->arity; i++)
1348 BTOR_ENQUEUE (queue, cur->e[cur->arity - i]);
1349 }
1350 } while (!BTOR_EMPTY_QUEUE (queue));
1351 BTOR_RELEASE_QUEUE (queue);
1352 btor_hashint_table_delete (cache);
1353 btor->time.occurrence += btor_util_time_stamp () - start;
1354 return is_cyclic;
1355 }
1356
1357 /* checks if we can substitute and normalizes arguments to substitution,
1358 * substitute left_result with right_result, exp is child of AND_NODE */
1359 static bool
normalize_substitution(Btor * btor,BtorNode * exp,BtorNode ** left_result,BtorNode ** right_result)1360 normalize_substitution (Btor *btor,
1361 BtorNode *exp,
1362 BtorNode **left_result,
1363 BtorNode **right_result)
1364 {
1365 assert (btor_opt_get (btor, BTOR_OPT_VAR_SUBST));
1366
1367 BtorNode *left, *right, *real_left, *real_right, *tmp, *inv, *var, *lambda;
1368 BtorNode *const_exp, *e0, *e1;
1369 uint32_t leadings;
1370 BtorBitVector *ic, *fc, *bits;
1371 BtorMemMgr *mm;
1372 BtorSubstCompKind comp;
1373 BtorSortId sort;
1374
1375 assert (btor);
1376 assert (exp);
1377 assert (left_result);
1378 assert (right_result);
1379 assert (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1);
1380 assert (btor_simplify_exp (btor, exp) == exp);
1381
1382 mm = btor->mm;
1383
1384 /* boolean BV_NODE, force assignment (right_result) w.r.t. phase */
1385 if (btor_node_is_bv_var (exp))
1386 {
1387 assert (btor_node_bv_get_width (btor, exp) == 1);
1388 sort = btor_sort_bv (btor, 1);
1389 if (btor_node_is_inverted (exp))
1390 {
1391 *left_result = btor_node_copy (btor, btor_node_real_addr (exp));
1392 *right_result = btor_exp_bv_zero (btor, sort);
1393 }
1394 else
1395 {
1396 *left_result = btor_node_copy (btor, exp);
1397 *right_result = btor_exp_bv_one (btor, sort);
1398 }
1399 btor_sort_release (btor, sort);
1400 return true;
1401 }
1402
1403 if (btor_node_is_bv_ult (exp))
1404 {
1405 e0 = btor_node_get_simplified (btor, btor_node_real_addr (exp)->e[0]);
1406 e1 = btor_node_get_simplified (btor, btor_node_real_addr (exp)->e[1]);
1407
1408 if (btor_node_is_bv_var (e0) || btor_node_is_bv_var (e1))
1409 {
1410 if (btor_node_is_inverted (exp))
1411 comp = BTOR_SUBST_COMP_UGTE_KIND;
1412 else
1413 comp = BTOR_SUBST_COMP_ULT_KIND;
1414
1415 if (btor_node_is_bv_var (e0))
1416 {
1417 var = e0;
1418 right = e1;
1419 }
1420 else
1421 {
1422 assert (btor_node_is_bv_var (e1));
1423 var = e1;
1424 right = e0;
1425 comp = reverse_subst_comp_kind (btor, comp);
1426 }
1427
1428 /* ~a comp b is equal to a reverse_comp ~b,
1429 * where comp in ult, ulte, ugt, ugte
1430 * (e.g. reverse_comp of ult is ugt) */
1431 if (btor_node_is_inverted (var))
1432 {
1433 var = btor_node_real_addr (var);
1434 right = btor_node_invert (right);
1435 comp = reverse_subst_comp_kind (btor, comp);
1436 }
1437
1438 /* we do not create a lambda (index) if variable is already in
1439 * substitution table */
1440 assert (!btor_node_is_inverted (var));
1441 if (btor_hashptr_table_get (btor->varsubst_constraints, var))
1442 return false;
1443
1444 if (!btor_node_is_bv_const (right)) return false;
1445
1446 if (btor_node_is_inverted (right))
1447 bits = btor_bv_not (mm, btor_node_bv_const_get_bits (right));
1448 else
1449 bits = btor_bv_copy (mm, btor_node_bv_const_get_bits (right));
1450
1451 if (comp == BTOR_SUBST_COMP_ULT_KIND || comp == BTOR_SUBST_COMP_ULTE_KIND)
1452 {
1453 leadings = btor_bv_get_num_leading_zeros (bits);
1454 if (leadings > 0)
1455 {
1456 sort = btor_sort_bv (btor, leadings);
1457 const_exp = btor_exp_bv_zero (btor, sort);
1458 btor_sort_release (btor, sort);
1459 sort = btor_sort_bv (btor,
1460 btor_node_bv_get_width (btor, var) - leadings);
1461 lambda = btor_exp_var (btor, sort, 0);
1462 btor_sort_release (btor, sort);
1463 tmp = btor_exp_bv_concat (btor, const_exp, lambda);
1464 insert_varsubst_constraint (btor, var, tmp);
1465 btor_node_release (btor, const_exp);
1466 btor_node_release (btor, lambda);
1467 btor_node_release (btor, tmp);
1468 }
1469 }
1470 else
1471 {
1472 assert (comp == BTOR_SUBST_COMP_UGT_KIND
1473 || comp == BTOR_SUBST_COMP_UGTE_KIND);
1474 leadings = btor_bv_get_num_leading_ones (bits);
1475 if (leadings > 0)
1476 {
1477 sort = btor_sort_bv (btor, leadings);
1478 const_exp = btor_exp_bv_ones (btor, sort);
1479 btor_sort_release (btor, sort);
1480 sort = btor_sort_bv (btor,
1481 btor_node_bv_get_width (btor, var) - leadings);
1482 lambda = btor_exp_var (btor, sort, 0);
1483 btor_sort_release (btor, sort);
1484 tmp = btor_exp_bv_concat (btor, const_exp, lambda);
1485 insert_varsubst_constraint (btor, var, tmp);
1486 btor_node_release (btor, const_exp);
1487 btor_node_release (btor, lambda);
1488 btor_node_release (btor, tmp);
1489 }
1490 }
1491
1492 btor_bv_free (btor->mm, bits);
1493 return false;
1494 }
1495 }
1496
1497 /* in the boolean case a != b is the same as a == ~b */
1498 if (btor_node_is_inverted (exp) && btor_node_is_bv_eq (exp)
1499 && btor_node_bv_get_width (btor, btor_node_real_addr (exp)->e[0]) == 1)
1500 {
1501 left = btor_node_get_simplified (btor, btor_node_real_addr (exp)->e[0]);
1502 right = btor_node_get_simplified (btor, btor_node_real_addr (exp)->e[1]);
1503
1504 if (btor_node_is_bv_var (left))
1505 {
1506 *left_result = btor_node_copy (btor, left);
1507 *right_result = btor_node_invert (btor_node_copy (btor, right));
1508 goto BTOR_NORMALIZE_SUBST_RESULT;
1509 }
1510
1511 if (btor_node_is_bv_var (right))
1512 {
1513 *left_result = btor_node_copy (btor, right);
1514 *right_result = btor_node_invert (btor_node_copy (btor, left));
1515 goto BTOR_NORMALIZE_SUBST_RESULT;
1516 }
1517 }
1518
1519 if (btor_node_is_inverted (exp) || !btor_node_is_array_or_bv_eq (exp))
1520 return false;
1521
1522 left = btor_node_get_simplified (btor, exp->e[0]);
1523 right = btor_node_get_simplified (btor, exp->e[1]);
1524 real_left = btor_node_real_addr (left);
1525 real_right = btor_node_real_addr (right);
1526
1527 if (!btor_node_is_bv_var (real_left) && !btor_node_is_bv_var (real_right)
1528 && !btor_node_is_uf (real_left) && !btor_node_is_uf (real_right))
1529 {
1530 if (btor_rewrite_linear_term (btor, left, &fc, left_result, &tmp))
1531 *right_result = btor_exp_bv_sub (btor, right, tmp);
1532 else if (btor_rewrite_linear_term (btor, right, &fc, left_result, &tmp))
1533 *right_result = btor_exp_bv_sub (btor, left, tmp);
1534 else
1535 return false;
1536
1537 btor->stats.gaussian_eliminations++;
1538
1539 btor_node_release (btor, tmp);
1540 ic = btor_bv_mod_inverse (btor->mm, fc);
1541 btor_bv_free (btor->mm, fc);
1542 inv = btor_exp_bv_const (btor, ic);
1543 btor_bv_free (btor->mm, ic);
1544 tmp = btor_exp_bv_mul (btor, *right_result, inv);
1545 btor_node_release (btor, inv);
1546 btor_node_release (btor, *right_result);
1547 *right_result = tmp;
1548 }
1549 else
1550 {
1551 if ((!btor_node_is_bv_var (real_left) && btor_node_is_bv_var (real_right))
1552 || (!btor_node_is_uf (real_left) && btor_node_is_uf (real_right)))
1553 {
1554 *left_result = right;
1555 *right_result = left;
1556 }
1557 else
1558 {
1559 *left_result = left;
1560 *right_result = right;
1561 }
1562
1563 btor_node_copy (btor, left);
1564 btor_node_copy (btor, right);
1565 }
1566
1567 BTOR_NORMALIZE_SUBST_RESULT:
1568 if (btor_node_is_inverted (*left_result))
1569 {
1570 *left_result = btor_node_invert (*left_result);
1571 *right_result = btor_node_invert (*right_result);
1572 }
1573
1574 if (occurrence_check (btor, *left_result, *right_result))
1575 {
1576 btor_node_release (btor, *left_result);
1577 btor_node_release (btor, *right_result);
1578 return false;
1579 }
1580
1581 return true;
1582 }
1583
1584 static void
insert_new_constraint(Btor * btor,BtorNode * exp)1585 insert_new_constraint (Btor *btor, BtorNode *exp)
1586 {
1587 assert (btor);
1588 assert (exp);
1589 assert (btor_node_bv_get_width (btor, exp) == 1);
1590 assert (!btor_node_real_addr (exp)->parameterized);
1591
1592 BtorBitVector *bits;
1593 BtorNode *left, *right, *real_exp;
1594
1595 exp = btor_simplify_exp (btor, exp);
1596 real_exp = btor_node_real_addr (exp);
1597
1598 if (btor_node_is_bv_const (real_exp))
1599 {
1600 bits = btor_node_bv_const_get_bits (real_exp);
1601 assert (btor_bv_get_width (bits) == 1);
1602 /* we do not add true/false */
1603 if ((btor_node_is_inverted (exp) && btor_bv_get_bit (bits, 0))
1604 || (!btor_node_is_inverted (exp) && !btor_bv_get_bit (bits, 0)))
1605 {
1606 BTORLOG (1,
1607 "inserted inconsistent constraint %s",
1608 btor_util_node2string (exp));
1609 btor->inconsistent = true;
1610 }
1611 else
1612 {
1613 assert ((btor_node_is_inverted (exp) && !btor_bv_get_bit (bits, 0))
1614 || (!btor_node_is_inverted (exp) && btor_bv_get_bit (bits, 0)));
1615 }
1616 return;
1617 }
1618
1619 if (!btor_hashptr_table_get (btor->synthesized_constraints, exp))
1620 {
1621 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1
1622 && btor_opt_get (btor, BTOR_OPT_VAR_SUBST)
1623 && normalize_substitution (btor, exp, &left, &right))
1624 {
1625 insert_varsubst_constraint (btor, left, right);
1626 btor_node_release (btor, left);
1627 btor_node_release (btor, right);
1628 }
1629 else
1630 {
1631 insert_into_constraint_tables (btor, exp);
1632 report_constraint_stats (btor, false);
1633 }
1634 }
1635 }
1636
1637 void
btor_reset_assumptions(Btor * btor)1638 btor_reset_assumptions (Btor *btor)
1639 {
1640 assert (btor);
1641
1642 BtorPtrHashTableIterator it;
1643 uint32_t i;
1644
1645 BTORLOG (2, "reset assumptions");
1646
1647 btor_iter_hashptr_init (&it, btor->assumptions);
1648 btor_iter_hashptr_queue (&it, btor->orig_assumptions);
1649 while (btor_iter_hashptr_has_next (&it))
1650 btor_node_release (btor, btor_iter_hashptr_next (&it));
1651 btor_hashptr_table_delete (btor->assumptions);
1652 btor_hashptr_table_delete (btor->orig_assumptions);
1653 btor->assumptions =
1654 btor_hashptr_table_new (btor->mm,
1655 (BtorHashPtr) btor_node_hash_by_id,
1656 (BtorCmpPtr) btor_node_compare_by_id);
1657 btor->orig_assumptions =
1658 btor_hashptr_table_new (btor->mm,
1659 (BtorHashPtr) btor_node_hash_by_id,
1660 (BtorCmpPtr) btor_node_compare_by_id);
1661
1662 for (i = 0; i < BTOR_COUNT_STACK (btor->failed_assumptions); i++)
1663 {
1664 if (BTOR_PEEK_STACK (btor->failed_assumptions, i))
1665 btor_node_release (btor, BTOR_PEEK_STACK (btor->failed_assumptions, i));
1666 }
1667 BTOR_RESET_STACK (btor->failed_assumptions);
1668 }
1669
1670 static void
reset_functions_with_model(Btor * btor)1671 reset_functions_with_model (Btor *btor)
1672 {
1673 BtorNode *cur;
1674 uint32_t i;
1675
1676 assert (btor);
1677
1678 for (i = 0; i < BTOR_COUNT_STACK (btor->functions_with_model); i++)
1679 {
1680 cur = btor->functions_with_model.start[i];
1681 assert (!btor_node_is_inverted (cur));
1682 if (!btor_node_is_simplified (cur))
1683 {
1684 assert (btor_node_is_fun (cur));
1685 assert (cur->rho);
1686 btor_hashptr_table_delete (cur->rho);
1687 cur->rho = 0;
1688 }
1689 btor_node_release (btor, cur);
1690 }
1691 BTOR_RESET_STACK (btor->functions_with_model);
1692 }
1693
1694 void
btor_reset_incremental_usage(Btor * btor)1695 btor_reset_incremental_usage (Btor *btor)
1696 {
1697 assert (btor);
1698
1699 btor_reset_assumptions (btor);
1700 reset_functions_with_model (btor);
1701 btor->valid_assignments = 0;
1702 btor_model_delete (btor);
1703 }
1704
1705 static void
add_constraint(Btor * btor,BtorNode * exp)1706 add_constraint (Btor *btor, BtorNode *exp)
1707 {
1708 assert (btor);
1709 assert (exp);
1710
1711 BtorNode *cur, *child;
1712 BtorNodePtrStack stack;
1713 BtorMemMgr *mm;
1714 BtorIntHashTable *mark;
1715
1716 exp = btor_simplify_exp (btor, exp);
1717 assert (!btor_node_is_fun (exp));
1718 assert (btor_node_bv_get_width (btor, exp) == 1);
1719 assert (!btor_node_real_addr (exp)->parameterized);
1720 mm = btor->mm;
1721 mark = btor_hashint_table_new (mm);
1722
1723 if (btor->valid_assignments) btor_reset_incremental_usage (btor);
1724
1725 if (!btor_node_is_inverted (exp) && btor_node_is_bv_and (exp))
1726 {
1727 BTOR_INIT_STACK (mm, stack);
1728 cur = exp;
1729 goto ADD_CONSTRAINT_ENTER_LOOP_WITHOUT_POP;
1730
1731 do
1732 {
1733 cur = BTOR_POP_STACK (stack);
1734 ADD_CONSTRAINT_ENTER_LOOP_WITHOUT_POP:
1735 assert (!btor_node_is_inverted (cur));
1736 assert (btor_node_is_bv_and (cur));
1737 if (!btor_hashint_table_contains (mark, cur->id))
1738 {
1739 btor_hashint_table_add (mark, cur->id);
1740 child = cur->e[1];
1741 if (!btor_node_is_inverted (child) && btor_node_is_bv_and (child))
1742 BTOR_PUSH_STACK (stack, child);
1743 else
1744 insert_new_constraint (btor, child);
1745 child = cur->e[0];
1746 if (!btor_node_is_inverted (child) && btor_node_is_bv_and (child))
1747 BTOR_PUSH_STACK (stack, child);
1748 else
1749 insert_new_constraint (btor, child);
1750 }
1751 } while (!BTOR_EMPTY_STACK (stack));
1752 BTOR_RELEASE_STACK (stack);
1753 }
1754 else
1755 insert_new_constraint (btor, exp);
1756
1757 btor_hashint_table_delete (mark);
1758 assert (btor_dbg_check_constraints_not_const (btor));
1759 }
1760
1761 void
btor_assert_exp(Btor * btor,BtorNode * exp)1762 btor_assert_exp (Btor *btor, BtorNode *exp)
1763 {
1764 assert (btor);
1765 assert (exp);
1766 exp = btor_simplify_exp (btor, exp);
1767 assert (!btor_node_is_fun (exp));
1768 assert (btor_node_bv_get_width (btor, exp) == 1);
1769 assert (!btor_node_real_addr (exp)->parameterized);
1770
1771 add_constraint (btor, exp);
1772 }
1773
1774 static int32_t
exp_to_cnf_lit(Btor * btor,BtorNode * exp)1775 exp_to_cnf_lit (Btor *btor, BtorNode *exp)
1776 {
1777 assert (btor);
1778 assert (exp);
1779 assert (btor_node_bv_get_width (btor, exp) == 1);
1780
1781 int32_t res, sign, val;
1782 BtorSATMgr *smgr;
1783 BtorAIGMgr *amgr;
1784 BtorAIG *aig;
1785
1786 exp = btor_simplify_exp (btor, exp);
1787
1788 sign = 1;
1789
1790 if (btor_node_is_inverted (exp))
1791 {
1792 exp = btor_node_invert (exp);
1793 sign *= -1;
1794 }
1795
1796 aig = exp_to_aig (btor, exp);
1797
1798 amgr = btor_get_aig_mgr (btor);
1799 smgr = btor_get_sat_mgr (btor);
1800
1801 if (btor_aig_is_const (aig))
1802 {
1803 res = smgr->true_lit;
1804 if (aig == BTOR_AIG_FALSE) sign *= -1;
1805 }
1806 else
1807 {
1808 if (BTOR_IS_INVERTED_AIG (aig))
1809 {
1810 aig = BTOR_INVERT_AIG (aig);
1811 sign *= -1;
1812 }
1813
1814 if (!aig->cnf_id) btor_aig_to_sat_tseitin (amgr, aig);
1815
1816 res = aig->cnf_id;
1817 btor_aig_release (amgr, aig);
1818
1819 if ((val = btor_sat_fixed (smgr, res)))
1820 {
1821 res = smgr->true_lit;
1822 if (val < 0) sign *= -1;
1823 }
1824 }
1825 res *= sign;
1826
1827 return res;
1828 }
1829
1830 void
btor_assume_exp(Btor * btor,BtorNode * exp)1831 btor_assume_exp (Btor *btor, BtorNode *exp)
1832 {
1833 assert (btor);
1834 assert (btor_opt_get (btor, BTOR_OPT_INCREMENTAL));
1835 assert (exp);
1836 assert (!btor_node_real_addr (exp)->parameterized);
1837
1838 if (btor->valid_assignments) btor_reset_incremental_usage (btor);
1839
1840 BTORLOG (2,
1841 "assume: %s (%s)",
1842 btor_util_node2string (exp),
1843 btor_util_node2string (btor_simplify_exp (btor, exp)));
1844
1845 if (!btor_hashptr_table_get (btor->orig_assumptions, exp))
1846 {
1847 btor_hashptr_table_add (btor->orig_assumptions, btor_node_copy (btor, exp));
1848 }
1849
1850 exp = btor_simplify_exp (btor, exp);
1851 if (!btor_hashptr_table_get (btor->assumptions, exp))
1852 {
1853 (void) btor_hashptr_table_add (btor->assumptions,
1854 btor_node_copy (btor, exp));
1855 }
1856 }
1857
1858 bool
btor_is_assumption_exp(Btor * btor,BtorNode * exp)1859 btor_is_assumption_exp (Btor *btor, BtorNode *exp)
1860 {
1861 assert (btor);
1862 assert (btor_opt_get (btor, BTOR_OPT_INCREMENTAL));
1863 assert (exp);
1864
1865 BTORLOG (2, "is_assumption: %s", btor_util_node2string (exp));
1866 return btor_hashptr_table_get (btor->orig_assumptions, exp) ? true : false;
1867 }
1868
1869 bool
btor_failed_exp(Btor * btor,BtorNode * exp)1870 btor_failed_exp (Btor *btor, BtorNode *exp)
1871 {
1872 assert (btor);
1873 assert (btor_opt_get (btor, BTOR_OPT_INCREMENTAL));
1874 assert (btor->last_sat_result == BTOR_RESULT_UNSAT);
1875 assert (exp);
1876 assert (btor_is_assumption_exp (btor, exp));
1877 BTORLOG (2,
1878 "check failed assumption: %s (%s)",
1879 btor_util_node2string (exp),
1880 btor_util_node2string (btor_simplify_exp (btor, exp)));
1881
1882 bool res;
1883 int32_t i, lit;
1884 double start;
1885 BtorAIG *aig;
1886 BtorNode *real_exp, *cur, *e;
1887 BtorNodePtrStack work_stack, assumptions;
1888 BtorSATMgr *smgr;
1889 BtorIntHashTable *mark;
1890
1891 start = btor_util_time_stamp ();
1892
1893 exp = btor_simplify_exp (btor, exp);
1894 assert (btor_node_real_addr (exp)->btor == btor);
1895 assert (!btor_node_is_fun (exp));
1896 assert (btor_node_bv_get_width (btor, exp) == 1);
1897 assert (!btor_node_real_addr (exp)->parameterized);
1898 mark = btor_hashint_table_new (btor->mm);
1899 smgr = btor_get_sat_mgr (btor);
1900 assert (smgr);
1901
1902 if (btor->inconsistent)
1903 {
1904 res = false;
1905 }
1906 else if (exp == btor->true_exp)
1907 {
1908 res = false;
1909 }
1910 else if (exp == btor_node_invert (btor->true_exp))
1911 {
1912 res = true;
1913 }
1914 else if (!btor_sat_is_initialized (smgr))
1915 {
1916 res = true;
1917 }
1918 else if (btor_node_is_inverted (exp) || !btor_node_is_bv_and (exp))
1919 {
1920 real_exp = btor_node_real_addr (exp);
1921 assert (btor->found_constraint_false || btor_node_is_synth (real_exp));
1922
1923 if (!btor_node_is_synth (real_exp))
1924 {
1925 res = false;
1926 }
1927 else if (btor->found_constraint_false)
1928 {
1929 res = ((btor_node_is_inverted (exp)
1930 && real_exp->av->aigs[0] == BTOR_AIG_TRUE)
1931 || (!btor_node_is_inverted (exp)
1932 && real_exp->av->aigs[0] == BTOR_AIG_FALSE));
1933 }
1934 else
1935 {
1936 if ((btor_node_is_inverted (exp)
1937 && real_exp->av->aigs[0] == BTOR_AIG_FALSE)
1938 || (!btor_node_is_inverted (exp)
1939 && real_exp->av->aigs[0] == BTOR_AIG_TRUE))
1940 {
1941 res = false;
1942 }
1943 else
1944 {
1945 lit = exp_to_cnf_lit (btor, exp);
1946 if (abs (lit) == smgr->true_lit)
1947 res = lit < 0;
1948 else
1949 res = btor_sat_failed (smgr, lit) > 0;
1950 }
1951 }
1952 }
1953 else
1954 {
1955 res = false;
1956 BTOR_INIT_STACK (btor->mm, assumptions);
1957 BTOR_INIT_STACK (btor->mm, work_stack);
1958 BTOR_PUSH_STACK (work_stack, exp);
1959 while (!BTOR_EMPTY_STACK (work_stack))
1960 {
1961 cur = BTOR_POP_STACK (work_stack);
1962 assert (!btor_node_is_inverted (cur));
1963 assert (btor_node_is_bv_and (cur));
1964 if (btor_hashint_table_contains (mark, cur->id)) continue;
1965 btor_hashint_table_add (mark, cur->id);
1966 for (i = 0; i < 2; i++)
1967 {
1968 e = cur->e[i];
1969 if (!btor_node_is_inverted (e) && btor_node_is_bv_and (e))
1970 BTOR_PUSH_STACK (work_stack, e);
1971 else
1972 {
1973 if (!btor_node_is_synth (btor_node_real_addr (e))) continue;
1974
1975 aig = btor_node_real_addr (e)->av->aigs[0];
1976 if ((btor_node_is_inverted (e) && aig == BTOR_AIG_FALSE)
1977 || (!btor_node_is_inverted (e) && aig == BTOR_AIG_TRUE))
1978 continue;
1979 if ((btor_node_is_inverted (e) && aig == BTOR_AIG_TRUE)
1980 || (!btor_node_is_inverted (e) && aig == BTOR_AIG_FALSE))
1981 goto ASSUMPTION_FAILED;
1982 if (btor->found_constraint_false) continue;
1983 BTOR_PUSH_STACK (assumptions, e);
1984 }
1985 }
1986 }
1987
1988 while (!BTOR_EMPTY_STACK (assumptions))
1989 {
1990 cur = BTOR_POP_STACK (assumptions);
1991 assert (btor_node_is_inverted (cur) || !btor_node_is_bv_and (cur));
1992 lit = exp_to_cnf_lit (btor, cur);
1993 if (lit == smgr->true_lit) continue;
1994 if (lit == -smgr->true_lit || btor_sat_failed (smgr, lit))
1995 {
1996 ASSUMPTION_FAILED:
1997 res = true;
1998 break;
1999 }
2000 }
2001 BTOR_RELEASE_STACK (work_stack);
2002 BTOR_RELEASE_STACK (assumptions);
2003 }
2004
2005 btor_hashint_table_delete (mark);
2006 btor->time.failed += btor_util_time_stamp () - start;
2007
2008 return res;
2009 }
2010
2011 void
btor_fixate_assumptions(Btor * btor)2012 btor_fixate_assumptions (Btor *btor)
2013 {
2014 BtorNode *exp;
2015 BtorNodePtrStack stack;
2016 BtorPtrHashTableIterator it;
2017 size_t i;
2018
2019 BTOR_INIT_STACK (btor->mm, stack);
2020 btor_iter_hashptr_init (&it, btor->assumptions);
2021 while (btor_iter_hashptr_has_next (&it))
2022 BTOR_PUSH_STACK (stack,
2023 btor_node_copy (btor, btor_iter_hashptr_next (&it)));
2024 for (i = 0; i < BTOR_COUNT_STACK (stack); i++)
2025 {
2026 exp = BTOR_PEEK_STACK (stack, i);
2027 btor_assert_exp (btor, exp);
2028 btor_node_release (btor, exp);
2029 }
2030 BTOR_RELEASE_STACK (stack);
2031 btor_reset_assumptions (btor);
2032 }
2033
2034 /*------------------------------------------------------------------------*/
2035
2036 static void
replace_constraint(Btor * btor,BtorNode * old,BtorNode * new)2037 replace_constraint (Btor *btor, BtorNode *old, BtorNode *new)
2038 {
2039 assert (btor);
2040 assert (old);
2041 assert (btor_node_is_regular (old));
2042 assert (old->constraint);
2043 assert (old->refs > 1);
2044 assert (!old->parameterized);
2045 assert (!btor_node_real_addr (new)->parameterized);
2046 assert (btor_node_is_simplified (old));
2047 assert (!btor_node_is_simplified (new));
2048
2049 BtorPtrHashTable *unsynthesized_constraints, *synthesized_constraints;
2050 BtorPtrHashTable *embedded_constraints, *pos, *neg;
2051 BtorNode *not_new, *not_old;
2052
2053 BTORLOG (1,
2054 "replace constraint: %s -> %s",
2055 btor_util_node2string (old),
2056 btor_util_node2string (new));
2057
2058 not_old = btor_node_invert (old);
2059 not_new = btor_node_invert (new);
2060 embedded_constraints = btor->embedded_constraints;
2061 unsynthesized_constraints = btor->unsynthesized_constraints;
2062 synthesized_constraints = btor->synthesized_constraints;
2063 pos = neg = 0;
2064
2065 if (btor_hashptr_table_get (unsynthesized_constraints, old))
2066 {
2067 add_constraint (btor, new);
2068 assert (!pos);
2069 pos = unsynthesized_constraints;
2070 }
2071
2072 if (btor_hashptr_table_get (unsynthesized_constraints, not_old))
2073 {
2074 add_constraint (btor, not_new);
2075 assert (!neg);
2076 neg = unsynthesized_constraints;
2077 }
2078
2079 if (btor_hashptr_table_get (synthesized_constraints, old))
2080 {
2081 add_constraint (btor, new);
2082 assert (!pos);
2083 pos = synthesized_constraints;
2084 }
2085
2086 if (btor_hashptr_table_get (synthesized_constraints, not_old))
2087 {
2088 add_constraint (btor, not_new);
2089 assert (!neg);
2090 neg = synthesized_constraints;
2091 }
2092
2093 if (pos)
2094 {
2095 btor_hashptr_table_remove (pos, old, 0, 0);
2096 btor_node_release (btor, old);
2097
2098 if (btor_hashptr_table_get (embedded_constraints, old))
2099 {
2100 btor_hashptr_table_remove (embedded_constraints, old, 0, 0);
2101 btor_node_release (btor, old);
2102 }
2103 }
2104
2105 if (neg)
2106 {
2107 btor_hashptr_table_remove (neg, not_old, 0, 0);
2108 btor_node_release (btor, not_old);
2109
2110 if (btor_hashptr_table_get (embedded_constraints, not_old))
2111 {
2112 btor_hashptr_table_remove (embedded_constraints, not_old, 0, 0);
2113 btor_node_release (btor, not_old);
2114 }
2115 }
2116
2117 old->constraint = 0;
2118 }
2119
2120 void
btor_set_simplified_exp(Btor * btor,BtorNode * exp,BtorNode * simplified)2121 btor_set_simplified_exp (Btor *btor, BtorNode *exp, BtorNode *simplified)
2122 {
2123 assert (btor);
2124 assert (exp);
2125 assert (simplified);
2126 assert (btor_node_is_regular (exp));
2127 assert (exp != btor_node_real_addr (simplified));
2128 assert (!btor_node_real_addr (simplified)->simplified);
2129 assert (exp->arity <= 3);
2130 assert (btor_node_get_sort_id (exp) == btor_node_get_sort_id (simplified));
2131 assert (exp->parameterized
2132 || !btor_node_real_addr (simplified)->parameterized);
2133 assert (!btor_node_real_addr (simplified)->parameterized
2134 || exp->parameterized);
2135
2136 BTORLOG (2,
2137 "set simplified: %s -> %s (synth: %u, param: %u)",
2138 btor_util_node2string (exp),
2139 btor_util_node2string (simplified),
2140 btor_node_is_synth (exp),
2141 exp->parameterized);
2142
2143 /* FIXME: indicator for slow-down in incremental mode, when too many
2144 * synthesized nodes are rewritten, it can significantly slow-down the
2145 * solver. */
2146 if (btor_node_is_synth (exp)) btor->stats.rewrite_synth++;
2147
2148 if (exp->simplified) btor_node_release (btor, exp->simplified);
2149
2150 exp->simplified = btor_node_copy (btor, simplified);
2151
2152 if (exp->constraint) replace_constraint (btor, exp, exp->simplified);
2153
2154 if (!btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST))
2155 {
2156 btor_node_set_to_proxy (btor, exp);
2157
2158 /* if simplified is parameterized, exp was also parameterized */
2159 if (btor_node_real_addr (simplified)->parameterized) exp->parameterized = 1;
2160 }
2161 }
2162
2163 /* Finds most simplified expression and shortens path to it */
2164 static BtorNode *
recursively_pointer_chase_simplified_exp(Btor * btor,BtorNode * exp)2165 recursively_pointer_chase_simplified_exp (Btor *btor, BtorNode *exp)
2166 {
2167 BtorNode *real_exp, *cur, *simplified, *not_simplified, *next;
2168 bool invert;
2169
2170 assert (btor);
2171 assert (exp);
2172
2173 real_exp = btor_node_real_addr (exp);
2174
2175 assert (real_exp->simplified);
2176 assert (btor_node_real_addr (real_exp->simplified)->simplified);
2177
2178 /* shorten path to simplified expression */
2179 invert = false;
2180 simplified = real_exp->simplified;
2181 do
2182 {
2183 assert (!btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST)
2184 || !btor_node_is_proxy (simplified));
2185 assert (btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST)
2186 || btor_node_is_proxy (simplified));
2187 if (btor_node_is_inverted (simplified)) invert = !invert;
2188 simplified = btor_node_real_addr (simplified)->simplified;
2189 } while (btor_node_real_addr (simplified)->simplified);
2190 /* 'simplified' is representative element */
2191 assert (!btor_node_real_addr (simplified)->simplified);
2192 if (invert) simplified = btor_node_invert (simplified);
2193
2194 invert = false;
2195 not_simplified = btor_node_invert (simplified);
2196 cur = btor_node_copy (btor, real_exp);
2197 do
2198 {
2199 if (btor_node_is_inverted (cur)) invert = !invert;
2200 cur = btor_node_real_addr (cur);
2201 next = btor_node_copy (btor, cur->simplified);
2202 btor_set_simplified_exp (btor, cur, invert ? not_simplified : simplified);
2203 btor_node_release (btor, cur);
2204 cur = next;
2205 } while (btor_node_real_addr (cur)->simplified);
2206 btor_node_release (btor, cur);
2207
2208 /* if starting expression is inverted, then we have to invert result */
2209 if (btor_node_is_inverted (exp)) simplified = btor_node_invert (simplified);
2210
2211 return simplified;
2212 }
2213
2214 BtorNode *
btor_node_get_simplified(Btor * btor,BtorNode * exp)2215 btor_node_get_simplified (Btor *btor, BtorNode *exp)
2216 {
2217 assert (btor);
2218 assert (exp);
2219 assert (!btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST)
2220 || !btor_node_is_proxy (exp));
2221
2222 (void) btor;
2223 BtorNode *real_exp;
2224
2225 real_exp = btor_node_real_addr (exp);
2226
2227 /* no simplified expression ? */
2228 if (!real_exp->simplified)
2229 {
2230 return exp;
2231 }
2232
2233 /* only one simplified expression ? */
2234 if (!btor_node_real_addr (real_exp->simplified)->simplified)
2235 {
2236 if (btor_node_is_inverted (exp))
2237 return btor_node_invert (real_exp->simplified);
2238 return exp->simplified;
2239 }
2240 return recursively_pointer_chase_simplified_exp (btor, exp);
2241 }
2242
2243 static BtorNode *
simplify_constraint_exp(Btor * btor,BtorNode * exp)2244 simplify_constraint_exp (Btor *btor, BtorNode *exp)
2245 {
2246 assert (btor);
2247 assert (exp);
2248 assert (btor_node_real_addr (exp)->constraint);
2249 assert (!btor_node_real_addr (exp)->simplified);
2250 /* embedded constraints rewriting enabled with rwl > 1 */
2251 assert (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1);
2252
2253 BtorNode *real_exp, *result, *not_exp;
2254
2255 real_exp = btor_node_real_addr (exp);
2256
2257 /* Do not simplify top-level constraint applies (we need the implication
2258 * dependencies for determining top applies when dual prop enabled) */
2259 if (btor_opt_get (btor, BTOR_OPT_FUN_DUAL_PROP)
2260 && btor_node_is_apply (real_exp))
2261 return exp;
2262
2263 not_exp = btor_node_invert (real_exp);
2264
2265 if (btor_node_is_bv_const (real_exp)) return exp;
2266
2267 if (btor_hashptr_table_get (btor->unsynthesized_constraints, real_exp))
2268 {
2269 result = btor->true_exp;
2270 }
2271 else if (btor_hashptr_table_get (btor->unsynthesized_constraints, not_exp))
2272 {
2273 result = btor_node_invert (btor->true_exp);
2274 }
2275 else if (btor_hashptr_table_get (btor->synthesized_constraints, real_exp))
2276 {
2277 result = btor->true_exp;
2278 }
2279 else
2280 {
2281 assert (btor_hashptr_table_get (btor->synthesized_constraints, not_exp));
2282 result = btor_node_invert (btor->true_exp);
2283 }
2284
2285 if (btor_node_is_inverted (exp)) return btor_node_invert (result);
2286
2287 return result;
2288 }
2289
2290 BtorNode *
btor_simplify_exp(Btor * btor,BtorNode * exp)2291 btor_simplify_exp (Btor *btor, BtorNode *exp)
2292 {
2293 assert (btor);
2294 assert (exp);
2295 assert (btor_node_real_addr (exp)->btor == btor);
2296 assert (btor_node_real_addr (exp)->refs > 0);
2297
2298 BtorNode *result;
2299
2300 result = btor_node_get_simplified (btor, exp);
2301
2302 /* NOTE: embedded constraints rewriting is enabled with rwl > 1 */
2303 if (btor_opt_get (btor, BTOR_OPT_SIMPLIFY_CONSTRAINTS)
2304 && btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 1
2305 && btor_node_real_addr (result)->constraint)
2306 return simplify_constraint_exp (btor, result);
2307
2308 assert (btor_node_real_addr (result)->btor == btor);
2309 assert (btor_node_real_addr (result)->refs > 0);
2310
2311 return result;
2312 }
2313
2314 BtorNode *
btor_substitute_nodes_node_map(Btor * btor,BtorNode * root,BtorNodeMap * substs,BtorIntHashTable * node_map)2315 btor_substitute_nodes_node_map (Btor *btor,
2316 BtorNode *root,
2317 BtorNodeMap *substs,
2318 BtorIntHashTable *node_map)
2319 {
2320 assert (btor);
2321 assert (root);
2322 assert (substs);
2323
2324 int32_t i;
2325 BtorMemMgr *mm;
2326 BtorNode *cur, *real_cur, *subst, *result, **e;
2327 BtorNodePtrStack visit, args, cleanup;
2328 BtorIntHashTable *mark, *mark_subst;
2329 BtorHashTableData *d;
2330 BtorNodeMapIterator it;
2331
2332 mm = btor->mm;
2333 mark = btor_hashint_map_new (mm);
2334 mark_subst = btor_hashint_map_new (mm);
2335 BTOR_INIT_STACK (mm, visit);
2336 BTOR_INIT_STACK (mm, args);
2337 BTOR_INIT_STACK (mm, cleanup);
2338 BTOR_PUSH_STACK (visit, root);
2339
2340 while (!BTOR_EMPTY_STACK (visit))
2341 {
2342 cur = BTOR_POP_STACK (visit);
2343 real_cur = btor_node_real_addr (cur);
2344 d = btor_hashint_map_get (mark, real_cur->id);
2345 if (!d)
2346 {
2347 subst = btor_nodemap_mapped (substs, real_cur);
2348 if (subst)
2349 {
2350 /* if this assertion fails we have a cyclic substitution */
2351 assert (!btor_hashint_map_get (mark, btor_node_real_addr (subst)->id)
2352 || btor_hashint_map_get (mark, btor_node_real_addr (subst)->id)
2353 ->as_ptr);
2354 BTOR_PUSH_STACK (visit, btor_node_cond_invert (cur, subst));
2355 btor_hashint_table_add (mark_subst, btor_node_real_addr (subst)->id);
2356 continue;
2357 }
2358
2359 (void) btor_hashint_map_add (mark, real_cur->id);
2360 BTOR_PUSH_STACK (visit, cur);
2361 for (i = real_cur->arity - 1; i >= 0; i--)
2362 BTOR_PUSH_STACK (visit, real_cur->e[i]);
2363 }
2364 else if (!d->as_ptr)
2365 {
2366 args.top -= real_cur->arity;
2367 e = args.top;
2368
2369 if (real_cur->arity == 0)
2370 {
2371 if (btor_node_is_param (real_cur)
2372 /* Do not create new param if 'real_cur' is already a
2373 * substitution */
2374 && !btor_hashint_table_contains (mark_subst, real_cur->id))
2375 {
2376 // TODO: make unique symbol !<num>++
2377 result = btor_exp_param (btor, real_cur->sort_id, 0);
2378 }
2379 else
2380 result = btor_node_copy (btor, real_cur);
2381 }
2382 else if (btor_node_is_bv_slice (real_cur))
2383 {
2384 result = btor_exp_bv_slice (btor,
2385 e[0],
2386 btor_node_bv_slice_get_upper (real_cur),
2387 btor_node_bv_slice_get_lower (real_cur));
2388 }
2389 else
2390 {
2391 /* if the param of a quantifier gets subtituted by a non-param,
2392 * we do not create a quantifier, but return the body instead */
2393 if (btor_node_is_quantifier (real_cur) && !btor_node_is_param (e[0]))
2394 result = btor_node_copy (btor, e[1]);
2395 else
2396 result = btor_exp_create (btor, real_cur->kind, e, real_cur->arity);
2397 }
2398 for (i = 0; i < real_cur->arity; i++) btor_node_release (btor, e[i]);
2399
2400 d->as_ptr = btor_node_copy (btor, result);
2401 BTOR_PUSH_STACK (cleanup, result);
2402 if (node_map)
2403 {
2404 assert (!btor_hashint_map_contains (node_map, real_cur->id));
2405 btor_hashint_map_add (node_map, real_cur->id)->as_int =
2406 btor_node_real_addr (result)->id;
2407 }
2408 PUSH_RESULT:
2409 assert (real_cur->sort_id == btor_node_real_addr (result)->sort_id);
2410 BTOR_PUSH_STACK (args, btor_node_cond_invert (cur, result));
2411 }
2412 else
2413 {
2414 assert (d->as_ptr);
2415 result = btor_node_copy (btor, d->as_ptr);
2416 goto PUSH_RESULT;
2417 }
2418 }
2419 assert (BTOR_COUNT_STACK (args) == 1);
2420 result = BTOR_POP_STACK (args);
2421
2422 /* update 'node_map' for substituted nodes */
2423 if (node_map)
2424 {
2425 btor_iter_nodemap_init (&it, substs);
2426 while (btor_iter_nodemap_has_next (&it))
2427 {
2428 subst = it.it.bucket->data.as_ptr;
2429 while (btor_nodemap_mapped (substs, subst))
2430 subst = btor_nodemap_mapped (substs, subst);
2431 cur = btor_iter_nodemap_next (&it);
2432 assert (!btor_hashint_map_contains (node_map, cur->id));
2433 btor_hashint_map_add (node_map, cur->id)->as_int =
2434 btor_node_real_addr (subst)->id;
2435 }
2436 }
2437
2438 while (!BTOR_EMPTY_STACK (cleanup))
2439 btor_node_release (btor, BTOR_POP_STACK (cleanup));
2440 BTOR_RELEASE_STACK (cleanup);
2441 BTOR_RELEASE_STACK (visit);
2442 BTOR_RELEASE_STACK (args);
2443 btor_hashint_map_delete (mark);
2444 btor_hashint_map_delete (mark_subst);
2445 return result;
2446 }
2447
2448 BtorNode *
btor_substitute_nodes(Btor * btor,BtorNode * root,BtorNodeMap * substs)2449 btor_substitute_nodes (Btor *btor, BtorNode *root, BtorNodeMap *substs)
2450 {
2451 return btor_substitute_nodes_node_map (btor, root, substs, 0);
2452 }
2453
2454 BtorNode *
btor_substitute_node(Btor * btor,BtorNode * root,BtorNode * node,BtorNode * subst)2455 btor_substitute_node (Btor *btor,
2456 BtorNode *root,
2457 BtorNode *node,
2458 BtorNode *subst)
2459 {
2460 BtorNodeMap *map = btor_nodemap_new (btor);
2461 btor_nodemap_map (map, node, subst);
2462 BtorNode *result = btor_substitute_nodes_node_map (btor, root, map, 0);
2463 btor_nodemap_delete (map);
2464 return result;
2465 }
2466
2467 /*------------------------------------------------------------------------*/
2468
2469 /* bit vector skeleton is always encoded, i.e., if btor_node_is_synth is true,
2470 * then it is also encoded. with option lazy_synthesize enabled,
2471 * 'btor_synthesize_exp' stops at feq and apply nodes */
2472 void
btor_synthesize_exp(Btor * btor,BtorNode * exp,BtorPtrHashTable * backannotation)2473 btor_synthesize_exp (Btor *btor,
2474 BtorNode *exp,
2475 BtorPtrHashTable *backannotation)
2476 {
2477 BtorNodePtrStack exp_stack;
2478 BtorNode *cur, *value, *args;
2479 BtorAIGVec *av0, *av1, *av2;
2480 BtorMemMgr *mm;
2481 BtorAIGVecMgr *avmgr;
2482 BtorPtrHashBucket *b;
2483 BtorPtrHashTable *static_rho;
2484 BtorPtrHashTableIterator it;
2485 char *indexed_name;
2486 const char *name;
2487 uint32_t count, i, j, len;
2488 bool is_same_children_mem;
2489 bool invert_av0 = false;
2490 bool invert_av1 = false;
2491 bool invert_av2 = false;
2492 double start;
2493 bool restart, opt_lazy_synth;
2494 BtorIntHashTable *cache;
2495
2496 assert (btor);
2497 assert (exp);
2498
2499 start = btor_util_time_stamp ();
2500 mm = btor->mm;
2501 avmgr = btor->avmgr;
2502 count = 0;
2503 cache = btor_hashint_table_new (mm);
2504 opt_lazy_synth = btor_opt_get (btor, BTOR_OPT_FUN_LAZY_SYNTHESIZE) == 1;
2505
2506 BTOR_INIT_STACK (mm, exp_stack);
2507 BTOR_PUSH_STACK (exp_stack, exp);
2508 BTORLOG (2, "%s: %s", __FUNCTION__, btor_util_node2string (exp));
2509
2510 while (!BTOR_EMPTY_STACK (exp_stack))
2511 {
2512 cur = btor_node_real_addr (BTOR_POP_STACK (exp_stack));
2513 assert (!btor_node_is_proxy (cur));
2514 assert (!btor_node_is_simplified (cur));
2515
2516 if (btor_node_is_synth (cur)) continue;
2517
2518 count++;
2519 if (!btor_hashint_table_contains (cache, cur->id))
2520 {
2521 if (btor_node_is_bv_const (cur))
2522 {
2523 cur->av = btor_aigvec_const (avmgr, btor_node_bv_const_get_bits (cur));
2524 BTORLOG (2, " synthesized: %s", btor_util_node2string (cur));
2525 /* no need to call btor_aigvec_to_sat_tseitin here */
2526 }
2527 /* encode bv skeleton inputs: var, apply, feq */
2528 else if (btor_node_is_bv_var (cur)
2529 || (btor_node_is_apply (cur) && !cur->parameterized)
2530 || btor_node_is_fun_eq (cur))
2531 {
2532 assert (!cur->parameterized);
2533 cur->av = btor_aigvec_var (avmgr, btor_node_bv_get_width (btor, cur));
2534
2535 if (btor_node_is_bv_var (cur) && backannotation
2536 && (name = btor_node_get_symbol (btor, cur)))
2537 {
2538 len = strlen (name) + 40;
2539 if (btor_node_bv_get_width (btor, cur) > 1)
2540 {
2541 indexed_name = btor_mem_malloc (mm, len);
2542 for (i = 0; i < cur->av->width; i++)
2543 {
2544 b = btor_hashptr_table_add (backannotation, cur->av->aigs[i]);
2545 assert (b->key == cur->av->aigs[i]);
2546 sprintf (indexed_name, "%s[%d]", name, cur->av->width - i - 1);
2547 b->data.as_str = btor_mem_strdup (mm, indexed_name);
2548 }
2549 btor_mem_free (mm, indexed_name, len);
2550 }
2551 else
2552 {
2553 assert (btor_node_bv_get_width (btor, cur) == 1);
2554 b = btor_hashptr_table_add (backannotation, cur->av->aigs[0]);
2555 assert (b->key == cur->av->aigs[0]);
2556 b->data.as_str = btor_mem_strdup (mm, name);
2557 }
2558 }
2559 BTORLOG (2, " synthesized: %s", btor_util_node2string (cur));
2560 btor_aigvec_to_sat_tseitin (avmgr, cur->av);
2561
2562 /* continue synthesizing children for apply and feq nodes if
2563 * lazy_synthesize is disabled */
2564 if (!opt_lazy_synth) goto PUSH_CHILDREN;
2565 }
2566 /* we stop at function nodes as they will be lazily synthesized and
2567 * encoded during consistency checking */
2568 else if (btor_node_is_fun (cur) && opt_lazy_synth)
2569 {
2570 continue;
2571 }
2572 else
2573 {
2574 PUSH_CHILDREN:
2575 assert (!opt_lazy_synth || !btor_node_is_fun (cur));
2576
2577 btor_hashint_table_add (cache, cur->id);
2578 BTOR_PUSH_STACK (exp_stack, cur);
2579 for (j = 1; j <= cur->arity; j++)
2580 BTOR_PUSH_STACK (exp_stack, cur->e[cur->arity - j]);
2581
2582 /* synthesize nodes in static_rho of lambda nodes */
2583 if (btor_node_is_lambda (cur))
2584 {
2585 static_rho = btor_node_lambda_get_static_rho (cur);
2586 if (static_rho)
2587 {
2588 btor_iter_hashptr_init (&it, static_rho);
2589 while (btor_iter_hashptr_has_next (&it))
2590 {
2591 value = it.bucket->data.as_ptr;
2592 args = btor_iter_hashptr_next (&it);
2593 BTOR_PUSH_STACK (exp_stack, btor_simplify_exp (btor, value));
2594 BTOR_PUSH_STACK (exp_stack, btor_simplify_exp (btor, args));
2595 }
2596 }
2597 }
2598 }
2599 }
2600 /* paremterized nodes, argument nodes and functions are not
2601 * synthesizable */
2602 else if (!cur->parameterized && !btor_node_is_args (cur)
2603 && !btor_node_is_fun (cur))
2604 {
2605 if (!opt_lazy_synth)
2606 {
2607 /* due to pushing nodes from static_rho onto 'exp_stack' a strict
2608 * DFS order is not guaranteed anymore. hence, we have to check
2609 * if one of the children of 'cur' is not yet synthesized and
2610 * thus, have to synthesize them before 'cur'. */
2611 restart = false;
2612 for (i = 0; i < cur->arity; i++)
2613 {
2614 if (!btor_node_is_synth (btor_node_real_addr (cur->e[i])))
2615 {
2616 BTOR_PUSH_STACK (exp_stack, cur->e[i]);
2617 restart = true;
2618 break;
2619 }
2620 }
2621 if (restart) continue;
2622 }
2623
2624 if (cur->arity == 1)
2625 {
2626 assert (btor_node_is_bv_slice (cur));
2627 invert_av0 = btor_node_is_inverted (cur->e[0]);
2628 av0 = btor_node_real_addr (cur->e[0])->av;
2629 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2630 cur->av = btor_aigvec_slice (avmgr,
2631 av0,
2632 btor_node_bv_slice_get_upper (cur),
2633 btor_node_bv_slice_get_lower (cur));
2634 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2635 }
2636 else if (cur->arity == 2)
2637 {
2638 /* We have to check if the children are in the same memory
2639 * place if they are in the same memory place. Then we need to
2640 * allocate memory for the AIG vectors if they are not, then
2641 * we can invert them in place and invert them back afterwards
2642 * (only if necessary) .
2643 */
2644 is_same_children_mem =
2645 btor_node_real_addr (cur->e[0]) == btor_node_real_addr (cur->e[1]);
2646 if (is_same_children_mem)
2647 {
2648 av0 = BTOR_AIGVEC_NODE (btor, cur->e[0]);
2649 av1 = BTOR_AIGVEC_NODE (btor, cur->e[1]);
2650 }
2651 else
2652 {
2653 invert_av0 = btor_node_is_inverted (cur->e[0]);
2654 av0 = btor_node_real_addr (cur->e[0])->av;
2655 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2656 invert_av1 = btor_node_is_inverted (cur->e[1]);
2657 av1 = btor_node_real_addr (cur->e[1])->av;
2658 if (invert_av1) btor_aigvec_invert (avmgr, av1);
2659 }
2660 switch (cur->kind)
2661 {
2662 case BTOR_BV_AND_NODE:
2663 cur->av = btor_aigvec_and (avmgr, av0, av1);
2664 break;
2665 case BTOR_BV_EQ_NODE:
2666 cur->av = btor_aigvec_eq (avmgr, av0, av1);
2667 break;
2668 case BTOR_BV_ADD_NODE:
2669 cur->av = btor_aigvec_add (avmgr, av0, av1);
2670 break;
2671 case BTOR_BV_MUL_NODE:
2672 cur->av = btor_aigvec_mul (avmgr, av0, av1);
2673 break;
2674 case BTOR_BV_ULT_NODE:
2675 cur->av = btor_aigvec_ult (avmgr, av0, av1);
2676 break;
2677 case BTOR_BV_SLL_NODE:
2678 cur->av = btor_aigvec_sll (avmgr, av0, av1);
2679 break;
2680 case BTOR_BV_SRL_NODE:
2681 cur->av = btor_aigvec_srl (avmgr, av0, av1);
2682 break;
2683 case BTOR_BV_UDIV_NODE:
2684 cur->av = btor_aigvec_udiv (avmgr, av0, av1);
2685 break;
2686 case BTOR_BV_UREM_NODE:
2687 cur->av = btor_aigvec_urem (avmgr, av0, av1);
2688 break;
2689 default:
2690 assert (cur->kind == BTOR_BV_CONCAT_NODE);
2691 cur->av = btor_aigvec_concat (avmgr, av0, av1);
2692 break;
2693 }
2694
2695 if (is_same_children_mem)
2696 {
2697 btor_aigvec_release_delete (avmgr, av0);
2698 btor_aigvec_release_delete (avmgr, av1);
2699 }
2700 else
2701 {
2702 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2703 if (invert_av1) btor_aigvec_invert (avmgr, av1);
2704 }
2705 if (!opt_lazy_synth) btor_aigvec_to_sat_tseitin (avmgr, cur->av);
2706 }
2707 else
2708 {
2709 assert (cur->arity == 3);
2710
2711 if (btor_node_is_bv_cond (cur))
2712 {
2713 is_same_children_mem =
2714 btor_node_real_addr (cur->e[0]) == btor_node_real_addr (cur->e[1])
2715 || btor_node_real_addr (cur->e[0])
2716 == btor_node_real_addr (cur->e[2])
2717 || btor_node_real_addr (cur->e[1])
2718 == btor_node_real_addr (cur->e[2]);
2719 if (is_same_children_mem)
2720 {
2721 av0 = BTOR_AIGVEC_NODE (btor, cur->e[0]);
2722 av1 = BTOR_AIGVEC_NODE (btor, cur->e[1]);
2723 av2 = BTOR_AIGVEC_NODE (btor, cur->e[2]);
2724 }
2725 else
2726 {
2727 invert_av0 = btor_node_is_inverted (cur->e[0]);
2728 av0 = btor_node_real_addr (cur->e[0])->av;
2729 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2730 invert_av1 = btor_node_is_inverted (cur->e[1]);
2731 av1 = btor_node_real_addr (cur->e[1])->av;
2732 if (invert_av1) btor_aigvec_invert (avmgr, av1);
2733 invert_av2 = btor_node_is_inverted (cur->e[2]);
2734 av2 = btor_node_real_addr (cur->e[2])->av;
2735 if (invert_av2) btor_aigvec_invert (avmgr, av2);
2736 }
2737 cur->av = btor_aigvec_cond (avmgr, av0, av1, av2);
2738 if (is_same_children_mem)
2739 {
2740 btor_aigvec_release_delete (avmgr, av2);
2741 btor_aigvec_release_delete (avmgr, av1);
2742 btor_aigvec_release_delete (avmgr, av0);
2743 }
2744 else
2745 {
2746 if (invert_av0) btor_aigvec_invert (avmgr, av0);
2747 if (invert_av1) btor_aigvec_invert (avmgr, av1);
2748 if (invert_av2) btor_aigvec_invert (avmgr, av2);
2749 }
2750 }
2751 }
2752 assert (cur->av);
2753 BTORLOG (2, " synthesized: %s", btor_util_node2string (cur));
2754 btor_aigvec_to_sat_tseitin (avmgr, cur->av);
2755 }
2756 }
2757 BTOR_RELEASE_STACK (exp_stack);
2758 btor_hashint_table_delete (cache);
2759
2760 if (count > 0 && btor_opt_get (btor, BTOR_OPT_VERBOSITY) > 3)
2761 BTOR_MSG (
2762 btor->msg, 3, "synthesized %u expressions into AIG vectors", count);
2763
2764 btor->time.synth_exp += btor_util_time_stamp () - start;
2765 }
2766
2767 /* forward assumptions to the SAT solver */
2768 void
btor_add_again_assumptions(Btor * btor)2769 btor_add_again_assumptions (Btor *btor)
2770 {
2771 assert (btor);
2772 assert (btor_dbg_check_assumptions_simp_free (btor));
2773
2774 int32_t i;
2775 BtorNode *exp, *cur, *e;
2776 BtorNodePtrStack stack;
2777 BtorPtrHashTable *assumptions;
2778 BtorPtrHashTableIterator it;
2779 BtorAIG *aig;
2780 BtorSATMgr *smgr;
2781 BtorAIGMgr *amgr;
2782 BtorIntHashTable *mark;
2783
2784 amgr = btor_get_aig_mgr (btor);
2785 smgr = btor_get_sat_mgr (btor);
2786
2787 BTOR_INIT_STACK (btor->mm, stack);
2788 mark = btor_hashint_table_new (btor->mm);
2789
2790 assumptions = btor_hashptr_table_new (btor->mm,
2791 (BtorHashPtr) btor_node_hash_by_id,
2792 (BtorCmpPtr) btor_node_compare_by_id);
2793
2794 btor_iter_hashptr_init (&it, btor->assumptions);
2795 while (btor_iter_hashptr_has_next (&it))
2796 {
2797 exp = btor_iter_hashptr_next (&it);
2798 assert (!btor_node_is_simplified (exp));
2799
2800 if (btor_node_is_inverted (exp) || !btor_node_is_bv_and (exp))
2801 {
2802 if (!btor_hashptr_table_get (assumptions, exp))
2803 btor_hashptr_table_add (assumptions, exp);
2804 }
2805 else
2806 {
2807 BTOR_PUSH_STACK (stack, exp);
2808 while (!BTOR_EMPTY_STACK (stack))
2809 {
2810 cur = BTOR_POP_STACK (stack);
2811 assert (!btor_node_is_inverted (cur));
2812 assert (btor_node_is_bv_and (cur));
2813 if (btor_hashint_table_contains (mark, cur->id)) continue;
2814 btor_hashint_table_add (mark, cur->id);
2815 for (i = 0; i < 2; i++)
2816 {
2817 e = cur->e[i];
2818 if (!btor_node_is_inverted (e) && btor_node_is_bv_and (e))
2819 BTOR_PUSH_STACK (stack, e);
2820 else if (!btor_hashptr_table_get (assumptions, e))
2821 btor_hashptr_table_add (assumptions, e);
2822 }
2823 }
2824 }
2825 }
2826
2827 btor_iter_hashptr_init (&it, assumptions);
2828 while (btor_iter_hashptr_has_next (&it))
2829 {
2830 cur = btor_iter_hashptr_next (&it);
2831 assert (btor_node_bv_get_width (btor, cur) == 1);
2832 assert (!btor_node_is_simplified (cur));
2833 aig = exp_to_aig (btor, cur);
2834 btor_aig_to_sat (amgr, aig);
2835 if (aig == BTOR_AIG_TRUE) continue;
2836 if (btor_sat_is_initialized (smgr))
2837 {
2838 assert (btor_aig_get_cnf_id (aig) != 0);
2839 btor_sat_assume (smgr, btor_aig_get_cnf_id (aig));
2840 }
2841 btor_aig_release (amgr, aig);
2842 }
2843
2844 BTOR_RELEASE_STACK (stack);
2845 btor_hashptr_table_delete (assumptions);
2846 btor_hashint_table_delete (mark);
2847 }
2848
2849 #if 0
2850 /* updates SAT assignments, reads assumptions and
2851 * returns if an assignment has changed
2852 */
2853 static int32_t
2854 update_sat_assignments (Btor * btor)
2855 {
2856 assert (btor);
2857
2858 BtorSATMgr *smgr;
2859
2860 smgr = btor_get_sat_mgr (btor);
2861 add_again_assumptions (btor);
2862 #ifndef NDEBUG
2863 int32_t result;
2864 result = timed_sat_sat (btor, -1);
2865 assert (result == BTOR_SAT);
2866 #else
2867 (void) timed_sat_sat (btor, -1);
2868 #endif
2869 return btor_sat_changed (smgr);
2870 }
2871 #endif
2872
2873 int32_t
btor_check_sat(Btor * btor,int32_t lod_limit,int32_t sat_limit)2874 btor_check_sat (Btor *btor, int32_t lod_limit, int32_t sat_limit)
2875 {
2876 assert (btor);
2877 assert (btor_opt_get (btor, BTOR_OPT_INCREMENTAL)
2878 || btor->btor_sat_btor_called == 0);
2879
2880 #ifndef NDEBUG
2881 bool check = true;
2882 #endif
2883 double start, delta;
2884 BtorSolverResult res;
2885 uint32_t engine;
2886
2887 start = btor_util_time_stamp ();
2888
2889 BTOR_MSG (btor->msg, 1, "calling SAT");
2890
2891 if (btor->valid_assignments == 1) btor_reset_incremental_usage (btor);
2892
2893 /* 'btor->assertions' contains all assertions that were asserted in context
2894 * levels > 0 (boolector_push). We assume all these assertions on every
2895 * btor_check_sat call since these assumptions are valid until the
2896 * corresponding context is popped. */
2897 if (BTOR_COUNT_STACK (btor->assertions) > 0)
2898 {
2899 assert (BTOR_COUNT_STACK (btor->assertions_trail) > 0);
2900 uint32_t i;
2901 for (i = 0; i < BTOR_COUNT_STACK (btor->assertions); i++)
2902 {
2903 btor_assume_exp (btor, BTOR_PEEK_STACK (btor->assertions, i));
2904 }
2905 }
2906
2907 #ifndef NDEBUG
2908 // NOTE: disable checking if quantifiers present for now (not supported yet)
2909 if (btor->quantifiers->count) check = false;
2910
2911 Btor *uclone = 0;
2912 if (check && btor_opt_get (btor, BTOR_OPT_CHK_UNCONSTRAINED)
2913 && btor_opt_get (btor, BTOR_OPT_UCOPT)
2914 && btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 2
2915 && !btor_opt_get (btor, BTOR_OPT_INCREMENTAL)
2916 && !btor_opt_get (btor, BTOR_OPT_MODEL_GEN)
2917 && !btor_opt_get (btor, BTOR_OPT_PRINT_DIMACS))
2918 {
2919 uclone = btor_clone_btor (btor);
2920 btor_opt_set (uclone, BTOR_OPT_UCOPT, 0);
2921 btor_opt_set (uclone, BTOR_OPT_CHK_UNCONSTRAINED, 0);
2922 btor_opt_set (uclone, BTOR_OPT_CHK_MODEL, 0);
2923 btor_opt_set (uclone, BTOR_OPT_CHK_FAILED_ASSUMPTIONS, 0);
2924 btor_set_term (uclone, 0, 0);
2925
2926 btor_opt_set (uclone, BTOR_OPT_ENGINE, BTOR_ENGINE_FUN);
2927 if (uclone->slv)
2928 {
2929 uclone->slv->api.delet (uclone->slv);
2930 uclone->slv = 0;
2931 }
2932 }
2933 BtorCheckModelContext *chkmodel = 0;
2934 if (check && btor_opt_get (btor, BTOR_OPT_CHK_MODEL))
2935 {
2936 chkmodel = btor_check_model_init (btor);
2937 }
2938 #endif
2939
2940 #ifndef NBTORLOG
2941 btor_opt_log_opts (btor);
2942 #endif
2943
2944 /* set option based on formula characteristics */
2945
2946 /* eliminate lambdas (define-fun) in the QF_BV case */
2947 if (btor->ufs->count == 0 && btor->feqs->count == 0
2948 && btor->lambdas->count > 0)
2949 {
2950 BTOR_MSG(btor->msg, 1,
2951 "no UFs or function equalities, enable beta-reduction=all");
2952 btor_opt_set (btor, BTOR_OPT_BETA_REDUCE, BTOR_BETA_REDUCE_ALL);
2953 }
2954
2955 // FIXME (ma): not sound with slice elimination. see red-vsl.proof3106.smt2
2956 /* disabling slice elimination is better on QF_ABV and BV */
2957 if (btor->ufs->count > 0 || btor->quantifiers->count > 0)
2958 {
2959 BTOR_MSG(btor->msg, 1,
2960 "found %s, disable slice elimination",
2961 btor->ufs->count > 0 ? "UFs" : "quantifiers");
2962 btor_opt_set (btor, BTOR_OPT_ELIMINATE_SLICES, 0);
2963 }
2964
2965 /* set options for quantifiers */
2966 if (btor->quantifiers->count > 0)
2967 {
2968 btor_opt_set (btor, BTOR_OPT_UCOPT, 0);
2969 btor_opt_set (btor, BTOR_OPT_BETA_REDUCE, BTOR_BETA_REDUCE_ALL);
2970 }
2971
2972 res = btor_simplify (btor);
2973
2974 if (res != BTOR_RESULT_UNSAT)
2975 {
2976 engine = btor_opt_get (btor, BTOR_OPT_ENGINE);
2977
2978 if (!btor->slv)
2979 {
2980 /* these engines work on QF_BV only */
2981 if (engine == BTOR_ENGINE_SLS && btor->ufs->count == 0
2982 && btor->feqs->count == 0)
2983 {
2984 assert (btor->lambdas->count == 0
2985 || btor_opt_get (btor, BTOR_OPT_BETA_REDUCE));
2986 BTOR_ABORT(btor->quantifiers->count,
2987 "Quantifiers not supported for -E sls");
2988 btor->slv = btor_new_sls_solver (btor);
2989 }
2990 else if (engine == BTOR_ENGINE_PROP && btor->ufs->count == 0
2991 && btor->feqs->count == 0)
2992 {
2993 assert (btor->lambdas->count == 0
2994 || btor_opt_get (btor, BTOR_OPT_BETA_REDUCE));
2995 BTOR_ABORT(btor->quantifiers->count,
2996 "Quantifiers not supported for -E prop");
2997 btor->slv = btor_new_prop_solver (btor);
2998 }
2999 else if (engine == BTOR_ENGINE_AIGPROP && btor->ufs->count == 0
3000 && btor->feqs->count == 0)
3001 {
3002 assert (btor->lambdas->count == 0
3003 || btor_opt_get (btor, BTOR_OPT_BETA_REDUCE));
3004 BTOR_ABORT(btor->quantifiers->count,
3005 "Quantifiers not supported for -E aigprop");
3006 btor->slv = btor_new_aigprop_solver (btor);
3007 }
3008 else if ((engine == BTOR_ENGINE_QUANT && btor->quantifiers->count > 0)
3009 || btor->quantifiers->count > 0)
3010 {
3011 BtorPtrHashTableIterator it;
3012 BtorNode *cur;
3013 btor_iter_hashptr_init (&it, btor->unsynthesized_constraints);
3014 btor_iter_hashptr_queue (&it, btor->synthesized_constraints);
3015 while (btor_iter_hashptr_has_next (&it))
3016 {
3017 cur = btor_iter_hashptr_next (&it);
3018 BTOR_ABORT (cur->lambda_below || cur->apply_below,
3019 "quantifiers with functions not supported yet");
3020 }
3021 btor->slv = btor_new_quantifier_solver (btor);
3022 }
3023 else
3024 {
3025 btor->slv = btor_new_fun_solver (btor);
3026 // TODO (ma): make options for lod_limit and sat_limit
3027 BTOR_FUN_SOLVER (btor)->lod_limit = lod_limit;
3028 BTOR_FUN_SOLVER (btor)->sat_limit = sat_limit;
3029 }
3030 }
3031
3032 assert (btor->slv);
3033 res = btor->slv->api.sat (btor->slv);
3034 }
3035 btor->last_sat_result = res;
3036 btor->btor_sat_btor_called++;
3037 btor->valid_assignments = 1;
3038
3039 if (btor_opt_get (btor, BTOR_OPT_MODEL_GEN) && res == BTOR_RESULT_SAT)
3040 {
3041 switch (btor_opt_get (btor, BTOR_OPT_ENGINE))
3042 {
3043 case BTOR_ENGINE_SLS:
3044 case BTOR_ENGINE_PROP:
3045 case BTOR_ENGINE_AIGPROP:
3046 btor->slv->api.generate_model (
3047 btor->slv, btor_opt_get (btor, BTOR_OPT_MODEL_GEN) == 2, false);
3048 break;
3049 default:
3050 btor->slv->api.generate_model (
3051 btor->slv, btor_opt_get (btor, BTOR_OPT_MODEL_GEN) == 2, true);
3052 }
3053 }
3054
3055 #ifndef NDEBUG
3056 if (uclone)
3057 {
3058 assert (btor_opt_get (btor, BTOR_OPT_UCOPT));
3059 assert (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 2);
3060 assert (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL));
3061 assert (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN));
3062 BtorSolverResult ucres = btor_check_sat (uclone, -1, -1);
3063 assert (res == ucres);
3064 btor_delete (uclone);
3065 }
3066
3067 if (chkmodel)
3068 {
3069 if (res == BTOR_RESULT_SAT && !btor_opt_get (btor, BTOR_OPT_UCOPT))
3070 {
3071 btor_check_model (chkmodel);
3072 }
3073 btor_check_model_delete (chkmodel);
3074 }
3075 #endif
3076
3077 #ifndef NDEBUG
3078 if (check && btor_opt_get (btor, BTOR_OPT_CHK_FAILED_ASSUMPTIONS)
3079 && !btor->inconsistent && btor->last_sat_result == BTOR_RESULT_UNSAT)
3080 btor_check_failed_assumptions (btor);
3081 #endif
3082
3083 delta = btor_util_time_stamp () - start;
3084
3085 BTOR_MSG (btor->msg,
3086 1,
3087 "SAT call %d returned %d in %.3f seconds",
3088 btor->btor_sat_btor_called + 1,
3089 res,
3090 delta);
3091
3092 btor->time.sat += delta;
3093
3094 return res;
3095 }
3096
3097 static bool
is_valid_argument(Btor * btor,BtorNode * exp)3098 is_valid_argument (Btor *btor, BtorNode *exp)
3099 {
3100 exp = btor_node_real_addr (exp);
3101 if (btor_node_is_fun (btor_simplify_exp (btor, exp))) return false;
3102 if (btor_node_is_array (btor_simplify_exp (btor, exp))) return false;
3103 /* scope of bound parmaters already closed (cannot be used anymore) */
3104 if (btor_node_is_param (exp) && btor_node_param_is_bound (exp)) return false;
3105 return true;
3106 }
3107
3108 int32_t
btor_fun_sort_check(Btor * btor,BtorNode * args[],uint32_t argc,BtorNode * fun)3109 btor_fun_sort_check (Btor *btor, BtorNode *args[], uint32_t argc, BtorNode *fun)
3110 {
3111 (void) btor;
3112 assert (btor);
3113 assert (argc > 0);
3114 assert (args);
3115 assert (fun);
3116 assert (btor_node_is_regular (fun));
3117 assert (btor_node_is_fun (btor_simplify_exp (btor, fun)));
3118 assert (argc == btor_node_fun_get_arity (btor, fun));
3119
3120 uint32_t i;
3121 int32_t pos;
3122 BtorSortId sort;
3123 BtorTupleSortIterator it;
3124
3125 assert (btor_sort_is_tuple (
3126 btor, btor_sort_fun_get_domain (btor, btor_node_get_sort_id (fun))));
3127 btor_iter_tuple_sort_init (
3128 &it, btor, btor_sort_fun_get_domain (btor, btor_node_get_sort_id (fun)));
3129 for (i = 0, pos = -1; i < argc; i++)
3130 {
3131 assert (btor_iter_tuple_sort_has_next (&it));
3132 sort = btor_iter_tuple_sort_next (&it);
3133 /* NOTE: we do not allow functions or arrays as arguments yet */
3134 if (!is_valid_argument (btor, args[i])
3135 || sort != btor_node_get_sort_id (args[i]))
3136 {
3137 pos = i;
3138 break;
3139 }
3140 }
3141 return pos;
3142 }
3143
3144 static BtorAIG *
exp_to_aig(Btor * btor,BtorNode * exp)3145 exp_to_aig (Btor *btor, BtorNode *exp)
3146 {
3147 BtorAIGMgr *amgr;
3148 BtorAIGVec *av;
3149 BtorAIG *result;
3150
3151 assert (btor);
3152 assert (exp);
3153 assert (btor_node_bv_get_width (btor, exp) == 1);
3154 assert (!btor_node_real_addr (exp)->parameterized);
3155
3156 amgr = btor_get_aig_mgr (btor);
3157
3158 btor_synthesize_exp (btor, exp, 0);
3159 av = btor_node_real_addr (exp)->av;
3160
3161 assert (av);
3162 assert (av->width == 1);
3163
3164 result = av->aigs[0];
3165
3166 if (btor_node_is_inverted (exp))
3167 result = btor_aig_not (amgr, result);
3168 else
3169 result = btor_aig_copy (amgr, result);
3170
3171 return result;
3172 }
3173
3174 BtorAIGVec *
btor_exp_to_aigvec(Btor * btor,BtorNode * exp,BtorPtrHashTable * backannotation)3175 btor_exp_to_aigvec (Btor *btor, BtorNode *exp, BtorPtrHashTable *backannotation)
3176 {
3177 BtorAIGVecMgr *avmgr;
3178 BtorAIGVec *result;
3179
3180 assert (exp);
3181
3182 avmgr = btor->avmgr;
3183
3184 btor_synthesize_exp (btor, exp, backannotation);
3185 result = btor_node_real_addr (exp)->av;
3186 assert (result);
3187
3188 if (btor_node_is_inverted (exp))
3189 result = btor_aigvec_not (avmgr, result);
3190 else
3191 result = btor_aigvec_copy (avmgr, result);
3192
3193 return result;
3194 }
3195