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