1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 dl_bmc_engine.cpp 7 8 Abstract: 9 10 BMC engine for fixedpoint solver. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2012-9-20 15 16 Revision History: 17 18 --*/ 19 20 #include "ast/datatype_decl_plugin.h" 21 #include "ast/dl_decl_plugin.h" 22 #include "ast/ast_smt_pp.h" 23 #include "ast/well_sorted.h" 24 #include "ast/rewriter/bool_rewriter.h" 25 #include "ast/rewriter/rewriter_def.h" 26 #include "ast/scoped_proof.h" 27 #include "smt/smt_solver.h" 28 #include "tactic/fd_solver/fd_solver.h" 29 #include "tactic/tactic.h" 30 #include "muz/base/dl_context.h" 31 #include "muz/base/dl_rule_transformer.h" 32 #include "muz/bmc/dl_bmc_engine.h" 33 #include "muz/transforms/dl_mk_slice.h" 34 #include "model/model_smt2_pp.h" 35 #include "muz/transforms/dl_transforms.h" 36 #include "muz/transforms/dl_mk_rule_inliner.h" 37 #include "muz/base/fp_params.hpp" 38 39 40 namespace datalog { 41 42 // --------------------------------------------------------------------------- 43 // Basic linear BMC based on indexed variables using quantified bit-vector domains. 44 45 class bmc::qlinear { 46 bmc& b; 47 ast_manager& m; 48 bv_util m_bv; 49 unsigned m_bit_width; 50 public: 51 qlinear(bmc& b): b(b), m(b.m), m_bv(m), m_bit_width(1) {} 52 53 lbool check() { 54 setup(); 55 m_bit_width = 4; 56 lbool res = l_false; 57 while (res == l_false) { 58 b.m_solver->push(); 59 IF_VERBOSE(1, verbose_stream() << "bit_width: " << m_bit_width << "\n";); 60 compile(); 61 b.checkpoint(); 62 func_decl_ref q = mk_q_func_decl(b.m_query_pred); 63 expr* T = m.mk_const(symbol("T"), mk_index_sort()); 64 expr_ref fml(m.mk_app(q, T), m); 65 b.assert_expr(fml); 66 res = b.m_solver->check_sat(0, nullptr); 67 68 if (res == l_true) { 69 res = get_model(); 70 } 71 b.m_solver->pop(1); 72 ++m_bit_width; 73 } 74 return res; 75 } 76 private: 77 78 sort_ref mk_index_sort() { 79 return sort_ref(m_bv.mk_sort(m_bit_width), m); 80 } 81 82 var_ref mk_index_var() { 83 return var_ref(m.mk_var(0, mk_index_sort()), m); 84 } 85 86 void compile() { 87 sort_ref index_sort = mk_index_sort(); 88 var_ref var = mk_index_var(); 89 sort* index_sorts[1] = { index_sort }; 90 symbol tick("T"); 91 rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); 92 rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); 93 for (; it != end; ++it) { 94 func_decl* p = it->m_key; 95 rule_vector const& rls = *it->m_value; 96 // Assert: forall level . p(T) => body of rule i + equalities for head of rule i 97 func_decl_ref pr = mk_q_func_decl(p); 98 expr_ref pred = expr_ref(m.mk_app(pr, var.get()), m); 99 expr_ref_vector rules(m), sub(m), conjs(m); 100 expr_ref trm(m), rule_body(m), rule_i(m); 101 for (unsigned i = 0; i < rls.size(); ++i) { 102 sub.reset(); 103 conjs.reset(); 104 rule& r = *rls[i]; 105 rule_i = m.mk_app(mk_q_rule(p, i), var.get()); 106 rules.push_back(rule_i); 107 108 mk_qrule_vars(r, i, sub); 109 110 // apply substitution to body. 111 var_subst vs(m, false); 112 for (unsigned k = 0; k < p->get_arity(); ++k) { 113 trm = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr()); 114 conjs.push_back(m.mk_eq(trm, mk_q_arg(p, k, true))); 115 } 116 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 117 func_decl* q = r.get_decl(j); 118 for (unsigned k = 0; k < q->get_arity(); ++k) { 119 trm = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr()); 120 conjs.push_back(m.mk_eq(trm, mk_q_arg(q, k, false))); 121 } 122 func_decl_ref qr = mk_q_func_decl(q); 123 conjs.push_back(m.mk_app(qr, m_bv.mk_bv_sub(var, mk_q_one()))); 124 } 125 for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { 126 trm = vs(r.get_tail(j), sub.size(), sub.c_ptr()); 127 conjs.push_back(trm); 128 } 129 if (r.get_uninterpreted_tail_size() > 0) { 130 conjs.push_back(m_bv.mk_ule(mk_q_one(), var)); 131 } 132 bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); 133 trm = m.mk_implies(rule_i, rule_body); 134 trm = m.mk_forall(1, index_sorts, &tick, trm, 1); 135 b.assert_expr(trm); 136 } 137 bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), trm); 138 trm = m.mk_implies(pred, trm); 139 trm = m.mk_forall(1, index_sorts, &tick, trm, 1); 140 SASSERT(is_well_sorted(m, trm)); 141 b.assert_expr(trm); 142 } 143 } 144 145 void setup() { 146 params_ref p; 147 p.set_uint("smt.relevancy", 2ul); 148 p.set_bool("smt.mbqi", true); 149 b.m_solver->updt_params(p); 150 b.m_rule_trace.reset(); 151 } 152 153 void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) { 154 ptr_vector<sort> sorts; 155 r.get_vars(m, sorts); 156 // populate substitution of bound variables. 157 sub.reset(); 158 sub.resize(sorts.size()); 159 160 for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { 161 expr* arg = r.get_head()->get_arg(k); 162 if (is_var(arg)) { 163 unsigned idx = to_var(arg)->get_idx(); 164 if (!sub[idx].get()) { 165 sub[idx] = mk_q_arg(r.get_decl(), k, true); 166 } 167 } 168 } 169 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 170 func_decl* q = r.get_decl(j); 171 for (unsigned k = 0; k < q->get_arity(); ++k) { 172 expr* arg = r.get_tail(j)->get_arg(k); 173 if (is_var(arg)) { 174 unsigned idx = to_var(arg)->get_idx(); 175 if (!sub[idx].get()) { 176 sub[idx] = mk_q_arg(q, k, false); 177 } 178 } 179 } 180 } 181 for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { 182 if (sorts[j] && !sub[j].get()) { 183 sub[j] = mk_q_var(r.get_decl(), sorts[j], rule_id, idx++); 184 } 185 } 186 } 187 188 expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) { 189 std::stringstream _name; 190 _name << pred->get_name() << "#" << rule_id << "_" << idx; 191 symbol nm(_name.str()); 192 var_ref var = mk_index_var(); 193 return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m); 194 } 195 196 expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current) { 197 SASSERT(idx < pred->get_arity()); 198 std::stringstream _name; 199 _name << pred->get_name() << "#" << idx; 200 symbol nm(_name.str()); 201 expr_ref var(mk_index_var(), m); 202 if (!is_current) { 203 var = m_bv.mk_bv_sub(var, mk_q_one()); 204 } 205 return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), pred->get_domain(idx)), var), m); 206 } 207 208 expr_ref mk_q_one() { 209 return mk_q_num(1); 210 } 211 212 expr_ref mk_q_num(unsigned i) { 213 return expr_ref(m_bv.mk_numeral(i, m_bit_width), m); 214 } 215 216 func_decl_ref mk_q_func_decl(func_decl* f) { 217 std::stringstream _name; 218 _name << f->get_name() << "#"; 219 symbol nm(_name.str()); 220 return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m); 221 } 222 223 func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id) { 224 std::stringstream _name; 225 _name << f->get_name() << "#" << rule_id; 226 symbol nm(_name.str()); 227 return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m); 228 } 229 230 231 expr_ref eval_q(model_ref& model, func_decl* f, unsigned i) { 232 func_decl_ref fn = mk_q_func_decl(f); 233 expr_ref t(m); 234 t = m.mk_app(mk_q_func_decl(f).get(), mk_q_num(i)); 235 return (*model)(t); 236 } 237 238 expr_ref eval_q(model_ref& model, expr* t, unsigned i) { 239 expr_ref tmp(m), result(m), num(m); 240 var_subst vs(m, false); 241 num = mk_q_num(i); 242 expr* nums[1] = { num }; 243 tmp = vs(t, 1, nums); 244 return (*model)(tmp); 245 } 246 247 lbool get_model() { 248 rule_manager& rm = b.m_ctx.get_rule_manager(); 249 func_decl_ref q = mk_q_func_decl(b.m_query_pred); 250 expr_ref T(m), rule_i(m), vl(m); 251 model_ref md; 252 proof_ref pr(m); 253 rule_unifier unifier(b.m_ctx); 254 rational num; 255 unsigned level, bv_size; 256 257 b.m_solver->get_model(md); 258 func_decl* pred = b.m_query_pred; 259 dl_decl_util util(m); 260 T = m.mk_const(symbol("T"), mk_index_sort()); 261 vl = (*md)(T); 262 VERIFY (m_bv.is_numeral(vl, num, bv_size)); 263 SASSERT(num.is_unsigned()); 264 level = num.get_unsigned(); 265 SASSERT(m.is_true(eval_q(md, b.m_query_pred, level))); 266 TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); 267 268 rule_ref r0(rm), r1(rm), r2(rm); 269 while (true) { 270 TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); 271 expr_ref_vector sub(m); 272 rule_vector const& rls = b.m_rules.get_predicate_rules(pred); 273 rule* r = nullptr; 274 unsigned i = 0; 275 for (; i < rls.size(); ++i) { 276 rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level).get()); 277 TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); 278 if (m.is_true(eval_q(md, rule_i, level))) { 279 r = rls[i]; 280 break; 281 } 282 } 283 SASSERT(r); 284 mk_qrule_vars(*r, i, sub); 285 b.m_rule_trace.push_back(r); 286 // we have rule, we have variable names of rule. 287 288 // extract values for the variables in the rule. 289 for (unsigned j = 0; j < sub.size(); ++j) { 290 expr_ref vl = eval_q(md, sub[j].get(), i); 291 if (vl) { 292 // vl can be 0 if the interpretation does not assign a value to it. 293 sub[j] = vl; 294 } 295 else { 296 sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); 297 } 298 } 299 svector<std::pair<unsigned, unsigned> > positions; 300 vector<expr_ref_vector> substs; 301 expr_ref fml(m), concl(m); 302 303 rm.to_formula(*r, fml); 304 r2 = r; 305 rm.substitute(r2, sub.size(), sub.c_ptr()); 306 proof_ref p(m); 307 if (r0) { 308 VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); 309 expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); 310 expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); 311 apply_subst(sub, sub2); 312 unifier.apply(*r0.get(), 0, *r2.get(), r1); 313 rm.to_formula(*r1.get(), concl); 314 scoped_proof _sp(m); 315 316 p = r->get_proof(); 317 if (!p) { 318 p = m.mk_asserted(fml); 319 } 320 proof* premises[2] = { pr, p }; 321 322 positions.push_back(std::make_pair(0, 1)); 323 324 substs.push_back(sub1); 325 substs.push_back(sub); 326 pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); 327 r0 = r1; 328 } 329 else { 330 rm.to_formula(*r, concl); 331 scoped_proof _sp(m); 332 p = r->get_proof(); 333 if (!p) { 334 p = m.mk_asserted(fml); 335 } 336 if (sub.empty()) { 337 pr = p; 338 } 339 else { 340 substs.push_back(sub); 341 proof* ps[1] = { p }; 342 pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); 343 } 344 r0 = r2; 345 } 346 347 if (level == 0) { 348 SASSERT(r->get_uninterpreted_tail_size() == 0); 349 break; 350 } 351 --level; 352 SASSERT(r->get_uninterpreted_tail_size() == 1); 353 pred = r->get_decl(0); 354 } 355 scoped_proof _sp(m); 356 apply(m, b.m_ctx.get_proof_converter().get(), pr); 357 b.m_answer = pr; 358 return l_true; 359 } 360 }; 361 362 363 // -------------------------------------------------------------------------- 364 // Basic non-linear BMC based on compiling into quantifiers. 365 366 class bmc::nonlinear { 367 bmc& b; 368 ast_manager& m; 369 370 public: 371 372 nonlinear(bmc& b): b(b), m(b.m) {} 373 374 lbool check() { 375 setup(); 376 for (unsigned i = 0; ; ++i) { 377 IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); 378 b.checkpoint(); 379 expr_ref_vector fmls(m); 380 compile(b.m_rules, fmls, i); 381 assert_fmls(fmls); 382 lbool res = check(i); 383 if (res == l_undef) { 384 return res; 385 } 386 if (res == l_true) { 387 get_model(i); 388 return res; 389 } 390 } 391 } 392 393 expr_ref compile_query(func_decl* query_pred, unsigned level) { 394 expr_ref_vector vars(m); 395 func_decl_ref level_p = mk_level_predicate(query_pred, level); 396 for (unsigned i = 0; i < level_p->get_arity(); ++i) { 397 std::stringstream _name; 398 _name << query_pred->get_name() << "#" << level << "_" << i; 399 symbol nm(_name.str()); 400 vars.push_back(m.mk_const(nm, level_p->get_domain(i))); 401 } 402 return expr_ref(m.mk_app(level_p, vars.size(), vars.c_ptr()), m); 403 } 404 405 void compile(rule_set const& rules, expr_ref_vector& result, unsigned level) { 406 bool_rewriter br(m); 407 rule_set::decl2rules::iterator it = rules.begin_grouped_rules(); 408 rule_set::decl2rules::iterator end = rules.end_grouped_rules(); 409 for (; it != end; ++it) { 410 func_decl* p = it->m_key; 411 rule_vector const& rls = *it->m_value; 412 413 // Assert: p_level(vars) => r1_level(vars) \/ r2_level(vars) \/ r3_level(vars) \/ ... 414 // Assert: r_i_level(vars) => exists aux_vars . body of rule i for level 415 416 func_decl_ref level_pred = mk_level_predicate(p, level); 417 expr_ref_vector rules(m); 418 expr_ref body(m), head(m); 419 for (unsigned i = 0; i < rls.size(); ++i) { 420 rule& r = *rls[i]; 421 func_decl_ref rule_i = mk_level_rule(p, i, level); 422 rules.push_back(apply_vars(rule_i)); 423 424 ptr_vector<sort> rule_vars; 425 expr_ref_vector args(m), conjs(m); 426 427 r.get_vars(m, rule_vars); 428 obj_hashtable<expr> used_vars; 429 unsigned num_vars = 0; 430 for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) { 431 expr* arg = r.get_head()->get_arg(i); 432 if (is_var(arg) && !used_vars.contains(arg)) { 433 used_vars.insert(arg); 434 args.push_back(arg); 435 rule_vars[to_var(arg)->get_idx()] = 0; 436 } 437 else { 438 sort* srt = m.get_sort(arg); 439 args.push_back(m.mk_var(rule_vars.size()+num_vars, srt)); 440 conjs.push_back(m.mk_eq(args.back(), arg)); 441 ++num_vars; 442 } 443 } 444 head = m.mk_app(rule_i, args.size(), args.c_ptr()); 445 for (unsigned i = 0; i < r.get_tail_size(); ++i) { 446 conjs.push_back(r.get_tail(i)); 447 } 448 br.mk_and(conjs.size(), conjs.c_ptr(), body); 449 450 replace_by_level_predicates(level, body); 451 body = skolemize_vars(r, args, rule_vars, body); 452 body = m.mk_implies(head, body); 453 body = bind_vars(body, head); 454 result.push_back(body); 455 } 456 br.mk_or(rules.size(), rules.c_ptr(), body); 457 head = apply_vars(level_pred); 458 body = m.mk_implies(head, body); 459 body = bind_vars(body, head); 460 result.push_back(body); 461 } 462 } 463 464 private: 465 466 void assert_fmls(expr_ref_vector const& fmls) { 467 for (unsigned i = 0; i < fmls.size(); ++i) { 468 b.assert_expr(fmls[i]); 469 } 470 } 471 472 void setup() { 473 params_ref p; 474 p.set_uint("smt.relevancy", 2ul); 475 b.m_solver->updt_params(p); 476 b.m_rule_trace.reset(); 477 } 478 479 lbool check(unsigned level) { 480 expr_ref p = compile_query(b.m_query_pred, level); 481 expr_ref q(m), q_at_level(m); 482 q = m.mk_fresh_const("q",m.mk_bool_sort()); 483 q_at_level = m.mk_implies(q, p); 484 b.assert_expr(q_at_level); 485 expr* qr = q.get(); 486 return b.m_solver->check_sat(1, &qr); 487 } 488 489 proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) { 490 if (!m.inc()) { 491 return proof_ref(nullptr, m); 492 } 493 TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); 494 rule_manager& rm = b.m_ctx.get_rule_manager(); 495 expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m); 496 expr_ref_vector args(m); 497 proof_ref_vector prs(m); 498 proof_ref pr(m); 499 500 // find the rule that was triggered by evaluating the arguments to prop. 501 rule_vector const& rls = b.m_rules.get_predicate_rules(pred); 502 rule* r = nullptr; 503 for (unsigned i = 0; i < rls.size(); ++i) { 504 func_decl_ref rule_i = mk_level_rule(pred, i, level); 505 prop_r = m.mk_app(rule_i, prop->get_num_args(), prop->get_args()); 506 TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "); 507 tout << (*md)(prop_r) << "\n"; 508 tout << *md << "\n"; 509 ); 510 if (md->is_true(prop_r)) { 511 r = rls[i]; 512 break; 513 } 514 } 515 if (!r) 516 throw default_exception("could not expand BMC rule"); 517 SASSERT(r); 518 b.m_rule_trace.push_back(r); 519 rm.to_formula(*r, fml); 520 IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";); 521 if (!r->get_proof()) { 522 IF_VERBOSE(0, r->display(b.m_ctx, verbose_stream() << "no proof associated with rule")); 523 throw default_exception("no proof associated with rule"); 524 } 525 prs.push_back(r->get_proof()); 526 unsigned sz = r->get_uninterpreted_tail_size(); 527 528 ptr_vector<sort> rule_vars; 529 r->get_vars(m, rule_vars); 530 args.append(prop->get_num_args(), prop->get_args()); 531 expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args); 532 if (sub.empty() && sz == 0) { 533 pr = prs[0].get(); 534 return pr; 535 } 536 for (unsigned j = 0; j < sub.size(); ++j) { 537 sub[j] = (*md)(sub[j].get()); 538 } 539 540 svector<std::pair<unsigned, unsigned> > positions; 541 vector<expr_ref_vector> substs; 542 var_subst vs(m, false); 543 544 substs.push_back(sub); 545 for (unsigned j = 0; j < sz; ++j) { 546 func_decl* head_j = r->get_decl(j); 547 app* body_j = r->get_tail(j); 548 prop_body = vs(body_j, sub.size(), sub.c_ptr()); 549 prs.push_back(get_proof(md, head_j, to_app(prop_body), level-1)); 550 positions.push_back(std::make_pair(j+1,0)); 551 substs.push_back(expr_ref_vector(m)); 552 } 553 pr = m.mk_hyper_resolve(sz+1, prs.c_ptr(), prop, positions, substs); 554 return pr; 555 } 556 557 void get_model(unsigned level) { 558 scoped_proof _sp(m); 559 expr_ref level_query = compile_query(b.m_query_pred, level); 560 model_ref md; 561 b.m_solver->get_model(md); 562 IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); 563 proof_ref pr(m); 564 pr = get_proof(md, b.m_query_pred, to_app(level_query), level); 565 apply(m, b.m_ctx.get_proof_converter().get(), pr); 566 b.m_answer = pr; 567 } 568 569 func_decl_ref mk_level_predicate(func_decl* p, unsigned level) { 570 std::stringstream _name; 571 _name << p->get_name() << "#" << level; 572 symbol nm(_name.str()); 573 return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); 574 } 575 576 func_decl_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { 577 std::stringstream _name; 578 _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; 579 symbol nm(_name.str()); 580 return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); 581 } 582 583 expr_ref apply_vars(func_decl* p) { 584 expr_ref_vector vars(m); 585 for (unsigned i = 0; i < p->get_arity(); ++i) { 586 vars.push_back(m.mk_var(i, p->get_domain(i))); 587 } 588 return expr_ref(m.mk_app(p, vars.size(), vars.c_ptr()), m); 589 } 590 591 // remove variables from dst that are in src. 592 void subtract_vars(ptr_vector<sort>& dst, ptr_vector<sort> const& src) { 593 for (unsigned i = 0; i < dst.size(); ++i) { 594 if (i >= src.size()) { 595 break; 596 } 597 if (src[i]) { 598 dst[i] = 0; 599 } 600 } 601 } 602 603 expr_ref_vector mk_skolem_binding(rule& r, ptr_vector<sort> const& vars, expr_ref_vector const& args) { 604 expr_ref_vector binding(m); 605 ptr_vector<sort> arg_sorts; 606 for (unsigned i = 0; i < args.size(); ++i) { 607 arg_sorts.push_back(m.get_sort(args[i])); 608 } 609 for (unsigned i = 0; i < vars.size(); ++i) { 610 if (vars[i]) { 611 func_decl_ref f = mk_body_func(r, arg_sorts, i, vars[i]); 612 binding.push_back(m.mk_app(f, args.size(), args.c_ptr())); 613 } 614 else { 615 binding.push_back(nullptr); 616 } 617 } 618 return binding; 619 } 620 621 expr_ref skolemize_vars(rule& r, expr_ref_vector const& args, ptr_vector<sort> const& vars, expr* e) { 622 expr_ref_vector binding = mk_skolem_binding(r, vars, args); 623 var_subst vs(m, false); 624 return vs(e, binding.size(), binding.c_ptr()); 625 } 626 627 func_decl_ref mk_body_func(rule& r, ptr_vector<sort> const& args, unsigned index, sort* s) { 628 std::stringstream _name; 629 _name << r.get_decl()->get_name() << "@" << index; 630 symbol name(_name.str()); 631 func_decl* f = m.mk_func_decl(name, args.size(), args.c_ptr(), s); 632 return func_decl_ref(f, m); 633 } 634 635 expr_ref bind_vars(expr* e, expr* pat) { 636 ptr_vector<sort> sorts; 637 svector<symbol> names; 638 expr_ref_vector binding(m), patterns(m); 639 expr_ref tmp(m), head(m); 640 expr_free_vars vars; 641 vars(e); 642 for (unsigned i = 0; i < vars.size(); ++i) { 643 if (vars[i]) { 644 binding.push_back(m.mk_var(sorts.size(), vars[i])); 645 sorts.push_back(vars[i]); 646 names.push_back(symbol(i)); 647 } 648 else { 649 binding.push_back(nullptr); 650 } 651 } 652 sorts.reverse(); 653 if (sorts.empty()) { 654 return expr_ref(e, m); 655 } 656 var_subst vs(m, false); 657 tmp = vs(e, binding.size(), binding.c_ptr()); 658 head = vs(pat, binding.size(), binding.c_ptr()); 659 patterns.push_back(m.mk_pattern(to_app(head))); 660 symbol qid, skid; 661 return expr_ref(m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qid, skid, 1, patterns.c_ptr()), m); 662 } 663 664 public: 665 class level_replacer { 666 nonlinear& n; 667 unsigned m_level; 668 bool is_predicate(func_decl* f) { 669 return n.b.m_ctx.is_predicate(f); 670 } 671 public: 672 level_replacer(nonlinear& n, unsigned level): n(n), m_level(level) {} 673 674 br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { 675 if (is_predicate(f)) { 676 if (m_level > 0) { 677 result = n.m.mk_app(n.mk_level_predicate(f, m_level-1), num_args, args); 678 } 679 else { 680 result = n.m.mk_false(); 681 } 682 return BR_DONE; 683 } 684 return BR_FAILED; 685 } 686 687 bool reduce_quantifier(quantifier* old_q, expr* new_body, expr_ref& result) { 688 if (is_ground(new_body)) { 689 result = new_body; 690 } 691 else { 692 expr * const * no_pats = &new_body; 693 result = n.m.update_quantifier(old_q, 0, nullptr, 1, no_pats, new_body); 694 } 695 return true; 696 } 697 }; 698 699 struct level_replacer_cfg : public default_rewriter_cfg { 700 level_replacer m_r; 701 702 level_replacer_cfg(nonlinear& nl, unsigned level): 703 m_r(nl, level) {} 704 705 bool rewrite_patterns() const { return false; } 706 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { 707 return m_r.mk_app_core(f, num, args, result); 708 } 709 bool reduce_quantifier(quantifier * old_q, 710 expr * new_body, 711 expr * const * new_patterns, 712 expr * const * new_no_patterns, 713 expr_ref & result, 714 proof_ref & result_pr) { 715 return m_r.reduce_quantifier(old_q, new_body, result); 716 } 717 718 }; 719 720 class level_replacer_star : public rewriter_tpl<level_replacer_cfg> { 721 level_replacer_cfg m_cfg; 722 public: 723 level_replacer_star(nonlinear& nl, unsigned level): 724 rewriter_tpl<level_replacer_cfg>(nl.m, false, m_cfg), 725 m_cfg(nl, level) 726 {} 727 }; 728 729 private: 730 731 void replace_by_level_predicates(unsigned level, expr_ref& fml) { 732 level_replacer_star rep(*this, level); 733 expr_ref tmp(m); 734 rep(fml, tmp); 735 fml = tmp; 736 } 737 738 739 }; 740 741 // -------------------------------------------------------------------------- 742 // Basic non-linear BMC based on compiling into data-types (it is inefficient) 743 744 class bmc::nonlinear_dt { 745 bmc& b; 746 ast_manager& m; 747 ast_ref_vector m_pinned; 748 sort_ref m_path_sort; 749 obj_map<func_decl, sort*> m_pred2sort; 750 obj_map<sort, func_decl*> m_sort2pred; 751 752 753 public: 754 nonlinear_dt(bmc& b): b(b), m(b.m), m_pinned(m), m_path_sort(m) {} 755 756 lbool check() { 757 setup(); 758 declare_datatypes(); 759 compile(); 760 return check_query(); 761 } 762 763 private: 764 void setup() { 765 m_pred2sort.reset(); 766 m_pinned.reset(); 767 m_sort2pred.reset(); 768 params_ref p; 769 p.set_uint("smt.relevancy", 2ul); 770 p.set_bool("smt.mbqi", false); 771 b.m_solver->updt_params(p); 772 b.m_rule_trace.reset(); 773 } 774 775 func_decl_ref mk_predicate(func_decl* pred) { 776 std::stringstream _name; 777 _name << pred->get_name() << "#"; 778 symbol nm(_name.str()); 779 sort* pred_trace_sort = m_pred2sort.find(pred); 780 return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); 781 } 782 783 func_decl_ref mk_rule(func_decl* p, unsigned rule_idx) { 784 std::stringstream _name; 785 _name << "rule:" << p->get_name() << "#" << rule_idx; 786 symbol nm(_name.str()); 787 sort* pred_trace_sort = m_pred2sort.find(p); 788 return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); 789 } 790 791 expr_ref mk_var(func_decl* pred, sort*s, unsigned idx, expr* path_arg, expr* trace_arg) { 792 std::stringstream _name; 793 _name << pred->get_name() << "#V_" << idx; 794 symbol nm(_name.str()); 795 func_decl_ref fn(m); 796 fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, s); 797 return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); 798 } 799 800 expr_ref mk_arg(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg) { 801 SASSERT(idx < pred->get_arity()); 802 std::stringstream _name; 803 _name << pred->get_name() << "#X_" << idx; 804 symbol nm(_name.str()); 805 func_decl_ref fn(m); 806 fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, pred->get_domain(idx)); 807 return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); 808 } 809 810 void mk_subst(datalog::rule& r, expr* path, app* trace, expr_ref_vector& sub) { 811 datatype_util dtu(m); 812 ptr_vector<sort> sorts; 813 func_decl* p = r.get_decl(); 814 ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); 815 // populate substitution of bound variables. 816 r.get_vars(m, sorts); 817 sub.reset(); 818 sub.resize(sorts.size()); 819 for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { 820 expr* arg = r.get_head()->get_arg(k); 821 if (is_var(arg)) { 822 unsigned idx = to_var(arg)->get_idx(); 823 if (!sub[idx].get()) { 824 sub[idx] = mk_arg(p, k, path, trace); 825 } 826 } 827 } 828 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 829 func_decl* q = r.get_decl(j); 830 expr_ref path_arg(m); 831 if (j == 0) { 832 path_arg = path; 833 } 834 else { 835 path_arg = m.mk_app(succs[j], path); 836 } 837 for (unsigned k = 0; k < q->get_arity(); ++k) { 838 expr* arg = r.get_tail(j)->get_arg(k); 839 if (is_var(arg)) { 840 unsigned idx = to_var(arg)->get_idx(); 841 if (!sub[idx].get()) { 842 sub[idx] = mk_arg(q, k, path_arg, trace->get_arg(j)); 843 } 844 } 845 } 846 } 847 for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { 848 if (sorts[j] && !sub[j].get()) { 849 sub[j] = mk_var(r.get_decl(), sorts[j], idx++, path, trace); 850 } 851 } 852 } 853 854 /** 855 \brief compile Horn rule into co-Horn implication. 856 forall args . R(path_var, rule_i(trace_vars)) => Body[X(path_var, rule_i(trace_vars)), Y(S_j(path_var), trace_vars_j)] 857 */ 858 void compile() { 859 datatype_util dtu(m); 860 861 rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); 862 rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); 863 for (; it != end; ++it) { 864 func_decl* p = it->m_key; 865 rule_vector const& rls = *it->m_value; 866 867 // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... 868 // where: r_i_level = body of rule i for level + equalities for head of rule i 869 870 expr_ref rule_body(m), tmp(m), pred(m), trace_arg(m), fml(m); 871 var_ref path_var(m), trace_var(m); 872 expr_ref_vector rules(m), sub(m), conjs(m), vars(m), patterns(m); 873 sort* pred_sort = m_pred2sort.find(p); 874 path_var = m.mk_var(0, m_path_sort); 875 trace_var = m.mk_var(1, pred_sort); 876 // sort* sorts[2] = { pred_sort, m_path_sort }; 877 ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(pred_sort); 878 ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort); 879 SASSERT(cnstrs.size() == rls.size()); 880 pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get()); 881 for (unsigned i = 0; i < rls.size(); ++i) { 882 sub.reset(); 883 conjs.reset(); 884 vars.reset(); 885 rule& r = *rls[i]; 886 func_decl_ref rule_pred_i = mk_rule(p, i); 887 888 // Create cnstr_rule_i(Vars) 889 func_decl* cnstr = cnstrs[i]; 890 rules.push_back(m.mk_app(rule_pred_i, trace_var.get(), path_var.get())); 891 unsigned arity = cnstr->get_arity(); 892 for (unsigned j = 0; j < arity; ++j) { 893 vars.push_back(m.mk_var(arity-j,cnstr->get_domain(j))); 894 } 895 trace_arg = m.mk_app(cnstr, vars.size(), vars.c_ptr()); 896 897 mk_subst(r, path_var, to_app(trace_arg), sub); 898 899 // apply substitution to body. 900 var_subst vs(m, false); 901 for (unsigned k = 0; k < p->get_arity(); ++k) { 902 tmp = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr()); 903 expr_ref arg = mk_arg(p, k, path_var, trace_arg); 904 conjs.push_back(m.mk_eq(tmp, arg)); 905 } 906 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 907 expr_ref path_arg(m); 908 if (j == 0) { 909 path_arg = path_var.get(); 910 } 911 else { 912 path_arg = m.mk_app(succs[j], path_var.get()); 913 } 914 func_decl* q = r.get_decl(j); 915 for (unsigned k = 0; k < q->get_arity(); ++k) { 916 tmp = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr()); 917 expr_ref arg = mk_arg(q, k, path_arg, vars[j].get()); 918 conjs.push_back(m.mk_eq(tmp, arg)); 919 } 920 func_decl_ref q_pred = mk_predicate(q); 921 conjs.push_back(m.mk_app(q_pred, vars[j].get(), path_arg)); 922 } 923 for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { 924 tmp = vs(r.get_tail(j), sub.size(), sub.c_ptr()); 925 conjs.push_back(tmp); 926 } 927 bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); 928 ptr_vector<sort> q_sorts; 929 vector<symbol> names; 930 for (unsigned i = 0; i < vars.size(); ++i) { 931 q_sorts.push_back(m.get_sort(vars[i].get())); 932 names.push_back(symbol(i+1)); 933 } 934 vars.push_back(path_var); 935 q_sorts.push_back(m.get_sort(path_var)); 936 names.push_back(symbol("path")); 937 SASSERT(names.size() == q_sorts.size()); 938 SASSERT(vars.size() == names.size()); 939 symbol qid = r.name(), skid; 940 tmp = m.mk_app(mk_predicate(p), trace_arg.get(), path_var.get()); 941 patterns.reset(); 942 patterns.push_back(m.mk_pattern(to_app(tmp))); 943 fml = m.mk_implies(tmp, rule_body); 944 fml = m.mk_forall(vars.size(), q_sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr()); 945 b.assert_expr(fml); 946 } 947 } 948 } 949 950 void declare_datatypes() { 951 rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); 952 rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); 953 datatype_util dtu(m); 954 ptr_vector<datatype_decl> dts; 955 956 obj_map<func_decl, unsigned> pred_idx; 957 for (unsigned i = 0; it != end; ++it, ++i) { 958 pred_idx.insert(it->m_key, i); 959 } 960 961 it = b.m_rules.begin_grouped_rules(); 962 for (; it != end; ++it) { 963 rule_vector const& rls = *it->m_value; 964 func_decl* pred = it->m_key; 965 ptr_vector<constructor_decl> cnstrs; 966 for (unsigned i = 0; i < rls.size(); ++i) { 967 rule* r = rls[i]; 968 ptr_vector<accessor_decl> accs; 969 for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) { 970 func_decl* q = r->get_decl(j); 971 unsigned idx = pred_idx.find(q); 972 std::stringstream _name; 973 _name << pred->get_name() << "_" << q->get_name() << j; 974 symbol name(_name.str()); 975 type_ref tr(idx); 976 accs.push_back(mk_accessor_decl(m, name, tr)); 977 } 978 std::stringstream _name; 979 _name << pred->get_name() << '_' << i; 980 symbol name(_name.str()); 981 _name << '?'; 982 symbol is_name(_name.str()); 983 cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); 984 } 985 dts.push_back(mk_datatype_decl(dtu, pred->get_name(), 0, nullptr, cnstrs.size(), cnstrs.c_ptr())); 986 } 987 988 989 sort_ref_vector new_sorts(m); 990 family_id dfid = m.mk_family_id("datatype"); 991 datatype_decl_plugin* dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(dfid)); 992 VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, nullptr, new_sorts)); 993 994 it = b.m_rules.begin_grouped_rules(); 995 for (unsigned i = 0; it != end; ++it, ++i) { 996 m_pred2sort.insert(it->m_key, new_sorts[i].get()); 997 m_sort2pred.insert(new_sorts[i].get(), it->m_key); 998 m_pinned.push_back(new_sorts[i].get()); 999 } 1000 if (!new_sorts.empty()) { 1001 TRACE("bmc", dtu.display_datatype(new_sorts[0].get(), tout);); 1002 } 1003 del_datatype_decls(dts.size(), dts.c_ptr()); 1004 1005 // declare path data-type. 1006 { 1007 new_sorts.reset(); 1008 dts.reset(); 1009 ptr_vector<constructor_decl> cnstrs; 1010 unsigned max_arity = 0; 1011 rule_set::iterator it = b.m_rules.begin(); 1012 rule_set::iterator end = b.m_rules.end(); 1013 for (; it != end; ++it) { 1014 rule* r = *it; 1015 unsigned sz = r->get_uninterpreted_tail_size(); 1016 max_arity = std::max(sz, max_arity); 1017 } 1018 cnstrs.push_back(mk_constructor_decl(symbol("Z#"), symbol("Z#?"), 0, nullptr)); 1019 1020 for (unsigned i = 0; i + 1 < max_arity; ++i) { 1021 std::stringstream _name; 1022 _name << "succ#" << i; 1023 symbol name(_name.str()); 1024 _name << "?"; 1025 symbol is_name(_name.str()); 1026 std::stringstream _name2; 1027 _name2 << "get_succ#" << i; 1028 ptr_vector<accessor_decl> accs; 1029 type_ref tr(0); 1030 accs.push_back(mk_accessor_decl(m, name, tr)); 1031 cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); 1032 } 1033 dts.push_back(mk_datatype_decl(dtu, symbol("Path"), 0, nullptr, cnstrs.size(), cnstrs.c_ptr())); 1034 VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, nullptr, new_sorts)); 1035 m_path_sort = new_sorts[0].get(); 1036 } 1037 } 1038 1039 proof_ref get_proof(model_ref& md, app* trace, app* path) { 1040 datatype_util dtu(m); 1041 rule_manager& rm = b.m_ctx.get_rule_manager(); 1042 sort* trace_sort = m.get_sort(trace); 1043 func_decl* p = m_sort2pred.find(trace_sort); 1044 datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p); 1045 ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(trace_sort); 1046 ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort); 1047 for (unsigned i = 0; i < cnstrs.size(); ++i) { 1048 if (trace->get_decl() == cnstrs[i]) { 1049 svector<std::pair<unsigned, unsigned> > positions; 1050 scoped_proof _sc(m); 1051 proof_ref_vector prs(m); 1052 expr_ref_vector sub(m); 1053 vector<expr_ref_vector> substs; 1054 proof_ref pr(m); 1055 expr_ref fml(m), head(m), tmp(m); 1056 app_ref path1(m); 1057 1058 // var_subst vs(m, false); 1059 mk_subst(*rules[i], path, trace, sub); 1060 rm.to_formula(*rules[i], fml); 1061 prs.push_back(rules[i]->get_proof()); 1062 unsigned sz = trace->get_num_args(); 1063 if (sub.empty() && sz == 0) { 1064 pr = prs[0].get(); 1065 return pr; 1066 } 1067 for (unsigned j = 0; j < sub.size(); ++j) { 1068 sub[j] = (*md)(sub.get(j)); 1069 } 1070 rule_ref rl(b.m_ctx.get_rule_manager()); 1071 rl = rules[i]; 1072 b.m_ctx.get_rule_manager().substitute(rl, sub.size(), sub.c_ptr()); 1073 1074 substs.push_back(sub); 1075 1076 for (unsigned j = 0; j < sz; ++j) { 1077 if (j == 0) { 1078 path1 = path; 1079 } 1080 else { 1081 path1 = m.mk_app(succs[j], path); 1082 } 1083 1084 prs.push_back(get_proof(md, to_app(trace->get_arg(j)), path1)); 1085 positions.push_back(std::make_pair(j+1,0)); 1086 substs.push_back(expr_ref_vector(m)); 1087 } 1088 head = rl->get_head(); 1089 pr = m.mk_hyper_resolve(sz+1, prs.c_ptr(), head, positions, substs); 1090 b.m_rule_trace.push_back(rl.get()); 1091 return pr; 1092 } 1093 } 1094 UNREACHABLE(); 1095 return proof_ref(nullptr, m); 1096 } 1097 1098 // instantiation of algebraic data-types takes care of the rest. 1099 lbool check_query() { 1100 sort* trace_sort = m_pred2sort.find(b.m_query_pred); 1101 func_decl_ref q = mk_predicate(b.m_query_pred); 1102 expr_ref trace(m), path(m), fml(m); 1103 trace = m.mk_const(symbol("trace"), trace_sort); 1104 path = m.mk_const(symbol("path"), m_path_sort); 1105 fml = m.mk_app(q, trace.get(), path.get()); 1106 b.assert_expr(fml); 1107 while (true) { 1108 lbool is_sat = b.m_solver->check_sat(0, nullptr); 1109 model_ref md; 1110 if (is_sat == l_false) { 1111 return is_sat; 1112 } 1113 b.m_solver->get_model(md); 1114 mk_answer(md, trace, path); 1115 return l_true; 1116 } 1117 } 1118 1119 bool check_model(model_ref& md, expr* trace) { 1120 expr_ref trace_val(m), eq(m); 1121 trace_val = (*md)(trace); 1122 eq = m.mk_eq(trace, trace_val); 1123 b.m_solver->push(); 1124 b.m_solver->assert_expr(eq); 1125 lbool is_sat = b.m_solver->check_sat(0, nullptr); 1126 if (is_sat != l_false) { 1127 b.m_solver->get_model(md); 1128 } 1129 b.m_solver->pop(1); 1130 if (is_sat == l_false) { 1131 IF_VERBOSE(1, verbose_stream() << "infeasible trace " << mk_pp(trace_val, m) << "\n";); 1132 eq = m.mk_not(eq); 1133 b.assert_expr(eq); 1134 } 1135 return is_sat != l_false; 1136 } 1137 1138 void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) { 1139 IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); 1140 trace = (*md)(trace); 1141 path = (*md)(path); 1142 IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n"; 1143 for (unsigned i = 0; i < b.m_solver->get_num_assertions(); ++i) { 1144 verbose_stream() << mk_pp(b.m_solver->get_assertion(i), m) << "\n"; 1145 }); 1146 scoped_proof _sp(m); 1147 proof_ref pr(m); 1148 pr = get_proof(md, to_app(trace), to_app(path)); 1149 apply(m, b.m_ctx.get_proof_converter().get(), pr); 1150 b.m_answer = pr; 1151 } 1152 1153 }; 1154 1155 // -------------------------------------------------------------------------- 1156 // Basic linear BMC based on incrementally unfolding the transition relation. 1157 1158 class bmc::linear { 1159 bmc& b; 1160 ast_manager& m; 1161 1162 public: 1163 linear(bmc& b): b(b), m(b.m) {} 1164 1165 lbool check() { 1166 setup(); 1167 unsigned max_depth = b.m_ctx.get_params().bmc_linear_unrolling_depth(); 1168 for (unsigned i = 0; i < max_depth; ++i) { 1169 IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); 1170 b.checkpoint(); 1171 compile(i); 1172 lbool res = check(i); 1173 if (res == l_undef) { 1174 return res; 1175 } 1176 if (res == l_true) { 1177 get_model(i); 1178 return res; 1179 } 1180 } 1181 return l_undef; 1182 } 1183 1184 private: 1185 1186 void get_model(unsigned level) { 1187 if (!m.inc()) { 1188 return; 1189 } 1190 rule_manager& rm = b.m_ctx.get_rule_manager(); 1191 expr_ref level_query = mk_level_predicate(b.m_query_pred, level); 1192 model_ref md; 1193 proof_ref pr(m); 1194 rule_unifier unifier(b.m_ctx); 1195 b.m_solver->get_model(md); 1196 func_decl* pred = b.m_query_pred; 1197 SASSERT(m.is_true(md->get_const_interp(to_app(level_query)->get_decl()))); 1198 1199 TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); 1200 1201 rule_ref r0(rm), r1(rm), r2(rm); 1202 while (true) { 1203 TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); 1204 expr_ref_vector sub(m); 1205 rule_vector const& rls = b.m_rules.get_predicate_rules(pred); 1206 rule* r = nullptr; 1207 unsigned i = 0; 1208 for (; i < rls.size(); ++i) { 1209 expr_ref rule_i = mk_level_rule(pred, i, level); 1210 TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); 1211 if (m.is_true(md->get_const_interp(to_app(rule_i)->get_decl()))) { 1212 r = rls[i]; 1213 break; 1214 } 1215 } 1216 SASSERT(r); 1217 b.m_rule_trace.push_back(r); 1218 mk_rule_vars(*r, level, i, sub); 1219 // we have rule, we have variable names of rule. 1220 1221 // extract values for the variables in the rule. 1222 for (unsigned j = 0; j < sub.size(); ++j) { 1223 expr* vl = md->get_const_interp(to_app(sub[j].get())->get_decl()); 1224 if (vl) { 1225 // vl can be 0 if the interpretation does not assign a value to it. 1226 sub[j] = vl; 1227 } 1228 else { 1229 sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); 1230 } 1231 } 1232 svector<std::pair<unsigned, unsigned> > positions; 1233 vector<expr_ref_vector> substs; 1234 expr_ref fml(m), concl(m); 1235 1236 rm.to_formula(*r, fml); 1237 r2 = r; 1238 rm.substitute(r2, sub.size(), sub.c_ptr()); 1239 proof_ref p(m); 1240 { 1241 scoped_proof _sp(m); 1242 p = r->get_proof(); 1243 if (!p) { 1244 p = m.mk_asserted(fml); 1245 } 1246 } 1247 1248 if (r0) { 1249 VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); 1250 expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); 1251 expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); 1252 apply_subst(sub, sub2); 1253 unifier.apply(*r0.get(), 0, *r2.get(), r1); 1254 rm.to_formula(*r1.get(), concl); 1255 1256 scoped_proof _sp(m); 1257 proof* premises[2] = { pr, p }; 1258 1259 positions.push_back(std::make_pair(0, 1)); 1260 1261 substs.push_back(sub1); 1262 substs.push_back(sub); 1263 pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); 1264 r0 = r1; 1265 } 1266 else { 1267 rm.to_formula(*r2.get(), concl); 1268 scoped_proof _sp(m); 1269 if (sub.empty()) { 1270 pr = p; 1271 } 1272 else { 1273 substs.push_back(sub); 1274 proof * ps[1] = { p }; 1275 pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); 1276 } 1277 r0 = r2; 1278 } 1279 1280 if (level == 0) { 1281 SASSERT(r->get_uninterpreted_tail_size() == 0); 1282 break; 1283 } 1284 --level; 1285 SASSERT(r->get_uninterpreted_tail_size() == 1); 1286 pred = r->get_decl(0); 1287 } 1288 scoped_proof _sp(m); 1289 apply(m, b.m_ctx.get_proof_converter().get(), pr); 1290 b.m_answer = pr; 1291 } 1292 1293 1294 void setup() { 1295 params_ref p; 1296 p.set_uint("smt.relevancy", 0ul); 1297 p.set_bool("smt.mbqi", false); 1298 b.m_solver->updt_params(p); 1299 b.m_rule_trace.reset(); 1300 } 1301 1302 1303 lbool check(unsigned level) { 1304 expr_ref level_query = mk_level_predicate(b.m_query_pred, level); 1305 expr* q = level_query.get(); 1306 return b.m_solver->check_sat(1, &q); 1307 } 1308 1309 expr_ref mk_level_predicate(func_decl* p, unsigned level) { 1310 return mk_level_predicate(p->get_name(), level); 1311 } 1312 1313 expr_ref mk_level_predicate(symbol const& name, unsigned level) { 1314 std::stringstream _name; 1315 _name << name << "#" << level; 1316 symbol nm(_name.str()); 1317 return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); 1318 } 1319 1320 expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level) { 1321 SASSERT(idx < pred->get_arity()); 1322 std::stringstream _name; 1323 _name << pred->get_name() << "#" << level << "_" << idx; 1324 symbol nm(_name.str()); 1325 return expr_ref(m.mk_const(nm, pred->get_domain(idx)), m); 1326 } 1327 1328 expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) { 1329 std::stringstream _name; 1330 _name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx; 1331 symbol nm(_name.str()); 1332 return expr_ref(m.mk_const(nm, s), m); 1333 } 1334 1335 expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { 1336 std::stringstream _name; 1337 _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; 1338 symbol nm(_name.str()); 1339 return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); 1340 } 1341 1342 void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) { 1343 ptr_vector<sort> sorts; 1344 r.get_vars(m, sorts); 1345 // populate substitution of bound variables. 1346 sub.reset(); 1347 sub.resize(sorts.size()); 1348 1349 for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { 1350 expr* arg = r.get_head()->get_arg(k); 1351 if (is_var(arg)) { 1352 unsigned idx = to_var(arg)->get_idx(); 1353 if (!sub[idx].get()) { 1354 sub[idx] = mk_level_arg(r.get_decl(), k, level); 1355 } 1356 } 1357 } 1358 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 1359 SASSERT(level > 0); 1360 func_decl* q = r.get_decl(j); 1361 for (unsigned k = 0; k < q->get_arity(); ++k) { 1362 expr* arg = r.get_tail(j)->get_arg(k); 1363 if (is_var(arg)) { 1364 unsigned idx = to_var(arg)->get_idx(); 1365 if (!sub[idx].get()) { 1366 sub[idx] = mk_level_arg(q, k, level-1); 1367 } 1368 } 1369 } 1370 } 1371 for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { 1372 if (sorts[j] && !sub[j].get()) { 1373 sub[j] = mk_level_var(r.get_decl(), sorts[j], rule_id, idx++, level); 1374 } 1375 } 1376 } 1377 1378 void compile(unsigned level) { 1379 rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); 1380 rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); 1381 for (; it != end; ++it) { 1382 func_decl* p = it->m_key; 1383 rule_vector const& rls = *it->m_value; 1384 1385 // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... 1386 // Assert: r_i_level => body of rule i for level + equalities for head of rule i 1387 1388 expr_ref level_pred = mk_level_predicate(p, level); 1389 expr_ref_vector rules(m), sub(m), conjs(m); 1390 expr_ref rule_body(m), tmp(m); 1391 for (unsigned i = 0; i < rls.size(); ++i) { 1392 sub.reset(); 1393 conjs.reset(); 1394 rule& r = *rls[i]; 1395 expr_ref rule_i = mk_level_rule(p, i, level); 1396 rules.push_back(rule_i); 1397 if (level == 0 && r.get_uninterpreted_tail_size() > 0) { 1398 tmp = m.mk_not(rule_i); 1399 b.assert_expr(tmp); 1400 continue; 1401 } 1402 1403 mk_rule_vars(r, level, i, sub); 1404 1405 // apply substitution to body. 1406 var_subst vs(m, false); 1407 for (unsigned k = 0; k < p->get_arity(); ++k) { 1408 tmp = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr()); 1409 conjs.push_back(m.mk_eq(tmp, mk_level_arg(p, k, level))); 1410 } 1411 for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { 1412 SASSERT(level > 0); 1413 func_decl* q = r.get_decl(j); 1414 for (unsigned k = 0; k < q->get_arity(); ++k) { 1415 tmp = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr()); 1416 conjs.push_back(m.mk_eq(tmp, mk_level_arg(q, k, level-1))); 1417 } 1418 conjs.push_back(mk_level_predicate(q, level-1)); 1419 } 1420 for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { 1421 tmp = vs(r.get_tail(j), sub.size(), sub.c_ptr()); 1422 conjs.push_back(tmp); 1423 } 1424 bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); 1425 rule_body = m.mk_implies(rule_i, rule_body); 1426 b.assert_expr(rule_body); 1427 } 1428 bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp); 1429 tmp = m.mk_implies(level_pred, tmp); 1430 b.assert_expr(tmp); 1431 } 1432 } 1433 }; 1434 1435 bmc::bmc(context& ctx): 1436 engine_base(ctx.get_manager(), "bmc"), 1437 m_ctx(ctx), 1438 m(ctx.get_manager()), 1439 m_solver(nullptr), 1440 m_rules(ctx), 1441 m_query_pred(m), 1442 m_answer(m), 1443 m_rule_trace(ctx.get_rule_manager()) { 1444 } 1445 1446 bmc::~bmc() {} 1447 1448 lbool bmc::query(expr* query) { 1449 m_solver = nullptr; 1450 m_answer = nullptr; 1451 m_ctx.ensure_opened(); 1452 m_rules.reset(); 1453 datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); 1454 rule_set& rules0 = m_ctx.get_rules(); 1455 datalog::rule_set old_rules(rules0); 1456 rule_manager.mk_query(query, rules0); 1457 expr_ref bg_assertion = m_ctx.get_background_assertion(); 1458 apply_default_transformation(m_ctx); 1459 1460 if (m_ctx.xform_slice()) { 1461 datalog::rule_transformer transformer(m_ctx); 1462 datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); 1463 transformer.register_plugin(slice); 1464 m_ctx.transform_rules(transformer); 1465 } 1466 1467 const rule_set& rules = m_ctx.get_rules(); 1468 if (rules.get_output_predicates().empty()) { 1469 return l_false; 1470 } 1471 1472 m_query_pred = rules.get_output_predicate(); 1473 m_rules.replace_rules(rules); 1474 m_rules.close(); 1475 m_ctx.reopen(); 1476 m_ctx.replace_rules(old_rules); 1477 1478 checkpoint(); 1479 1480 IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); 1481 1482 params_ref p; 1483 if (m_rules.get_num_rules() == 0) { 1484 return l_false; 1485 } 1486 if (m_rules.get_predicate_rules(m_query_pred).empty()) { 1487 return l_false; 1488 } 1489 1490 if (is_linear()) { 1491 if (m_ctx.get_engine() == QBMC_ENGINE) { 1492 m_solver = mk_smt_solver(m, p, symbol::null); 1493 qlinear ql(*this); 1494 return ql.check(); 1495 } 1496 else { 1497 if (m_rules.is_finite_domain()) { 1498 m_solver = mk_fd_solver(m, p); 1499 } 1500 else { 1501 m_solver = mk_smt_solver(m, p, symbol::null); 1502 } 1503 linear lin(*this); 1504 return lin.check(); 1505 } 1506 } 1507 else { 1508 m_solver = mk_smt_solver(m, p, symbol::null); 1509 IF_VERBOSE(0, verbose_stream() << "WARNING: non-linear BMC is highly inefficient\n";); 1510 nonlinear nl(*this); 1511 return nl.check(); 1512 } 1513 } 1514 1515 void bmc::assert_expr(expr* e) { 1516 TRACE("bmc", tout << mk_pp(e, m) << "\n";); 1517 m_solver->assert_expr(e); 1518 } 1519 1520 bool bmc::is_linear() const { 1521 unsigned sz = m_rules.get_num_rules(); 1522 for (unsigned i = 0; i < sz; ++i) { 1523 if (m_rules.get_rule(i)->get_uninterpreted_tail_size() > 1) { 1524 return false; 1525 } 1526 if (m_rules.get_rule_manager().has_quantifiers(*m_rules.get_rule(i))) { 1527 return false; 1528 } 1529 } 1530 return true; 1531 } 1532 1533 void bmc::checkpoint() { 1534 tactic::checkpoint(m); 1535 } 1536 1537 void bmc::display_certificate(std::ostream& out) const { 1538 out << mk_pp(m_answer, m) << "\n"; 1539 } 1540 1541 void bmc::collect_statistics(statistics& st) const { 1542 if (m_solver) m_solver->collect_statistics(st); 1543 } 1544 1545 void bmc::reset_statistics() { 1546 // m_solver->reset_statistics(); 1547 } 1548 1549 expr_ref bmc::get_answer() { 1550 return m_answer; 1551 } 1552 1553 proof_ref bmc::get_proof() { 1554 return proof_ref(to_app(m_answer), m); 1555 } 1556 1557 void bmc::get_rules_along_trace(datalog::rule_ref_vector& rules) { 1558 rules.append(m_rule_trace); 1559 } 1560 1561 void bmc::compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level) { 1562 nonlinear nl(*this); 1563 nl.compile(rules, fmls, level); 1564 } 1565 1566 expr_ref bmc::compile_query(func_decl* query_pred, unsigned level) { 1567 nonlinear nl(*this); 1568 return nl.compile_query(query_pred, level); 1569 } 1570 1571 }; 1572 1573 template class rewriter_tpl<datalog::bmc::nonlinear::level_replacer_cfg>; 1574