diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h index 2e3406e10e2..cc1744d4e9f 100644 --- a/src/ast/proofs/proof_utils.h +++ b/src/ast/proofs/proof_utils.h @@ -106,7 +106,7 @@ class elim_aux_assertions { { ast_manager &m = args.get_manager(); bool_rewriter brwr(m); - brwr.set_flat(false); + brwr.set_flat_and_or(false); if (m.is_or(decl)) { mk_or_core(args, res); } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index ca034337f94..39b6de67311 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -59,7 +59,7 @@ class bit_blaster : public bit_blaster_tpl { public: bit_blaster(ast_manager & m, bit_blaster_params const & params); bit_blaster_params const & get_params() const { return this->m_params; } - void set_flat(bool f) { m_rw.set_flat(f); } + void set_flat_and_or(bool f) { m_rw.set_flat_and_or(f); } }; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 13e6a3511c6..801ebf4b594 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -75,7 +75,7 @@ class blaster : public bit_blaster_tpl { bit_blaster_tpl(blaster_cfg(m_rewriter, m_util)), m_rewriter(m), m_util(m) { - m_rewriter.set_flat(false); + m_rewriter.set_flat_and_or(false); m_rewriter.set_elim_and(true); } diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index fb2b0795bb3..80495853ae1 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -24,7 +24,7 @@ Module Name: void bool_rewriter::updt_params(params_ref const & _p) { bool_rewriter_params p(_p); - m_flat = p.flat(); + m_flat_and_or = p.flat(); m_elim_and = p.elim_and(); m_elim_ite = p.elim_ite(); m_local_ctx = p.local_ctx(); @@ -555,7 +555,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ result = arg; \ return true; \ } \ - if (m_flat && m().is_or(arg)) { \ + if (m_flat_and_or && m().is_or(arg)) { \ unsigned sz = to_app(arg)->get_num_args(); \ for (unsigned j = 0; j < sz; j++) { \ expr * arg_arg = to_app(arg)->get_arg(j); \ diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 5820026b7de..a25a0f8a31e 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -50,7 +50,7 @@ Module Name: */ class bool_rewriter { ast_manager & m_manager; - bool m_flat; + bool m_flat_and_or; bool m_local_ctx; bool m_elim_and; bool m_blast_distinct; @@ -83,8 +83,8 @@ class bool_rewriter { family_id get_fid() const { return m().get_basic_family_id(); } bool is_eq(expr * t) const { return m().is_eq(t); } - bool flat() const { return m_flat; } - void set_flat(bool f) { m_flat = f; } + bool flat_and_or() const { return m_flat_and_or; } + void set_flat_and_or(bool f) { m_flat_and_or = f; } bool elim_and() const { return m_elim_and; } void set_elim_and(bool f) { m_elim_and = f; } void reset_local_ctx_cost() { m_local_ctx_cost = 0; } @@ -111,7 +111,7 @@ class bool_rewriter { mk_and_as_or(num_args, args, result); return BR_DONE; } - else if (m_flat) { + else if (m_flat_and_or) { return mk_flat_and_core(num_args, args, result); } else { @@ -119,7 +119,7 @@ class bool_rewriter { } } br_status mk_or_core(unsigned num_args, expr * const * args, expr_ref & result) { - return m_flat ? + return m_flat_and_or ? mk_flat_or_core(num_args, args, result) : mk_nflat_or_core(num_args, args, result); } @@ -234,7 +234,7 @@ class bool_rewriter { struct bool_rewriter_cfg : public default_rewriter_cfg { bool_rewriter m_r; - bool flat_assoc(func_decl * f) const { return m_r.flat() && (m_r.m().is_and(f) || m_r.m().is_or(f)); } + bool flat_assoc(func_decl * f) const { return m_r.flat_and_or() && (m_r.m().is_and(f) || m_r.m().is_or(f)); } bool rewrite_patterns() const { return false; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = nullptr; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 843345a46e0..0c2a09e78de 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -86,7 +86,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_dt(m), m_pinned(m) { bool flat = true; - m_b_rw.set_flat(flat); + m_b_rw.set_flat_and_or(flat); m_a_rw.set_flat(flat); m_bv_rw.set_flat(flat); m_bv_rw.set_mkbv2num(true); diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index f103f876aa7..a5a35878e3b 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -55,7 +55,7 @@ namespace bv { m_ackerman(*this), m_bb(m, get_config()), m_find(*this) { - m_bb.set_flat(false); + m_bb.set_flat_and_or(false); } bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) { diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 2d405895fbb..c418115a9e8 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -866,7 +866,7 @@ class pb2bv_tactic : public tactic { m_used_dependencies(m), m_rw(*this) { updt_params(p); - m_b_rw.set_flat(false); // no flattening otherwise will blowup the memory + m_b_rw.set_flat_and_or(false); // no flattening otherwise will blowup the memory m_b_rw.set_elim_and(true); } diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index c141aaa3bb3..eec05b604d3 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -116,7 +116,7 @@ class tseitin_cnf_tactic : public tactic { m_rw(_m), m_num_aux_vars(0) { updt_params(p); - m_rw.set_flat(false); + m_rw.set_flat_and_or(false); } void updt_params(params_ref const & p) {