From e86a918ae7f6f54a9865b40caaba1b594a6d6892 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Mar 2025 11:30:08 -0700 Subject: [PATCH] turn on ite simplification by default --- src/ast/rewriter/bool_rewriter.cpp | 9 +++------ src/ast/rewriter/bool_rewriter.h | 1 - src/params/bool_rewriter_params.pyg | 1 - 3 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 4dc0f3549..c90777c30 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -34,7 +34,6 @@ void bool_rewriter::updt_params(params_ref const & _p) { m_blast_distinct = p.blast_distinct(); m_blast_distinct_threshold = p.blast_distinct_threshold(); m_ite_extra_rules = p.ite_extra_rules(); - m_elim_ite_value_tree = p.elim_ite_value_tree(); } void bool_rewriter::get_param_descrs(param_descrs & r) { @@ -681,11 +680,9 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) return BR_REWRITE2; } - if (m_elim_ite_value_tree) { - result = simplify_eq_ite(val, ite); - if (result) - return BR_REWRITE_FULL; - } + result = simplify_eq_ite(val, ite); + if (result) + return BR_REWRITE_FULL; return BR_FAILED; } diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 9a7d3b357..12eaff20a 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -61,7 +61,6 @@ class bool_rewriter { unsigned m_local_ctx_limit; unsigned m_local_ctx_cost; bool m_elim_ite; - bool m_elim_ite_value_tree; ptr_vector m_todo1, m_todo2; unsigned_vector m_counts1, m_counts2; expr_fast_mark1 m_marked; diff --git a/src/params/bool_rewriter_params.pyg b/src/params/bool_rewriter_params.pyg index e10e08d46..87578470e 100644 --- a/src/params/bool_rewriter_params.pyg +++ b/src/params/bool_rewriter_params.pyg @@ -7,7 +7,6 @@ def_module_params(module_name='rewriter', ("sort_disjunctions", BOOL, True, "sort subterms in disjunctions"), ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), ('elim_ite', BOOL, True, "eliminate ite in favor of and/or"), - ('elim_ite_value_tree', BOOL, False, "eliminate equations 'v = ite(...)' where v is a value and each leaf in the ite tree is a value"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"), ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"),