1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 user_solver.cpp 7 8 Abstract: 9 10 User propagator plugin. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2020-09-23 15 16 --*/ 17 18 #include "sat/smt/user_solver.h" 19 #include "sat/smt/euf_solver.h" 20 21 namespace user_solver { 22 solver(euf::solver & ctx)23 solver::solver(euf::solver& ctx) : 24 th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user")) 25 {} 26 ~solver()27 solver::~solver() { 28 dealloc(m_api_context); 29 } 30 add_expr(expr * e)31 unsigned solver::add_expr(expr* e) { 32 force_push(); 33 ctx.internalize(e, false); 34 euf::enode* n = expr2enode(e); 35 if (is_attached_to_var(n)) 36 return n->get_th_var(get_id()); 37 euf::theory_var v = mk_var(n); 38 ctx.attach_th_var(n, this, v); 39 return v; 40 } 41 propagate_cb(unsigned num_fixed,unsigned const * fixed_ids,unsigned num_eqs,unsigned const * eq_lhs,unsigned const * eq_rhs,expr * conseq)42 void solver::propagate_cb( 43 unsigned num_fixed, unsigned const* fixed_ids, 44 unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, 45 expr* conseq) { 46 m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); 47 DEBUG_CODE(validate_propagation();); 48 } 49 check()50 sat::check_result solver::check() { 51 if (!(bool)m_final_eh) 52 return sat::check_result::CR_DONE; 53 unsigned sz = m_prop.size(); 54 m_final_eh(m_user_context, this); 55 return sz == m_prop.size() ? sat::check_result::CR_DONE : sat::check_result::CR_CONTINUE; 56 } 57 new_fixed_eh(euf::theory_var v,expr * value,unsigned num_lits,sat::literal const * jlits)58 void solver::new_fixed_eh(euf::theory_var v, expr* value, unsigned num_lits, sat::literal const* jlits) { 59 if (!m_fixed_eh) 60 return; 61 force_push(); 62 m_id2justification.setx(v, sat::literal_vector(num_lits, jlits), sat::literal_vector()); 63 m_fixed_eh(m_user_context, this, v, value); 64 } 65 asserted(sat::literal lit)66 void solver::asserted(sat::literal lit) { 67 if (!m_fixed_eh) 68 return; 69 force_push(); 70 auto* n = bool_var2enode(lit.var()); 71 euf::theory_var v = n->get_th_var(get_id()); 72 sat::literal_vector lits; 73 lits.push_back(lit); 74 m_id2justification.setx(v, lits, sat::literal_vector()); 75 m_fixed_eh(m_user_context, this, v, lit.sign() ? m.mk_false() : m.mk_true()); 76 } 77 push_core()78 void solver::push_core() { 79 th_euf_solver::push_core(); 80 m_prop_lim.push_back(m_prop.size()); 81 m_push_eh(m_user_context); 82 } 83 pop_core(unsigned num_scopes)84 void solver::pop_core(unsigned num_scopes) { 85 th_euf_solver::pop_core(num_scopes); 86 unsigned old_sz = m_prop_lim.size() - num_scopes; 87 m_prop.shrink(m_prop_lim[old_sz]); 88 m_prop_lim.shrink(old_sz); 89 m_pop_eh(m_user_context, num_scopes); 90 } 91 unit_propagate()92 bool solver::unit_propagate() { 93 if (m_qhead == m_prop.size()) 94 return false; 95 force_push(); 96 ctx.push(value_trail<unsigned>(m_qhead)); 97 unsigned np = m_stats.m_num_propagations; 98 for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) { 99 auto const& prop = m_prop[m_qhead]; 100 sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true); 101 if (s().value(lit) != l_true) { 102 s().assign(lit, mk_justification(m_qhead)); 103 ++m_stats.m_num_propagations; 104 } 105 } 106 return np < m_stats.m_num_propagations; 107 } 108 collect_statistics(::statistics & st) const109 void solver::collect_statistics(::statistics& st) const { 110 st.update("user-propagations", m_stats.m_num_propagations); 111 st.update("user-watched", get_num_vars()); 112 } 113 mk_justification(unsigned prop_idx)114 sat::justification solver::mk_justification(unsigned prop_idx) { 115 void* mem = get_region().allocate(justification::get_obj_size()); 116 sat::constraint_base::initialize(mem, this); 117 auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(prop_idx); 118 return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index()); 119 } 120 get_antecedents(sat::literal l,sat::ext_justification_idx idx,sat::literal_vector & r,bool probing)121 void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) { 122 auto& j = justification::from_index(idx); 123 auto const& prop = m_prop[j.m_propagation_index]; 124 for (unsigned id : prop.m_ids) 125 r.append(m_id2justification[id]); 126 for (auto const& p : prop.m_eqs) 127 ctx.add_antecedent(var2enode(p.first), var2enode(p.second)); 128 } 129 130 /* 131 * All assumptions and equalities have to be true in the current scope. 132 * A caller could mistakingly supply some assumption that isn't set. 133 */ validate_propagation()134 void solver::validate_propagation() { 135 auto const& prop = m_prop.back(); 136 for (unsigned id : prop.m_ids) 137 for (auto lit: m_id2justification[id]) 138 VERIFY(s().value(lit) == l_true); 139 for (auto const& p : prop.m_eqs) 140 VERIFY(var2enode(p.first)->get_root() == var2enode(p.second)->get_root()); 141 } 142 display(std::ostream & out) const143 std::ostream& solver::display(std::ostream& out) const { 144 for (unsigned i = 0; i < get_num_vars(); ++i) 145 out << i << ": " << mk_pp(var2expr(i), m) << "\n"; 146 return out; 147 } 148 display_justification(std::ostream & out,sat::ext_justification_idx idx) const149 std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { 150 auto& j = justification::from_index(idx); 151 auto const& prop = m_prop[j.m_propagation_index]; 152 for (unsigned id : prop.m_ids) 153 out << id << ": " << m_id2justification[id]; 154 for (auto const& p : prop.m_eqs) 155 out << "v" << p.first << " == v" << p.second << " "; 156 return out; 157 } 158 display_constraint(std::ostream & out,sat::ext_constraint_idx idx) const159 std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { 160 return display_justification(out, idx); 161 } 162 clone(euf::solver & dst_ctx)163 euf::th_solver* solver::clone(euf::solver& dst_ctx) { 164 auto* result = alloc(solver, dst_ctx); 165 for (unsigned i = 0; i < get_num_vars(); ++i) 166 result->add_expr(ctx.copy(dst_ctx, var2enode(i))->get_expr()); 167 return result; 168 } 169 170 } 171 172