setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. F…

…ixing conservative setting to be after constructor in asserted_formulas. fixes #4586

Signed-off-by: Nikolaj Bjorner <[email protected]>

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;
 }
 

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> {
     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<push_app_ite_cfg>(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> {
     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<ng_push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg),
-        m_cfg(m, conservative)
+        m_cfg(m)
     {}
+    void set_conservative(bool c) { m_cfg.set_conservative(c); }
 };
 
 

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;

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;

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;