1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_justification.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-25. 15 16 Revision History: 17 18 --*/ 19 #include "smt/smt_context.h" 20 #include "smt/smt_conflict_resolution.h" 21 #include "ast/ast_pp.h" 22 #include "ast/ast_ll_pp.h" 23 #include <memory> 24 25 namespace smt { 26 27 justification_proof_wrapper(context & ctx,proof * pr,bool in_region)28 justification_proof_wrapper::justification_proof_wrapper(context & ctx, proof * pr, bool in_region): 29 justification(in_region), 30 m_proof(pr) { 31 ctx.get_manager().inc_ref(pr); 32 } 33 del_eh(ast_manager & m)34 void justification_proof_wrapper::del_eh(ast_manager & m) { 35 m.dec_ref(m_proof); 36 m_proof = nullptr; 37 } 38 mk_proof(conflict_resolution & cr)39 proof * justification_proof_wrapper::mk_proof(conflict_resolution & cr) { 40 return m_proof; 41 } 42 unit_resolution_justification(region & r,justification * js,unsigned num_lits,literal const * lits)43 unit_resolution_justification::unit_resolution_justification(region & r, 44 justification * js, 45 unsigned num_lits, 46 literal const * lits): 47 m_antecedent(js), 48 m_num_literals(num_lits) { 49 SASSERT(!js || js->in_region()); 50 m_literals = new (r) literal[num_lits]; 51 memcpy(m_literals, lits, sizeof(literal) * num_lits); 52 TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";); 53 SASSERT(m_num_literals > 0); 54 } 55 unit_resolution_justification(justification * js,unsigned num_lits,literal const * lits)56 unit_resolution_justification::unit_resolution_justification(justification * js, 57 unsigned num_lits, 58 literal const * lits): 59 justification(false), // object is not allocated in a region 60 m_antecedent(js), 61 m_num_literals(num_lits) { 62 SASSERT(!js || !js->in_region()); 63 m_literals = alloc_vect<literal>(num_lits); 64 memcpy(m_literals, lits, sizeof(literal) * num_lits); 65 TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";); 66 SASSERT(num_lits != 0); 67 } 68 ~unit_resolution_justification()69 unit_resolution_justification::~unit_resolution_justification() { 70 if (!in_region()) { 71 dealloc_svect(m_literals); // I don't need to invoke destructor... 72 dealloc(m_antecedent); 73 } 74 } 75 get_antecedents(conflict_resolution & cr)76 void unit_resolution_justification::get_antecedents(conflict_resolution & cr) { 77 if (m_antecedent) 78 cr.mark_justification(m_antecedent); 79 for (unsigned i = 0; i < m_num_literals; i++) 80 cr.mark_literal(m_literals[i]); 81 } 82 mk_proof(conflict_resolution & cr)83 proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) { 84 SASSERT(m_antecedent); 85 ast_manager& m = cr.get_manager(); 86 proof_ref_vector prs(m); 87 proof * pr = cr.get_proof(m_antecedent); 88 if (!pr) 89 return pr; 90 prs.push_back(pr); 91 for (unsigned i = 0; i < m_num_literals; i++) { 92 proof * pr = cr.get_proof(m_literals[i]); 93 if (!pr) 94 return pr; 95 else 96 prs.push_back(pr); 97 } 98 TRACE("unit_resolution_justification_bug", 99 tout << "in mk_proof\n" << literal_vector(m_num_literals, m_literals) << "\n"; 100 for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m);); 101 return m.mk_unit_resolution(prs.size(), prs.c_ptr()); 102 } 103 get_antecedents(conflict_resolution & cr)104 void eq_conflict_justification::get_antecedents(conflict_resolution & cr) { 105 SASSERT(m_node1->get_root()->is_interpreted()); 106 SASSERT(m_node2->get_root()->is_interpreted()); 107 cr.mark_eq(m_node1, m_node1->get_root()); 108 cr.mark_eq(m_node2, m_node2->get_root()); 109 cr.mark_justified_eq(m_node1, m_node2, m_js); 110 } 111 mk_proof(conflict_resolution & cr)112 proof * eq_conflict_justification::mk_proof(conflict_resolution & cr) { 113 ast_manager & m = cr.get_manager(); 114 bool visited = true; 115 ptr_buffer<proof> prs; 116 117 if (m_node1 != m_node1->get_root()) { 118 proof * pr = cr.get_proof(m_node1, m_node1->get_root()); 119 if (pr && m.proofs_enabled()) 120 pr = m.mk_symmetry(pr); 121 prs.push_back(pr); 122 if (!pr) 123 visited = false; 124 } 125 126 SASSERT(m_node1 != m_node2); 127 proof * pr = cr.get_proof(m_node1, m_node2, m_js); 128 prs.push_back(pr); 129 if (!pr) 130 visited = false; 131 132 if (m_node2 != m_node2->get_root()) { 133 proof * pr = cr.get_proof(m_node2, m_node2->get_root()); 134 prs.push_back(pr); 135 if (!pr) 136 visited = false; 137 } 138 139 if (!visited) 140 return nullptr; 141 142 expr * lhs = m_node1->get_root()->get_owner(); 143 expr * rhs = m_node2->get_root()->get_owner(); 144 proof * pr1 = m.mk_transitivity(prs.size(), prs.c_ptr(), lhs, rhs); 145 proof * pr2 = m.mk_rewrite(m.mk_eq(lhs, rhs), m.mk_false()); 146 return m.mk_modus_ponens(pr1, pr2); 147 } 148 get_antecedents(conflict_resolution & cr)149 void eq_root_propagation_justification::get_antecedents(conflict_resolution & cr) { 150 cr.mark_eq(m_node, m_node->get_root()); 151 } 152 mk_proof(conflict_resolution & cr)153 proof * eq_root_propagation_justification::mk_proof(conflict_resolution & cr) { 154 ast_manager & m = cr.get_manager(); 155 expr * var = m_node->get_owner(); 156 expr * val = m_node->get_root()->get_owner(); 157 SASSERT(m.is_true(val) || m.is_false(val)); 158 proof * pr1 = cr.get_proof(m_node, m_node->get_root()); 159 if (pr1) { 160 expr * lit; 161 if (m.is_true(val)) 162 lit = var; 163 else 164 lit = m.mk_not(var); 165 proof * pr2 = m.mk_rewrite(m.get_fact(pr1), lit); 166 return m.mk_modus_ponens(pr1, pr2); 167 } 168 return nullptr; 169 } 170 get_antecedents(conflict_resolution & cr)171 void eq_propagation_justification::get_antecedents(conflict_resolution & cr) { 172 if (m_node1 != m_node2) cr.mark_eq(m_node1, m_node2); 173 } 174 mk_proof(conflict_resolution & cr)175 proof * eq_propagation_justification::mk_proof(conflict_resolution & cr) { 176 return cr.get_proof(m_node1, m_node2); 177 } 178 179 get_antecedents(conflict_resolution & cr)180 void mp_iff_justification::get_antecedents(conflict_resolution & cr) { 181 if (m_node1 == m_node2) 182 return; 183 cr.mark_eq(m_node1, m_node2); 184 context & ctx = cr.get_context(); 185 bool_var v = ctx.enode2bool_var(m_node1); 186 lbool val = ctx.get_assignment(v); 187 literal l(v, val == l_false); 188 cr.mark_literal(l); 189 } 190 mk_proof(conflict_resolution & cr)191 proof * mp_iff_justification::mk_proof(conflict_resolution & cr) { 192 ast_manager& m = cr.get_manager(); 193 if (m_node1 == m_node2) 194 return m.mk_reflexivity(m_node1->get_owner()); 195 proof * pr1 = cr.get_proof(m_node1, m_node2); 196 context & ctx = cr.get_context(); 197 bool_var v = ctx.enode2bool_var(m_node1); 198 lbool val = ctx.get_assignment(v); 199 literal l(v, val == l_false); 200 proof * pr2 = cr.get_proof(l); 201 if (pr1 && pr2) { 202 203 proof * pr; 204 SASSERT(m.has_fact(pr1)); 205 SASSERT(m.has_fact(pr2)); 206 app* fact1 = to_app(m.get_fact(pr1)); 207 app* fact2 = to_app(m.get_fact(pr2)); 208 SASSERT(m.is_iff(fact1)); 209 if (fact1->get_arg(1) == fact2) { 210 pr1 = m.mk_symmetry(pr1); 211 fact1 = to_app(m.get_fact(pr1)); 212 } 213 SASSERT(m.is_iff(fact1)); 214 215 if (l.sign()) { 216 SASSERT(m.is_not(fact2)); 217 expr* lhs = fact1->get_arg(0); 218 expr* rhs = fact1->get_arg(1); 219 if (lhs != fact2->get_arg(0)) { 220 pr1 = m.mk_symmetry(pr1); 221 fact1 = to_app(m.get_fact(pr1)); 222 std::swap(lhs, rhs); 223 } 224 SASSERT(lhs == fact2->get_arg(0)); 225 app* new_lhs = fact2; 226 app* new_rhs = m.mk_not(rhs); 227 pr1 = m.mk_congruence(new_lhs, new_rhs, 1, &pr1); 228 } 229 pr = m.mk_modus_ponens(pr2, pr1); 230 231 TRACE("mp_iff_justification", tout << mk_pp(fact1, m) << "\n" << mk_pp(fact2, m) << "\n" << 232 mk_pp(m.get_fact(pr), m) << "\n";); 233 return pr; 234 } 235 return nullptr; 236 } 237 simple_justification(region & r,unsigned num_lits,literal const * lits)238 simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits): 239 m_num_literals(num_lits) { 240 if (num_lits != 0) { 241 m_literals = new (r) literal[num_lits]; 242 memcpy(m_literals, lits, sizeof(literal) * num_lits); 243 #ifdef Z3DEBUG 244 for (unsigned i = 0; i < num_lits; i++) { 245 SASSERT(lits[i] != null_literal); 246 } 247 #endif 248 } 249 } 250 get_antecedents(conflict_resolution & cr)251 void simple_justification::get_antecedents(conflict_resolution & cr) { 252 for (unsigned i = 0; i < m_num_literals; i++) 253 cr.mark_literal(m_literals[i]); 254 } 255 antecedent2proof(conflict_resolution & cr,ptr_buffer<proof> & result)256 bool simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) { 257 bool visited = true; 258 for (unsigned i = 0; i < m_num_literals; i++) { 259 proof * pr = cr.get_proof(m_literals[i]); 260 if (pr == nullptr) 261 visited = false; 262 else 263 result.push_back(pr); 264 } 265 return visited; 266 } 267 mk_proof(conflict_resolution & cr)268 proof * theory_axiom_justification::mk_proof(conflict_resolution & cr) { 269 context & ctx = cr.get_context(); 270 ast_manager & m = cr.get_manager(); 271 expr_ref_vector lits(m); 272 for (unsigned i = 0; i < m_num_literals; i++) { 273 expr_ref l(m); 274 ctx.literal2expr(m_literals[i], l); 275 lits.push_back(std::move(l)); 276 } 277 if (lits.size() == 1) 278 return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); 279 else 280 return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.c_ptr()), 0, nullptr, m_params.size(), m_params.c_ptr()); 281 } 282 mk_proof(conflict_resolution & cr)283 proof * theory_propagation_justification::mk_proof(conflict_resolution & cr) { 284 ptr_buffer<proof> prs; 285 if (!antecedent2proof(cr, prs)) 286 return nullptr; 287 context & ctx = cr.get_context(); 288 ast_manager & m = cr.get_manager(); 289 expr_ref fact(m); 290 ctx.literal2expr(m_consequent, fact); 291 return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.c_ptr(), m_params.size(), m_params.c_ptr()); 292 } 293 mk_proof(conflict_resolution & cr)294 proof * theory_conflict_justification::mk_proof(conflict_resolution & cr) { 295 ptr_buffer<proof> prs; 296 if (!antecedent2proof(cr, prs)) 297 return nullptr; 298 ast_manager & m = cr.get_manager(); 299 return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.c_ptr(), m_params.size(), m_params.c_ptr()); 300 } 301 ext_simple_justification(region & r,unsigned num_lits,literal const * lits,unsigned num_eqs,enode_pair const * eqs)302 ext_simple_justification::ext_simple_justification(region & r, unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs): 303 simple_justification(r, num_lits, lits), 304 m_num_eqs(num_eqs) { 305 m_eqs = new (r) enode_pair[num_eqs]; 306 std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs); 307 DEBUG_CODE({ 308 for (unsigned i = 0; i < num_eqs; i++) { 309 SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root()); 310 } 311 }); 312 } 313 get_antecedents(conflict_resolution & cr)314 void ext_simple_justification::get_antecedents(conflict_resolution & cr) { 315 simple_justification::get_antecedents(cr); 316 for (unsigned i = 0; i < m_num_eqs; i++) { 317 enode_pair const & p = m_eqs[i]; 318 cr.mark_eq(p.first, p.second); 319 } 320 } 321 antecedent2proof(conflict_resolution & cr,ptr_buffer<proof> & result)322 bool ext_simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) { 323 bool visited = simple_justification::antecedent2proof(cr, result); 324 for (unsigned i = 0; i < m_num_eqs; i++) { 325 enode_pair const & p = m_eqs[i]; 326 proof * pr = cr.get_proof(p.first, p.second); 327 if (pr == nullptr) 328 visited = false; 329 else 330 result.push_back(pr); 331 } 332 return visited; 333 } 334 mk_proof(conflict_resolution & cr)335 proof * ext_theory_propagation_justification::mk_proof(conflict_resolution & cr) { 336 ptr_buffer<proof> prs; 337 if (!antecedent2proof(cr, prs)) 338 return nullptr; 339 context & ctx = cr.get_context(); 340 ast_manager & m = cr.get_manager(); 341 expr_ref fact(m); 342 ctx.literal2expr(m_consequent, fact); 343 return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.c_ptr(), m_params.size(), m_params.c_ptr()); 344 } 345 mk_proof(conflict_resolution & cr)346 proof * ext_theory_conflict_justification::mk_proof(conflict_resolution & cr) { 347 ptr_buffer<proof> prs; 348 if (!antecedent2proof(cr, prs)) 349 return nullptr; 350 ast_manager & m = cr.get_manager(); 351 return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.c_ptr(), m_params.size(), m_params.c_ptr()); 352 } 353 mk_proof(conflict_resolution & cr)354 proof * ext_theory_eq_propagation_justification::mk_proof(conflict_resolution & cr) { 355 ptr_buffer<proof> prs; 356 if (!antecedent2proof(cr, prs)) 357 return nullptr; 358 ast_manager & m = cr.get_manager(); 359 context & ctx = cr.get_context(); 360 expr * fact = ctx.mk_eq_atom(m_lhs->get_owner(), m_rhs->get_owner()); 361 return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.c_ptr(), m_params.size(), m_params.c_ptr()); 362 } 363 364 theory_lemma_justification(family_id fid,context & ctx,unsigned num_lits,literal const * lits,unsigned num_params,parameter * params)365 theory_lemma_justification::theory_lemma_justification(family_id fid, context & ctx, unsigned num_lits, literal const * lits, 366 unsigned num_params, parameter* params): 367 justification(false), 368 m_th_id(fid), 369 m_params(num_params, params), 370 m_num_literals(num_lits) { 371 ast_manager& m = ctx.get_manager(); 372 m_literals = alloc_svect(expr*, num_lits); 373 for (unsigned i = 0; i < num_lits; i++) { 374 bool sign = lits[i].sign(); 375 expr * v = ctx.bool_var2expr(lits[i].var()); 376 m.inc_ref(v); 377 m_literals[i] = TAG(expr*, v, sign); 378 } 379 SASSERT(!in_region()); 380 } 381 ~theory_lemma_justification()382 theory_lemma_justification::~theory_lemma_justification() { 383 SASSERT(!in_region()); 384 dealloc_svect(m_literals); 385 } 386 del_eh(ast_manager & m)387 void theory_lemma_justification::del_eh(ast_manager & m) { 388 for (unsigned i = 0; i < m_num_literals; i++) { 389 expr* v = UNTAG(expr*, m_literals[i]); 390 m.dec_ref(v); 391 } 392 m_params.reset(); 393 } 394 mk_proof(conflict_resolution & cr)395 proof * theory_lemma_justification::mk_proof(conflict_resolution & cr) { 396 ast_manager & m = cr.get_manager(); 397 expr_ref_vector lits(m); 398 for (unsigned i = 0; i < m_num_literals; i++) { 399 bool sign = GET_TAG(m_literals[i]) != 0; 400 expr * v = UNTAG(expr*, m_literals[i]); 401 lits.push_back(sign ? m.mk_not(v) : v); 402 } 403 if (lits.size() == 1) 404 return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); 405 else 406 return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.c_ptr()), 0, nullptr, m_params.size(), m_params.c_ptr()); 407 } 408 409 }; 410 411