1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 cofactor_elim_term_ite.cpp
7
8 Abstract:
9
10 Eliminate term if-then-else's using cofactors.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-06-05.
15
16 Revision History:
17
18 --*/
19 #include "tactic/core/cofactor_elim_term_ite.h"
20 #include "ast/rewriter/mk_simplified_app.h"
21 #include "ast/rewriter/rewriter_def.h"
22 #include "ast/for_each_expr.h"
23 #include "ast/ast_smt2_pp.h"
24 #include "ast/ast_ll_pp.h"
25 #include "tactic/tactic.h"
26
27 struct cofactor_elim_term_ite::imp {
28 ast_manager & m;
29 params_ref m_params;
30 unsigned long long m_max_memory;
31 bool m_cofactor_equalities;
32
checkpointcofactor_elim_term_ite::imp33 void checkpoint() {
34 if (memory::get_allocation_size() > m_max_memory)
35 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
36 tactic::checkpoint(m);
37 }
38
39 // Collect atoms that contain term if-then-else
40 struct analyzer {
41 struct frame {
42 expr * m_t;
43 unsigned m_first:1;
44 unsigned m_form_ctx:1;
framecofactor_elim_term_ite::imp::analyzer::frame45 frame(expr * t, bool form_ctx):m_t(t), m_first(true), m_form_ctx(form_ctx) {}
46 };
47
48 ast_manager & m;
49 imp & m_owner;
50 obj_hashtable<expr> m_candidates;
51 expr_fast_mark1 m_processed;
52 expr_fast_mark2 m_has_term_ite;
53 svector<frame> m_frame_stack;
54
analyzercofactor_elim_term_ite::imp::analyzer55 analyzer(ast_manager & _m, imp & owner):m(_m), m_owner(owner) {}
56
push_framecofactor_elim_term_ite::imp::analyzer57 void push_frame(expr * t, bool form_ctx) {
58 m_frame_stack.push_back(frame(t, form_ctx && m.is_bool(t)));
59 }
60
visitcofactor_elim_term_ite::imp::analyzer61 void visit(expr * t, bool form_ctx, bool & visited) {
62 if (!m_processed.is_marked(t)) {
63 visited = false;
64 push_frame(t, form_ctx);
65 }
66 }
67
save_candidatecofactor_elim_term_ite::imp::analyzer68 void save_candidate(expr * t, bool form_ctx) {
69 if (!form_ctx)
70 return;
71 if (!m.is_bool(t))
72 return;
73 if (!m_has_term_ite.is_marked(t))
74 return;
75 if (!is_app(t))
76 return;
77 if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
78 switch (to_app(t)->get_decl_kind()) {
79 case OP_OR:
80 case OP_AND:
81 case OP_NOT:
82 case OP_XOR:
83 case OP_IMPLIES:
84 case OP_TRUE:
85 case OP_FALSE:
86 case OP_ITE:
87 return;
88 case OP_EQ:
89 case OP_DISTINCT:
90 if (m.is_bool(to_app(t)->get_arg(0)))
91 return;
92 break;
93 default:
94 break;
95 }
96 }
97 // it is an atom in a formula context (i.e., it is not nested inside a term),
98 // and it contains a term if-then-else.
99 m_candidates.insert(t);
100 }
101
operator ()cofactor_elim_term_ite::imp::analyzer102 void operator()(expr * t) {
103 SASSERT(m.is_bool(t));
104 push_frame(t, true);
105 SASSERT(!m_frame_stack.empty());
106 while (!m_frame_stack.empty()) {
107 frame & fr = m_frame_stack.back();
108 expr * t = fr.m_t;
109 bool form_ctx = fr.m_form_ctx;
110 TRACE("cofactor", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
111
112 m_owner.checkpoint();
113
114 if (m_processed.is_marked(t)) {
115 save_candidate(t, form_ctx);
116 m_frame_stack.pop_back();
117 continue;
118 }
119
120 if (m.is_term_ite(t)) {
121 m_has_term_ite.mark(t);
122 m_processed.mark(t);
123 m_frame_stack.pop_back();
124 continue;
125 }
126
127 if (fr.m_first) {
128 fr.m_first = false;
129 bool visited = true;
130 if (is_app(t)) {
131 unsigned num_args = to_app(t)->get_num_args();
132 for (unsigned i = 0; i < num_args; i++)
133 visit(to_app(t)->get_arg(i), form_ctx, visited);
134 }
135 // ignoring quantifiers
136 if (!visited)
137 continue;
138 }
139
140 if (is_app(t)) {
141 unsigned num_args = to_app(t)->get_num_args();
142 unsigned i;
143 for (i = 0; i < num_args; i++) {
144 if (m_has_term_ite.is_marked(to_app(t)->get_arg(i)))
145 break;
146 }
147 if (i < num_args) {
148 m_has_term_ite.mark(t);
149 TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
150 save_candidate(t, form_ctx);
151 }
152 }
153 else {
154 SASSERT(is_quantifier(t) || is_var(t));
155 // ignoring quantifiers... they are treated as black boxes.
156 }
157 m_processed.mark(t);
158 m_frame_stack.pop_back();
159 }
160 m_processed.reset();
161 m_has_term_ite.reset();
162 }
163 };
164
get_firstcofactor_elim_term_ite::imp165 expr * get_first(expr * t) {
166 TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
167 typedef std::pair<expr *, unsigned> frame;
168 expr_fast_mark1 visited;
169 sbuffer<frame> stack;
170 stack.push_back(frame(t, 0));
171 while (!stack.empty()) {
172 start:
173 checkpoint();
174 frame & fr = stack.back();
175 expr * curr = fr.first;
176 if (m.is_term_ite(curr))
177 return to_app(curr)->get_arg(0);
178 switch (curr->get_kind()) {
179 case AST_VAR:
180 case AST_QUANTIFIER:
181 // ignore quantifiers
182 stack.pop_back();
183 break;
184 case AST_APP: {
185 unsigned num_args = to_app(curr)->get_num_args();
186 while (fr.second < num_args) {
187 expr * arg = to_app(curr)->get_arg(fr.second);
188 fr.second++;
189 if (arg->get_ref_count() > 1) {
190 if (visited.is_marked(arg))
191 continue;
192 visited.mark(arg);
193 }
194 switch (arg->get_kind()) {
195 case AST_VAR:
196 case AST_QUANTIFIER:
197 // ignore quantifiers
198 break;
199 case AST_APP:
200 if (to_app(arg)->get_num_args() > 0) {
201 stack.push_back(frame(arg, 0));
202 goto start;
203 }
204 break;
205 default:
206 UNREACHABLE();
207 break;
208 }
209 }
210 stack.pop_back();
211 break;
212 }
213 default:
214 UNREACHABLE();
215 break;
216 }
217 }
218 return nullptr;
219 }
220
221 /**
222 \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
223 */
get_bestcofactor_elim_term_ite::imp224 expr * get_best(expr * t) {
225 TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
226 typedef std::pair<expr *, unsigned> frame;
227 obj_map<expr, unsigned> occs;
228 expr_fast_mark1 visited;
229 sbuffer<frame> stack;
230
231 stack.push_back(frame(t, 0));
232 while (!stack.empty()) {
233 start:
234 checkpoint();
235 frame & fr = stack.back();
236 expr * curr = fr.first;
237 switch (curr->get_kind()) {
238 case AST_VAR:
239 case AST_QUANTIFIER:
240 // ignore quantifiers
241 stack.pop_back();
242 break;
243 case AST_APP: {
244 unsigned num_args = to_app(curr)->get_num_args();
245 bool is_term_ite = m.is_term_ite(curr);
246 while (fr.second < num_args) {
247 expr * arg = to_app(curr)->get_arg(fr.second);
248 if (fr.second == 0 && is_term_ite) {
249 unsigned num = 0;
250 if (occs.find(arg, num))
251 occs.insert(arg, num+1);
252 else
253 occs.insert(arg, 1);
254 }
255 fr.second++;
256 if (arg->get_ref_count() > 1) {
257 if (visited.is_marked(arg))
258 continue;
259 visited.mark(arg);
260 }
261 switch (arg->get_kind()) {
262 case AST_VAR:
263 case AST_QUANTIFIER:
264 // ignore quantifiers
265 break;
266 case AST_APP:
267 if (to_app(arg)->get_num_args() > 0) {
268 stack.push_back(frame(arg, 0));
269 goto start;
270 }
271 break;
272 default:
273 UNREACHABLE();
274 break;
275 }
276 }
277 stack.pop_back();
278 break;
279 }
280 default:
281 UNREACHABLE();
282 break;
283 }
284 }
285 expr * best = nullptr;
286 unsigned best_occs = 0;
287 obj_map<expr, unsigned>::iterator it = occs.begin();
288 obj_map<expr, unsigned>::iterator end = occs.end();
289 for (; it != end; ++it) {
290 if ((!best) ||
291 (get_depth(it->m_key) < get_depth(best)) ||
292 (get_depth(it->m_key) == get_depth(best) && it->m_value > best_occs) ||
293 // break ties by giving preference to equalities
294 (get_depth(it->m_key) == get_depth(best) && it->m_value == best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) {
295 best = it->m_key;
296 best_occs = it->m_value;
297 }
298 }
299 visited.reset();
300 CTRACE("cofactor", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
301 return best;
302 }
303
updt_paramscofactor_elim_term_ite::imp304 void updt_params(params_ref const & p) {
305 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
306 m_cofactor_equalities = p.get_bool("cofactor_equalities", true);
307 }
308
collect_param_descrscofactor_elim_term_ite::imp309 void collect_param_descrs(param_descrs & r) {
310 r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.");
311 }
312
313
314 struct cofactor_rw_cfg : public default_rewriter_cfg {
315 ast_manager & m;
316 imp & m_owner;
317 obj_hashtable<expr> * m_has_term_ite;
318 mk_simplified_app m_mk_app;
319 expr * m_atom;
320 bool m_sign;
321 expr * m_term;
322 app * m_value;
323 bool m_strict_lower;
324 app * m_lower;
325 bool m_strict_upper;
326 app * m_upper;
327
cofactor_rw_cfgcofactor_elim_term_ite::imp::cofactor_rw_cfg328 cofactor_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> * has_term_ite = nullptr):
329 m(_m),
330 m_owner(owner),
331 m_has_term_ite(has_term_ite),
332 m_mk_app(m, owner.m_params) {
333 }
334
max_steps_exceededcofactor_elim_term_ite::imp::cofactor_rw_cfg335 bool max_steps_exceeded(unsigned num_steps) const {
336 m_owner.checkpoint();
337 return false;
338 }
339
pre_visitcofactor_elim_term_ite::imp::cofactor_rw_cfg340 bool pre_visit(expr * t) {
341 return true;
342 }
343
set_cofactor_atomcofactor_elim_term_ite::imp::cofactor_rw_cfg344 void set_cofactor_atom(expr * t) {
345 if (m.is_not(t)) {
346 m_atom = to_app(t)->get_arg(0);
347 m_sign = true;
348 m_term = nullptr;
349 // TODO: bounds
350 }
351 else {
352 m_atom = t;
353 m_sign = false;
354 m_term = nullptr;
355 expr * lhs;
356 expr * rhs;
357 if (m_owner.m_cofactor_equalities && m.is_eq(t, lhs, rhs)) {
358 if (m.is_unique_value(lhs)) {
359 m_term = rhs;
360 m_value = to_app(lhs);
361 TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
362 }
363 else if (m.is_unique_value(rhs)) {
364 m_term = lhs;
365 m_value = to_app(rhs);
366 TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
367 }
368 }
369 // TODO: bounds
370 }
371 }
372
rewrite_patternscofactor_elim_term_ite::imp::cofactor_rw_cfg373 bool rewrite_patterns() const { return false; }
374
reduce_appcofactor_elim_term_ite::imp::cofactor_rw_cfg375 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
376 result_pr = nullptr;
377 return m_mk_app.mk_core(f, num, args, result);
378 }
379
get_substcofactor_elim_term_ite::imp::cofactor_rw_cfg380 bool get_subst(expr * s, expr * & t, proof * & pr) {
381 pr = nullptr;
382
383 if (s == m_atom) {
384 t = m_sign ? m.mk_false() : m.mk_true();
385 return true;
386 }
387
388 if (s == m_term && m_value != nullptr) {
389 t = m_value;
390 return true;
391 }
392
393 // TODO: handle simple bounds
394 // Example: s is of the form (<= s 10) and m_term == s, and m_upper is 9
395 // then rewrite to true.
396
397 return false;
398 }
399
400 };
401
402 struct cofactor_rw : rewriter_tpl<cofactor_rw_cfg> {
403 cofactor_rw_cfg m_cfg;
404 public:
cofactor_rwcofactor_elim_term_ite::imp::cofactor_rw405 cofactor_rw(ast_manager & m, imp & owner, obj_hashtable<expr> * has_term_ite = nullptr):
406 rewriter_tpl<cofactor_rw_cfg>(m, false, m_cfg),
407 m_cfg(m, owner, has_term_ite) {
408 }
409
set_cofactor_atomcofactor_elim_term_ite::imp::cofactor_rw410 void set_cofactor_atom(expr * t) {
411 m_cfg.set_cofactor_atom(t);
412 reset();
413 }
414 };
415
416 struct main_rw_cfg : public default_rewriter_cfg {
417 ast_manager & m;
418 imp & m_owner;
419 cofactor_rw m_cofactor;
420 obj_hashtable<expr> const & m_candidates;
421 obj_map<expr, expr*> m_cache;
422 expr_ref_vector m_cache_domain;
423
main_rw_cfgcofactor_elim_term_ite::imp::main_rw_cfg424 main_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> & candidates):
425 m(_m),
426 m_owner(owner),
427 m_cofactor(m, m_owner),
428 m_candidates(candidates),
429 m_cache_domain(_m) {
430 }
431
max_steps_exceededcofactor_elim_term_ite::imp::main_rw_cfg432 bool max_steps_exceeded(unsigned num_steps) const {
433 m_owner.checkpoint();
434 return false;
435 }
436
pre_visitcofactor_elim_term_ite::imp::main_rw_cfg437 bool pre_visit(expr * t) {
438 return m.is_bool(t) && !is_quantifier(t);
439 }
440
get_substcofactor_elim_term_ite::imp::main_rw_cfg441 bool get_subst(expr * s, expr * & t, proof * & t_pr) {
442 if (m_candidates.contains(s)) {
443 t_pr = nullptr;
444
445 if (m_cache.find(s, t))
446 return true;
447 unsigned step = 0;
448 TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(s, m) << "\n";);
449 expr_ref curr(m);
450 curr = s;
451 while (true) {
452 // expr * c = m_owner.get_best(curr);
453 expr * c = m_owner.get_first(curr);
454 if (c == nullptr) {
455 m_cache.insert(s, curr);
456 m_cache_domain.push_back(curr);
457 t = curr.get();
458 return true;
459 }
460 step++;
461 expr_ref pos_cofactor(m);
462 expr_ref neg_cofactor(m);
463 m_cofactor.set_cofactor_atom(c);
464 m_cofactor(curr, pos_cofactor);
465 expr_ref neg_c(m);
466 neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);
467 m_cofactor.set_cofactor_atom(neg_c);
468 m_cofactor(curr, neg_cofactor);
469 curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
470 TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
471 }
472 }
473 return false;
474 }
475 };
476
477 struct main_rw : rewriter_tpl<main_rw_cfg> {
478 main_rw_cfg m_cfg;
479 public:
main_rwcofactor_elim_term_ite::imp::main_rw480 main_rw(ast_manager & m, imp & owner, obj_hashtable<expr> & candidates):
481 rewriter_tpl<main_rw_cfg>(m, false, m_cfg),
482 m_cfg(m, owner, candidates) {
483 }
484 };
485
486 struct bottom_up_elim {
487 typedef std::pair<expr*, bool> frame;
488 ast_manager & m;
489 imp & m_owner;
490 obj_map<expr, expr*> m_cache;
491 expr_ref_vector m_cache_domain;
492 obj_hashtable<expr> m_has_term_ite;
493 svector<frame> m_frames;
494 cofactor_rw m_cofactor;
495
bottom_up_elimcofactor_elim_term_ite::imp::bottom_up_elim496 bottom_up_elim(ast_manager & _m, imp & owner):
497 m(_m),
498 m_owner(owner),
499 m_cache_domain(m),
500 m_cofactor(m, owner, &m_has_term_ite) {
501 }
502
is_atomcofactor_elim_term_ite::imp::bottom_up_elim503 bool is_atom(expr * t) const {
504 if (!m.is_bool(t))
505 return false;
506 if (!is_app(t))
507 return false;
508 if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
509 switch (to_app(t)->get_decl_kind()) {
510 case OP_EQ:
511 case OP_DISTINCT:
512 if (m.is_bool(to_app(t)->get_arg(0)))
513 return false;
514 else
515 return true;
516 default:
517 return false;
518 }
519 }
520 return true;
521 }
522
cofactorcofactor_elim_term_ite::imp::bottom_up_elim523 void cofactor(expr * t, expr_ref & r) {
524 unsigned step = 0;
525 TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
526 expr_ref curr(m);
527 curr = t;
528 while (true) {
529 expr * c = m_owner.get_best(curr);
530 // expr * c = m_owner.get_first(curr);
531 if (c == nullptr) {
532 r = curr.get();
533 return;
534 }
535 step++;
536 expr_ref pos_cofactor(m);
537 expr_ref neg_cofactor(m);
538 m_cofactor.set_cofactor_atom(c);
539 m_cofactor(curr, pos_cofactor);
540 expr_ref neg_c(m);
541 neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);
542 m_cofactor.set_cofactor_atom(neg_c);
543 m_cofactor(curr, neg_cofactor);
544 if (pos_cofactor == neg_cofactor) {
545 curr = pos_cofactor;
546 }
547 else if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
548 curr = c;
549 }
550 else if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
551 curr = neg_c;
552 }
553 else {
554 curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
555 }
556 TRACE("cofactor",
557 tout << "cofactor_ite step: " << step << "\n";
558 tout << "cofactor: " << mk_ismt2_pp(c, m) << "\n";
559 tout << mk_ismt2_pp(curr, m) << "\n";);
560 }
561 }
562
visitcofactor_elim_term_ite::imp::bottom_up_elim563 void visit(expr * t, bool & visited) {
564 if (!m_cache.contains(t)) {
565 m_frames.push_back(frame(t, true));
566 visited = false;
567 }
568 }
569
operator ()cofactor_elim_term_ite::imp::bottom_up_elim570 void operator()(expr * t, expr_ref & r) {
571 ptr_vector<expr> new_args;
572 SASSERT(m_frames.empty());
573 m_frames.push_back(frame(t, true));
574 while (!m_frames.empty()) {
575 m_owner.checkpoint();
576 frame & fr = m_frames.back();
577 expr * t = fr.first;
578 TRACE("cofactor_bug", tout << "processing: " << t->get_id() << " :first " << fr.second << "\n";);
579 if (!is_app(t)) {
580 m_cache.insert(t, t);
581 m_frames.pop_back();
582 continue;
583 }
584 if (m_cache.contains(t)) {
585 m_frames.pop_back();
586 continue;
587 }
588 if (fr.second) {
589 fr.second = false;
590 bool visited = true;
591 unsigned i = to_app(t)->get_num_args();
592 while (i > 0) {
593 --i;
594 expr * arg = to_app(t)->get_arg(i);
595 visit(arg, visited);
596 }
597 if (!visited)
598 continue;
599 }
600 new_args.reset();
601 bool has_new_args = false;
602 bool has_term_ite = false;
603 unsigned num = to_app(t)->get_num_args();
604 for (unsigned i = 0; i < num; i++) {
605 expr * arg = to_app(t)->get_arg(i);
606 expr * new_arg = nullptr;
607 TRACE("cofactor_bug", tout << "collecting child: " << arg->get_id() << "\n";);
608 m_cache.find(arg, new_arg);
609 SASSERT(new_arg != 0);
610 if (new_arg != arg)
611 has_new_args = true;
612 if (m_has_term_ite.contains(new_arg))
613 has_term_ite = true;
614 new_args.push_back(new_arg);
615 }
616 if (m.is_term_ite(t))
617 has_term_ite = true;
618 expr_ref new_t(m);
619 if (has_new_args)
620 new_t = m.mk_app(to_app(t)->get_decl(), num, new_args.data());
621 else
622 new_t = t;
623 if (has_term_ite && is_atom(new_t)) {
624 // update new_t
625 expr_ref new_new_t(m);
626 m_has_term_ite.insert(new_t);
627 cofactor(new_t, new_new_t);
628 m_has_term_ite.erase(new_t);
629 new_t = new_new_t;
630 has_term_ite = false;
631 }
632 if (has_term_ite)
633 m_has_term_ite.insert(new_t);
634 SASSERT(new_t.get() != 0);
635 TRACE("cofactor_bug", tout << "caching: " << t->get_id() << "\n";);
636 #if 0
637 counter ++;
638 verbose_stream() << counter << "\n";
639 #endif
640 m_cache.insert(t, new_t);
641 m_cache_domain.push_back(new_t);
642 m_frames.pop_back();
643 }
644 expr * result = nullptr;
645 m_cache.find(t, result);
646 r = result;
647 }
648 };
649
impcofactor_elim_term_ite::imp650 imp(ast_manager & _m, params_ref const & p):
651 m(_m),
652 m_params(p),
653 m_cofactor_equalities(true) {
654 updt_params(p);
655 }
656
operator ()cofactor_elim_term_ite::imp657 void operator()(expr * t, expr_ref & r) {
658 #if 0
659 analyzer proc(m, *this);
660 proc(t);
661 main_rw rw(m, *this, proc.m_candidates);
662 rw(t, r);
663 #else
664 bottom_up_elim proc(m, *this);
665 proc(t, r);
666 #endif
667 }
668 };
669
670
cofactor_elim_term_ite(ast_manager & m,params_ref const & p)671 cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const & p):
672 m_imp(alloc(imp, m, p)),
673 m_params(p) {
674 }
675
~cofactor_elim_term_ite()676 cofactor_elim_term_ite::~cofactor_elim_term_ite() {
677 dealloc(m_imp);
678 }
679
updt_params(params_ref const & p)680 void cofactor_elim_term_ite::updt_params(params_ref const & p) {
681 m_imp->updt_params(p);
682 }
683
collect_param_descrs(param_descrs & r)684 void cofactor_elim_term_ite::collect_param_descrs(param_descrs & r) {
685 m_imp->collect_param_descrs(r);
686 }
687
operator ()(expr * t,expr_ref & r)688 void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
689 m_imp->operator()(t, r);
690 }
691
692
cleanup()693 void cofactor_elim_term_ite::cleanup() {
694 ast_manager & m = m_imp->m;
695 imp * d = alloc(imp, m, m_params);
696 std::swap(d, m_imp);
697 dealloc(d);
698 }
699
700