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 "btoraig.h"
10 #include "btoraigvec.h"
11 #include "btorbeta.h"
12 #include "btorbv.h"
13 #include "btorcore.h"
14 #include "btorexp.h"
15 #include "btorlog.h"
16 #include "btormodel.h"
17 #include "btormsg.h"
18 #include "btorrwcache.h"
19 #include "btorsat.h"
20 #include "btorslvaigprop.h"
21 #include "btorslvfun.h"
22 #include "btorslvprop.h"
23 #include "btorslvsls.h"
24 #include "btorsort.h"
25 #include "sat/btorlgl.h"
26 #include "utils/btorhashint.h"
27 #include "utils/btorhashptr.h"
28 #include "utils/btornodemap.h"
29 #include "utils/btorstack.h"
30 #include "utils/btorutil.h"
31
32 #include <assert.h>
33 #include <stdio.h>
34 #include <stdlib.h>
35
36 BTOR_DECLARE_STACK (BtorNodePtrStackPtr, BtorNodePtrStack *);
37 BTOR_DECLARE_STACK (BtorPtrHashTablePtrPtr, BtorPtrHashTable **);
38
39 /*------------------------------------------------------------------------*/
40
41 void *
btor_clone_key_as_node(BtorMemMgr * mm,const void * map,const void * key)42 btor_clone_key_as_node (BtorMemMgr *mm, const void *map, const void *key)
43 {
44 assert (map);
45 assert (key);
46
47 BtorNode *exp, *cloned_exp;
48 BtorNodeMap *exp_map;
49
50 (void) mm;
51 exp = (BtorNode *) key;
52 exp_map = (BtorNodeMap *) map;
53 cloned_exp = btor_nodemap_mapped (exp_map, exp);
54 assert (cloned_exp);
55 return cloned_exp;
56 }
57
58 void *
btor_clone_key_as_str(BtorMemMgr * mm,const void * map,const void * key)59 btor_clone_key_as_str (BtorMemMgr *mm, const void *map, const void *key)
60 {
61 assert (mm);
62 assert (key);
63
64 (void) map;
65
66 return btor_mem_strdup (mm, (char *) key);
67 }
68
69 void *
btor_clone_key_as_static_str(BtorMemMgr * mm,const void * map,const void * key)70 btor_clone_key_as_static_str (BtorMemMgr *mm, const void *map, const void *key)
71 {
72 (void) mm;
73 (void) map;
74 return (void *) key;
75 }
76
77 void *
btor_clone_key_as_bv_tuple(BtorMemMgr * mm,const void * map,const void * t)78 btor_clone_key_as_bv_tuple (BtorMemMgr *mm, const void *map, const void *t)
79 {
80 assert (mm);
81 assert (t);
82 (void) map;
83 return btor_bv_copy_tuple (mm, (BtorBitVectorTuple *) t);
84 }
85
86 void *
btor_clone_key_as_rw_cache_tuple(BtorMemMgr * mm,const void * map,const void * t)87 btor_clone_key_as_rw_cache_tuple (BtorMemMgr *mm,
88 const void *map,
89 const void *t)
90 {
91 assert (mm);
92 assert (t);
93 (void) map;
94
95 BtorRwCacheTuple *res;
96 BTOR_CNEW (mm, res);
97 memcpy (res, t, sizeof (BtorRwCacheTuple));
98 return res;
99 }
100
101 void
btor_clone_data_as_node_ptr(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)102 btor_clone_data_as_node_ptr (BtorMemMgr *mm,
103 const void *map,
104 BtorHashTableData *data,
105 BtorHashTableData *cloned_data)
106 {
107 assert (map);
108 assert (data);
109 assert (cloned_data);
110
111 BtorNode *exp, *cloned_exp;
112 BtorNodeMap *exp_map;
113
114 (void) mm;
115 exp = (BtorNode *) data->as_ptr;
116 exp_map = (BtorNodeMap *) map;
117 cloned_exp = btor_nodemap_mapped (exp_map, exp);
118 assert (cloned_exp);
119 cloned_data->as_ptr = cloned_exp;
120 }
121
122 void
btor_clone_data_as_str_ptr(BtorMemMgr * mm,const void * str_table,BtorHashTableData * data,BtorHashTableData * cloned_data)123 btor_clone_data_as_str_ptr (BtorMemMgr *mm,
124 const void *str_table,
125 BtorHashTableData *data,
126 BtorHashTableData *cloned_data)
127 {
128 assert (str_table);
129 assert (data);
130 assert (cloned_data);
131
132 char *str;
133
134 (void) mm;
135 str = data->as_str;
136 assert (btor_hashptr_table_get ((BtorPtrHashTable *) str_table, str));
137
138 cloned_data->as_str =
139 (char *) btor_hashptr_table_get ((BtorPtrHashTable *) str_table, str)
140 ->key;
141 }
142
143 void
btor_clone_data_as_int(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)144 btor_clone_data_as_int (BtorMemMgr *mm,
145 const void *map,
146 BtorHashTableData *data,
147 BtorHashTableData *cloned_data)
148 {
149 assert (data);
150 assert (cloned_data);
151
152 (void) mm;
153 (void) map;
154 cloned_data->as_int = data->as_int;
155 }
156
157 void
btor_clone_data_as_dbl(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)158 btor_clone_data_as_dbl (BtorMemMgr *mm,
159 const void *map,
160 BtorHashTableData *data,
161 BtorHashTableData *cloned_data)
162 {
163 assert (data);
164 assert (cloned_data);
165
166 (void) mm;
167 (void) map;
168
169 cloned_data->as_dbl = data->as_dbl;
170 }
171
172 void
btor_clone_data_as_bv_ptr(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)173 btor_clone_data_as_bv_ptr (BtorMemMgr *mm,
174 const void *map,
175 BtorHashTableData *data,
176 BtorHashTableData *cloned_data)
177 {
178 assert (mm);
179 assert (data);
180 assert (cloned_data);
181
182 (void) map;
183 cloned_data->as_ptr = btor_bv_copy (mm, (BtorBitVector *) data->as_ptr);
184 }
185
186 void
btor_clone_data_as_ptr_htable(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)187 btor_clone_data_as_ptr_htable (BtorMemMgr *mm,
188 const void *map,
189 BtorHashTableData *data,
190 BtorHashTableData *cloned_data)
191 {
192 assert (mm);
193 assert (map);
194 assert (data);
195 assert (cloned_data);
196
197 BtorPtrHashTable *table;
198 BtorNodeMap *exp_map;
199
200 table = (BtorPtrHashTable *) data->as_ptr;
201 exp_map = (BtorNodeMap *) map;
202
203 cloned_data->as_ptr = btor_hashptr_table_clone (
204 mm, table, btor_clone_key_as_node, 0, exp_map, 0);
205 }
206
207 void
btor_clone_data_as_int_htable(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)208 btor_clone_data_as_int_htable (BtorMemMgr *mm,
209 const void *map,
210 BtorHashTableData *data,
211 BtorHashTableData *cloned_data)
212 {
213 (void) map;
214 assert (mm);
215 assert (map);
216 assert (data);
217 assert (cloned_data);
218
219 BtorIntHashTable *table, *res;
220
221 table = (BtorIntHashTable *) data->as_ptr;
222
223 res = btor_hashint_table_new (mm);
224
225 BTOR_DELETEN (mm, res->keys, res->size);
226 BTOR_DELETEN (mm, res->hop_info, res->size);
227
228 res->size = table->size;
229 res->count = table->count;
230 BTOR_CNEWN (mm, res->keys, res->size);
231 BTOR_CNEWN (mm, res->hop_info, res->size);
232 if (table->data) BTOR_CNEWN (mm, res->data, res->size);
233
234 memcpy (res->keys, table->keys, table->size);
235 memcpy (res->hop_info, table->hop_info, table->size);
236 if (table->data) memcpy (res->data, table->data, table->size);
237
238 cloned_data->as_ptr = res;
239 }
240
241 void
btor_clone_data_as_bv_ptr_htable(BtorMemMgr * mm,const void * map,BtorHashTableData * data,BtorHashTableData * cloned_data)242 btor_clone_data_as_bv_ptr_htable (BtorMemMgr *mm,
243 const void *map,
244 BtorHashTableData *data,
245 BtorHashTableData *cloned_data)
246 {
247 assert (mm);
248 assert (data);
249 assert (cloned_data);
250
251 BtorPtrHashTable *table;
252 table = (BtorPtrHashTable *) data->as_ptr;
253 cloned_data->as_ptr = btor_hashptr_table_clone (mm,
254 table,
255 btor_clone_key_as_bv_tuple,
256 btor_clone_data_as_bv_ptr,
257 map,
258 map);
259 }
260
261 /*------------------------------------------------------------------------*/
262
263 static void
clone_sorts_unique_table(Btor * btor,Btor * clone)264 clone_sorts_unique_table (Btor *btor, Btor *clone)
265 {
266 assert (btor);
267 assert (clone);
268
269 uint32_t i, j;
270 BtorSort *sort, *csort;
271 BtorSortId cid;
272 BtorSortIdStack elements;
273 BtorSortUniqueTable *table, *res;
274 BtorMemMgr *mm;
275
276 mm = clone->mm;
277 table = &btor->sorts_unique_table;
278 res = &clone->sorts_unique_table;
279
280 BTOR_INIT_STACK (mm, elements);
281
282 BTOR_CNEWN (mm, res->chains, table->size);
283 res->size = table->size;
284 res->num_elements = 0;
285 res->mm = mm;
286 BTOR_INIT_STACK (mm, res->id2sort);
287
288 for (i = 0; i < BTOR_COUNT_STACK (table->id2sort); i++)
289 {
290 sort = BTOR_PEEK_STACK (table->id2sort, i);
291
292 if (!sort)
293 {
294 BTOR_PUSH_STACK (res->id2sort, 0);
295 continue;
296 }
297
298 switch (sort->kind)
299 {
300 #if 0
301 case BTOR_BOOL_SORT:
302 cid = btor_sort_bool (clone);
303 break;
304 #endif
305 case BTOR_BV_SORT: cid = btor_sort_bv (clone, sort->bitvec.width); break;
306 #if 0
307 case BTOR_LST_SORT:
308 cid = btor_sort_lst (clone, sort->lst.head->id, sort->lst.tail->id);
309 break;
310
311 case BTOR_ARRAY_SORT:
312 cid = btor_sort_array (clone, sort->array.index->id,
313 sort->array.element->id);
314 break;
315 #endif
316 case BTOR_FUN_SORT:
317 assert (BTOR_PEEK_STACK (res->id2sort, sort->fun.domain->id));
318 cid =
319 btor_sort_fun (clone, sort->fun.domain->id, sort->fun.codomain->id);
320 break;
321
322 case BTOR_TUPLE_SORT:
323 BTOR_RESET_STACK (elements);
324 for (j = 0; j < sort->tuple.num_elements; j++)
325 BTOR_PUSH_STACK (elements, sort->tuple.elements[j]->id);
326 cid = btor_sort_tuple (
327 clone, elements.start, BTOR_COUNT_STACK (elements));
328 break;
329
330 default: cid = 0; break;
331 }
332 assert (cid);
333 csort = BTOR_PEEK_STACK (res->id2sort, cid);
334 assert (csort->refs == 1);
335 assert (csort->id == sort->id);
336 assert (csort->kind == sort->kind);
337 assert (csort->table != sort->table);
338 }
339
340 /* update sort references (must be the same as in table) */
341 assert (BTOR_COUNT_STACK (table->id2sort) == BTOR_COUNT_STACK (res->id2sort));
342 for (i = 0; i < BTOR_COUNT_STACK (res->id2sort); i++)
343 {
344 sort = BTOR_PEEK_STACK (table->id2sort, i);
345 csort = BTOR_PEEK_STACK (res->id2sort, i);
346 if (!sort)
347 {
348 assert (!csort);
349 continue;
350 }
351 assert (csort->id == sort->id);
352 assert (csort->parents == sort->parents);
353 assert (csort->ext_refs == 0);
354 assert (sort->refs == csort->refs - 1 + sort->refs - sort->parents);
355 csort->refs = sort->refs;
356 csort->ext_refs = sort->ext_refs;
357 }
358 assert (res->num_elements == table->num_elements);
359 BTOR_RELEASE_STACK (elements);
360 }
361
362 #if 0
363 static void
364 clone_sorts_unique_table (BtorMemMgr * mm,
365 BtorSortUniqueTable * table,
366 BtorSortUniqueTable * res)
367 {
368 assert (mm);
369 assert (table);
370 assert (res);
371
372 uint32_t i, j;
373 BtorSort *sort, *csort, *tmp;
374 BtorSortPtrStack elements;
375
376 BTOR_INIT_STACK (elements);
377
378 BTOR_CNEWN (mm, res->chains, table->size);
379 res->size = table->size;
380 res->num_elements = 0;
381 res->mm = mm;
382 BTOR_INIT_STACK (res->id2sort);
383
384 for (i = 0; i < BTOR_COUNT_STACK (table->id2sort); i++)
385 {
386 sort = BTOR_PEEK_STACK (table->id2sort, i);
387
388 if (!sort)
389 {
390 BTOR_PUSH_STACK (res->mm, res->id2sort, 0);
391 continue;
392 }
393
394 switch (sort->kind)
395 {
396 case BTOR_BOOL_SORT:
397 csort = btor_sort_bool (res);
398 break;
399
400 case BTOR_BV_SORT:
401 csort = btor_sort_bv (res, sort->bitvec.len);
402 break;
403
404 case BTOR_LST_SORT:
405 csort = btor_sort_lst (res,
406 BTOR_PEEK_STACK (res->id2sort, sort->lst.head->id),
407 BTOR_PEEK_STACK (res->id2sort, sort->lst.tail->id));
408 break;
409
410 case BTOR_ARRAY_SORT:
411 csort = btor_sort_array (res,
412 BTOR_PEEK_STACK (res->id2sort, sort->array.index->id),
413 BTOR_PEEK_STACK (res->id2sort,
414 sort->array.element->id));
415 break;
416
417 case BTOR_FUN_SORT:
418 tmp = BTOR_PEEK_STACK (res->id2sort, sort->fun.domain->id);
419 assert (tmp);
420 if (sort->fun.arity > 1)
421 {
422 assert (sort->fun.domain->kind == BTOR_TUPLE_SORT);
423 assert (tmp->kind == BTOR_TUPLE_SORT);
424 assert (sort->fun.arity == tmp->tuple.num_elements);
425 csort = btor_sort_fun (res, tmp->tuple.elements,
426 sort->fun.arity,
427 BTOR_PEEK_STACK (res->id2sort,
428 sort->fun.codomain->id));
429 }
430 else
431 {
432 assert (sort->fun.domain->kind != BTOR_TUPLE_SORT
433 && sort->fun.domain->kind != BTOR_LST_SORT);
434 csort = btor_sort_fun (res, &tmp, 1,
435 BTOR_PEEK_STACK (res->id2sort,
436 sort->fun.codomain->id));
437 }
438 break;
439
440 case BTOR_TUPLE_SORT:
441 BTOR_RESET_STACK (elements);
442 for (j = 0; j < sort->tuple.num_elements; j++)
443 BTOR_PUSH_STACK (mm, elements,
444 BTOR_PEEK_STACK (res->id2sort,
445 sort->tuple.elements[j]->id));
446 csort = btor_sort_tuple (res, elements.start,
447 BTOR_COUNT_STACK (elements));
448 break;
449
450 default:
451 csort = 0;
452 break;
453 }
454 assert (csort);
455 assert (csort->refs == 1);
456 assert (csort->id == sort->id);
457 assert (csort->kind == sort->kind);
458 assert (csort->table != sort->table);
459 }
460
461 /* update sort references (must be the same as in table) */
462 assert (BTOR_COUNT_STACK (table->id2sort) == BTOR_COUNT_STACK (res->id2sort));
463 for (i = 0; i < BTOR_COUNT_STACK (res->id2sort); i++)
464 {
465 sort = BTOR_PEEK_STACK (table->id2sort, i);
466 csort = BTOR_PEEK_STACK (res->id2sort, i);
467 if (!sort)
468 {
469 assert (!csort);
470 continue;
471 }
472 assert (csort->id == sort->id);
473 assert (csort->parents == sort->parents);
474 assert (csort->ext_refs == 0);
475 assert (sort->refs == csort->refs - 1 + sort->refs - sort->parents);
476 csort->refs = sort->refs;
477 csort->ext_refs = sort->ext_refs;
478 }
479 assert (res->num_elements == table->num_elements);
480 BTOR_RELEASE_STACK (mm, elements);
481 }
482 #endif
483
484 static BtorNode *
clone_exp(Btor * clone,BtorNode * exp,BtorNodePtrPtrStack * parents,BtorNodePtrPtrStack * nodes,BtorNodePtrStack * rhos,BtorNodePtrStack * static_rhos,BtorNodeMap * exp_map,bool exp_layer_only,bool clone_simplified)485 clone_exp (Btor *clone,
486 BtorNode *exp,
487 BtorNodePtrPtrStack *parents,
488 BtorNodePtrPtrStack *nodes,
489 BtorNodePtrStack *rhos,
490 BtorNodePtrStack *static_rhos,
491 BtorNodeMap *exp_map,
492 bool exp_layer_only,
493 bool clone_simplified)
494 {
495 assert (clone);
496 assert (exp);
497 assert (btor_node_is_regular (exp));
498 assert (parents);
499 assert (nodes);
500 assert (exp_map);
501
502 uint32_t i;
503 BtorBitVector *bits;
504 BtorNode *res;
505 BtorParamNode *param;
506 BtorMemMgr *mm;
507
508 mm = clone->mm;
509
510 res = btor_mem_malloc (mm, exp->bytes);
511 memcpy (res, exp, exp->bytes);
512
513 /* ------------------- BTOR_VAR_NODE_STRUCT (all nodes) -----------------> */
514 if (btor_node_is_bv_const (exp))
515 {
516 bits = btor_bv_copy (mm, btor_node_bv_const_get_bits (exp));
517 btor_node_bv_const_set_bits (res, bits);
518 bits = btor_bv_copy (mm, btor_node_bv_const_get_invbits (exp));
519 btor_node_bv_const_set_invbits (res, bits);
520 }
521
522 /* Note: no need to cache aig vectors here (exp->av is unique to exp). */
523 if (btor_node_is_fun (exp))
524 {
525 if (exp_layer_only)
526 res->rho = 0;
527 else if (exp->rho)
528 {
529 BTOR_PUSH_STACK (*rhos, res);
530 BTOR_PUSH_STACK (*rhos, exp);
531 }
532 }
533 else if (exp->av)
534 res->av = exp_layer_only ? 0 : btor_aigvec_clone (exp->av, clone->avmgr);
535
536 assert (!exp->next || !btor_node_is_invalid (exp->next));
537 BTOR_PUSH_STACK_IF (exp->next, *nodes, &res->next);
538
539 assert (!btor_node_is_simplified (exp) || !btor_node_is_invalid (exp->simplified));
540 if (clone_simplified || btor_node_is_proxy (exp))
541 {
542 BTOR_PUSH_STACK_IF (exp->simplified, *nodes, &res->simplified);
543 }
544 else
545 {
546 res->simplified = 0;
547 }
548
549 res->btor = clone;
550
551 assert (!exp->first_parent || !btor_node_is_invalid (exp->first_parent));
552 assert (!exp->last_parent || !btor_node_is_invalid (exp->last_parent));
553
554 BTOR_PUSH_STACK_IF (exp->first_parent, *parents, &res->first_parent);
555 BTOR_PUSH_STACK_IF (exp->last_parent, *parents, &res->last_parent);
556 /* <---------------------------------------------------------------------- */
557
558 /* ------------ BTOR_BV_ADDITIONAL_VAR_NODE_STRUCT (all nodes) ----------> */
559 if (!btor_node_is_bv_const (exp))
560 {
561 if (!btor_node_is_bv_var (exp) && !btor_node_is_param (exp))
562 {
563 if (exp->arity)
564 {
565 for (i = 0; i < exp->arity; i++)
566 {
567 res->e[i] = btor_nodemap_mapped (exp_map, exp->e[i]);
568 assert (exp->e[i] != res->e[i]);
569 assert (res->e[i]);
570 }
571 }
572
573 for (i = 0; i < exp->arity; i++)
574 {
575 assert (!exp->prev_parent[i]
576 || !btor_node_is_invalid (exp->prev_parent[i]));
577 assert (!exp->next_parent[i]
578 || !btor_node_is_invalid (exp->next_parent[i]));
579
580 BTOR_PUSH_STACK_IF (
581 exp->prev_parent[i], *parents, &res->prev_parent[i]);
582 BTOR_PUSH_STACK_IF (
583 exp->next_parent[i], *parents, &res->next_parent[i]);
584 }
585 }
586 }
587 /* <---------------------------------------------------------------------- */
588
589 if (btor_node_is_param (exp))
590 {
591 param = (BtorParamNode *) exp;
592 assert (!btor_node_param_is_bound (exp)
593 || !btor_node_is_invalid (btor_node_param_get_binder (exp)));
594 assert (!param->assigned_exp
595 || !btor_node_is_invalid (param->assigned_exp));
596
597 BTOR_PUSH_STACK_IF (
598 param->binder, *nodes, (BtorNode **) &((BtorParamNode *) res)->binder);
599 BTOR_PUSH_STACK_IF (param->assigned_exp,
600 *nodes,
601 (BtorNode **) &((BtorParamNode *) res)->assigned_exp);
602 }
603
604 if (btor_node_is_binder (exp))
605 {
606 if (btor_node_is_lambda (exp) && btor_node_lambda_get_static_rho (exp))
607 {
608 BTOR_PUSH_STACK (*static_rhos, res);
609 BTOR_PUSH_STACK (*static_rhos, exp);
610 }
611 assert (!btor_node_binder_get_body (exp)
612 || !btor_node_is_invalid (btor_node_binder_get_body (exp)));
613 BTOR_PUSH_STACK_IF (btor_node_binder_get_body (exp),
614 *nodes,
615 &((BtorBinderNode *) res)->body);
616 }
617
618 btor_nodemap_map (exp_map, exp, res);
619
620 return res;
621 }
622
623 void
btor_clone_node_ptr_stack(BtorMemMgr * mm,BtorNodePtrStack * stack,BtorNodePtrStack * res,BtorNodeMap * exp_map,bool is_zero_terminated)624 btor_clone_node_ptr_stack (BtorMemMgr *mm,
625 BtorNodePtrStack *stack,
626 BtorNodePtrStack *res,
627 BtorNodeMap *exp_map,
628 bool is_zero_terminated)
629 {
630 assert (stack);
631 assert (res);
632 assert (exp_map);
633
634 uint32_t i, n;
635 BtorNode *cloned_exp;
636 bool has_zero_terminated;
637
638 BTOR_INIT_STACK (mm, *res);
639 assert (BTOR_SIZE_STACK (*stack) || !BTOR_COUNT_STACK (*stack));
640 if (BTOR_SIZE_STACK (*stack))
641 {
642 BTOR_NEWN (mm, res->start, BTOR_SIZE_STACK (*stack));
643 res->top = res->start;
644 res->end = res->start + BTOR_SIZE_STACK (*stack);
645
646 n = BTOR_COUNT_STACK (*stack);
647 has_zero_terminated = n && !BTOR_PEEK_STACK (*stack, n - 1);
648 if (is_zero_terminated && has_zero_terminated) n -= 1;
649
650 for (i = 0; i < n; i++)
651 {
652 assert ((*stack).start[i]);
653 cloned_exp = btor_nodemap_mapped (exp_map, (*stack).start[i]);
654 assert (cloned_exp);
655 BTOR_PUSH_STACK (*res, cloned_exp);
656 }
657
658 if (is_zero_terminated && has_zero_terminated) BTOR_PUSH_STACK (*res, 0);
659 }
660 assert (BTOR_COUNT_STACK (*stack) == BTOR_COUNT_STACK (*res));
661 assert (BTOR_SIZE_STACK (*stack) == BTOR_SIZE_STACK (*res));
662 }
663
664 static void
clone_nodes_id_table(Btor * btor,Btor * clone,BtorNodePtrStack * res,BtorNodeMap * exp_map,bool exp_layer_only,BtorNodePtrStack * rhos,bool clone_simplified)665 clone_nodes_id_table (Btor *btor,
666 Btor *clone,
667 BtorNodePtrStack *res,
668 BtorNodeMap *exp_map,
669 bool exp_layer_only,
670 BtorNodePtrStack *rhos,
671 bool clone_simplified)
672 {
673 assert (btor);
674 assert (clone);
675 assert (res);
676 assert (exp_map);
677
678 size_t i;
679 int32_t tag;
680 BtorNode **tmp, *exp, *cloned_exp;
681 BtorMemMgr *mm;
682 BtorNodePtrStack *id_table;
683 BtorNodePtrPtrStack parents, nodes;
684 BtorPtrHashTable *t;
685 BtorNodePtrStack static_rhos;
686
687 mm = clone->mm;
688 id_table = &btor->nodes_id_table;
689
690 BTOR_INIT_STACK (mm, parents);
691 BTOR_INIT_STACK (mm, nodes);
692 BTOR_INIT_STACK (mm, static_rhos);
693
694 BTOR_INIT_STACK (mm, *res);
695 assert (BTOR_SIZE_STACK (*id_table) || !BTOR_COUNT_STACK (*id_table));
696
697 if (BTOR_SIZE_STACK (*id_table))
698 {
699 BTOR_NEWN (mm, res->start, BTOR_SIZE_STACK (*id_table));
700 res->top = res->start + BTOR_COUNT_STACK (*id_table);
701 res->end = res->start + BTOR_SIZE_STACK (*id_table);
702 res->start[0] = 0;
703
704 /* first element (id = 0) is empty */
705 for (i = 1; i < BTOR_COUNT_STACK (*id_table); i++)
706 {
707 exp = id_table->start[i];
708 res->start[i] = exp ? clone_exp (clone,
709 exp,
710 &parents,
711 &nodes,
712 rhos,
713 &static_rhos,
714 exp_map,
715 exp_layer_only,
716 clone_simplified)
717 : 0;
718 assert (!exp || res->start[i]->id > 0);
719 assert (!exp || (size_t) res->start[i]->id == i);
720 }
721 }
722 assert (BTOR_COUNT_STACK (*res) == BTOR_COUNT_STACK (*id_table));
723 assert (BTOR_SIZE_STACK (*res) == BTOR_SIZE_STACK (*id_table));
724
725 /* update children, parent, lambda and next pointers of expressions */
726 while (!BTOR_EMPTY_STACK (nodes))
727 {
728 tmp = BTOR_POP_STACK (nodes);
729 assert (*tmp);
730 *tmp = btor_nodemap_mapped (exp_map, *tmp);
731 assert (*tmp);
732 }
733
734 while (!BTOR_EMPTY_STACK (parents))
735 {
736 tmp = BTOR_POP_STACK (parents);
737 assert (*tmp);
738 tag = btor_node_get_tag (*tmp);
739 *tmp = btor_nodemap_mapped (exp_map, btor_node_real_addr (*tmp));
740 assert (*tmp);
741 *tmp = btor_node_set_tag (*tmp, tag);
742 }
743
744 /* clone static_rho tables */
745 while (!BTOR_EMPTY_STACK (static_rhos))
746 {
747 exp = BTOR_POP_STACK (static_rhos);
748 cloned_exp = BTOR_POP_STACK (static_rhos);
749 assert (btor_node_is_lambda (exp));
750 assert (btor_node_is_lambda (cloned_exp));
751 t = btor_node_lambda_get_static_rho (exp);
752 assert (t);
753 btor_node_lambda_set_static_rho (
754 cloned_exp,
755 btor_hashptr_table_clone (mm,
756 t,
757 btor_clone_key_as_node,
758 btor_clone_data_as_node_ptr,
759 exp_map,
760 exp_map));
761 }
762
763 BTOR_RELEASE_STACK (parents);
764 BTOR_RELEASE_STACK (nodes);
765 BTOR_RELEASE_STACK (static_rhos);
766 }
767
768 static void
clone_nodes_unique_table(Btor * btor,Btor * clone,BtorNodeMap * exp_map)769 clone_nodes_unique_table (Btor *btor, Btor *clone, BtorNodeMap *exp_map)
770 {
771 assert (btor);
772 assert (clone);
773 assert (exp_map);
774
775 uint32_t i;
776 BtorNodeUniqueTable *table, *res;
777 BtorMemMgr *mm;
778
779 mm = clone->mm;
780 table = &btor->nodes_unique_table;
781 res = &clone->nodes_unique_table;
782
783 BTOR_CNEWN (mm, res->chains, table->size);
784 res->size = table->size;
785 res->num_elements = table->num_elements;
786
787 for (i = 0; i < table->size; i++)
788 {
789 if (!table->chains[i]) continue;
790 res->chains[i] = btor_nodemap_mapped (exp_map, table->chains[i]);
791 assert (res->chains[i]);
792 }
793 }
794
795 #define MEM_INT_HASH_TABLE(table) \
796 ((table) ? sizeof (*(table)) + (table)->size * sizeof (int32_t) \
797 + (table)->size * sizeof (uint8_t) \
798 : 0)
799
800 #define MEM_INT_HASH_MAP(table) \
801 ((table) ? MEM_INT_HASH_TABLE (table) \
802 + (table)->size * sizeof (BtorHashTableData) \
803 : 0)
804
805 #define MEM_PTR_HASH_TABLE(table) \
806 ((table) ? sizeof (*(table)) + (table)->size * sizeof (BtorPtrHashBucket *) \
807 + (table)->count * sizeof (BtorPtrHashBucket) \
808 : 0)
809
810 #define CHKCLONE_MEM_INT_HASH_TABLE(table, clone) \
811 do \
812 { \
813 assert (MEM_INT_HASH_TABLE (table) == MEM_INT_HASH_TABLE (clone)); \
814 } while (0)
815
816 #define CHKCLONE_MEM_INT_HASH_MAP(table, clone) \
817 do \
818 { \
819 assert (MEM_INT_HASH_MAP (table) == MEM_INT_HASH_MAP (clone)); \
820 } while (0)
821
822 #define CHKCLONE_MEM_PTR_HASH_TABLE(table, clone) \
823 do \
824 { \
825 assert (MEM_PTR_HASH_TABLE (table) == MEM_PTR_HASH_TABLE (clone)); \
826 } while (0)
827
828 #define CLONE_PTR_HASH_TABLE(table) \
829 do \
830 { \
831 clone->table = btor_hashptr_table_clone ( \
832 mm, btor->table, btor_clone_key_as_node, 0, emap, 0); \
833 CHKCLONE_MEM_PTR_HASH_TABLE (btor->table, clone->table); \
834 } while (0)
835
836 #define CLONE_PTR_HASH_TABLE_DATA(table, data_func) \
837 do \
838 { \
839 BTORLOG_TIMESTAMP (delta); \
840 clone->table = btor_hashptr_table_clone ( \
841 mm, btor->table, btor_clone_key_as_node, data_func, emap, emap); \
842 BTORLOG (2, \
843 " clone " #table " table: %.3f s", \
844 (btor_util_time_stamp () - delta)); \
845 CHKCLONE_MEM_PTR_HASH_TABLE (btor->table, clone->table); \
846 } while (0)
847
848 #if 0
849 #define CLONE_INT_HASH_MAP_DATA(table, data_func) \
850 do \
851 { \
852 BTORLOG_TIMESTAMP (delta); \
853 clone->table = btor_hashint_map_clone (mm, btor->table, data_func, 0); \
854 BTORLOG (2, \
855 " clone " #table " table: %.3f s", \
856 (btor_util_time_stamp () - delta)); \
857 CHKCLONE_MEM_INT_HASH_MAP (btor->table, clone->table); \
858 } while (0)
859 #endif
860
861 #define MEM_BITVEC(bv) ((bv) ? btor_bv_size (bv) : 0)
862
863 static Btor *
clone_aux_btor(Btor * btor,BtorNodeMap ** exp_map,bool exp_layer_only,bool clone_slv,bool clone_simplified)864 clone_aux_btor (Btor *btor,
865 BtorNodeMap **exp_map,
866 bool exp_layer_only,
867 bool clone_slv,
868 bool clone_simplified)
869 {
870 assert (btor);
871 assert (exp_layer_only
872 || btor_sat_mgr_has_clone_support (btor_get_sat_mgr (btor)));
873 Btor *clone;
874 BtorNodeMap *emap = 0;
875 BtorMemMgr *mm;
876 double start, delta;
877 uint32_t i, len;
878 char *prefix, *clone_prefix;
879 BtorNode *exp, *cloned_exp;
880 BtorPtrHashTableIterator pit;
881 BtorNodePtrStack rhos;
882 #ifndef NDEBUG
883 uint32_t h;
884 size_t allocated;
885 BtorNode *cur;
886 BtorAIGMgr *amgr;
887 BtorBVAss *bvass;
888 BtorFunAss *funass;
889 BtorPtrHashTableIterator cpit, ncpit;
890 BtorIntHashTableIterator iit, ciit;
891 BtorSort *sort;
892 char **ind, **val;
893 amgr = exp_layer_only ? 0 : btor_get_aig_mgr (btor);
894 BtorHashTableData *data, *cdata;
895 BtorOption o;
896 #endif
897
898 BTORLOG (2, "start cloning btor %p ...", btor);
899 start = btor_util_time_stamp ();
900 btor->stats.clone_calls += 1;
901
902 mm = btor_mem_mgr_new ();
903 BTOR_CNEW (mm, clone);
904 #ifndef NDEBUG
905 allocated = sizeof (Btor);
906 #endif
907 memcpy (clone, btor, sizeof (Btor));
908 clone->mm = mm;
909 btor_rng_clone (&btor->rng, &clone->rng);
910
911 BTOR_CLR (&clone->cbs);
912 btor_opt_clone_opts (btor, clone);
913 #ifndef NDEBUG
914 allocated += BTOR_OPT_NUM_OPTS * sizeof (BtorOpt);
915 for (o = btor_opt_first (btor); btor_opt_is_valid (btor, o);
916 o = btor_opt_next (btor, o))
917 {
918 if (btor->options[o].valstr)
919 allocated += strlen (btor->options[o].valstr) + 1;
920 if (btor->options[o].options)
921 allocated += MEM_PTR_HASH_TABLE (clone->options[o].options)
922 + clone->options[o].options->count * sizeof (BtorOptHelp);
923 }
924 allocated += MEM_PTR_HASH_TABLE (clone->str2opt);
925 #endif
926 assert (allocated == clone->mm->allocated);
927
928 /* always auto cleanup internal and external references (may be dangling
929 * otherise) */
930 btor_opt_set (clone, BTOR_OPT_AUTO_CLEANUP, 1);
931 btor_opt_set (clone, BTOR_OPT_AUTO_CLEANUP_INTERNAL, 1);
932
933 if (exp_layer_only)
934 {
935 /* reset */
936 clone->btor_sat_btor_called = 0;
937 clone->last_sat_result = 0;
938 btor_reset_time (clone);
939 #ifndef NDEBUG
940 /* we need to explicitely reset the pointer to the table, since
941 * it is the memcpy-ied pointer of btor->stats.rw_rules_applied */
942 clone->stats.rw_rules_applied = 0;
943 #endif
944 btor_reset_stats (clone);
945 #ifndef NDEBUG
946 allocated += MEM_PTR_HASH_TABLE (clone->stats.rw_rules_applied);
947 assert (allocated == clone->mm->allocated);
948 #endif
949 }
950
951 clone->msg = btor_msg_new (clone);
952 assert ((allocated += sizeof (BtorMsg)) == clone->mm->allocated);
953
954 /* set msg prefix for clone */
955 clone_prefix = "clone";
956 len = btor->msg->prefix ? strlen (btor->msg->prefix) : 0;
957 len += strlen (clone_prefix) + 1;
958 #ifndef NDEBUG
959 allocated += len + 1;
960 #endif
961 BTOR_NEWN (clone->mm, prefix, len + 1);
962 sprintf (prefix, "%s>%s", btor->msg->prefix, clone_prefix);
963 btor_set_msg_prefix (clone, prefix);
964 BTOR_DELETEN (clone->mm, prefix, len + 1);
965
966 if (exp_layer_only)
967 {
968 clone->bv_assignments = btor_ass_new_bv_list (mm);
969 assert ((allocated += sizeof (BtorBVAssList)) == clone->mm->allocated);
970 }
971 else
972 {
973 BTORLOG_TIMESTAMP (delta);
974 clone->bv_assignments =
975 btor_ass_clone_bv_list (clone->mm, btor->bv_assignments);
976 BTORLOG (
977 1, " clone BV assignments: %.3f s", (btor_util_time_stamp () - delta));
978 #ifndef NDEBUG
979 for (bvass = btor->bv_assignments->first; bvass; bvass = bvass->next)
980 allocated +=
981 sizeof (BtorBVAss) + strlen (btor_ass_get_bv_str (bvass)) + 1;
982 assert ((allocated += sizeof (BtorBVAssList)) == clone->mm->allocated);
983 #endif
984 }
985
986 if (exp_layer_only)
987 {
988 clone->fun_assignments = btor_ass_new_fun_list (mm);
989 assert ((allocated += sizeof (BtorFunAssList)) == clone->mm->allocated);
990 }
991 else
992 {
993 BTORLOG_TIMESTAMP (delta);
994 clone->fun_assignments =
995 btor_ass_clone_fun_list (clone->mm, btor->fun_assignments);
996 BTORLOG (2,
997 " clone array assignments: %.3f s",
998 (btor_util_time_stamp () - delta));
999 #ifndef NDEBUG
1000 for (funass = btor->fun_assignments->first; funass; funass = funass->next)
1001 {
1002 allocated += sizeof (BtorFunAss) + 2 * funass->size * sizeof (char *);
1003 btor_ass_get_fun_indices_values (funass, &ind, &val, funass->size);
1004 for (i = 0; i < funass->size; i++)
1005 allocated += strlen (ind[i]) + 1 + strlen (val[i]) + 1;
1006 }
1007 assert ((allocated += sizeof (BtorFunAssList)) == clone->mm->allocated);
1008 #endif
1009 }
1010
1011 if (btor->avmgr)
1012 {
1013 if (exp_layer_only)
1014 {
1015 clone->avmgr = btor_aigvec_mgr_new (clone);
1016 assert ((allocated += sizeof (BtorAIGVecMgr) + sizeof (BtorAIGMgr)
1017 + sizeof (BtorSATMgr)
1018 /* true and false AIGs */
1019 + 2 * sizeof (BtorAIG *)
1020 + sizeof (int32_t)) /* unique table chains */
1021 == clone->mm->allocated);
1022 }
1023 else
1024 {
1025 BTORLOG_TIMESTAMP (delta);
1026 clone->avmgr = btor_aigvec_mgr_clone (clone, btor->avmgr);
1027 BTORLOG (2, " clone AIG mgr: %.3f s", (btor_util_time_stamp () - delta));
1028 #ifndef NDEBUG
1029 allocated +=
1030 sizeof (BtorAIGVecMgr) + sizeof (BtorAIGMgr)
1031 + sizeof (BtorSATMgr)
1032 /* memory of AIG nodes */
1033 + (amgr->cur_num_aigs + amgr->cur_num_aig_vars) * sizeof (BtorAIG)
1034 /* children for AND AIGs */
1035 + amgr->cur_num_aigs * sizeof (int32_t) * 2
1036 /* unique table chain */
1037 + amgr->table.size * sizeof (int32_t)
1038 + BTOR_SIZE_STACK (amgr->id2aig) * sizeof (BtorAIG *)
1039 + BTOR_SIZE_STACK (amgr->cnfid2aig) * sizeof (int32_t);
1040 #ifdef BTOR_USE_LINGELING
1041 assert (strcmp (amgr->smgr->name, "Lingeling") == 0
1042 || strcmp (amgr->smgr->name, "DIMACS Printer") == 0);
1043 assert (strcmp (amgr->smgr->name, "DIMACS Printer") != 0
1044 || strcmp (((BtorCnfPrinter *) amgr->smgr->solver)->smgr->name,
1045 "Lingeling")
1046 == 0);
1047 allocated += amgr->smgr->solver ? sizeof (BtorLGL) : 0;
1048 if (strcmp (amgr->smgr->name, "DIMACS Printer") == 0)
1049 {
1050 BtorCnfPrinter *cnf_printer = ((BtorCnfPrinter *) amgr->smgr->solver);
1051 allocated +=
1052 sizeof (BtorCnfPrinter) + sizeof (BtorSATMgr)
1053 + BTOR_SIZE_STACK (cnf_printer->clauses) * sizeof (int32_t)
1054 + BTOR_SIZE_STACK (cnf_printer->assumptions) * sizeof (int32_t);
1055 }
1056 #endif
1057 assert (allocated == clone->mm->allocated);
1058 #endif
1059 }
1060 }
1061
1062 BTORLOG_TIMESTAMP (delta);
1063 clone_sorts_unique_table (btor, clone);
1064 BTORLOG (2,
1065 " clone sorts unique table: %.3f s",
1066 (btor_util_time_stamp () - delta));
1067 #ifndef NDEBUG
1068 allocated += btor->sorts_unique_table.size * sizeof (BtorSort *)
1069 + btor->sorts_unique_table.num_elements * sizeof (BtorSort)
1070 + BTOR_SIZE_STACK (btor->sorts_unique_table.id2sort)
1071 * sizeof (BtorSort *);
1072 for (i = 0; i < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort); i++)
1073 {
1074 sort = BTOR_PEEK_STACK (btor->sorts_unique_table.id2sort, i);
1075 if (!sort || sort->kind != BTOR_TUPLE_SORT) continue;
1076 allocated += sort->tuple.num_elements * sizeof (BtorSort *);
1077 }
1078 assert (allocated == clone->mm->allocated);
1079 #endif
1080
1081 emap = btor_nodemap_new (clone);
1082 assert ((allocated += sizeof (*emap) + MEM_PTR_HASH_TABLE (emap->table))
1083 == clone->mm->allocated);
1084
1085 BTOR_INIT_STACK (btor->mm, rhos);
1086 BTORLOG_TIMESTAMP (delta);
1087 clone_nodes_id_table (btor,
1088 clone,
1089 &clone->nodes_id_table,
1090 emap,
1091 exp_layer_only,
1092 &rhos,
1093 clone_simplified);
1094 BTORLOG (
1095 2, " clone nodes id table: %.3f s", (btor_util_time_stamp () - delta));
1096 #ifndef NDEBUG
1097 for (i = 1; i < BTOR_COUNT_STACK (btor->nodes_id_table); i++)
1098 {
1099 if (!(cur = BTOR_PEEK_STACK (btor->nodes_id_table, i))) continue;
1100 allocated += cur->bytes;
1101 if (btor_node_is_bv_const (cur))
1102 {
1103 allocated += MEM_BITVEC (btor_node_bv_const_get_bits (cur));
1104 allocated += MEM_BITVEC (btor_node_bv_const_get_invbits (cur));
1105 }
1106 if (!exp_layer_only)
1107 {
1108 if (!btor_node_is_fun (cur) && cur->av)
1109 allocated += sizeof (*(cur->av)) + cur->av->width * sizeof (BtorAIG *);
1110 }
1111 if (btor_node_is_lambda (cur) && btor_node_lambda_get_static_rho (cur))
1112 allocated += MEM_PTR_HASH_TABLE (btor_node_lambda_get_static_rho (cur));
1113 }
1114 /* Note: hash table is initialized with size 1 */
1115 allocated += (emap->table->size - 1) * sizeof (BtorPtrHashBucket *)
1116 + emap->table->count * sizeof (BtorPtrHashBucket)
1117 + BTOR_SIZE_STACK (btor->nodes_id_table) * sizeof (BtorNode *);
1118 assert (allocated == clone->mm->allocated);
1119 #endif
1120
1121 clone->true_exp = btor_nodemap_mapped (emap, btor->true_exp);
1122 assert (clone->true_exp);
1123
1124 BTORLOG_TIMESTAMP (delta);
1125 clone_nodes_unique_table (btor, clone, emap);
1126 BTORLOG (2,
1127 " clone nodes unique table: %.3f s",
1128 (btor_util_time_stamp () - delta));
1129 assert ((allocated += btor->nodes_unique_table.size * sizeof (BtorNode *))
1130 == clone->mm->allocated);
1131
1132 clone->symbols = btor_hashptr_table_clone (mm,
1133 btor->symbols,
1134 btor_clone_key_as_str,
1135 btor_clone_data_as_node_ptr,
1136 0,
1137 emap);
1138 #ifndef NDEBUG
1139 uint32_t str_bytes = 0;
1140 btor_iter_hashptr_init (&pit, btor->symbols);
1141 while (btor_iter_hashptr_has_next (&pit))
1142 str_bytes +=
1143 (strlen ((char *) btor_iter_hashptr_next (&pit)) + 1) * sizeof (char);
1144 assert ((allocated += MEM_PTR_HASH_TABLE (btor->symbols) + str_bytes)
1145 == clone->mm->allocated);
1146 #endif
1147 clone->node2symbol = btor_hashptr_table_clone (mm,
1148 btor->node2symbol,
1149 btor_clone_key_as_node,
1150 btor_clone_data_as_str_ptr,
1151 emap,
1152 clone->symbols);
1153 #ifndef NDEBUG
1154 assert ((allocated += MEM_PTR_HASH_TABLE (btor->node2symbol))
1155 == clone->mm->allocated);
1156 #endif
1157
1158 CLONE_PTR_HASH_TABLE_DATA (inputs, btor_clone_data_as_int);
1159 assert ((allocated += MEM_PTR_HASH_TABLE (btor->inputs))
1160 == clone->mm->allocated);
1161 CLONE_PTR_HASH_TABLE (bv_vars);
1162 assert ((allocated += MEM_PTR_HASH_TABLE (btor->bv_vars))
1163 == clone->mm->allocated);
1164 CLONE_PTR_HASH_TABLE (ufs);
1165 assert ((allocated += MEM_PTR_HASH_TABLE (btor->ufs))
1166 == clone->mm->allocated);
1167 CLONE_PTR_HASH_TABLE_DATA (lambdas, btor_clone_data_as_int);
1168 assert ((allocated += MEM_PTR_HASH_TABLE (btor->lambdas))
1169 == clone->mm->allocated);
1170 CLONE_PTR_HASH_TABLE_DATA (quantifiers, btor_clone_data_as_int);
1171 assert ((allocated += MEM_PTR_HASH_TABLE (btor->quantifiers))
1172 == clone->mm->allocated);
1173 CLONE_PTR_HASH_TABLE (exists_vars);
1174 assert ((allocated += MEM_PTR_HASH_TABLE (btor->exists_vars))
1175 == clone->mm->allocated);
1176 CLONE_PTR_HASH_TABLE (forall_vars);
1177 assert ((allocated += MEM_PTR_HASH_TABLE (btor->forall_vars))
1178 == clone->mm->allocated);
1179 CLONE_PTR_HASH_TABLE_DATA (feqs, btor_clone_data_as_int);
1180 assert ((allocated += MEM_PTR_HASH_TABLE (btor->feqs))
1181 == clone->mm->allocated);
1182 CLONE_PTR_HASH_TABLE_DATA (substitutions, btor_clone_data_as_node_ptr);
1183 assert ((allocated += MEM_PTR_HASH_TABLE (btor->substitutions))
1184 == clone->mm->allocated);
1185 CLONE_PTR_HASH_TABLE_DATA (varsubst_constraints, btor_clone_data_as_node_ptr);
1186 assert ((allocated += MEM_PTR_HASH_TABLE (btor->varsubst_constraints))
1187 == clone->mm->allocated);
1188 CLONE_PTR_HASH_TABLE (embedded_constraints);
1189 assert ((allocated += MEM_PTR_HASH_TABLE (btor->embedded_constraints))
1190 == clone->mm->allocated);
1191 CLONE_PTR_HASH_TABLE (unsynthesized_constraints);
1192 assert ((allocated += MEM_PTR_HASH_TABLE (btor->unsynthesized_constraints))
1193 == clone->mm->allocated);
1194 CLONE_PTR_HASH_TABLE (synthesized_constraints);
1195 assert ((allocated += MEM_PTR_HASH_TABLE (btor->synthesized_constraints))
1196 == clone->mm->allocated);
1197 CLONE_PTR_HASH_TABLE (assumptions);
1198 assert ((allocated += MEM_PTR_HASH_TABLE (btor->assumptions))
1199 == clone->mm->allocated);
1200 CLONE_PTR_HASH_TABLE (orig_assumptions);
1201 assert ((allocated += MEM_PTR_HASH_TABLE (btor->orig_assumptions))
1202 == clone->mm->allocated);
1203 btor_clone_node_ptr_stack (
1204 mm, &btor->failed_assumptions, &clone->failed_assumptions, emap, true);
1205 assert ((allocated +=
1206 BTOR_SIZE_STACK (btor->failed_assumptions) * sizeof (BtorNode *))
1207 == clone->mm->allocated);
1208
1209 clone->assertions_cache =
1210 btor_hashint_table_clone (clone->mm, btor->assertions_cache);
1211 assert ((allocated += MEM_INT_HASH_TABLE (btor->assertions_cache))
1212 == clone->mm->allocated);
1213
1214 btor_clone_node_ptr_stack (
1215 mm, &btor->assertions, &clone->assertions, emap, false);
1216 assert (
1217 (allocated += BTOR_SIZE_STACK (btor->assertions) * sizeof (BtorNode *))
1218 == clone->mm->allocated);
1219
1220 BTOR_INIT_STACK (clone->mm, clone->assertions_trail);
1221 for (i = 0; i < BTOR_COUNT_STACK (btor->assertions_trail); i++)
1222 BTOR_PUSH_STACK (clone->assertions_trail,
1223 BTOR_PEEK_STACK (btor->assertions_trail, i));
1224 BTOR_ADJUST_STACK (btor->assertions_trail, clone->assertions_trail);
1225 assert ((allocated +=
1226 BTOR_SIZE_STACK (btor->assertions_trail) * sizeof (uint32_t))
1227 == clone->mm->allocated);
1228
1229 if (btor->bv_model)
1230 {
1231 clone->bv_model = btor_model_clone_bv (clone, btor->bv_model, false);
1232 #ifndef NDEBUG
1233 btor_iter_hashint_init (&iit, btor->bv_model);
1234 btor_iter_hashint_init (&ciit, clone->bv_model);
1235 while (btor_iter_hashint_has_next (&iit))
1236 {
1237 data = btor_iter_hashint_next_data (&iit);
1238 cdata = btor_iter_hashint_next_data (&ciit);
1239 assert (btor_bv_size ((BtorBitVector *) data->as_ptr)
1240 == btor_bv_size ((BtorBitVector *) cdata->as_ptr));
1241 allocated += btor_bv_size ((BtorBitVector *) cdata->as_ptr);
1242 }
1243 #endif
1244 }
1245 assert ((allocated += MEM_INT_HASH_MAP (btor->bv_model))
1246 == clone->mm->allocated);
1247 #ifndef NDEBUG
1248 if (!exp_layer_only && btor->stats.rw_rules_applied)
1249 {
1250 clone->stats.rw_rules_applied =
1251 btor_hashptr_table_clone (mm,
1252 btor->stats.rw_rules_applied,
1253 btor_clone_key_as_static_str,
1254 btor_clone_data_as_int,
1255 0,
1256 0);
1257 assert ((allocated += MEM_PTR_HASH_TABLE (btor->stats.rw_rules_applied))
1258 == clone->mm->allocated);
1259 }
1260 #endif
1261 if (btor->fun_model)
1262 {
1263 clone->fun_model = btor_model_clone_fun (clone, btor->fun_model, false);
1264 #ifndef NDEBUG
1265 btor_iter_hashint_init (&iit, btor->fun_model);
1266 btor_iter_hashint_init (&ciit, clone->fun_model);
1267 while (btor_iter_hashint_has_next (&iit))
1268 {
1269 data = btor_iter_hashint_next_data (&iit);
1270 cdata = btor_iter_hashint_next_data (&ciit);
1271 assert (MEM_PTR_HASH_TABLE ((BtorPtrHashTable *) data->as_ptr)
1272 == MEM_PTR_HASH_TABLE ((BtorPtrHashTable *) cdata->as_ptr));
1273 allocated += MEM_PTR_HASH_TABLE ((BtorPtrHashTable *) data->as_ptr);
1274 btor_iter_hashptr_init (&ncpit, ((BtorPtrHashTable *) data->as_ptr));
1275 while (btor_iter_hashptr_has_next (&ncpit))
1276 {
1277 allocated += btor_bv_size ((BtorBitVector *) ncpit.bucket->data.as_ptr);
1278 allocated += btor_bv_size_tuple (
1279 (BtorBitVectorTuple *) btor_iter_hashptr_next (&ncpit));
1280 }
1281 }
1282 #endif
1283 }
1284 assert ((allocated += MEM_INT_HASH_MAP (btor->fun_model))
1285 == clone->mm->allocated);
1286
1287 /* NOTE: we need bv_model for cloning rhos */
1288 while (!BTOR_EMPTY_STACK (rhos))
1289 {
1290 exp = BTOR_POP_STACK (rhos);
1291 cloned_exp = BTOR_POP_STACK (rhos);
1292 assert (btor_node_is_fun (exp));
1293 assert (btor_node_is_fun (cloned_exp));
1294 assert (exp->rho);
1295 cloned_exp->rho = btor_hashptr_table_clone (mm,
1296 exp->rho,
1297 btor_clone_key_as_node,
1298 btor_clone_data_as_node_ptr,
1299 emap,
1300 emap);
1301 #ifndef NDEBUG
1302 allocated += MEM_PTR_HASH_TABLE (cloned_exp->rho);
1303 #endif
1304 }
1305 BTOR_RELEASE_STACK (rhos);
1306 assert (allocated == clone->mm->allocated);
1307
1308 if (exp_layer_only)
1309 {
1310 BTOR_INIT_STACK (mm, clone->functions_with_model);
1311 /* we need to decrement the reference count of the cloned expressions
1312 * that were pushed onto the functions_with_model stack. */
1313 for (i = 0; i < BTOR_COUNT_STACK (btor->functions_with_model); i++)
1314 btor_node_release (
1315 clone,
1316 btor_nodemap_mapped (
1317 emap, BTOR_PEEK_STACK (btor->functions_with_model, i)));
1318 }
1319 else
1320 {
1321 BTORLOG_TIMESTAMP (delta);
1322 btor_clone_node_ptr_stack (mm,
1323 &btor->functions_with_model,
1324 &clone->functions_with_model,
1325 emap,
1326 false);
1327 BTORLOG (2,
1328 " clone functions_with_model: %.3f s",
1329 btor_util_time_stamp () - delta);
1330 assert ((allocated +=
1331 BTOR_SIZE_STACK (btor->functions_with_model) * sizeof (BtorNode *))
1332 == clone->mm->allocated);
1333 }
1334
1335 BTORLOG_TIMESTAMP (delta);
1336 btor_clone_node_ptr_stack (mm, &btor->outputs, &clone->outputs, emap, false);
1337 BTORLOG (2, " clone outputs: %.3f s", btor_util_time_stamp () - delta);
1338 assert ((allocated += BTOR_SIZE_STACK (btor->outputs) * sizeof (BtorNode *))
1339 == clone->mm->allocated);
1340
1341 BTORLOG_TIMESTAMP (delta);
1342 clone->parameterized =
1343 btor_hashptr_table_clone (mm,
1344 btor->parameterized,
1345 btor_clone_key_as_node,
1346 btor_clone_data_as_int_htable,
1347 emap,
1348 emap);
1349 BTORLOG (2,
1350 " clone parameterized table: %.3f s",
1351 (btor_util_time_stamp () - delta));
1352 #ifndef NDEBUG
1353 CHKCLONE_MEM_PTR_HASH_TABLE (btor->parameterized, clone->parameterized);
1354 allocated += MEM_PTR_HASH_TABLE (btor->parameterized);
1355 btor_iter_hashptr_init (&pit, btor->parameterized);
1356 btor_iter_hashptr_init (&cpit, clone->parameterized);
1357 while (btor_iter_hashptr_has_next (&pit))
1358 {
1359 assert (btor_hashint_table_size (pit.bucket->data.as_ptr)
1360 == btor_hashint_table_size (cpit.bucket->data.as_ptr));
1361 allocated += btor_hashint_table_size (cpit.bucket->data.as_ptr);
1362 (void) btor_iter_hashptr_next (&pit);
1363 (void) btor_iter_hashptr_next (&cpit);
1364 }
1365 assert (allocated == clone->mm->allocated);
1366 #endif
1367 BTOR_NEW (mm, clone->rw_cache);
1368 clone->rw_cache->btor = clone;
1369 clone->rw_cache->cache = btor_hashptr_table_clone (
1370 mm, btor->rw_cache->cache, btor_clone_key_as_rw_cache_tuple, 0, 0, 0);
1371 #ifndef NDEBUG
1372 CHKCLONE_MEM_PTR_HASH_TABLE (btor->rw_cache->cache, clone->rw_cache->cache);
1373 allocated += sizeof (*btor->rw_cache);
1374 allocated += btor->rw_cache->cache->count * sizeof (BtorRwCacheTuple);
1375 allocated += MEM_PTR_HASH_TABLE (btor->rw_cache->cache);
1376 #endif
1377
1378 /* move synthesized constraints to unsynthesized if we only clone the exp
1379 * layer */
1380 if (exp_layer_only)
1381 {
1382 #ifndef NDEBUG
1383 allocated -= MEM_PTR_HASH_TABLE (clone->synthesized_constraints);
1384 allocated -= MEM_PTR_HASH_TABLE (clone->unsynthesized_constraints);
1385 #endif
1386 btor_iter_hashptr_init (&pit, clone->synthesized_constraints);
1387 while (btor_iter_hashptr_has_next (&pit))
1388 {
1389 exp = btor_iter_hashptr_next (&pit);
1390 btor_hashptr_table_add (clone->unsynthesized_constraints, exp);
1391 }
1392 btor_hashptr_table_delete (clone->synthesized_constraints);
1393 clone->synthesized_constraints =
1394 btor_hashptr_table_new (mm,
1395 (BtorHashPtr) btor_node_hash_by_id,
1396 (BtorCmpPtr) btor_node_compare_by_id);
1397 #ifndef NDEBUG
1398 allocated += MEM_PTR_HASH_TABLE (clone->synthesized_constraints);
1399 allocated += MEM_PTR_HASH_TABLE (clone->unsynthesized_constraints);
1400 assert (allocated == clone->mm->allocated);
1401 #endif
1402 }
1403
1404 if (clone_slv && btor->slv)
1405 clone->slv = btor->slv->api.clone (clone, btor->slv, emap);
1406 else
1407 clone->slv = 0;
1408 assert (!clone_slv || (btor->slv && clone->slv)
1409 || (!btor->slv && !clone->slv));
1410 #ifndef NDEBUG
1411 if (clone->slv)
1412 {
1413 if (clone->slv->kind == BTOR_FUN_SOLVER_KIND)
1414 {
1415 BtorFunSolver *slv = BTOR_FUN_SOLVER (btor);
1416 BtorFunSolver *cslv = BTOR_FUN_SOLVER (clone);
1417
1418 allocated += sizeof (BtorFunSolver);
1419
1420 allocated += MEM_PTR_HASH_TABLE (slv->lemmas);
1421 allocated += BTOR_SIZE_STACK (slv->cur_lemmas) * sizeof (BtorNode *);
1422
1423 if (slv->score)
1424 {
1425 h = btor_opt_get (btor, BTOR_OPT_FUN_JUST_HEURISTIC);
1426 if (h == BTOR_JUST_HEUR_BRANCH_MIN_APP)
1427 {
1428 CHKCLONE_MEM_PTR_HASH_TABLE (slv->score, cslv->score);
1429 allocated += MEM_PTR_HASH_TABLE (slv->score);
1430
1431 btor_iter_hashptr_init (&pit, slv->score);
1432 btor_iter_hashptr_init (&cpit, cslv->score);
1433 while (btor_iter_hashptr_has_next (&pit))
1434 {
1435 assert (MEM_PTR_HASH_TABLE (
1436 (BtorPtrHashTable *) pit.bucket->data.as_ptr)
1437 == MEM_PTR_HASH_TABLE (
1438 (BtorPtrHashTable *) cpit.bucket->data.as_ptr));
1439 allocated += MEM_PTR_HASH_TABLE (
1440 (BtorPtrHashTable *) pit.bucket->data.as_ptr);
1441 (void) btor_iter_hashptr_next (&pit);
1442 (void) btor_iter_hashptr_next (&cpit);
1443 }
1444 }
1445 else
1446 {
1447 assert (h == BTOR_JUST_HEUR_BRANCH_MIN_DEP);
1448 allocated += MEM_PTR_HASH_TABLE (slv->score);
1449 }
1450 }
1451
1452 assert (BTOR_SIZE_STACK (slv->stats.lemmas_size)
1453 == BTOR_SIZE_STACK (cslv->stats.lemmas_size));
1454 assert (BTOR_COUNT_STACK (slv->stats.lemmas_size)
1455 == BTOR_COUNT_STACK (cslv->stats.lemmas_size));
1456 allocated += BTOR_SIZE_STACK (slv->stats.lemmas_size) * sizeof (uint32_t);
1457 }
1458 else if (clone->slv->kind == BTOR_SLS_SOLVER_KIND)
1459 {
1460 BtorSLSMove *m;
1461 BtorSLSSolver *slv = BTOR_SLS_SOLVER (btor);
1462 BtorSLSSolver *cslv = BTOR_SLS_SOLVER (clone);
1463
1464 CHKCLONE_MEM_INT_HASH_MAP (slv->roots, cslv->roots);
1465 CHKCLONE_MEM_INT_HASH_MAP (slv->score, cslv->score);
1466 CHKCLONE_MEM_INT_HASH_MAP (slv->weights, cslv->weights);
1467
1468 allocated += sizeof (BtorSLSSolver) + MEM_INT_HASH_MAP (cslv->roots)
1469 + MEM_INT_HASH_MAP (cslv->score)
1470 + MEM_INT_HASH_MAP (cslv->weights);
1471
1472 if (slv->weights)
1473 allocated += slv->weights->count * sizeof (BtorSLSConstrData);
1474
1475 assert (BTOR_SIZE_STACK (slv->moves) == BTOR_SIZE_STACK (cslv->moves));
1476 assert (BTOR_COUNT_STACK (slv->moves) == BTOR_COUNT_STACK (cslv->moves));
1477
1478 allocated += BTOR_SIZE_STACK (cslv->moves) * sizeof (BtorSLSMove *)
1479 + BTOR_COUNT_STACK (cslv->moves) * sizeof (BtorSLSMove);
1480
1481 for (i = 0; i < BTOR_COUNT_STACK (cslv->moves); i++)
1482 {
1483 assert (BTOR_PEEK_STACK (cslv->moves, i));
1484 m = BTOR_PEEK_STACK (cslv->moves, i);
1485 assert (MEM_PTR_HASH_TABLE (m->cans)
1486 == MEM_PTR_HASH_TABLE (BTOR_PEEK_STACK (cslv->moves, i)->cans));
1487 allocated += MEM_PTR_HASH_TABLE (m->cans);
1488 btor_iter_hashint_init (&iit, m->cans);
1489 while (btor_iter_hashint_has_next (&iit))
1490 allocated +=
1491 btor_bv_size (btor_iter_hashint_next_data (&iit)->as_ptr);
1492 }
1493
1494 if (cslv->max_cans)
1495 {
1496 assert (slv->max_cans);
1497 assert (slv->max_cans->count == cslv->max_cans->count);
1498 allocated += MEM_PTR_HASH_TABLE (cslv->max_cans);
1499 btor_iter_hashint_init (&iit, cslv->max_cans);
1500 while (btor_iter_hashint_has_next (&iit))
1501 allocated +=
1502 btor_bv_size (btor_iter_hashint_next_data (&iit)->as_ptr);
1503 }
1504 }
1505 else if (clone->slv->kind == BTOR_PROP_SOLVER_KIND)
1506 {
1507 BtorPropSolver *slv = BTOR_PROP_SOLVER (btor);
1508 BtorPropSolver *cslv = BTOR_PROP_SOLVER (clone);
1509
1510 CHKCLONE_MEM_INT_HASH_MAP (slv->roots, cslv->roots);
1511 CHKCLONE_MEM_INT_HASH_MAP (slv->score, cslv->score);
1512
1513 allocated += sizeof (BtorPropSolver) + MEM_PTR_HASH_TABLE (cslv->roots)
1514 + MEM_PTR_HASH_TABLE (cslv->score);
1515 }
1516 else if (clone->slv->kind == BTOR_AIGPROP_SOLVER_KIND)
1517 {
1518 BtorAIGPropSolver *slv = BTOR_AIGPROP_SOLVER (btor);
1519 BtorAIGPropSolver *cslv = BTOR_AIGPROP_SOLVER (clone);
1520
1521 if (slv->aprop)
1522 {
1523 assert (cslv->aprop);
1524 CHKCLONE_MEM_PTR_HASH_TABLE (slv->aprop->roots, cslv->aprop->roots);
1525 CHKCLONE_MEM_PTR_HASH_TABLE (slv->aprop->score, cslv->aprop->score);
1526 CHKCLONE_MEM_PTR_HASH_TABLE (slv->aprop->model, cslv->aprop->model);
1527 allocated += sizeof (BtorAIGProp)
1528 + MEM_PTR_HASH_TABLE (cslv->aprop->roots)
1529 + MEM_PTR_HASH_TABLE (cslv->aprop->score)
1530 + MEM_PTR_HASH_TABLE (cslv->aprop->model);
1531 }
1532
1533 allocated += sizeof (BtorAIGPropSolver);
1534 }
1535
1536 assert (allocated == clone->mm->allocated);
1537 }
1538 #endif
1539
1540 clone->parse_error_msg = NULL;
1541 #ifndef NDEBUG
1542 clone->clone = NULL;
1543 #endif
1544 clone->close_apitrace = 0;
1545
1546 if (exp_map)
1547 *exp_map = emap;
1548 else
1549 btor_nodemap_delete (emap);
1550
1551 #ifndef NDEBUG
1552 /* flag sanity checks */
1553 btor_iter_hashptr_init (&pit, btor->synthesized_constraints);
1554 btor_iter_hashptr_queue (&pit, btor->unsynthesized_constraints);
1555 btor_iter_hashptr_queue (&pit, btor->embedded_constraints);
1556 while (btor_iter_hashptr_has_next (&pit))
1557 {
1558 exp = btor_iter_hashptr_next (&pit);
1559 assert (btor_node_real_addr (exp)->constraint);
1560 }
1561 #endif
1562
1563 btor->time.cloning += btor_util_time_stamp () - start;
1564 BTORLOG (2, "cloning total: %.3f s", btor->time.cloning);
1565 return clone;
1566 }
1567
1568 Btor *
btor_clone_btor(Btor * btor)1569 btor_clone_btor (Btor *btor)
1570 {
1571 assert (btor);
1572 return clone_aux_btor (
1573 btor,
1574 0,
1575 !btor_sat_mgr_has_clone_support (btor_get_sat_mgr (btor)),
1576 true,
1577 true);
1578 }
1579
1580 Btor *
btor_clone_exp_layer(Btor * btor,BtorNodeMap ** exp_map,bool clone_simplified)1581 btor_clone_exp_layer (Btor *btor, BtorNodeMap **exp_map, bool clone_simplified)
1582 {
1583 assert (btor);
1584 return clone_aux_btor (btor, exp_map, true, true, clone_simplified);
1585 }
1586
1587 Btor *
btor_clone_formula(Btor * btor)1588 btor_clone_formula (Btor *btor)
1589 {
1590 assert (btor);
1591 return clone_aux_btor (btor, 0, true, false, true);
1592 }
1593
1594 BtorSortId
btor_clone_recursively_rebuild_sort(Btor * btor,Btor * clone,BtorSortId sort)1595 btor_clone_recursively_rebuild_sort (Btor *btor, Btor *clone, BtorSortId sort)
1596 {
1597 uint32_t i;
1598 BtorSort *s;
1599 BtorSortId r, s0, s1;
1600 BtorSortPtrStack sort_stack;
1601 BtorIntHashTable *map;
1602 BtorHashTableData *d;
1603 BtorMemMgr *mm;
1604 BtorSortIdStack sort_ids;
1605
1606 mm = btor->mm;
1607 map = btor_hashint_map_new (mm);
1608
1609 s = btor_sort_get_by_id (btor, sort);
1610
1611 BTOR_INIT_STACK (mm, sort_ids);
1612 BTOR_INIT_STACK (mm, sort_stack);
1613 BTOR_PUSH_STACK (sort_stack, s);
1614 while (!BTOR_EMPTY_STACK (sort_stack))
1615 {
1616 s = BTOR_POP_STACK (sort_stack);
1617 d = btor_hashint_map_get (map, s->id);
1618 if (!d)
1619 {
1620 btor_hashint_map_add (map, s->id);
1621
1622 BTOR_PUSH_STACK (sort_stack, s);
1623 switch (s->kind)
1624 {
1625 case BTOR_ARRAY_SORT:
1626 BTOR_PUSH_STACK (sort_stack, s->array.element);
1627 BTOR_PUSH_STACK (sort_stack, s->array.index);
1628 break;
1629 case BTOR_LST_SORT:
1630 BTOR_PUSH_STACK (sort_stack, s->lst.head);
1631 BTOR_PUSH_STACK (sort_stack, s->lst.tail);
1632 break;
1633 case BTOR_FUN_SORT:
1634 BTOR_PUSH_STACK (sort_stack, s->fun.domain);
1635 BTOR_PUSH_STACK (sort_stack, s->fun.codomain);
1636 break;
1637 case BTOR_TUPLE_SORT:
1638 for (i = 0; i < s->tuple.num_elements; i++)
1639 BTOR_PUSH_STACK (sort_stack, s->tuple.elements[i]);
1640 break;
1641 default: assert (s->kind == BTOR_BOOL_SORT || s->kind == BTOR_BV_SORT);
1642 }
1643 }
1644 else if (!d->as_int)
1645 {
1646 switch (s->kind)
1647 {
1648 case BTOR_ARRAY_SORT:
1649 s0 = btor_hashint_map_get (map, s->array.index->id)->as_int;
1650 s1 = btor_hashint_map_get (map, s->array.element->id)->as_int;
1651 r = btor_sort_array (clone, s0, s1);
1652 break;
1653 #if 0
1654 case BTOR_LST_SORT:
1655 s0 = btor_hashint_map_get (map, s->lst.head->id)->as_int;
1656 s1 = btor_hashint_map_get (map, s->lst.tail->id)->as_int;
1657 r = btor_lst_sort (clone, s0, s1);
1658 break;
1659 #endif
1660 case BTOR_FUN_SORT:
1661 s0 = btor_hashint_map_get (map, s->fun.domain->id)->as_int;
1662 s1 = btor_hashint_map_get (map, s->fun.codomain->id)->as_int;
1663 r = btor_sort_fun (clone, s0, s1);
1664 break;
1665 case BTOR_TUPLE_SORT:
1666 for (i = 0; i < s->tuple.num_elements; i++)
1667 {
1668 s0 = btor_hashint_map_get (map, s->tuple.elements[i]->id)->as_int;
1669 BTOR_PUSH_STACK (sort_ids, s0);
1670 }
1671 r = btor_sort_tuple (clone, sort_ids.start, s->tuple.num_elements);
1672 BTOR_RESET_STACK (sort_ids);
1673 break;
1674 case BTOR_BOOL_SORT: r = btor_sort_bool (clone); break;
1675 default:
1676 assert (s->kind == BTOR_BV_SORT);
1677 r = btor_sort_bv (clone, s->bitvec.width);
1678 }
1679 assert (r);
1680 d->as_int = r;
1681 }
1682 }
1683 d = btor_hashint_map_get (map, sort);
1684 assert (d);
1685 assert (d->as_int);
1686 r = btor_sort_copy (clone, d->as_int);
1687
1688 for (i = 0; i < map->size; i++)
1689 {
1690 if (!map->keys[i]) continue;
1691 s0 = map->data[i].as_int;
1692 btor_sort_release (clone, s0);
1693 }
1694 btor_hashint_map_delete (map);
1695 BTOR_RELEASE_STACK (sort_ids);
1696 BTOR_RELEASE_STACK (sort_stack);
1697 return r;
1698 }
1699
1700 BtorNode *
btor_clone_recursively_rebuild_exp(Btor * btor,Btor * clone,BtorNode * exp,BtorNodeMap * exp_map,uint32_t rewrite_level)1701 btor_clone_recursively_rebuild_exp (Btor *btor,
1702 Btor *clone,
1703 BtorNode *exp,
1704 BtorNodeMap *exp_map,
1705 uint32_t rewrite_level)
1706 {
1707 assert (btor);
1708 assert (exp);
1709 assert (btor_node_real_addr (exp)->btor == btor);
1710 assert (exp_map);
1711
1712 uint32_t i, rwl;
1713 char *symbol;
1714 BtorNode *real_exp, *cur, *cur_clone, *e[3];
1715 BtorNodePtrStack work_stack;
1716 BtorIntHashTable *mark;
1717 BtorMemMgr *mm;
1718 BtorPtrHashBucket *b;
1719 BtorSortId sort;
1720
1721 mm = btor->mm;
1722 mark = btor_hashint_table_new (mm);
1723
1724 /* in some cases we may want to rebuild the expressions with a certain
1725 * rewrite level */
1726 rwl = btor_opt_get (clone, BTOR_OPT_REWRITE_LEVEL);
1727 if (rwl > 0) btor_opt_set (clone, BTOR_OPT_REWRITE_LEVEL, rewrite_level);
1728
1729 BTOR_INIT_STACK (mm, work_stack);
1730
1731 real_exp = btor_node_real_addr (exp);
1732 BTOR_PUSH_STACK (work_stack, real_exp);
1733 while (!BTOR_EMPTY_STACK (work_stack))
1734 {
1735 cur = btor_node_real_addr (BTOR_POP_STACK (work_stack));
1736
1737 if (btor_nodemap_mapped (exp_map, cur)) continue;
1738
1739 if (!btor_hashint_table_contains (mark, cur->id))
1740 {
1741 btor_hashint_table_add (mark, cur->id);
1742 BTOR_PUSH_STACK (work_stack, cur);
1743 for (i = 0; i < cur->arity; i++) BTOR_PUSH_STACK (work_stack, cur->e[i]);
1744 }
1745 else
1746 {
1747 assert (!btor_nodemap_mapped (exp_map, cur));
1748 assert (!btor_node_is_proxy (cur));
1749 for (i = 0; i < cur->arity; i++)
1750 {
1751 e[i] = btor_nodemap_mapped (exp_map, cur->e[i]);
1752 assert (e[i]);
1753 }
1754 switch (cur->kind)
1755 {
1756 case BTOR_BV_CONST_NODE:
1757 cur_clone = btor_exp_bv_const (clone, btor_node_bv_const_get_bits (cur));
1758 break;
1759 case BTOR_VAR_NODE:
1760 b = btor_hashptr_table_get (btor->node2symbol, cur);
1761 symbol = b ? b->data.as_str : 0;
1762 if (symbol && (b = btor_hashptr_table_get (clone->symbols, symbol)))
1763 {
1764 cur_clone = btor_node_copy (clone, b->data.as_ptr);
1765 assert (cur_clone->sort_id == cur->sort_id);
1766 assert (cur_clone->kind == cur->kind);
1767 }
1768 else
1769 {
1770 sort = btor_sort_bv (clone, btor_node_bv_get_width (btor, cur));
1771 cur_clone = btor_exp_var (clone, sort, symbol);
1772 btor_sort_release (clone, sort);
1773 }
1774 break;
1775 case BTOR_PARAM_NODE:
1776 b = btor_hashptr_table_get (btor->node2symbol, cur);
1777 symbol = b ? b->data.as_str : 0;
1778 if (symbol && (b = btor_hashptr_table_get (clone->symbols, symbol)))
1779 {
1780 cur_clone = btor_node_copy (clone, b->data.as_ptr);
1781 assert (cur_clone->sort_id == cur->sort_id);
1782 assert (cur_clone->kind == cur->kind);
1783 }
1784 else
1785 {
1786 sort = btor_sort_bv (clone, btor_node_bv_get_width (btor, cur));
1787 cur_clone = btor_exp_param (clone, sort, symbol);
1788 btor_sort_release (clone, sort);
1789 }
1790 break;
1791 case BTOR_UF_NODE:
1792 b = btor_hashptr_table_get (btor->node2symbol, cur);
1793 symbol = b ? b->data.as_str : 0;
1794 if (symbol && (b = btor_hashptr_table_get (clone->symbols, symbol)))
1795 {
1796 cur_clone = btor_node_copy (clone, b->data.as_ptr);
1797 assert (cur_clone->sort_id == cur->sort_id);
1798 assert (cur_clone->kind == cur->kind);
1799 }
1800 else
1801 {
1802 sort =
1803 btor_clone_recursively_rebuild_sort (btor, clone, cur->sort_id);
1804 cur_clone = btor_exp_uf (clone, sort, symbol);
1805 btor_sort_release (clone, sort);
1806 }
1807 break;
1808 case BTOR_BV_SLICE_NODE:
1809 cur_clone = btor_exp_bv_slice (clone,
1810 e[0],
1811 btor_node_bv_slice_get_upper (cur),
1812 btor_node_bv_slice_get_lower (cur));
1813 break;
1814 case BTOR_BV_AND_NODE:
1815 cur_clone = btor_exp_bv_and (clone, e[0], e[1]);
1816 break;
1817 case BTOR_BV_EQ_NODE:
1818 case BTOR_FUN_EQ_NODE:
1819 cur_clone = btor_exp_eq (clone, e[0], e[1]);
1820 break;
1821 case BTOR_BV_ADD_NODE:
1822 cur_clone = btor_exp_bv_add (clone, e[0], e[1]);
1823 break;
1824 case BTOR_BV_MUL_NODE:
1825 cur_clone = btor_exp_bv_mul (clone, e[0], e[1]);
1826 break;
1827 case BTOR_BV_ULT_NODE:
1828 cur_clone = btor_exp_bv_ult (clone, e[0], e[1]);
1829 break;
1830 case BTOR_BV_SLL_NODE:
1831 cur_clone = btor_exp_bv_sll (clone, e[0], e[1]);
1832 break;
1833 case BTOR_BV_SRL_NODE:
1834 cur_clone = btor_exp_bv_srl (clone, e[0], e[1]);
1835 break;
1836 case BTOR_BV_UDIV_NODE:
1837 cur_clone = btor_exp_bv_udiv (clone, e[0], e[1]);
1838 break;
1839 case BTOR_BV_UREM_NODE:
1840 cur_clone = btor_exp_bv_urem (clone, e[0], e[1]);
1841 break;
1842 case BTOR_BV_CONCAT_NODE:
1843 cur_clone = btor_exp_bv_concat (clone, e[0], e[1]);
1844 break;
1845 case BTOR_LAMBDA_NODE:
1846 assert (!btor_node_param_get_assigned_exp (e[0]));
1847 btor_node_param_set_binder (e[0], 0);
1848 cur_clone = btor_exp_lambda (clone, e[0], e[1]);
1849 break;
1850 case BTOR_APPLY_NODE:
1851 // FIXME use btor_exp_apply as soon as applies are
1852 // generated with rewriting (currently without)
1853 // cur_clone = btor_exp_apply (clone, e[0], e[1]);
1854 cur_clone = btor_node_create_apply (clone, e[0], e[1]);
1855 break;
1856 case BTOR_ARGS_NODE:
1857 cur_clone = btor_exp_args (clone, e, cur->arity);
1858 break;
1859 case BTOR_EXISTS_NODE:
1860 cur_clone = btor_exp_exists (clone, e[0], e[1]);
1861 break;
1862 case BTOR_FORALL_NODE:
1863 cur_clone = btor_exp_forall (clone, e[0], e[1]);
1864 break;
1865 default:
1866 assert (btor_node_is_bv_cond (cur));
1867 cur_clone = btor_exp_cond (clone, e[0], e[1], e[2]);
1868 }
1869 btor_nodemap_map (exp_map, cur, cur_clone);
1870 btor_node_release (clone, cur_clone);
1871 }
1872 }
1873
1874 BTOR_RELEASE_STACK (work_stack);
1875 btor_hashint_table_delete (mark);
1876
1877 /* reset rewrite_level to original value */
1878 btor_opt_set (clone, BTOR_OPT_REWRITE_LEVEL, rwl);
1879 return btor_node_copy (clone, btor_nodemap_mapped (exp_map, exp));
1880 }
1881