From a6a041ec5db6b1566985bf3c72dd20b78092ae1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2020 13:43:54 -0700 Subject: [PATCH] setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/push_app_ite.cpp | 7 ++++--- src/ast/rewriter/push_app_ite.h | 15 +++++++++------ src/smt/asserted_formulas.cpp | 2 ++ src/smt/asserted_formulas.h | 6 +++--- src/smt/smt_setup.cpp | 11 +++-------- 5 files changed, 21 insertions(+), 20 deletions(-) diff --git a/src/ast/rewriter/push_app_ite.cpp b/src/ast/rewriter/push_app_ite.cpp index 411c61d8e..0282aa602 100644 --- a/src/ast/rewriter/push_app_ite.cpp +++ b/src/ast/rewriter/push_app_ite.cpp @@ -48,9 +48,10 @@ bool push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * con } } CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n"; - tout << decl->get_name(); - for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m); - tout << "\n";); + tout << "conservative " << m_conservative << "\n"; + tout << decl->get_name(); + for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m); + tout << "\n";); return found_ite; } diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h index ec4317abb..ae3af1222 100644 --- a/src/ast/rewriter/push_app_ite.h +++ b/src/ast/rewriter/push_app_ite.h @@ -32,7 +32,8 @@ struct push_app_ite_cfg : public default_rewriter_cfg { bool m_conservative; virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args); br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); - push_app_ite_cfg(ast_manager& m, bool conservative = true): m(m), m_conservative(conservative) {} + push_app_ite_cfg(ast_manager& m): m(m), m_conservative(true) {} + void set_conservative(bool c) { m_conservative = c; } bool rewrite_patterns() const { return false; } }; @@ -46,26 +47,28 @@ class ng_push_app_ite_cfg : public push_app_ite_cfg { protected: bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override; public: - ng_push_app_ite_cfg(ast_manager& m, bool conservative = true): push_app_ite_cfg(m, conservative) {} + ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {} virtual ~ng_push_app_ite_cfg() {} }; struct push_app_ite_rw : public rewriter_tpl { push_app_ite_cfg m_cfg; public: - push_app_ite_rw(ast_manager& m, bool conservative = true): + push_app_ite_rw(ast_manager& m): rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, conservative) + m_cfg(m) {} + void set_conservative(bool c) { m_cfg.set_conservative(c); } }; struct ng_push_app_ite_rw : public rewriter_tpl { ng_push_app_ite_cfg m_cfg; public: - ng_push_app_ite_rw(ast_manager& m, bool conservative = true): + ng_push_app_ite_rw(ast_manager& m): rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, conservative) + m_cfg(m) {} + void set_conservative(bool c) { m_cfg.set_conservative(c); } }; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 8da9c8fad..b1abbd341 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -260,6 +260,8 @@ void asserted_formulas::reduce() { if (!invoke(m_reduce_asserted_formulas)) return; if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_lift_ite)) return; + m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE); + m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE); if (!invoke(m_ng_lift_ite)) return; if (!invoke(m_elim_term_ite)) return; if (!invoke(m_refine_inj_axiom)) return; diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 2f72aba1d..2d8dec542 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -170,8 +170,8 @@ class asserted_formulas { #define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE) \ class NAME : public simplify_fmls { \ - FUNCTOR m_functor; \ public: \ + FUNCTOR m_functor; \ NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \ virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \ m_functor(j.get_fml(), n, p); \ @@ -186,8 +186,8 @@ class asserted_formulas { MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true); MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true); MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true); - MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true); - MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true); + MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true); + MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true); reduce_asserted_formulas_fn m_reduce_asserted_formulas; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 96e46dbbf..c477dbeca 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -521,10 +521,6 @@ namespace smt { m_params.m_relevancy_lvl = 2; m_params.m_arith_eq2ineq = true; m_params.m_eliminate_term_ite = true; - // if (st.m_num_exprs < 5000 && st.m_num_ite_terms < 50) { // safeguard to avoid high memory consumption - // TODO: implement analysis function to decide where lift ite is too expensive. - // m_params.m_lift_ite = LI_FULL; - // } } else { m_params.m_eliminate_term_ite = true; @@ -643,15 +639,13 @@ namespace smt { m_params.m_eliminate_bounds = true; m_params.m_qi_quick_checker = MC_UNSAT; m_params.m_qi_lazy_threshold = 20; - // m_params.m_qi_max_eager_multipatterns = 10; /// <<< HACK m_params.m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-) // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general) // It destroys the existing patterns. // m_params.m_macro_finder = true; - // - m_params.m_ng_lift_ite = LI_FULL; + m_params.m_ng_lift_ite = LI_CONSERVATIVE; TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); m_context.register_plugin(alloc(smt::theory_i_arith, m_context)); setup_arrays(); @@ -665,6 +659,7 @@ namespace smt { } void setup::setup_AUFLIRA(bool simple_array) { + TRACE("setup", tout << "AUFLIRA\n";); m_params.m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; m_params.m_phase_selection = PS_ALWAYS_FALSE; m_params.m_eliminate_bounds = true; @@ -674,7 +669,7 @@ namespace smt { m_params.m_qi_lazy_threshold = 20; // m_params.m_macro_finder = true; - m_params.m_ng_lift_ite = LI_FULL; + m_params.m_ng_lift_ite = LI_CONSERVATIVE; m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP m_params.m_array_lazy_ieq = true; m_params.m_array_lazy_ieq_delay = 4;