1 /** 2 Copyright (c) 2017 Arie Gurfinkel 3 4 Module Name: 5 6 spacer_iuc_solver.h 7 8 Abstract: 9 10 A solver that produces interpolated unsat cores 11 12 Author: 13 14 Arie Gurfinkel 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include"solver/solver.h" 22 #include"ast/expr_substitution.h" 23 #include"util/stopwatch.h" 24 namespace spacer { 25 class iuc_solver : public solver { 26 private: 27 struct def_manager { 28 iuc_solver & m_parent; 29 expr_ref_vector m_defs; 30 obj_map<expr, app*> m_expr2proxy; 31 obj_map<app, app*> m_proxy2def; 32 def_managerdef_manager33 def_manager(iuc_solver &parent) : 34 m_parent(parent), m_defs(m_parent.m) 35 {} 36 37 bool is_proxy(app *k, app_ref &v); 38 app* mk_proxy(expr *v); 39 void reset(); 40 bool is_proxy_def(expr *v); 41 42 }; 43 44 friend struct def_manager; 45 ast_manager& m; 46 solver& m_solver; 47 app_ref_vector m_proxies; 48 unsigned m_num_proxies; 49 vector<def_manager> m_defs; 50 def_manager m_base_defs; 51 expr_ref_vector m_assumptions; 52 unsigned m_first_assumption; 53 bool m_is_proxied; 54 55 stopwatch m_iuc_sw; 56 stopwatch m_hyp_reduce1_sw; 57 stopwatch m_hyp_reduce2_sw; 58 stopwatch m_learn_core_sw; 59 60 expr_substitution m_elim_proxies_sub; 61 bool m_split_literals; 62 unsigned m_iuc; 63 unsigned m_iuc_arith; 64 bool m_print_farkas_stats; 65 bool m_old_hyp_reducer; 66 bool is_proxy(expr *e, app_ref &def); 67 void undo_proxies_in_core(expr_ref_vector &v); 68 app* mk_proxy(expr *v); 69 app* fresh_proxy(); 70 void elim_proxies(expr_ref_vector &v); 71 public: 72 iuc_solver(solver &solver, unsigned iuc, unsigned iuc_arith, 73 bool print_farkas_stats, bool old_hyp_reducer, 74 bool split_literals = false) : 75 m(solver.get_manager()), 76 m_solver(solver), 77 m_proxies(m), 78 m_num_proxies(0), 79 m_base_defs(*this), 80 m_assumptions(m), 81 m_first_assumption(0), 82 m_is_proxied(false), 83 m_elim_proxies_sub(m, false, true), 84 m_split_literals(split_literals), 85 m_iuc(iuc), 86 m_iuc_arith(iuc_arith), 87 m_print_farkas_stats(print_farkas_stats), 88 m_old_hyp_reducer(old_hyp_reducer) 89 {} 90 ~iuc_solver()91 ~iuc_solver() override {} 92 93 /* iuc solver specific */ 94 virtual void get_iuc(expr_ref_vector &core); set_split_literals(bool v)95 void set_split_literals(bool v) { m_split_literals = v; } 96 bool mk_proxies(expr_ref_vector &v, unsigned from = 0); 97 void undo_proxies(expr_ref_vector &v); 98 99 void push_bg(expr *e); 100 void pop_bg(unsigned n); 101 unsigned get_num_bg(); 102 get_full_unsat_core(ptr_vector<expr> & core)103 void get_full_unsat_core(ptr_vector<expr> &core) { 104 expr_ref_vector _core(m); 105 m_solver.get_unsat_core(_core); 106 core.append(_core.size(), _core.data()); 107 } 108 109 /* solver interface */ 110 translate(ast_manager & m,params_ref const & p)111 solver* translate(ast_manager &m, params_ref const &p) override { 112 return m_solver.translate(m, p); 113 } updt_params(params_ref const & p)114 void updt_params(params_ref const &p) override { m_solver.updt_params(p); } reset_params(params_ref const & p)115 void reset_params(params_ref const &p) override { m_solver.reset_params(p); } get_params()116 const params_ref &get_params() const override { return m_solver.get_params(); } push_params()117 void push_params() override { m_solver.push_params(); } pop_params()118 void pop_params() override { m_solver.pop_params(); } collect_param_descrs(param_descrs & r)119 void collect_param_descrs(param_descrs &r) override { m_solver.collect_param_descrs(r); } set_produce_models(bool f)120 void set_produce_models(bool f) override { m_solver.set_produce_models(f); } assert_expr_core(expr * t)121 void assert_expr_core(expr *t) override { m_solver.assert_expr(t); } assert_expr_core2(expr * t,expr * a)122 void assert_expr_core2(expr *t, expr *a) override { NOT_IMPLEMENTED_YET(); } set_phase(expr * e)123 void set_phase(expr* e) override { m_solver.set_phase(e); } get_phase()124 phase* get_phase() override { return m_solver.get_phase(); } set_phase(phase * p)125 void set_phase(phase* p) override { m_solver.set_phase(p); } move_to_front(expr * e)126 void move_to_front(expr* e) override { m_solver.move_to_front(e); } cube(expr_ref_vector &,unsigned)127 expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } get_levels(ptr_vector<expr> const & vars,unsigned_vector & depth)128 void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); } get_trail()129 expr_ref_vector get_trail() override { return m_solver.get_trail(); } 130 131 void push() override; 132 void pop(unsigned n) override; get_scope_level()133 unsigned get_scope_level() const override { return m_solver.get_scope_level(); } 134 135 lbool check_sat_core(unsigned num_assumptions, expr * const *assumptions) override; 136 lbool check_sat_cc(const expr_ref_vector &cube, vector<expr_ref_vector> const & clauses) override; set_progress_callback(progress_callback * callback)137 void set_progress_callback(progress_callback *callback) override { 138 m_solver.set_progress_callback(callback); 139 } get_num_assertions()140 unsigned get_num_assertions() const override { return m_solver.get_num_assertions(); } get_assertion(unsigned idx)141 expr * get_assertion(unsigned idx) const override { return m_solver.get_assertion(idx); } get_num_assumptions()142 unsigned get_num_assumptions() const override { return m_solver.get_num_assumptions(); } get_assumption(unsigned idx)143 expr * get_assumption(unsigned idx) const override { return m_solver.get_assumption(idx); } display(std::ostream & out,unsigned n,expr * const * es)144 std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const override { 145 return m_solver.display(out, n, es); 146 } 147 148 /* check_sat_result interface */ 149 150 void collect_statistics(statistics &st) const override ; 151 virtual void reset_statistics(); 152 153 void get_unsat_core(expr_ref_vector &r) override; get_model_core(model_ref & m)154 void get_model_core(model_ref &m) override {m_solver.get_model(m);} get_proof()155 proof *get_proof() override {return m_solver.get_proof();} reason_unknown()156 std::string reason_unknown() const override { return m_solver.reason_unknown(); } set_reason_unknown(char const * msg)157 void set_reason_unknown(char const* msg) override { m_solver.set_reason_unknown(msg); } get_labels(svector<symbol> & r)158 void get_labels(svector<symbol> &r) override { m_solver.get_labels(r); } get_manager()159 ast_manager& get_manager() const override { return m; } 160 161 virtual void refresh(); 162 163 class scoped_mk_proxy { 164 iuc_solver &m_s; 165 expr_ref_vector &m_v; 166 public: scoped_mk_proxy(iuc_solver & s,expr_ref_vector & v)167 scoped_mk_proxy(iuc_solver &s, expr_ref_vector &v) : m_s(s), m_v(v) { 168 m_s.mk_proxies(m_v); 169 } ~scoped_mk_proxy()170 ~scoped_mk_proxy() { m_s.undo_proxies(m_v); } 171 }; 172 173 class scoped_bg { 174 iuc_solver &m_s; 175 unsigned m_bg_sz; 176 public: scoped_bg(iuc_solver & s)177 scoped_bg(iuc_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {} ~scoped_bg()178 ~scoped_bg() { 179 if (m_s.get_num_bg() > m_bg_sz) { 180 m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); 181 } 182 } 183 }; 184 }; 185 } 186