1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 qfufbv_tactic.cpp 7 8 Abstract: 9 10 Tactic for QF_UFBV 11 12 Author: 13 14 Leonardo (leonardo) 2012-02-27 15 Mikolas Janota 16 17 Notes: 18 19 --*/ 20 #include "tactic/tactical.h" 21 #include "tactic/core/simplify_tactic.h" 22 #include "tactic/core/propagate_values_tactic.h" 23 #include "tactic/core/solve_eqs_tactic.h" 24 #include "tactic/core/elim_uncnstr_tactic.h" 25 #include "smt/tactic/smt_tactic.h" 26 #include "tactic/bv/max_bv_sharing_tactic.h" 27 #include "tactic/bv/bv_size_reduction_tactic.h" 28 #include "tactic/core/reduce_args_tactic.h" 29 #include "tactic/smtlogics/qfbv_tactic.h" 30 #include "tactic/smtlogics/qfufbv_tactic_params.hpp" 31 /////////////// 32 #include "model/model_smt2_pp.h" 33 #include "ackermannization/lackr.h" 34 #include "ackermannization/ackermannization_params.hpp" 35 #include "tactic/smtlogics/qfufbv_ackr_model_converter.h" 36 /////////////// 37 #include "sat/sat_solver/inc_sat_solver.h" 38 #include "tactic/smtlogics/qfaufbv_tactic.h" 39 #include "tactic/smtlogics/qfbv_tactic.h" 40 #include "tactic/smtlogics/smt_tactic_select.h" 41 #include "solver/tactic2solver.h" 42 #include "tactic/bv/bv_bound_chk_tactic.h" 43 #include "ackermannization/ackermannize_bv_tactic.h" 44 /////////////// 45 46 class qfufbv_ackr_tactic : public tactic { 47 public: 48 qfufbv_ackr_tactic(ast_manager& m, params_ref const& p) 49 : m_m(m) 50 , m_p(p) 51 , m_use_sat(false) 52 , m_inc_use_sat(false) 53 {} 54 55 ~qfufbv_ackr_tactic() override { } 56 57 void operator()(goal_ref const & g, goal_ref_buffer & result) override { 58 ast_manager& m(g->m()); 59 tactic_report report("qfufbv_ackr", *g); 60 fail_if_unsat_core_generation("qfufbv_ackr", g); 61 fail_if_proof_generation("qfufbv_ackr", g); 62 63 TRACE("goal", g->display(tout);); 64 // running implementation 65 ptr_vector<expr> flas; 66 const unsigned sz = g->size(); 67 for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); 68 scoped_ptr<solver> uffree_solver = setup_sat(); 69 lackr imp(m, m_p, m_st, flas, uffree_solver.get()); 70 const lbool o = imp.operator()(); 71 flas.reset(); 72 // report result 73 goal_ref resg(alloc(goal, *g, true)); 74 if (o == l_false) 75 resg->assert_expr(m.mk_false()); 76 if (o == l_undef) { 77 g->inc_depth(); 78 result.push_back(g.get()); 79 } 80 else { 81 result.push_back(resg.get()); 82 } 83 // report model 84 if (g->models_enabled() && o == l_true) { 85 model_ref abstr_model = imp.get_model(); 86 resg->add(mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model)); 87 } 88 } 89 90 void updt_params(params_ref const & _p) override { 91 qfufbv_tactic_params p(_p); 92 m_use_sat = p.sat_backend(); 93 m_inc_use_sat = p.inc_sat_backend(); 94 } 95 96 void collect_statistics(statistics & st) const override { 97 ackermannization_params p(m_p); 98 if (!p.eager()) st.update("lackr-its", m_st.m_it); 99 st.update("ackr-constraints", m_st.m_ackrs_sz); 100 } 101 102 void reset_statistics() override { m_st.reset(); } 103 104 void cleanup() override { } 105 106 tactic* translate(ast_manager& m) override { 107 return alloc(qfufbv_ackr_tactic, m, m_p); 108 } 109 private: 110 ast_manager& m_m; 111 params_ref m_p; 112 lackr_stats m_st; 113 bool m_use_sat; 114 bool m_inc_use_sat; 115 116 solver* setup_sat() { 117 solver * sat = nullptr; 118 if (m_use_sat) { 119 if (m_inc_use_sat) { 120 sat = mk_inc_sat_solver(m_m, m_p); 121 } 122 else { 123 tactic_ref t = mk_qfbv_tactic(m_m, m_p); 124 sat = mk_tactic2solver(m_m, t.get(), m_p); 125 } 126 } 127 else { 128 tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); 129 sat = mk_tactic2solver(m_m, t.get(), m_p); 130 } 131 SASSERT(sat != nullptr); 132 sat->set_produce_models(true); 133 return sat; 134 } 135 136 137 }; 138 139 static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { 140 params_ref simp2_p = p; 141 simp2_p.set_bool("pull_cheap_ite", true); 142 simp2_p.set_bool("push_ite_bv", false); 143 simp2_p.set_bool("local_ctx", true); 144 simp2_p.set_uint("local_ctx_limit", 10000000); 145 146 simp2_p.set_bool("ite_extra_rules", true); 147 simp2_p.set_bool("mul2concat", true); 148 149 params_ref ctx_simp_p; 150 ctx_simp_p.set_uint("max_depth", 32); 151 ctx_simp_p.set_uint("max_steps", 5000000); 152 153 return and_then( 154 mk_simplify_tactic(m), 155 mk_propagate_values_tactic(m), 156 if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))), 157 //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p), 158 mk_solve_eqs_tactic(m), 159 mk_elim_uncnstr_tactic(m), 160 if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), 161 mk_max_bv_sharing_tactic(m), 162 using_params(mk_simplify_tactic(m), simp2_p) 163 ); 164 } 165 166 static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { 167 return and_then(mk_simplify_tactic(m), 168 mk_propagate_values_tactic(m), 169 mk_solve_eqs_tactic(m), 170 mk_elim_uncnstr_tactic(m), 171 if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), 172 if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), 173 mk_max_bv_sharing_tactic(m), 174 if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) 175 ); 176 } 177 178 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { 179 params_ref main_p; 180 main_p.set_bool("elim_and", true); 181 main_p.set_bool("blast_distinct", true); 182 183 tactic * const preamble_st = mk_qfufbv_preamble(m, p); 184 185 tactic * st = using_params( 186 and_then(preamble_st, 187 cond(mk_is_qfbv_probe(), 188 mk_qfbv_tactic(m), 189 mk_smt_tactic_select(m, p))), 190 main_p); 191 192 st->updt_params(p); 193 return st; 194 } 195 196 tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { 197 tactic * const preamble_t = mk_qfufbv_preamble1(m, p); 198 199 tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p); 200 return and_then(preamble_t, 201 cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic_select(m, p))); 202 } 203