1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_context_inv.cpp 7 8 Abstract: 9 10 SMT logical contexts: invariant 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-21. 15 16 Revision History: 17 18 --*/ 19 #include "smt/smt_context.h" 20 #include "ast/ast_pp.h" 21 #include "ast/ast_ll_pp.h" 22 #include "ast/ast_smt2_pp.h" 23 24 namespace smt { 25 26 #ifdef Z3DEBUG is_watching_clause(literal l,clause const * cls) const27 bool context::is_watching_clause(literal l, clause const * cls) const { 28 watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]); 29 return wl.find_clause(cls) != wl.end_clause(); 30 } 31 check_clause(clause const * cls) const32 bool context::check_clause(clause const * cls) const { 33 SASSERT(is_watching_clause(~cls->get_literal(0), cls)); 34 SASSERT(is_watching_clause(~cls->get_literal(1), cls)); 35 #if 0 36 for (literal l : *cls) { 37 // holds, TBD re-enable when ready to re-check 38 // SASSERT(!track_occs() || m_lit_occs[l.index()] > 0); 39 } 40 #endif 41 return true; 42 } 43 check_clauses(clause_vector const & v) const44 bool context::check_clauses(clause_vector const & v) const { 45 for (clause* cls : v) 46 if (!cls->deleted()) 47 check_clause(cls); 48 return true; 49 } 50 check_watch_list(literal l) const51 bool context::check_watch_list(literal l) const { 52 watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]); 53 l.neg(); 54 watch_list::clause_iterator it = wl.begin_clause(); 55 watch_list::clause_iterator end = wl.end_clause(); 56 for (; it != end; ++it) { 57 clause * cls = *it; 58 TRACE("watch_list", tout << "l: "; display_literal(tout, l); tout << "\n"; 59 display_clause(tout, cls); tout << "\n";); 60 SASSERT(l == cls->get_literal(0) || l == cls->get_literal(1)); 61 } 62 return true; 63 } 64 check_watch_list(unsigned l_idx) const65 bool context::check_watch_list(unsigned l_idx) const { 66 return check_watch_list(to_literal(l_idx)); 67 } 68 check_bin_watch_lists() const69 bool context::check_bin_watch_lists() const { 70 if (binary_clause_opt_enabled()) { 71 vector<watch_list>::const_iterator it = m_watches.begin(); 72 vector<watch_list>::const_iterator end = m_watches.end(); 73 for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { 74 literal l1 = to_literal(l_idx); 75 watch_list const & wl = *it; 76 literal const * it2 = wl.begin_literals(); 77 literal const * end2 = wl.end_literals(); 78 for (; it2 != end2; ++it2) { 79 literal l2 = *it2; 80 watch_list const & wl = m_watches[(~l2).index()]; 81 SASSERT(wl.find_literal(~l1) != wl.end_literals()); 82 } 83 } 84 } 85 return true; 86 } 87 check_enode(enode * n) const88 bool context::check_enode(enode * n) const { 89 SASSERT(n->check_invariant()); 90 bool is_true_eq = n->is_true_eq(); 91 bool cg_inv = 92 n->get_num_args() == 0 || 93 (!is_true_eq && (!n->is_cgc_enabled() || n->is_cgr() == (m_cg_table.contains_ptr(n)))) || 94 (is_true_eq && !m_cg_table.contains_ptr(n)); 95 CTRACE("check_enode", !cg_inv, 96 tout << "n: #" << n->get_expr_id() << ", m_cg: #" << n->m_cg->get_expr_id() << ", contains: " << m_cg_table.contains(n) << "\n"; display(tout);); 97 SASSERT(cg_inv); 98 return true; 99 } 100 check_enodes() const101 bool context::check_enodes() const { 102 for (enode* n : m_enodes) { 103 check_enode(n); 104 } 105 return true; 106 } 107 check_invariant() const108 bool context::check_invariant() const { 109 check_bin_watch_lists(); 110 check_clauses(m_aux_clauses); 111 check_clauses(m_lemmas); 112 check_enodes(); 113 SASSERT(m_cg_table.check_invariant()); 114 return true; 115 } 116 check_missing_clause_propagation(clause_vector const & v) const117 bool context::check_missing_clause_propagation(clause_vector const & v) const { 118 for (clause * cls : v) { 119 CTRACE("missing_propagation", is_unit_clause(cls), display_clause_detail(tout, cls); tout << "\n";); 120 SASSERT(!is_unit_clause(cls)); 121 } 122 return true; 123 } 124 check_missing_bin_clause_propagation() const125 bool context::check_missing_bin_clause_propagation() const { 126 if (binary_clause_opt_enabled()) { 127 SASSERT(m_watches.size() == m_assignment.size()); 128 vector<watch_list>::const_iterator it = m_watches.begin(); 129 vector<watch_list>::const_iterator end = m_watches.end(); 130 for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { 131 literal l = to_literal(l_idx); 132 watch_list const & wl = *it; 133 if (get_assignment(l) == l_true) { 134 literal const * it2 = wl.begin_literals(); 135 literal const * end2 = wl.end_literals(); 136 for (; it2 != end2; ++it2) { 137 literal l2 = *it2; 138 SASSERT(get_assignment(l2) == l_true); 139 } 140 } 141 } 142 } 143 return true; 144 } 145 check_missing_eq_propagation() const146 bool context::check_missing_eq_propagation() const { 147 for (enode* n : m_enodes) { 148 SASSERT(!n->is_true_eq() || get_assignment(n) == l_true); 149 if (n->is_eq() && get_assignment(n) == l_true) { 150 SASSERT(n->is_true_eq()); 151 } 152 } 153 return true; 154 } 155 check_missing_congruence() const156 bool context::check_missing_congruence() const { 157 for (enode* n : m_enodes) { 158 for (enode* n2 : m_enodes) { 159 if (n->get_root() != n2->get_root()) { 160 if (n->is_true_eq() && n2->is_true_eq()) 161 continue; 162 CTRACE("missing_propagation", congruent(n, n2), 163 tout << mk_pp(n->get_expr(), m) << "\n" << mk_pp(n2->get_expr(), m) << "\n"; 164 display(tout);); 165 SASSERT(!congruent(n, n2)); 166 } 167 } 168 } 169 return true; 170 } 171 check_missing_bool_enode_propagation() const172 bool context::check_missing_bool_enode_propagation() const { 173 for (enode* n : m_enodes) { 174 if (m.is_bool(n->get_expr()) && get_assignment(n) == l_undef) { 175 enode * first = n; 176 do { 177 CTRACE("missing_propagation", get_assignment(n) != l_undef, 178 tout << mk_pp(first->get_expr(), m) << "\nassignment: " << get_assignment(first) << "\n" 179 << mk_pp(n->get_expr(), m) << "\nassignment: " << get_assignment(n) << "\n";); 180 SASSERT(get_assignment(n) == l_undef); 181 n = n->get_next(); 182 } 183 while (n != first); 184 } 185 } 186 return true; 187 } 188 check_missing_propagation() const189 bool context::check_missing_propagation() const { 190 check_missing_clause_propagation(m_lemmas); 191 check_missing_clause_propagation(m_aux_clauses); 192 check_missing_bin_clause_propagation(); 193 // check_missing_eq_propagation(); 194 check_missing_congruence(); 195 check_missing_bool_enode_propagation(); 196 return true; 197 } 198 check_relevancy(expr_ref_vector const & v) const199 bool context::check_relevancy(expr_ref_vector const & v) const { 200 return m_relevancy_propagator->check_relevancy(v); 201 } 202 check_relevancy() const203 bool context::check_relevancy() const { 204 if (!relevancy()) 205 return true; 206 check_relevancy(m_b_internalized_stack); 207 check_relevancy(m_e_internalized_stack); 208 unsigned sz = m_asserted_formulas.get_num_formulas(); 209 for (unsigned i = 0; i < sz; i++) { 210 expr * n = m_asserted_formulas.get_formula(i); 211 if (m.is_or(n)) { 212 CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m) << "\n";); 213 SASSERT(is_relevant(n)); 214 TRACE("check_relevancy", tout << "checking:\n" << mk_ll_pp(n, m) << "\n";); 215 SASSERT(m_relevancy_propagator->check_relevancy_or(to_app(n), true)); 216 } 217 else if (m.is_not(n)) { 218 CTRACE("relevancy_bug", !is_relevant(to_app(n)->get_arg(0)), tout << "n: " << mk_ismt2_pp(n, m) << "\n";); 219 SASSERT(is_relevant(to_app(n)->get_arg(0))); 220 } 221 else { 222 CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m) << "\n";); 223 SASSERT(is_relevant(n)); 224 } 225 } 226 return true; 227 } 228 229 /** 230 \brief Check if expressions attached to bool_variables and enodes have a consistent assignment. 231 For all a, b. root(a) == root(b) ==> get_assignment(a) == get_assignment(b) 232 */ check_eqc_bool_assignment() const233 bool context::check_eqc_bool_assignment() const { 234 for (enode* e : m_enodes) { 235 if (m.is_bool(e->get_expr())) { 236 enode * r = e->get_root(); 237 CTRACE("eqc_bool", get_assignment(e) != get_assignment(r), 238 tout << "#" << e->get_expr_id() << "\n" << mk_pp(e->get_expr(), m) << "\n"; 239 tout << "#" << r->get_expr_id() << "\n" << mk_pp(r->get_expr(), m) << "\n"; 240 tout << "assignments: " << get_assignment(e) << " " << get_assignment(r) << "\n"; 241 display(tout);); 242 SASSERT(get_assignment(e) == get_assignment(r)); 243 } 244 } 245 return true; 246 } 247 check_bool_var_vector_sizes() const248 bool context::check_bool_var_vector_sizes() const { 249 SASSERT(m_assignment.size() == 2 * m_bdata.size()); 250 SASSERT(m_watches.size() == 2 * m_bdata.size()); 251 SASSERT(m_bdata.size() == m_activity.size()); 252 SASSERT(m_bool_var2expr.size() == m_bdata.size()); 253 return true; 254 } 255 256 /** 257 \brief Check the following property: 258 259 - for every equality atom (= lhs rhs) assigned to false, relevant: 260 if lhs->get_root() and rhs->get_root() are attached to theory variables v1 and v2 of theory t, 261 then there is an entry (t, v1', v2') in m_propagated_th_diseqs such that, 262 (= get_enode(v1') get_enode(v2')) is congruent to (= lhs rhs). 263 */ check_th_diseq_propagation() const264 bool context::check_th_diseq_propagation() const { 265 TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";); 266 unsigned num = get_num_bool_vars(); 267 if (inconsistent() || get_manager().limit().is_canceled()) { 268 return true; 269 } 270 for (bool_var v = 0; v < num; v++) { 271 if (has_enode(v)) { 272 enode * n = bool_var2enode(v); 273 if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m.is_iff(n->get_expr())) { 274 TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_expr_id() << " " << mk_bounded_pp(n->get_expr(), m) << "\n";); 275 enode * lhs = n->get_arg(0)->get_root(); 276 enode * rhs = n->get_arg(1)->get_root(); 277 if (rhs->is_interpreted() && lhs->is_interpreted()) 278 continue; 279 if (lhs == rhs) 280 continue; 281 TRACE("check_th_diseq_propagation", tout << "num. theory_vars: " << lhs->get_num_th_vars() << " " 282 << mk_pp(lhs->get_expr()->get_sort(), m) << "\n";); 283 theory_var_list * l = lhs->get_th_var_list(); 284 while (l) { 285 theory_id th_id = l->get_id(); 286 theory * th = get_theory(th_id); 287 TRACE("check_th_diseq_propagation", tout << "checking theory: " << m.get_family_name(th_id) << "\n";); 288 // if the theory doesn't use diseqs, then the diseqs are not propagated. 289 if (th->use_diseqs() && rhs->get_th_var(th_id) != null_theory_var) { 290 bool found = false; 291 // lhs and rhs are attached to theory th_id 292 for (new_th_eq const& eq : m_propagated_th_diseqs) { 293 if (eq.m_th_id == th_id) { 294 enode * lhs_prime = th->get_enode(eq.m_lhs)->get_root(); 295 enode * rhs_prime = th->get_enode(eq.m_rhs)->get_root(); 296 297 if ((lhs == lhs_prime && rhs == rhs_prime) || 298 (rhs == lhs_prime && lhs == rhs_prime)) { 299 TRACE("check_th_diseq_propagation", tout << "ok v" << v << " " << get_assignment(v) << "\n";); 300 found = true; 301 break; 302 } 303 } 304 } 305 CTRACE("check_th_diseq_propagation", !found, 306 tout 307 << "checking theory: " << m.get_family_name(th_id) << "\n" 308 << "root: #" << n->get_root()->get_expr_id() << " node: #" << n->get_expr_id() << "\n" 309 << mk_pp(n->get_expr(), m) << "\n" 310 << "lhs: #" << lhs->get_expr_id() << ", rhs: #" << rhs->get_expr_id() << "\n" 311 << mk_bounded_pp(lhs->get_expr(), m) << " " << mk_bounded_pp(rhs->get_expr(), m) << "\n";); 312 VERIFY(found); 313 } 314 l = l->get_next(); 315 } 316 } 317 } 318 } 319 return true; 320 } 321 check_missing_diseq_conflict() const322 bool context::check_missing_diseq_conflict() const { 323 for (enode_pair const& p : m_diseq_vector) { 324 enode * n1 = p.first; 325 enode * n2 = p.second; 326 if (n1->get_root() == n2->get_root()) { 327 TRACE("diseq_bug", 328 tout << "n1: #" << n1->get_expr_id() << ", n2: #" << n2->get_expr_id() << 329 ", r: #" << n1->get_root()->get_expr_id() << "\n"; 330 tout << "n1 parents:\n"; display_parent_eqs(tout, n1); 331 tout << "n2 parents:\n"; display_parent_eqs(tout, n2); 332 tout << "r parents:\n"; display_parent_eqs(tout, n1->get_root()); 333 ); 334 UNREACHABLE(); 335 } 336 } 337 return true; 338 } 339 340 #endif 341 validate_justification(bool_var v,bool_var_data const & d,b_justification const & j)342 bool context::validate_justification(bool_var v, bool_var_data const& d, b_justification const& j) { 343 if (j.get_kind() == b_justification::CLAUSE && v != true_bool_var) { 344 clause* cls = j.get_clause(); 345 literal l = cls->get_literal(0); 346 if (l.var() != v) { 347 l = cls->get_literal(1); 348 } 349 SASSERT(l.var() == v); 350 SASSERT(m_assignment[l.index()] == l_true); 351 } 352 return true; 353 } 354 validate_model()355 bool context::validate_model() { 356 if (!m_proto_model) { 357 return true; 358 } 359 for (literal lit : m_assigned_literals) { 360 if (!is_relevant(lit)) { 361 continue; 362 } 363 expr_ref n(m), res(m); 364 literal2expr(lit, n); 365 if (!is_ground(n)) { 366 continue; 367 } 368 switch (get_assignment(lit)) { 369 case l_undef: 370 break; 371 case l_true: 372 if (!m_proto_model->eval(n, res, false)) 373 return true; 374 CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 375 if (m.is_false(res)) { 376 return false; 377 } 378 break; 379 case l_false: 380 if (!m_proto_model->eval(n, res, false)) 381 return true; 382 CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 383 if (m.is_true(res)) { 384 return false; 385 } 386 break; 387 } 388 } 389 return true; 390 } 391 392 /** 393 \brief validate unsat core returned by 394 */ validate_unsat_core()395 void context::validate_unsat_core() { 396 if (!get_fparams().m_core_validate) { 397 return; 398 } 399 warning_msg("Users should not set smt.core.validate. This option is for debugging only."); 400 context ctx(get_manager(), get_fparams(), get_params()); 401 ptr_vector<expr> assertions; 402 get_assertions(assertions); 403 unsigned sz = assertions.size(); 404 for (unsigned i = 0; i < sz; ++i) { 405 ctx.assert_expr(assertions[i]); 406 } 407 sz = m_unsat_core.size(); 408 for (unsigned i = 0; i < sz; ++i) { 409 ctx.assert_expr(m_unsat_core.get(i)); 410 } 411 lbool res = ctx.check(); 412 switch (res) { 413 case l_false: 414 break; 415 case l_true: 416 throw default_exception("Core could not be validated"); 417 case l_undef: 418 IF_VERBOSE(1, verbose_stream() << "core validation produced unknown\n"); 419 break; 420 } 421 } 422 423 }; 424 425