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