1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     sat_th.cpp
7 
8 Abstract:
9 
10     Theory plugin base classes
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2020-08-25
15 
16 --*/
17 
18 #include "sat/smt/sat_th.h"
19 #include "sat/smt/euf_solver.h"
20 #include "tactic/tactic_exception.h"
21 
22 namespace euf {
23 
visit_rec(ast_manager & m,expr * a,bool sign,bool root,bool redundant)24     bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) {
25         IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n");
26         flet<bool> _is_learned(m_is_redundant, redundant);
27         svector<sat::eframe>::scoped_stack _sc(m_stack);
28         unsigned sz = m_stack.size();
29         visit(a);
30         while (m_stack.size() > sz) {
31         loop:
32             if (!m.inc())
33                 throw tactic_exception(m.limit().get_cancel_msg());
34             unsigned fsz = m_stack.size();
35             expr* e = m_stack[fsz-1].m_e;
36             if (visited(e)) {
37                 m_stack.pop_back();
38                 continue;
39             }
40             unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
41 
42             while (m_stack[fsz - 1].m_idx < num) {
43                 expr* arg = to_app(e)->get_arg(m_stack[fsz - 1].m_idx);
44                 m_stack[fsz - 1].m_idx++;
45                 if (!visit(arg))
46                     goto loop;
47             }
48             if (!post_visit(e, sign, root && a == e))
49                 return false;
50             m_stack.pop_back();
51         }
52         return true;
53     }
54 
th_euf_solver(euf::solver & ctx,symbol const & name,euf::theory_id id)55     th_euf_solver::th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id):
56         th_solver(ctx.get_manager(), name, id),
57         ctx(ctx)
58     {}
59 
get_config() const60     smt_params const& th_euf_solver::get_config() const {
61         return ctx.get_config();
62     }
63 
get_region()64     region& th_euf_solver::get_region() {
65         return ctx.get_region();
66     }
67 
get_trail_stack()68     trail_stack<euf::solver>& th_euf_solver::get_trail_stack() {
69         return ctx.get_trail_stack();
70     }
71 
expr2enode(expr * e) const72     enode* th_euf_solver::expr2enode(expr* e) const {
73         return ctx.get_enode(e);
74     }
75 
expr2literal(expr * e) const76     sat::literal th_euf_solver::expr2literal(expr* e) const {
77         return ctx.expr2literal(e);
78     }
79 
bool_var2expr(sat::bool_var v) const80     expr* th_euf_solver::bool_var2expr(sat::bool_var v) const {
81         return ctx.bool_var2expr(v);
82     }
83 
literal2expr(sat::literal lit) const84     expr_ref th_euf_solver::literal2expr(sat::literal lit) const {
85         return ctx.literal2expr(lit);
86     }
87 
mk_var(enode * n)88     theory_var th_euf_solver::mk_var(enode * n) {
89         force_push();
90         SASSERT(!is_attached_to_var(n));
91         euf::theory_var v = m_var2enode.size();
92         m_var2enode.push_back(n);
93         return v;
94     }
95 
is_attached_to_var(enode * n) const96     bool th_euf_solver::is_attached_to_var(enode* n) const {
97         theory_var v = n->get_th_var(get_id());
98         return v != null_theory_var && var2enode(v) == n;
99     }
100 
get_th_var(expr * e) const101     theory_var th_euf_solver::get_th_var(expr* e) const {
102         return get_th_var(ctx.get_enode(e));
103     }
104 
push_core()105     void th_euf_solver::push_core() {
106         m_var2enode_lim.push_back(m_var2enode.size());
107     }
108 
pop_core(unsigned num_scopes)109     void th_euf_solver::pop_core(unsigned num_scopes) {
110         unsigned new_lvl = m_var2enode_lim.size() - num_scopes;
111         m_var2enode.shrink(m_var2enode_lim[new_lvl]);
112         m_var2enode_lim.shrink(new_lvl);
113     }
114 
pop(unsigned n)115     void th_euf_solver::pop(unsigned n) {
116         unsigned k = std::min(m_num_scopes, n);
117         m_num_scopes -= k;
118         n -= k;
119         if (n > 0)
120             pop_core(n);
121     }
122 
mk_status()123     sat::status th_euf_solver::mk_status() {
124         return sat::status::th(m_is_redundant, get_id());
125     }
126 
add_unit(sat::literal lit)127     bool th_euf_solver::add_unit(sat::literal lit) {
128         bool was_true = is_true(lit);
129         ctx.s().add_clause(1, &lit, mk_status());
130         return !was_true;
131     }
132 
add_units(sat::literal_vector const & lits)133     bool th_euf_solver::add_units(sat::literal_vector const& lits) {
134         bool is_new = false;
135         for (auto lit : lits)
136             if (add_unit(lit))
137                 is_new = true;
138         return is_new;
139     }
140 
add_clause(sat::literal a,sat::literal b)141     bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {
142         bool was_true = is_true(a, b);
143         sat::literal lits[2] = { a, b };
144         ctx.s().add_clause(2, lits, mk_status());
145         return !was_true;
146     }
147 
add_clause(sat::literal a,sat::literal b,sat::literal c)148     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
149         bool was_true = is_true(a, b, c);
150         sat::literal lits[3] = { a, b, c };
151         ctx.s().add_clause(3, lits, mk_status());
152         return !was_true;
153     }
154 
add_clause(sat::literal a,sat::literal b,sat::literal c,sat::literal d)155     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
156         bool was_true = is_true(a, b, c, d);
157         sat::literal lits[4] = { a, b, c, d };
158         ctx.s().add_clause(4, lits, mk_status());
159         return !was_true;
160     }
161 
add_clause(sat::literal_vector const & lits)162     bool th_euf_solver::add_clause(sat::literal_vector const& lits) {
163         bool was_true = false;
164         for (auto lit : lits)
165             was_true |= is_true(lit);
166         s().add_clause(lits.size(), lits.c_ptr(), mk_status());
167         return !was_true;
168     }
169 
add_equiv(sat::literal a,sat::literal b)170     void th_euf_solver::add_equiv(sat::literal a, sat::literal b) {
171         add_clause(~a, b);
172         add_clause(a, ~b);
173     }
174 
add_equiv_and(sat::literal a,sat::literal_vector const & bs)175     void th_euf_solver::add_equiv_and(sat::literal a, sat::literal_vector const& bs) {
176         for (auto b : bs)
177             add_clause(~a, b);
178         sat::literal_vector _bs;
179         for (auto b : bs)
180             _bs.push_back(~b);
181         _bs.push_back(a);
182         add_clause(_bs);
183     }
184 
is_true(sat::literal lit)185     bool th_euf_solver::is_true(sat::literal lit) {
186         return ctx.s().value(lit) == l_true;
187     }
188 
mk_enode(expr * e,bool suppress_args)189     euf::enode* th_euf_solver::mk_enode(expr* e, bool suppress_args) {
190         m_args.reset();
191         if (!suppress_args)
192             for (expr* arg : *to_app(e))
193                 m_args.push_back(expr2enode(arg));
194         euf::enode* n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr());
195         ctx.attach_node(n);
196         return n;
197     }
198 
rewrite(expr_ref & a)199     void th_euf_solver::rewrite(expr_ref& a) {
200         ctx.get_rewriter()(a);
201     }
202 
mk_eq(expr * e1,expr * e2)203     expr_ref th_euf_solver::mk_eq(expr* e1, expr* e2) {
204         return ctx.mk_eq(e1, e2);
205     }
206 
mk_literal(expr * e) const207     sat::literal th_euf_solver::mk_literal(expr* e) const {
208         return ctx.mk_literal(e);
209     }
210 
eq_internalize(expr * a,expr * b)211     sat::literal th_euf_solver::eq_internalize(expr* a, expr* b) {
212         return mk_literal(ctx.mk_eq(a, b));
213     }
214 
e_internalize(expr * e)215     euf::enode* th_euf_solver::e_internalize(expr* e) {
216         euf::enode* n = expr2enode(e);
217         if (!n) {
218             ctx.internalize(e, m_is_redundant);
219             n = expr2enode(e);
220         }
221         return n;
222     }
223 
random()224     unsigned th_euf_solver::random() {
225         return ctx.s().rand()();
226     }
227 
get_obj_size(unsigned num_lits,unsigned num_eqs)228     size_t th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) {
229         return sat::constraint_base::obj_size(sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs);
230     }
231 
th_propagation(unsigned n_lits,sat::literal const * lits,unsigned n_eqs,enode_pair const * eqs)232     th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
233         m_num_literals = n_lits;
234         m_num_eqs = n_eqs;
235         m_literals = reinterpret_cast<literal*>(reinterpret_cast<char*>(this) + sizeof(th_propagation));
236         for (unsigned i = 0; i < n_lits; ++i)
237             m_literals[i] = lits[i];
238         m_eqs = reinterpret_cast<enode_pair*>(reinterpret_cast<char*>(this) + sizeof(th_propagation) + sizeof(literal) * n_lits);
239         for (unsigned i = 0; i < n_eqs; ++i)
240             m_eqs[i] = eqs[i];
241     }
242 
mk(th_euf_solver & th,sat::literal_vector const & lits,enode_pair_vector const & eqs)243     th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) {
244         return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr());
245     }
246 
mk(th_euf_solver & th,unsigned n_lits,sat::literal const * lits,unsigned n_eqs,enode_pair const * eqs)247     th_propagation* th_propagation::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
248         region& r = th.ctx.get_region();
249         void* mem = r.allocate(get_obj_size(n_lits, n_eqs));
250         sat::constraint_base::initialize(mem, &th);
251         return new (sat::constraint_base::ptr2mem(mem)) th_propagation(n_lits, lits, n_eqs, eqs);
252     }
253 
mk(th_euf_solver & th,enode_pair_vector const & eqs)254     th_propagation* th_propagation::mk(th_euf_solver& th, enode_pair_vector const& eqs) {
255         return mk(th, 0, nullptr, eqs.size(), eqs.c_ptr());
256     }
257 
mk(th_euf_solver & th,sat::literal lit)258     th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit) {
259         return mk(th, 1, &lit, 0, nullptr);
260     }
261 
mk(th_euf_solver & th,sat::literal lit,euf::enode * x,euf::enode * y)262     th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
263         enode_pair eq(x, y);
264         return mk(th, 1, &lit, 1, &eq);
265     }
266 
mk(th_euf_solver & th,euf::enode * x,euf::enode * y)267     th_propagation* th_propagation::mk(th_euf_solver& th, euf::enode* x, euf::enode* y) {
268         enode_pair eq(x, y);
269         return mk(th, 0, nullptr, 1, &eq);
270     }
271 
display(std::ostream & out) const272     std::ostream& th_propagation::display(std::ostream& out) const {
273         for (auto lit : euf::th_propagation::lits(*this))
274             out << lit << " ";
275         for (auto eq : euf::th_propagation::eqs(*this))
276             out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " ";
277         return out;
278     }
279 
280 
281 }
282