diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 27161320e..b5ffa808a 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -29,30 +29,1382 @@ Revision History: #include "model_smt2_pp.h" #include "ast_smt_pp.h" #include "well_sorted.h" +#include "rewriter_def.h" namespace datalog { + + // --------------------------------------------------------------------------- + // Basic linear BMC based on indexed variables using quantified bit-vector domains. + + class bmc::qlinear { + bmc& b; + ast_manager& m; + bv_util m_bv; + unsigned m_bit_width; + public: + qlinear(bmc& b): b(b), m(b.m), m_bv(m), m_bit_width(1) {} + + + lbool check() { + setup(); + m_bit_width = 4; + lbool res = l_false; + while (res == l_false) { + b.m_solver.push(); + IF_VERBOSE(1, verbose_stream() << "bit_width: " << m_bit_width << "\n";); + compile(); + b.checkpoint(); + func_decl_ref q = mk_q_func_decl(b.m_query_pred); + expr* T = m.mk_const(symbol("T"), mk_index_sort()); + expr_ref fml(m.mk_app(q, T), m); + b.assert_expr(fml); + res = b.m_solver.check(); + + if (res == l_true) { + res = get_model(); + } + b.m_solver.pop(1); + ++m_bit_width; + } + return res; + } + private: + + sort_ref mk_index_sort() { + return sort_ref(m_bv.mk_sort(m_bit_width), m); + } + + var_ref mk_index_var() { + return var_ref(m.mk_var(0, mk_index_sort()), m); + } + + void compile() { + sort_ref index_sort = mk_index_sort(); + var_ref var = mk_index_var(); + sort* index_sorts[1] = { index_sort }; + symbol tick("T"); + rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); + rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); + for (; it != end; ++it) { + func_decl* p = it->m_key; + rule_vector const& rls = *it->m_value; + // Assert: forall level . p(T) => body of rule i + equalities for head of rule i + func_decl_ref pr = mk_q_func_decl(p); + expr_ref pred = expr_ref(m.mk_app(pr, var.get()), m); + expr_ref_vector rules(m), sub(m), conjs(m); + expr_ref trm(m), rule_body(m), rule_i(m); + for (unsigned i = 0; i < rls.size(); ++i) { + sub.reset(); + conjs.reset(); + rule& r = *rls[i]; + rule_i = m.mk_app(mk_q_rule(p, i), var.get()); + rules.push_back(rule_i); + + mk_qrule_vars(r, i, sub); + + // apply substitution to body. + var_subst vs(m, false); + for (unsigned k = 0; k < p->get_arity(); ++k) { + vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), trm); + conjs.push_back(m.mk_eq(trm, mk_q_arg(p, k, true))); + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + func_decl* q = r.get_decl(j); + for (unsigned k = 0; k < q->get_arity(); ++k) { + vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), trm); + conjs.push_back(m.mk_eq(trm, mk_q_arg(q, k, false))); + } + func_decl_ref qr = mk_q_func_decl(q); + conjs.push_back(m.mk_app(qr, m_bv.mk_bv_sub(var, mk_q_one()))); + } + for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { + vs(r.get_tail(j), sub.size(), sub.c_ptr(), trm); + conjs.push_back(trm); + } + if (r.get_uninterpreted_tail_size() > 0) { + conjs.push_back(m_bv.mk_ule(mk_q_one(), var)); + } + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); + trm = m.mk_implies(rule_i, rule_body); + trm = m.mk_forall(1, index_sorts, &tick, trm, 1); + b.assert_expr(trm); + } + bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), trm); + trm = m.mk_implies(pred, trm); + trm = m.mk_forall(1, index_sorts, &tick, trm, 1); + SASSERT(is_well_sorted(m, trm)); + b.assert_expr(trm); + } + } + + void setup() { + b.m_fparams.m_relevancy_lvl = 2; + b.m_fparams.m_model = true; + b.m_fparams.m_model_compact = true; + b.m_fparams.m_mbqi = true; + } + + void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) { + ptr_vector sorts; + r.get_vars(sorts); + // populate substitution of bound variables. + sub.reset(); + sub.resize(sorts.size()); + + for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { + expr* arg = r.get_head()->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_q_arg(r.get_decl(), k, true); + } + } + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + func_decl* q = r.get_decl(j); + for (unsigned k = 0; k < q->get_arity(); ++k) { + expr* arg = r.get_tail(j)->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_q_arg(q, k, false); + } + } + } + } + for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { + if (sorts[j] && !sub[j].get()) { + sub[j] = mk_q_var(r.get_decl(), sorts[j], rule_id, idx++); + } + } + } + + expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) { + std::stringstream _name; + _name << pred->get_name() << "#" << rule_id << "_" << idx; + symbol nm(_name.str().c_str()); + var_ref var = mk_index_var(); + return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m); + } + + expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current) { + SASSERT(idx < pred->get_arity()); + std::stringstream _name; + _name << pred->get_name() << "#" << idx; + symbol nm(_name.str().c_str()); + expr_ref var(mk_index_var(), m); + if (!is_current) { + var = m_bv.mk_bv_sub(var, mk_q_one()); + } + return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), pred->get_domain(idx)), var), m); + } + + expr_ref mk_q_one() { + return mk_q_num(1); + } + + expr_ref mk_q_num(unsigned i) { + return expr_ref(m_bv.mk_numeral(i, m_bit_width), m); + } + + func_decl_ref mk_q_func_decl(func_decl* f) { + std::stringstream _name; + _name << f->get_name() << "#"; + symbol nm(_name.str().c_str()); + return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m); + } + + func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id) { + std::stringstream _name; + _name << f->get_name() << "#" << rule_id; + symbol nm(_name.str().c_str()); + return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m); + } + + + expr_ref eval_q(model_ref& model, func_decl* f, unsigned i) { + func_decl_ref fn = mk_q_func_decl(f); + expr_ref t(m), result(m); + t = m.mk_app(mk_q_func_decl(f).get(), mk_q_num(i)); + model->eval(t, result); + return result; + } + + expr_ref eval_q(model_ref& model, expr* t, unsigned i) { + expr_ref tmp(m), result(m), num(m); + var_subst vs(m, false); + num = mk_q_num(i); + expr* nums[1] = { num }; + vs(t, 1, nums, tmp); + model->eval(tmp, result); + return result; + } + + lbool get_model() { + rule_manager& rm = b.m_ctx.get_rule_manager(); + func_decl_ref q = mk_q_func_decl(b.m_query_pred); + expr_ref T(m), rule_i(m), vl(m); + model_ref md; + proof_ref pr(m); + rule_unifier unifier(b.m_ctx); + rational num; + unsigned level, bv_size; + + b.m_solver.get_model(md); + func_decl* pred = b.m_query_pred; + dl_decl_util util(m); + T = m.mk_const(symbol("T"), mk_index_sort()); + md->eval(T, vl); + VERIFY (m_bv.is_numeral(vl, num, bv_size)); + SASSERT(num.is_unsigned()); + level = num.get_unsigned(); + SASSERT(m.is_true(eval_q(md, b.m_query_pred, level))); + TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); + + rule_ref r0(rm), r1(rm), r2(rm); + while (true) { + TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); + expr_ref_vector sub(m); + rule_vector const& rls = b.m_rules.get_predicate_rules(pred); + rule* r = 0; + unsigned i = 0; + for (; i < rls.size(); ++i) { + rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level).get()); + TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); + if (m.is_true(eval_q(md, rule_i, level))) { + r = rls[i]; + break; + } + } + SASSERT(r); + mk_qrule_vars(*r, i, sub); + // we have rule, we have variable names of rule. + + // extract values for the variables in the rule. + for (unsigned j = 0; j < sub.size(); ++j) { + expr_ref vl = eval_q(md, sub[j].get(), i); + if (vl) { + // vl can be 0 if the interpretation does not assign a value to it. + sub[j] = vl; + } + else { + sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); + } + } + svector > positions; + vector substs; + expr_ref fml(m), concl(m); + + r->to_formula(fml); + r2 = r; + rm.substitute(r2, sub.size(), sub.c_ptr()); + if (r0) { + VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); + expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); + expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); + apply_subst(sub, sub2); + unifier.apply(*r0.get(), 0, *r2.get(), r1); + r1->to_formula(concl); + scoped_coarse_proof _sp(m); + + proof* p = m.mk_asserted(fml); + proof* premises[2] = { pr, p }; + + positions.push_back(std::make_pair(0, 1)); + + substs.push_back(sub1); + substs.push_back(sub); + pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); + r0 = r1; + } + else { + r2->to_formula(concl); + scoped_coarse_proof _sp(m); + proof* p = m.mk_asserted(fml); + if (sub.empty()) { + pr = p; + } + else { + substs.push_back(sub); + pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + } + r0 = r2; + } + + if (level == 0) { + SASSERT(r->get_uninterpreted_tail_size() == 0); + break; + } + --level; + SASSERT(r->get_uninterpreted_tail_size() == 1); + pred = r->get_decl(0); + } + scoped_coarse_proof _sp(m); + apply(m, b.m_pc.get(), pr); + b.m_answer = pr; + return l_true; + } + }; + + + // -------------------------------------------------------------------------- + // Basic non-linear BMC based on compiling into quantifiers. + + class bmc::nonlinear { + bmc& b; + ast_manager& m; + + public: + + nonlinear(bmc& b): b(b), m(b.m) {} + + lbool check() { + setup(); + for (unsigned i = 0; ; ++i) { + IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); + b.checkpoint(); + expr_ref_vector fmls(m); + compile(b.m_rules, fmls, i); + assert_fmls(fmls); + lbool res = check(i); + if (res == l_undef) { + return res; + } + if (res == l_true) { + get_model(i); + return res; + } + } + } + + expr_ref compile_query(func_decl* query_pred, unsigned level) { + expr_ref_vector vars(m); + func_decl_ref level_p = mk_level_predicate(query_pred, level); + for (unsigned i = 0; i < level_p->get_arity(); ++i) { + std::stringstream _name; + _name << query_pred->get_name() << "#" << level << "_" << i; + symbol nm(_name.str().c_str()); + vars.push_back(m.mk_const(nm, level_p->get_domain(i))); + } + return expr_ref(m.mk_app(level_p, vars.size(), vars.c_ptr()), m); + } + + void compile(rule_set const& rules, expr_ref_vector& result, unsigned level) { + bool_rewriter br(m); + rule_set::decl2rules::iterator it = rules.begin_grouped_rules(); + rule_set::decl2rules::iterator end = rules.end_grouped_rules(); + for (; it != end; ++it) { + func_decl* p = it->m_key; + rule_vector const& rls = *it->m_value; + + // Assert: p_level(vars) => r1_level(vars) \/ r2_level(vars) \/ r3_level(vars) \/ ... + // Assert: r_i_level(vars) => exists aux_vars . body of rule i for level + + func_decl_ref level_pred = mk_level_predicate(p, level); + expr_ref_vector rules(m); + expr_ref body(m), head(m); + for (unsigned i = 0; i < rls.size(); ++i) { + rule& r = *rls[i]; + func_decl_ref rule_i = mk_level_rule(p, i, level); + rules.push_back(apply_vars(rule_i)); + + ptr_vector rule_vars; + expr_ref_vector args(m), conjs(m); + + r.get_vars(rule_vars); + obj_hashtable used_vars; + unsigned num_vars = 0; + for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) { + expr* arg = r.get_head()->get_arg(i); + if (is_var(arg) && !used_vars.contains(arg)) { + used_vars.insert(arg); + args.push_back(arg); + rule_vars[to_var(arg)->get_idx()] = 0; + } + else { + sort* srt = m.get_sort(arg); + args.push_back(m.mk_var(rule_vars.size()+num_vars, srt)); + conjs.push_back(m.mk_eq(args.back(), arg)); + ++num_vars; + } + } + head = m.mk_app(rule_i, args.size(), args.c_ptr()); + for (unsigned i = 0; i < r.get_tail_size(); ++i) { + conjs.push_back(r.get_tail(i)); + } + br.mk_and(conjs.size(), conjs.c_ptr(), body); + + replace_by_level_predicates(level, body); + body = skolemize_vars(r, args, rule_vars, body); + body = m.mk_implies(head, body); + body = bind_vars(body, head); + result.push_back(body); + } + br.mk_or(rules.size(), rules.c_ptr(), body); + head = apply_vars(level_pred); + body = m.mk_implies(head, body); + body = bind_vars(body, head); + result.push_back(body); + } + } + + private: + + void assert_fmls(expr_ref_vector const& fmls) { + for (unsigned i = 0; i < fmls.size(); ++i) { + b.assert_expr(fmls[i]); + } + } + + void setup() { + b.m_fparams.m_model = true; + b.m_fparams.m_model_compact = true; + b.m_fparams.m_mbqi = true; + b.m_fparams.m_relevancy_lvl = 2; + } + + lbool check(unsigned level) { + expr_ref p = compile_query(b.m_query_pred, level); + expr_ref q(m), q_at_level(m); + q = m.mk_fresh_const("q",m.mk_bool_sort()); + q_at_level = m.mk_implies(q, p); + b.assert_expr(q_at_level); + expr* qr = q.get(); + return b.m_solver.check(1, &qr); + } + + proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) { + TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); + + expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m); + expr_ref_vector args(m); + proof_ref_vector prs(m); + proof_ref pr(m); + + // find the rule that was triggered by evaluating the arguments to prop. + rule_vector const& rls = b.m_rules.get_predicate_rules(pred); + rule* r = 0; + for (unsigned i = 0; i < rls.size(); ++i) { + func_decl_ref rule_i = mk_level_rule(pred, i, level); + TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); + prop_r = m.mk_app(rule_i, prop->get_num_args(), prop->get_args()); + md->eval(prop_r, prop_v); + if (m.is_true(prop_v)) { + r = rls[i]; + break; + } + } + SASSERT(r); + r->to_formula(fml); + IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";); + prs.push_back(m.mk_asserted(fml)); + unsigned sz = r->get_uninterpreted_tail_size(); + + ptr_vector rule_vars; + r->get_vars(rule_vars); + args.append(prop->get_num_args(), prop->get_args()); + expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args); + if (sub.empty() && sz == 0) { + pr = prs[0].get(); + return pr; + } + for (unsigned j = 0; j < sub.size(); ++j) { + md->eval(sub[j].get(), tmp); + sub[j] = tmp; + } + + svector > positions; + vector substs; + var_subst vs(m, false); + + substs.push_back(sub); + for (unsigned j = 0; j < sz; ++j) { + func_decl* head_j = r->get_decl(j); + app* body_j = r->get_tail(j); + vs(body_j, sub.size(), sub.c_ptr(), prop_body); + prs.push_back(get_proof(md, head_j, to_app(prop_body), level-1)); + positions.push_back(std::make_pair(j+1,0)); + substs.push_back(expr_ref_vector(m)); + } + pr = m.mk_hyper_resolve(sz+1, prs.c_ptr(), prop, positions, substs); + return pr; + } + + void get_model(unsigned level) { + scoped_coarse_proof _sp(m); + expr_ref level_query = compile_query(b.m_query_pred, level); + model_ref md; + b.m_solver.get_model(md); + IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); + proof_ref pr = get_proof(md, b.m_query_pred, to_app(level_query), level); + apply(m, b.m_pc.get(), pr); + b.m_answer = pr; + } + + func_decl_ref mk_level_predicate(func_decl* p, unsigned level) { + std::stringstream _name; + _name << p->get_name() << "#" << level; + symbol nm(_name.str().c_str()); + return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); + } + + func_decl_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { + std::stringstream _name; + _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; + symbol nm(_name.str().c_str()); + return func_decl_ref(m.mk_func_decl(nm, p->get_arity(), p->get_domain(), m.mk_bool_sort()), m); + } + + expr_ref apply_vars(func_decl* p) { + expr_ref_vector vars(m); + for (unsigned i = 0; i < p->get_arity(); ++i) { + vars.push_back(m.mk_var(i, p->get_domain(i))); + } + return expr_ref(m.mk_app(p, vars.size(), vars.c_ptr()), m); + } + + // remove variables from dst that are in src. + void subtract_vars(ptr_vector& dst, ptr_vector const& src) { + for (unsigned i = 0; i < dst.size(); ++i) { + if (i >= src.size()) { + break; + } + if (src[i]) { + dst[i] = 0; + } + } + } + + expr_ref_vector mk_skolem_binding(rule& r, ptr_vector const& vars, expr_ref_vector const& args) { + expr_ref_vector binding(m); + ptr_vector arg_sorts; + for (unsigned i = 0; i < args.size(); ++i) { + arg_sorts.push_back(m.get_sort(args[i])); + } + for (unsigned i = 0; i < vars.size(); ++i) { + if (vars[i]) { + func_decl_ref f = mk_body_func(r, arg_sorts, i, vars[i]); + binding.push_back(m.mk_app(f, args.size(), args.c_ptr())); + } + else { + binding.push_back(0); + } + } + return binding; + } + + expr_ref skolemize_vars(rule& r, expr_ref_vector const& args, ptr_vector const& vars, expr* e) { + expr_ref result(m); + expr_ref_vector binding = mk_skolem_binding(r, vars, args); + var_subst vs(m, false); + vs(e, binding.size(), binding.c_ptr(), result); + return result; + } + + func_decl_ref mk_body_func(rule& r, ptr_vector const& args, unsigned index, sort* s) { + std::stringstream _name; + _name << r.get_decl()->get_name() << "@" << index; + symbol name(_name.str().c_str()); + func_decl* f = m.mk_func_decl(name, args.size(), args.c_ptr(), s); + return func_decl_ref(f, m); + } + + expr_ref bind_vars(expr* e, expr* pat) { + ptr_vector vars, sorts; + svector names; + expr_ref_vector binding(m), patterns(m); + expr_ref tmp(m), head(m); + get_free_vars(e, vars); + for (unsigned i = 0; i < vars.size(); ++i) { + if (vars[i]) { + binding.push_back(m.mk_var(sorts.size(), vars[i])); + sorts.push_back(vars[i]); + names.push_back(symbol(i)); + } + else { + binding.push_back(0); + } + } + sorts.reverse(); + if (sorts.empty()) { + return expr_ref(e, m); + } + var_subst vs(m, false); + vs(e, binding.size(), binding.c_ptr(), tmp); + vs(pat, binding.size(), binding.c_ptr(), head); + patterns.push_back(m.mk_pattern(to_app(head))); + symbol qid, skid; + return expr_ref(m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qid, skid, 1, patterns.c_ptr()), m); + } + + public: + class level_replacer { + nonlinear& n; + unsigned m_level; + bool is_predicate(func_decl* f) { + return n.b.m_ctx.is_predicate(f); + } + public: + level_replacer(nonlinear& n, unsigned level): n(n), m_level(level) {} + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + if (is_predicate(f)) { + if (m_level > 0) { + result = n.m.mk_app(n.mk_level_predicate(f, m_level-1), num_args, args); + } + else { + result = n.m.mk_false(); + } + return BR_DONE; + } + return BR_FAILED; + } + + bool reduce_quantifier(quantifier* old_q, expr* new_body, expr_ref& result) { + if (is_ground(new_body)) { + result = new_body; + } + else { + expr * const * no_pats = &new_body; + result = n.m.update_quantifier(old_q, 0, 0, 1, no_pats, new_body); + } + return true; + } + }; + + struct level_replacer_cfg : public default_rewriter_cfg { + level_replacer m_r; + + level_replacer_cfg(nonlinear& nl, unsigned level): + m_r(nl, level) {} + + bool rewrite_patterns() const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + return m_r.mk_app_core(f, num, args, result); + } + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + return m_r.reduce_quantifier(old_q, new_body, result); + } + + }; + + class level_replacer_star : public rewriter_tpl { + level_replacer_cfg m_cfg; + public: + level_replacer_star(nonlinear& nl, unsigned level): + rewriter_tpl(nl.m, false, m_cfg), + m_cfg(nl, level) + {} + }; + + private: + + void replace_by_level_predicates(unsigned level, expr_ref& fml) { + level_replacer_star rep(*this, level); + expr_ref tmp(m); + rep(fml, tmp); + fml = tmp; + } + + + }; + + // -------------------------------------------------------------------------- + // Basic non-linear BMC based on compiling into data-types (it is inefficient) + + class bmc::nonlinear_dt { + bmc& b; + ast_manager& m; + ast_ref_vector m_pinned; + sort_ref m_path_sort; + obj_map m_pred2sort; + obj_map m_sort2pred; + + + public: + nonlinear_dt(bmc& b): b(b), m(b.m), m_pinned(m), m_path_sort(m) {} + + lbool check() { + setup(); + declare_datatypes(); + compile(); + return check_query(); + } + + private: + void setup() { + m_pred2sort.reset(); + m_pinned.reset(); + m_sort2pred.reset(); + b.m_fparams.m_relevancy_lvl = 0; + b.m_fparams.m_model = true; + b.m_fparams.m_model_compact = true; + b.m_fparams.m_mbqi = false; + b.m_fparams.m_relevancy_lvl = 2; + } + + func_decl_ref mk_predicate(func_decl* pred) { + std::stringstream _name; + _name << pred->get_name() << "#"; + symbol nm(_name.str().c_str()); + sort* pred_trace_sort = m_pred2sort.find(pred); + return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); + } + + func_decl_ref mk_rule(func_decl* p, unsigned rule_idx) { + std::stringstream _name; + _name << "rule:" << p->get_name() << "#" << rule_idx; + symbol nm(_name.str().c_str()); + sort* pred_trace_sort = m_pred2sort.find(p); + return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); + } + + expr_ref mk_var(func_decl* pred, sort*s, unsigned idx, expr* path_arg, expr* trace_arg) { + std::stringstream _name; + _name << pred->get_name() << "#V_" << idx; + symbol nm(_name.str().c_str()); + func_decl_ref fn(m); + fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, s); + return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); + } + + expr_ref mk_arg(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg) { + SASSERT(idx < pred->get_arity()); + std::stringstream _name; + _name << pred->get_name() << "#X_" << idx; + symbol nm(_name.str().c_str()); + func_decl_ref fn(m); + fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, pred->get_domain(idx)); + return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); + } + + void mk_subst(datalog::rule& r, expr* path, app* trace, expr_ref_vector& sub) { + datatype_util dtu(m); + ptr_vector sorts; + func_decl* p = r.get_decl(); + ptr_vector const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); + // populate substitution of bound variables. + r.get_vars(sorts); + sub.reset(); + sub.resize(sorts.size()); + for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { + expr* arg = r.get_head()->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_arg(p, k, path, trace); + } + } + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + func_decl* q = r.get_decl(j); + expr_ref path_arg(m); + if (j == 0) { + path_arg = path; + } + else { + path_arg = m.mk_app(succs[j], path); + } + for (unsigned k = 0; k < q->get_arity(); ++k) { + expr* arg = r.get_tail(j)->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_arg(q, k, path_arg, trace->get_arg(j)); + } + } + } + } + for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { + if (sorts[j] && !sub[j].get()) { + sub[j] = mk_var(r.get_decl(), sorts[j], idx++, path, trace); + } + } + } + + /** + \brief compile Horn rule into co-Horn implication. + 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)] + */ + void compile() { + datatype_util dtu(m); + + rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); + rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); + for (; it != end; ++it) { + func_decl* p = it->m_key; + rule_vector const& rls = *it->m_value; + + // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... + // where: r_i_level = body of rule i for level + equalities for head of rule i + + expr_ref rule_body(m), tmp(m), pred(m), trace_arg(m), fml(m); + var_ref path_var(m), trace_var(m); + expr_ref_vector rules(m), sub(m), conjs(m), vars(m), patterns(m); + sort* pred_sort = m_pred2sort.find(p); + path_var = m.mk_var(0, m_path_sort); + trace_var = m.mk_var(1, pred_sort); + // sort* sorts[2] = { pred_sort, m_path_sort }; + ptr_vector const& cnstrs = *dtu.get_datatype_constructors(pred_sort); + ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); + SASSERT(cnstrs.size() == rls.size()); + pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get()); + for (unsigned i = 0; i < rls.size(); ++i) { + sub.reset(); + conjs.reset(); + vars.reset(); + rule& r = *rls[i]; + func_decl_ref rule_pred_i = mk_rule(p, i); + + // Create cnstr_rule_i(Vars) + func_decl* cnstr = cnstrs[i]; + rules.push_back(m.mk_app(rule_pred_i, trace_var.get(), path_var.get())); + unsigned arity = cnstr->get_arity(); + for (unsigned j = 0; j < arity; ++j) { + vars.push_back(m.mk_var(arity-j,cnstr->get_domain(j))); + } + trace_arg = m.mk_app(cnstr, vars.size(), vars.c_ptr()); + + mk_subst(r, path_var, to_app(trace_arg), sub); + + // apply substitution to body. + var_subst vs(m, false); + for (unsigned k = 0; k < p->get_arity(); ++k) { + vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp); + expr_ref arg = mk_arg(p, k, path_var, trace_arg); + conjs.push_back(m.mk_eq(tmp, arg)); + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + expr_ref path_arg(m); + if (j == 0) { + path_arg = path_var.get(); + } + else { + path_arg = m.mk_app(succs[j], path_var.get()); + } + func_decl* q = r.get_decl(j); + for (unsigned k = 0; k < q->get_arity(); ++k) { + vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp); + expr_ref arg = mk_arg(q, k, path_arg, vars[j].get()); + conjs.push_back(m.mk_eq(tmp, arg)); + } + func_decl_ref q_pred = mk_predicate(q); + conjs.push_back(m.mk_app(q_pred, vars[j].get(), path_arg)); + } + for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { + vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp); + conjs.push_back(tmp); + } + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); + ptr_vector q_sorts; + vector names; + for (unsigned i = 0; i < vars.size(); ++i) { + q_sorts.push_back(m.get_sort(vars[i].get())); + names.push_back(symbol(i+1)); + } + vars.push_back(path_var); + q_sorts.push_back(m.get_sort(path_var)); + names.push_back(symbol("path")); + SASSERT(names.size() == q_sorts.size()); + SASSERT(vars.size() == names.size()); + symbol qid = r.name(), skid; + tmp = m.mk_app(mk_predicate(p), trace_arg.get(), path_var.get()); + patterns.reset(); + patterns.push_back(m.mk_pattern(to_app(tmp))); + fml = m.mk_implies(tmp, rule_body); + fml = m.mk_forall(vars.size(), q_sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr()); + b.assert_expr(fml); + } + } + } + + void declare_datatypes() { + rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); + rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); + datatype_util dtu(m); + ptr_vector dts; + + obj_map pred_idx; + for (unsigned i = 0; it != end; ++it, ++i) { + pred_idx.insert(it->m_key, i); + } + + it = b.m_rules.begin_grouped_rules(); + for (; it != end; ++it) { + rule_vector const& rls = *it->m_value; + func_decl* pred = it->m_key; + ptr_vector cnstrs; + for (unsigned i = 0; i < rls.size(); ++i) { + rule* r = rls[i]; + ptr_vector accs; + for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) { + func_decl* q = r->get_decl(j); + unsigned idx = pred_idx.find(q); + std::stringstream _name; + _name << pred->get_name() << "_" << q->get_name() << j; + symbol name(_name.str().c_str()); + type_ref tr(idx); + accs.push_back(mk_accessor_decl(name, tr)); + } + std::stringstream _name; + _name << pred->get_name() << "_" << i; + symbol name(_name.str().c_str()); + _name << "?"; + symbol is_name(_name.str().c_str()); + cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); + } + dts.push_back(mk_datatype_decl(pred->get_name(), cnstrs.size(), cnstrs.c_ptr())); + } + + + sort_ref_vector new_sorts(m); + family_id dfid = m.get_family_id("datatype"); + datatype_decl_plugin* dtp = static_cast(m.get_plugin(dfid)); + VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); + + it = b.m_rules.begin_grouped_rules(); + for (unsigned i = 0; it != end; ++it, ++i) { + m_pred2sort.insert(it->m_key, new_sorts[i].get()); + m_sort2pred.insert(new_sorts[i].get(), it->m_key); + m_pinned.push_back(new_sorts[i].get()); + } + if (new_sorts.size() > 0) { + TRACE("bmc", dtu.display_datatype(new_sorts[0].get(), tout);); + } + del_datatype_decls(dts.size(), dts.c_ptr()); + + // declare path data-type. + { + new_sorts.reset(); + dts.reset(); + ptr_vector cnstrs; + unsigned max_arity = 0; + rule_set::iterator it = b.m_rules.begin(); + rule_set::iterator end = b.m_rules.end(); + for (; it != end; ++it) { + rule* r = *it; + unsigned sz = r->get_uninterpreted_tail_size(); + max_arity = std::max(sz, max_arity); + } + cnstrs.push_back(mk_constructor_decl(symbol("Z#"), symbol("Z#?"), 0, 0)); + + for (unsigned i = 0; i + 1 < max_arity; ++i) { + std::stringstream _name; + _name << "succ#" << i; + symbol name(_name.str().c_str()); + _name << "?"; + symbol is_name(_name.str().c_str()); + std::stringstream _name2; + _name2 << "get_succ#" << i; + symbol acc_name(_name2.str().c_str()); + ptr_vector accs; + type_ref tr(0); + accs.push_back(mk_accessor_decl(name, tr)); + cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); + } + dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr())); + VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); + m_path_sort = new_sorts[0].get(); + } + } + + proof_ref get_proof(model_ref& md, app* trace, app* path) { + datatype_util dtu(m); + sort* trace_sort = m.get_sort(trace); + func_decl* p = m_sort2pred.find(trace_sort); + datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p); + ptr_vector const& cnstrs = *dtu.get_datatype_constructors(trace_sort); + ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); + for (unsigned i = 0; i < cnstrs.size(); ++i) { + if (trace->get_decl() == cnstrs[i]) { + svector > positions; + scoped_coarse_proof _sc(m); + proof_ref_vector prs(m); + expr_ref_vector sub(m); + vector substs; + proof_ref pr(m); + expr_ref fml(m), head(m), tmp(m); + app_ref path1(m); + + var_subst vs(m, false); + mk_subst(*rules[i], path, trace, sub); + rules[i]->to_formula(fml); + prs.push_back(m.mk_asserted(fml)); + unsigned sz = trace->get_num_args(); + if (sub.empty() && sz == 0) { + pr = prs[0].get(); + return pr; + } + for (unsigned j = 0; j < sub.size(); ++j) { + md->eval(sub[j].get(), tmp); + sub[j] = tmp; + } + rule_ref rl(b.m_ctx.get_rule_manager()); + rl = rules[i]; + b.m_ctx.get_rule_manager().substitute(rl, sub.size(), sub.c_ptr()); + + substs.push_back(sub); + + for (unsigned j = 0; j < sz; ++j) { + if (j == 0) { + path1 = path; + } + else { + path1 = m.mk_app(succs[j], path); + } + + prs.push_back(get_proof(md, to_app(trace->get_arg(j)), path1)); + positions.push_back(std::make_pair(j+1,0)); + substs.push_back(expr_ref_vector(m)); + } + head = rl->get_head(); + pr = m.mk_hyper_resolve(sz+1, prs.c_ptr(), head, positions, substs); + return pr; + } + } + UNREACHABLE(); + return proof_ref(0, m); + } + + // instantiation of algebraic data-types takes care of the rest. + lbool check_query() { + sort* trace_sort = m_pred2sort.find(b.m_query_pred); + func_decl_ref q = mk_predicate(b.m_query_pred); + expr_ref trace(m), path(m), fml(m); + trace = m.mk_const(symbol("trace"), trace_sort); + path = m.mk_const(symbol("path"), m_path_sort); + fml = m.mk_app(q, trace.get(), path.get()); + b.assert_expr(fml); + while (true) { + lbool is_sat = b.m_solver.check(); + model_ref md; + if (is_sat == l_false) { + return is_sat; + } + b.m_solver.get_model(md); + mk_answer(md, trace, path); + return l_true; + } + } + + bool check_model(model_ref& md, expr* trace) { + expr_ref trace_val(m), eq(m); + md->eval(trace, trace_val); + eq = m.mk_eq(trace, trace_val); + b.m_solver.push(); + b.m_solver.assert_expr(eq); + lbool is_sat = b.m_solver.check(); + if (is_sat != l_false) { + b.m_solver.get_model(md); + } + b.m_solver.pop(1); + if (is_sat == l_false) { + IF_VERBOSE(1, verbose_stream() << "infeasible trace " << mk_pp(trace_val, m) << "\n";); + eq = m.mk_not(eq); + b.assert_expr(eq); + } + return is_sat != l_false; + } + + void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) { + proof_ref pr(m); + IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); + md->eval(trace, trace); + md->eval(path, path); + IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n"; + for (unsigned i = 0; i < b.m_solver.size(); ++i) { + verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n"; + }); + b.m_answer = get_proof(md, to_app(trace), to_app(path)); + } + + }; + + // -------------------------------------------------------------------------- + // Basic linear BMC based on incrementally unfolding the transition relation. + + class bmc::linear { + bmc& b; + ast_manager& m; + + public: + linear(bmc& b): b(b), m(b.m) {} + + lbool check() { + setup(); + for (unsigned i = 0; ; ++i) { + IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); + b.checkpoint(); + compile(i); + lbool res = check(i); + if (res == l_undef) { + return res; + } + if (res == l_true) { + get_model(i); + return res; + } + } + } + + private: + + void get_model(unsigned level) { + rule_manager& rm = b.m_ctx.get_rule_manager(); + expr_ref level_query = mk_level_predicate(b.m_query_pred, level); + model_ref md; + proof_ref pr(m); + rule_unifier unifier(b.m_ctx); + b.m_solver.get_model(md); + func_decl* pred = b.m_query_pred; + SASSERT(m.is_true(md->get_const_interp(to_app(level_query)->get_decl()))); + + TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); + + rule_ref r0(rm), r1(rm), r2(rm); + while (true) { + TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); + expr_ref_vector sub(m); + rule_vector const& rls = b.m_rules.get_predicate_rules(pred); + rule* r = 0; + unsigned i = 0; + for (; i < rls.size(); ++i) { + expr_ref rule_i = mk_level_rule(pred, i, level); + TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); + if (m.is_true(md->get_const_interp(to_app(rule_i)->get_decl()))) { + r = rls[i]; + break; + } + } + SASSERT(r); + mk_rule_vars(*r, level, i, sub); + // we have rule, we have variable names of rule. + + // extract values for the variables in the rule. + for (unsigned j = 0; j < sub.size(); ++j) { + expr* vl = md->get_const_interp(to_app(sub[j].get())->get_decl()); + if (vl) { + // vl can be 0 if the interpretation does not assign a value to it. + sub[j] = vl; + } + else { + sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); + } + } + svector > positions; + vector substs; + expr_ref fml(m), concl(m); + + r->to_formula(fml); + r2 = r; + rm.substitute(r2, sub.size(), sub.c_ptr()); + if (r0) { + VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); + expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); + expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); + apply_subst(sub, sub2); + unifier.apply(*r0.get(), 0, *r2.get(), r1); + r1->to_formula(concl); + scoped_coarse_proof _sp(m); + + proof* p = m.mk_asserted(fml); + proof* premises[2] = { pr, p }; + + positions.push_back(std::make_pair(0, 1)); + + substs.push_back(sub1); + substs.push_back(sub); + pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); + r0 = r1; + } + else { + r2->to_formula(concl); + scoped_coarse_proof _sp(m); + proof* p = m.mk_asserted(fml); + if (sub.empty()) { + pr = p; + } + else { + substs.push_back(sub); + pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + } + r0 = r2; + } + + if (level == 0) { + SASSERT(r->get_uninterpreted_tail_size() == 0); + break; + } + --level; + SASSERT(r->get_uninterpreted_tail_size() == 1); + pred = r->get_decl(0); + } + scoped_coarse_proof _sp(m); + apply(m, b.m_pc.get(), pr); + b.m_answer = pr; + } + + + void setup() { + b.m_fparams.m_relevancy_lvl = 0; + b.m_fparams.m_model = true; + b.m_fparams.m_model_compact = true; + b.m_fparams.m_mbqi = false; + // m_fparams.m_auto_config = false; + } + + + lbool check(unsigned level) { + expr_ref level_query = mk_level_predicate(b.m_query_pred, level); + expr* q = level_query.get(); + return b.m_solver.check(1, &q); + } + + expr_ref mk_level_predicate(func_decl* p, unsigned level) { + return mk_level_predicate(p->get_name(), level); + } + + expr_ref mk_level_predicate(symbol const& name, unsigned level) { + std::stringstream _name; + _name << name << "#" << level; + symbol nm(_name.str().c_str()); + return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); + } + + expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level) { + SASSERT(idx < pred->get_arity()); + std::stringstream _name; + _name << pred->get_name() << "#" << level << "_" << idx; + symbol nm(_name.str().c_str()); + return expr_ref(m.mk_const(nm, pred->get_domain(idx)), m); + } + + expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) { + std::stringstream _name; + _name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx; + symbol nm(_name.str().c_str()); + return expr_ref(m.mk_const(nm, s), m); + } + + expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { + std::stringstream _name; + _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; + symbol nm(_name.str().c_str()); + return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); + } + + void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) { + ptr_vector sorts; + r.get_vars(sorts); + // populate substitution of bound variables. + sub.reset(); + sub.resize(sorts.size()); + + for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { + expr* arg = r.get_head()->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_level_arg(r.get_decl(), k, level); + } + } + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + SASSERT(level > 0); + func_decl* q = r.get_decl(j); + for (unsigned k = 0; k < q->get_arity(); ++k) { + expr* arg = r.get_tail(j)->get_arg(k); + if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + if (!sub[idx].get()) { + sub[idx] = mk_level_arg(q, k, level-1); + } + } + } + } + for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { + if (sorts[j] && !sub[j].get()) { + sub[j] = mk_level_var(r.get_decl(), sorts[j], rule_id, idx++, level); + } + } + } + + void compile(unsigned level) { + rule_set::decl2rules::iterator it = b.m_rules.begin_grouped_rules(); + rule_set::decl2rules::iterator end = b.m_rules.end_grouped_rules(); + for (; it != end; ++it) { + func_decl* p = it->m_key; + rule_vector const& rls = *it->m_value; + + // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... + // Assert: r_i_level => body of rule i for level + equalities for head of rule i + + expr_ref level_pred = mk_level_predicate(p, level); + expr_ref_vector rules(m), sub(m), conjs(m); + expr_ref rule_body(m), tmp(m); + for (unsigned i = 0; i < rls.size(); ++i) { + sub.reset(); + conjs.reset(); + rule& r = *rls[i]; + expr_ref rule_i = mk_level_rule(p, i, level); + rules.push_back(rule_i); + if (level == 0 && r.get_uninterpreted_tail_size() > 0) { + tmp = m.mk_not(rule_i); + b.assert_expr(tmp); + continue; + } + + mk_rule_vars(r, level, i, sub); + + // apply substitution to body. + var_subst vs(m, false); + for (unsigned k = 0; k < p->get_arity(); ++k) { + vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp); + conjs.push_back(m.mk_eq(tmp, mk_level_arg(p, k, level))); + } + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + SASSERT(level > 0); + func_decl* q = r.get_decl(j); + for (unsigned k = 0; k < q->get_arity(); ++k) { + vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp); + conjs.push_back(m.mk_eq(tmp, mk_level_arg(q, k, level-1))); + } + conjs.push_back(mk_level_predicate(q, level-1)); + } + for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { + vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp); + conjs.push_back(tmp); + } + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); + rule_body = m.mk_implies(rule_i, rule_body); + b.assert_expr(rule_body); + } + bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp); + tmp = m.mk_implies(level_pred, tmp); + b.assert_expr(tmp); + } + } + }; + bmc::bmc(context& ctx): m_ctx(ctx), m(ctx.get_manager()), m_solver(m, m_fparams), - m_pinned(m), m_rules(ctx), m_query_pred(m), m_answer(m), - m_cancel(false), - m_path_sort(m), - m_bv(m) { - } + m_cancel(false) { + } bmc::~bmc() {} lbool bmc::query(expr* query) { m_solver.reset(); - m_pinned.reset(); - m_pred2sort.reset(); - m_sort2pred.reset(); - m_pred2newpred.reset(); - m_pred2args.reset(); m_answer = 0; m_ctx.ensure_opened(); @@ -93,984 +1445,39 @@ namespace datalog { if (is_linear()) { if (m_ctx.get_engine() == QBMC_ENGINE) { - return check_qlinear(); + qlinear ql(*this); + return ql.check(); + } + else { + linear lin(*this); + return lin.check(); } - return check_linear(); } else { IF_VERBOSE(0, verbose_stream() << "WARNING: non-linear BMC is highly inefficient\n";); - return check_nonlinear(); + nonlinear nl(*this); + return nl.check(); } } + void bmc::assert_expr(expr* e) { + TRACE("bmc", tout << mk_pp(e, m) << "\n";); + m_solver.assert_expr(e); + } + bool bmc::is_linear() const { unsigned sz = m_rules.get_num_rules(); for (unsigned i = 0; i < sz; ++i) { if (m_rules.get_rule(i)->get_uninterpreted_tail_size() > 1) { return false; } + if (m_rules.get_rule(i)->has_quantifiers()) { + return false; + } } return true; } - // -------------------------------------------------------------------------- - // Basic linear BMC based on incrementally unfolding the transition relation. - - void bmc::get_model_linear(unsigned level) { - rule_manager& rm = m_ctx.get_rule_manager(); - expr_ref level_query = mk_level_predicate(m_query_pred, level); - model_ref md; - proof_ref pr(m); - rule_unifier unifier(m_ctx); - m_solver.get_model(md); - func_decl* pred = m_query_pred; - SASSERT(m.is_true(md->get_const_interp(to_app(level_query)->get_decl()))); - dl_decl_util util(m); - - TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); - - rule_ref r0(rm), r1(rm), r2(rm); - while (true) { - TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); - expr_ref_vector sub(m); - rule_vector const& rls = m_rules.get_predicate_rules(pred); - rule* r = 0; - unsigned i = 0; - for (; i < rls.size(); ++i) { - expr_ref rule_i = mk_level_rule(pred, i, level); - TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); - if (m.is_true(md->get_const_interp(to_app(rule_i)->get_decl()))) { - r = rls[i]; - break; - } - } - SASSERT(r); - mk_rule_vars(*r, level, i, sub); - // we have rule, we have variable names of rule. - - // extract values for the variables in the rule. - for (unsigned j = 0; j < sub.size(); ++j) { - expr* vl = md->get_const_interp(to_app(sub[j].get())->get_decl()); - if (vl) { - // vl can be 0 if the interpretation does not assign a value to it. - sub[j] = vl; - } - else { - sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); - } - } - svector > positions; - vector substs; - expr_ref fml(m), concl(m); - - r->to_formula(fml); - r2 = r; - rm.substitute(r2, sub.size(), sub.c_ptr()); - if (r0) { - VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); - expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); - expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); - apply_subst(sub, sub2); - unifier.apply(*r0.get(), 0, *r2.get(), r1); - r1->to_formula(concl); - scoped_coarse_proof _sp(m); - - proof* p = m.mk_asserted(fml); - proof* premises[2] = { pr, p }; - - positions.push_back(std::make_pair(0, 1)); - - substs.push_back(sub1); - substs.push_back(sub); - pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); - r0 = r1; - } - else { - r2->to_formula(concl); - scoped_coarse_proof _sp(m); - proof* p = m.mk_asserted(fml); - if (sub.empty()) { - pr = p; - } - else { - substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); - } - r0 = r2; - } - - if (level == 0) { - SASSERT(r->get_uninterpreted_tail_size() == 0); - break; - } - --level; - SASSERT(r->get_uninterpreted_tail_size() == 1); - pred = r->get_decl(0); - } - scoped_coarse_proof _sp(m); - apply(m, m_pc.get(), pr); - m_answer = pr; - } - - - void bmc::setup_linear() { - m_fparams.m_relevancy_lvl = 0; - m_fparams.m_model = true; - m_fparams.m_model_compact = true; - m_fparams.m_mbqi = false; - // m_fparams.m_auto_config = false; - } - - lbool bmc::check_linear() { - setup_linear(); - for (unsigned i = 0; ; ++i) { - IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); - checkpoint(); - compile_linear(i); - lbool res = check_linear(i); - if (res == l_undef) { - return res; - } - if (res == l_true) { - get_model_linear(i); - return res; - } - } - } - - lbool bmc::check_linear(unsigned level) { - expr_ref level_query = mk_level_predicate(m_query_pred, level); - expr* q = level_query.get(); - return m_solver.check(1, &q); - } - - void bmc::assert_expr(expr* e) { - TRACE("bmc", tout << mk_pp(e, m) << "\n";); - m_solver.assert_expr(e); - } - - expr_ref bmc::mk_level_predicate(func_decl* p, unsigned level) { - return mk_level_predicate(p->get_name(), level); - } - - expr_ref bmc::mk_level_predicate(symbol const& name, unsigned level) { - std::stringstream _name; - _name << name << "#" << level; - symbol nm(_name.str().c_str()); - return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); - } - - expr_ref bmc::mk_level_arg(func_decl* pred, unsigned idx, unsigned level) { - SASSERT(idx < pred->get_arity()); - std::stringstream _name; - _name << pred->get_name() << "#" << level << "_" << idx; - symbol nm(_name.str().c_str()); - return expr_ref(m.mk_const(nm, pred->get_domain(idx)), m); - } - - expr_ref bmc::mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) { - std::stringstream _name; - _name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx; - symbol nm(_name.str().c_str()); - return expr_ref(m.mk_const(nm, s), m); - } - - expr_ref bmc::mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level) { - std::stringstream _name; - _name << "rule:" << p->get_name() << "#" << level << "_" << rule_idx; - symbol nm(_name.str().c_str()); - return expr_ref(m.mk_const(nm, m.mk_bool_sort()), m); - } - - void bmc::mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) { - sort_ref_vector sorts(m); - r.get_vars(sorts); - // populate substitution of bound variables. - sub.reset(); - sub.resize(sorts.size()); - - for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { - expr* arg = r.get_head()->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_level_arg(r.get_decl(), k, level); - } - } - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - SASSERT(level > 0); - func_decl* q = r.get_decl(j); - for (unsigned k = 0; k < q->get_arity(); ++k) { - expr* arg = r.get_tail(j)->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_level_arg(q, k, level-1); - } - } - } - } - for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { - if (sorts[j].get() && !sub[j].get()) { - sub[j] = mk_level_var(r.get_decl(), sorts[j].get(), rule_id, idx++, level); - } - } - } - - void bmc::compile_linear(unsigned level) { - rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(); - rule_set::decl2rules::iterator end = m_rules.end_grouped_rules(); - for (; it != end; ++it) { - func_decl* p = it->m_key; - rule_vector const& rls = *it->m_value; - - // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... - // Assert: r_i_level => body of rule i for level + equalities for head of rule i - - expr_ref level_pred = mk_level_predicate(p, level); - expr_ref_vector rules(m), sub(m), conjs(m); - expr_ref rule_body(m), tmp(m); - for (unsigned i = 0; i < rls.size(); ++i) { - sub.reset(); - conjs.reset(); - rule& r = *rls[i]; - expr_ref rule_i = mk_level_rule(p, i, level); - rules.push_back(rule_i); - if (level == 0 && r.get_uninterpreted_tail_size() > 0) { - tmp = m.mk_not(rule_i); - assert_expr(tmp); - continue; - } - - mk_rule_vars(r, level, i, sub); - - // apply substitution to body. - var_subst vs(m, false); - for (unsigned k = 0; k < p->get_arity(); ++k) { - vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp); - conjs.push_back(m.mk_eq(tmp, mk_level_arg(p, k, level))); - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - SASSERT(level > 0); - func_decl* q = r.get_decl(j); - for (unsigned k = 0; k < q->get_arity(); ++k) { - vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp); - conjs.push_back(m.mk_eq(tmp, mk_level_arg(q, k, level-1))); - } - conjs.push_back(mk_level_predicate(q, level-1)); - } - for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { - vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp); - conjs.push_back(tmp); - } - bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); - rule_body = m.mk_implies(rule_i, rule_body); - assert_expr(rule_body); - } - bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp); - tmp = m.mk_implies(level_pred, tmp); - assert_expr(tmp); - } - } - - // --------------------------------------------------------------------------- - // Basic linear BMC based on indexed variables using quantified bit-vector domains. - - lbool bmc::check_qlinear() { - setup_qlinear(); - m_bit_width = 4; - lbool res = l_false; - while (res == l_false) { - m_solver.push(); - IF_VERBOSE(1, verbose_stream() << "bit_width: " << m_bit_width << "\n";); - compile_qlinear(); - checkpoint(); - func_decl_ref q = mk_q_func_decl(m_query_pred); - expr* T = m.mk_const(symbol("T"), mk_index_sort()); - expr_ref fml(m.mk_app(q, T), m); - assert_expr(fml); - res = m_solver.check(); - - if (res == l_true) { - res = get_model_qlinear(); - } - m_solver.pop(1); - ++m_bit_width; - } - return res; - } - - sort_ref bmc::mk_index_sort() { - return sort_ref(m_bv.mk_sort(m_bit_width), m); - } - - var_ref bmc::mk_index_var() { - return var_ref(m.mk_var(0, mk_index_sort()), m); - } - - void bmc::compile_qlinear() { - sort_ref index_sort = mk_index_sort(); - var_ref var = mk_index_var(); - sort* index_sorts[1] = { index_sort }; - symbol tick("T"); - rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(); - rule_set::decl2rules::iterator end = m_rules.end_grouped_rules(); - for (; it != end; ++it) { - func_decl* p = it->m_key; - rule_vector const& rls = *it->m_value; - // Assert: forall level . p(T) => body of rule i + equalities for head of rule i - func_decl_ref pr = mk_q_func_decl(p); - expr_ref pred = expr_ref(m.mk_app(pr, var.get()), m); - expr_ref_vector rules(m), sub(m), conjs(m); - expr_ref trm(m), rule_body(m), rule_i(m); - for (unsigned i = 0; i < rls.size(); ++i) { - sub.reset(); - conjs.reset(); - rule& r = *rls[i]; - rule_i = m.mk_app(mk_q_rule(p, i), var.get()); - rules.push_back(rule_i); - - mk_qrule_vars(r, i, sub); - - // apply substitution to body. - var_subst vs(m, false); - for (unsigned k = 0; k < p->get_arity(); ++k) { - vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), trm); - conjs.push_back(m.mk_eq(trm, mk_q_arg(p, k, true))); - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - func_decl* q = r.get_decl(j); - for (unsigned k = 0; k < q->get_arity(); ++k) { - vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), trm); - conjs.push_back(m.mk_eq(trm, mk_q_arg(q, k, false))); - } - func_decl_ref qr = mk_q_func_decl(q); - conjs.push_back(m.mk_app(qr, m_bv.mk_bv_sub(var, mk_q_one()))); - } - for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { - vs(r.get_tail(j), sub.size(), sub.c_ptr(), trm); - conjs.push_back(trm); - } - if (r.get_uninterpreted_tail_size() > 0) { - conjs.push_back(m_bv.mk_ule(mk_q_one(), var)); - } - bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); - trm = m.mk_implies(rule_i, rule_body); - trm = m.mk_forall(1, index_sorts, &tick, trm, 1); - assert_expr(trm); - } - bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), trm); - trm = m.mk_implies(pred, trm); - trm = m.mk_forall(1, index_sorts, &tick, trm, 1); - SASSERT(is_well_sorted(m, trm)); - assert_expr(trm); - } - } - - void bmc::setup_qlinear() { - m_fparams.m_relevancy_lvl = 2; - m_fparams.m_model = true; - m_fparams.m_model_compact = true; - m_fparams.m_mbqi = true; - } - - void bmc::mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) { - sort_ref_vector sorts(m); - r.get_vars(sorts); - // populate substitution of bound variables. - sub.reset(); - sub.resize(sorts.size()); - - for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { - expr* arg = r.get_head()->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_q_arg(r.get_decl(), k, true); - } - } - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - func_decl* q = r.get_decl(j); - for (unsigned k = 0; k < q->get_arity(); ++k) { - expr* arg = r.get_tail(j)->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_q_arg(q, k, false); - } - } - } - } - for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { - if (sorts[j].get() && !sub[j].get()) { - sub[j] = mk_q_var(r.get_decl(), sorts[j].get(), rule_id, idx++); - } - } - } - - expr_ref bmc::mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) { - std::stringstream _name; - _name << pred->get_name() << "#" << rule_id << "_" << idx; - symbol nm(_name.str().c_str()); - var_ref var = mk_index_var(); - return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m); - } - - expr_ref bmc::mk_q_arg(func_decl* pred, unsigned idx, bool is_current) { - SASSERT(idx < pred->get_arity()); - std::stringstream _name; - _name << pred->get_name() << "#" << idx; - symbol nm(_name.str().c_str()); - expr_ref var(mk_index_var(), m); - if (!is_current) { - var = m_bv.mk_bv_sub(var, mk_q_one()); - } - return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), pred->get_domain(idx)), var), m); - } - - expr_ref bmc::mk_q_one() { - return mk_q_num(1); - } - - expr_ref bmc::mk_q_num(unsigned i) { - return expr_ref(m_bv.mk_numeral(i, m_bit_width), m); - } - - func_decl_ref bmc::mk_q_func_decl(func_decl* f) { - std::stringstream _name; - _name << f->get_name() << "#"; - symbol nm(_name.str().c_str()); - return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m); - } - - func_decl_ref bmc::mk_q_rule(func_decl* f, unsigned rule_id) { - std::stringstream _name; - _name << f->get_name() << "#" << rule_id; - symbol nm(_name.str().c_str()); - return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m); - } - - - expr_ref bmc::eval_q(model_ref& model, func_decl* f, unsigned i) { - func_decl_ref fn = mk_q_func_decl(f); - expr_ref t(m), result(m); - t = m.mk_app(mk_q_func_decl(f).get(), mk_q_num(i)); - model->eval(t, result); - return result; - } - - expr_ref bmc::eval_q(model_ref& model, expr* t, unsigned i) { - expr_ref tmp(m), result(m), num(m); - var_subst vs(m, false); - num = mk_q_num(i); - expr* nums[1] = { num }; - vs(t, 1, nums, tmp); - model->eval(tmp, result); - return result; - } - - lbool bmc::get_model_qlinear() { - rule_manager& rm = m_ctx.get_rule_manager(); - func_decl_ref q = mk_q_func_decl(m_query_pred); - expr_ref T(m), rule_i(m), vl(m); - model_ref md; - proof_ref pr(m); - rule_unifier unifier(m_ctx); - rational num; - unsigned level, bv_size; - - m_solver.get_model(md); - func_decl* pred = m_query_pred; - dl_decl_util util(m); - T = m.mk_const(symbol("T"), mk_index_sort()); - md->eval(T, vl); - VERIFY (m_bv.is_numeral(vl, num, bv_size)); - SASSERT(num.is_unsigned()); - level = num.get_unsigned(); - SASSERT(m.is_true(eval_q(md, m_query_pred, level))); - TRACE("bmc", model_smt2_pp(tout, m, *md, 0);); - - rule_ref r0(rm), r1(rm), r2(rm); - while (true) { - TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); - expr_ref_vector sub(m); - rule_vector const& rls = m_rules.get_predicate_rules(pred); - rule* r = 0; - unsigned i = 0; - for (; i < rls.size(); ++i) { - rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level).get()); - TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); - if (m.is_true(eval_q(md, rule_i, level))) { - r = rls[i]; - break; - } - } - SASSERT(r); - mk_qrule_vars(*r, i, sub); - // we have rule, we have variable names of rule. - - // extract values for the variables in the rule. - for (unsigned j = 0; j < sub.size(); ++j) { - expr_ref vl = eval_q(md, sub[j].get(), i); - if (vl) { - // vl can be 0 if the interpretation does not assign a value to it. - sub[j] = vl; - } - else { - sub[j] = m.mk_var(j, m.get_sort(sub[j].get())); - } - } - svector > positions; - vector substs; - expr_ref fml(m), concl(m); - - r->to_formula(fml); - r2 = r; - rm.substitute(r2, sub.size(), sub.c_ptr()); - if (r0) { - VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); - expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); - expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false); - apply_subst(sub, sub2); - unifier.apply(*r0.get(), 0, *r2.get(), r1); - r1->to_formula(concl); - scoped_coarse_proof _sp(m); - - proof* p = m.mk_asserted(fml); - proof* premises[2] = { pr, p }; - - positions.push_back(std::make_pair(0, 1)); - - substs.push_back(sub1); - substs.push_back(sub); - pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); - r0 = r1; - } - else { - r2->to_formula(concl); - scoped_coarse_proof _sp(m); - proof* p = m.mk_asserted(fml); - if (sub.empty()) { - pr = p; - } - else { - substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); - } - r0 = r2; - } - - if (level == 0) { - SASSERT(r->get_uninterpreted_tail_size() == 0); - break; - } - --level; - SASSERT(r->get_uninterpreted_tail_size() == 1); - pred = r->get_decl(0); - } - scoped_coarse_proof _sp(m); - apply(m, m_pc.get(), pr); - m_answer = pr; - return l_true; - } - - // -------------------------------------------------------------------------- - // Basic non-linear BMC based on compiling into data-types (it is inefficient) - - - lbool bmc::check_nonlinear() { - setup_nonlinear(); - declare_datatypes(); - compile_nonlinear(); - return check_query(); - } - - void bmc::setup_nonlinear() { - setup_linear(); - m_fparams.m_relevancy_lvl = 2; - } - - func_decl_ref bmc::mk_predicate(func_decl* pred) { - std::stringstream _name; - _name << pred->get_name() << "#"; - symbol nm(_name.str().c_str()); - sort* pred_trace_sort = m_pred2sort.find(pred); - return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); - } - - func_decl_ref bmc::mk_rule(func_decl* p, unsigned rule_idx) { - std::stringstream _name; - _name << "rule:" << p->get_name() << "#" << rule_idx; - symbol nm(_name.str().c_str()); - sort* pred_trace_sort = m_pred2sort.find(p); - return func_decl_ref(m.mk_func_decl(nm, pred_trace_sort, m_path_sort, m.mk_bool_sort()), m); - } - - expr_ref bmc::mk_var_nonlinear(func_decl* pred, sort*s, unsigned idx, expr* path_arg, expr* trace_arg) { - std::stringstream _name; - _name << pred->get_name() << "#V_" << idx; - symbol nm(_name.str().c_str()); - func_decl_ref fn(m); - fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, s); - return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); - } - - expr_ref bmc::mk_arg_nonlinear(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg) { - SASSERT(idx < pred->get_arity()); - std::stringstream _name; - _name << pred->get_name() << "#X_" << idx; - symbol nm(_name.str().c_str()); - func_decl_ref fn(m); - fn = m.mk_func_decl(nm, m_pred2sort.find(pred), m_path_sort, pred->get_domain(idx)); - return expr_ref(m.mk_app(fn, trace_arg, path_arg), m); - } - - void bmc::mk_subst(datalog::rule& r, expr* path, app* trace, expr_ref_vector& sub) { - datatype_util dtu(m); - sort_ref_vector sorts(m); - func_decl* p = r.get_decl(); - ptr_vector const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); - // populate substitution of bound variables. - r.get_vars(sorts); - sub.reset(); - sub.resize(sorts.size()); - for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) { - expr* arg = r.get_head()->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_arg_nonlinear(p, k, path, trace); - } - } - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - func_decl* q = r.get_decl(j); - expr_ref path_arg(m); - if (j == 0) { - path_arg = path; - } - else { - path_arg = m.mk_app(succs[j], path); - } - for (unsigned k = 0; k < q->get_arity(); ++k) { - expr* arg = r.get_tail(j)->get_arg(k); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (!sub[idx].get()) { - sub[idx] = mk_arg_nonlinear(q, k, path_arg, trace->get_arg(j)); - } - } - } - } - for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) { - if (sorts[j].get() && !sub[j].get()) { - sub[j] = mk_var_nonlinear(r.get_decl(), sorts[j].get(), idx++, path, trace); - } - } - } - - /** - \brief compile Horn rule into co-Horn implication. - 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)] - */ - void bmc::compile_nonlinear() { - datatype_util dtu(m); - - rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(); - rule_set::decl2rules::iterator end = m_rules.end_grouped_rules(); - for (; it != end; ++it) { - func_decl* p = it->m_key; - rule_vector const& rls = *it->m_value; - - // Assert: p_level => r1_level \/ r2_level \/ r3_level \/ ... - // where: r_i_level = body of rule i for level + equalities for head of rule i - - expr_ref rule_body(m), tmp(m), pred(m), trace_arg(m), fml(m); - var_ref path_var(m), trace_var(m); - expr_ref_vector rules(m), sub(m), conjs(m), vars(m), patterns(m); - sort* pred_sort = m_pred2sort.find(p); - path_var = m.mk_var(0, m_path_sort); - trace_var = m.mk_var(1, pred_sort); - // sort* sorts[2] = { pred_sort, m_path_sort }; - ptr_vector const& cnstrs = *dtu.get_datatype_constructors(pred_sort); - ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); - SASSERT(cnstrs.size() == rls.size()); - pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get()); - for (unsigned i = 0; i < rls.size(); ++i) { - sub.reset(); - conjs.reset(); - vars.reset(); - rule& r = *rls[i]; - func_decl_ref rule_pred_i = mk_rule(p, i); - - // Create cnstr_rule_i(Vars) - func_decl* cnstr = cnstrs[i]; - rules.push_back(m.mk_app(rule_pred_i, trace_var.get(), path_var.get())); - unsigned arity = cnstr->get_arity(); - for (unsigned j = 0; j < arity; ++j) { - vars.push_back(m.mk_var(arity-j,cnstr->get_domain(j))); - } - trace_arg = m.mk_app(cnstr, vars.size(), vars.c_ptr()); - - mk_subst(r, path_var, to_app(trace_arg), sub); - - // apply substitution to body. - var_subst vs(m, false); - for (unsigned k = 0; k < p->get_arity(); ++k) { - vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp); - expr_ref arg = mk_arg_nonlinear(p, k, path_var, trace_arg); - conjs.push_back(m.mk_eq(tmp, arg)); - } - for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { - expr_ref path_arg(m); - if (j == 0) { - path_arg = path_var.get(); - } - else { - path_arg = m.mk_app(succs[j], path_var.get()); - } - func_decl* q = r.get_decl(j); - for (unsigned k = 0; k < q->get_arity(); ++k) { - vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp); - expr_ref arg = mk_arg_nonlinear(q, k, path_arg, vars[j].get()); - conjs.push_back(m.mk_eq(tmp, arg)); - } - func_decl_ref q_pred = mk_predicate(q); - conjs.push_back(m.mk_app(q_pred, vars[j].get(), path_arg)); - } - for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { - vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp); - conjs.push_back(tmp); - } - bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body); - ptr_vector q_sorts; - vector names; - for (unsigned i = 0; i < vars.size(); ++i) { - q_sorts.push_back(m.get_sort(vars[i].get())); - names.push_back(symbol(i+1)); - } - vars.push_back(path_var); - q_sorts.push_back(m.get_sort(path_var)); - names.push_back(symbol("path")); - SASSERT(names.size() == q_sorts.size()); - SASSERT(vars.size() == names.size()); - symbol qid = r.name(), skid; - tmp = m.mk_app(mk_predicate(p), trace_arg.get(), path_var.get()); - patterns.reset(); - patterns.push_back(m.mk_pattern(to_app(tmp))); - fml = m.mk_implies(tmp, rule_body); - fml = m.mk_forall(vars.size(), q_sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr()); - assert_expr(fml); - - } - } - } - - void bmc::declare_datatypes() { - rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(); - rule_set::decl2rules::iterator end = m_rules.end_grouped_rules(); - datatype_util dtu(m); - ptr_vector dts; - - obj_map pred_idx; - for (unsigned i = 0; it != end; ++it, ++i) { - pred_idx.insert(it->m_key, i); - } - - it = m_rules.begin_grouped_rules(); - for (; it != end; ++it) { - rule_vector const& rls = *it->m_value; - func_decl* pred = it->m_key; - ptr_vector cnstrs; - for (unsigned i = 0; i < rls.size(); ++i) { - rule* r = rls[i]; - ptr_vector accs; - for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) { - func_decl* q = r->get_decl(j); - unsigned idx = pred_idx.find(q); - std::stringstream _name; - _name << pred->get_name() << "_" << q->get_name() << j; - symbol name(_name.str().c_str()); - type_ref tr(idx); - accs.push_back(mk_accessor_decl(name, tr)); - } - std::stringstream _name; - _name << pred->get_name() << "_" << i; - symbol name(_name.str().c_str()); - _name << "?"; - symbol is_name(_name.str().c_str()); - cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); - } - dts.push_back(mk_datatype_decl(pred->get_name(), cnstrs.size(), cnstrs.c_ptr())); - } - - - sort_ref_vector new_sorts(m); - family_id dfid = m.get_family_id("datatype"); - datatype_decl_plugin* dtp = static_cast(m.get_plugin(dfid)); - VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); - - it = m_rules.begin_grouped_rules(); - for (unsigned i = 0; it != end; ++it, ++i) { - m_pred2sort.insert(it->m_key, new_sorts[i].get()); - m_sort2pred.insert(new_sorts[i].get(), it->m_key); - m_pinned.push_back(new_sorts[i].get()); - } - if (new_sorts.size() > 0) { - TRACE("bmc", dtu.display_datatype(new_sorts[0].get(), tout);); - } - del_datatype_decls(dts.size(), dts.c_ptr()); - - // declare path data-type. - { - new_sorts.reset(); - dts.reset(); - ptr_vector cnstrs; - unsigned max_arity = 0; - rule_set::iterator it = m_rules.begin(); - rule_set::iterator end = m_rules.end(); - for (; it != end; ++it) { - rule* r = *it; - unsigned sz = r->get_uninterpreted_tail_size(); - max_arity = std::max(sz, max_arity); - } - cnstrs.push_back(mk_constructor_decl(symbol("Z#"), symbol("Z#?"), 0, 0)); - - for (unsigned i = 0; i + 1 < max_arity; ++i) { - std::stringstream _name; - _name << "succ#" << i; - symbol name(_name.str().c_str()); - _name << "?"; - symbol is_name(_name.str().c_str()); - std::stringstream _name2; - _name2 << "get_succ#" << i; - symbol acc_name(_name2.str().c_str()); - ptr_vector accs; - type_ref tr(0); - accs.push_back(mk_accessor_decl(name, tr)); - cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); - } - dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr())); - VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); - m_path_sort = new_sorts[0].get(); - } - } - - proof_ref bmc::get_proof(model_ref& md, app* trace, app* path) { - datatype_util dtu(m); - sort* trace_sort = m.get_sort(trace); - func_decl* p = m_sort2pred.find(trace_sort); - datalog::rule_vector const& rules = m_rules.get_predicate_rules(p); - ptr_vector const& cnstrs = *dtu.get_datatype_constructors(trace_sort); - ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); - // bool found = false; - for (unsigned i = 0; i < cnstrs.size(); ++i) { - if (trace->get_decl() == cnstrs[i]) { - // found = true; - svector > positions; - scoped_coarse_proof _sc(m); - proof_ref_vector prs(m); - expr_ref_vector sub(m); - vector substs; - proof_ref pr(m); - expr_ref fml(m), head(m), tmp(m); - app_ref path1(m); - - var_subst vs(m, false); - mk_subst(*rules[i], path, trace, sub); - rules[i]->to_formula(fml); - prs.push_back(m.mk_asserted(fml)); - unsigned sz = trace->get_num_args(); - if (sub.empty() && sz == 0) { - pr = prs[0].get(); - return pr; - } - for (unsigned j = 0; j < sub.size(); ++j) { - md->eval(sub[j].get(), tmp); - sub[j] = tmp; - } - rule_ref rl(m_ctx.get_rule_manager()); - rl = rules[i]; - m_ctx.get_rule_manager().substitute(rl, sub.size(), sub.c_ptr()); - - substs.push_back(sub); - - for (unsigned j = 0; j < sz; ++j) { - if (j == 0) { - path1 = path; - } - else { - path1 = m.mk_app(succs[j], path); - } - - prs.push_back(get_proof(md, to_app(trace->get_arg(j)), path1)); - positions.push_back(std::make_pair(j+1,0)); - substs.push_back(expr_ref_vector(m)); - } - head = rl->get_head(); - pr = m.mk_hyper_resolve(sz+1, prs.c_ptr(), head, positions, substs); - return pr; - } - } - UNREACHABLE(); - return proof_ref(0, m); - } - - // instantiation of algebraic data-types takes care of the rest. - lbool bmc::check_query() { - sort* trace_sort = m_pred2sort.find(m_query_pred); - func_decl_ref q = mk_predicate(m_query_pred); - expr_ref trace(m), path(m), fml(m); - trace = m.mk_const(symbol("trace"), trace_sort); - path = m.mk_const(symbol("path"), m_path_sort); - fml = m.mk_app(q, trace.get(), path.get()); - assert_expr(fml); - while (true) { - lbool is_sat = m_solver.check(); - model_ref md; - if (is_sat == l_false) { - return is_sat; - } - m_solver.get_model(md); - mk_answer_nonlinear(md, trace, path); - return l_true; - } - } - - bool bmc::check_model_nonlinear(model_ref& md, expr* trace) { - expr_ref trace_val(m), eq(m); - md->eval(trace, trace_val); - eq = m.mk_eq(trace, trace_val); - m_solver.push(); - m_solver.assert_expr(eq); - lbool is_sat = m_solver.check(); - if (is_sat != l_false) { - m_solver.get_model(md); - } - m_solver.pop(1); - if (is_sat == l_false) { - IF_VERBOSE(1, verbose_stream() << "infeasible trace " << mk_pp(trace_val, m) << "\n";); - eq = m.mk_not(eq); - m_solver.assert_expr(eq); - } - return is_sat != l_false; - } - - void bmc::mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path) { - proof_ref pr(m); - IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); - md->eval(trace, trace); - md->eval(path, path); - IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n"; - for (unsigned i = 0; i < m_solver.size(); ++i) { - verbose_stream() << mk_pp(m_solver.get_formulas()[i], m) << "\n"; - }); - m_answer = get_proof(md, to_app(trace), to_app(path)); - } - - void bmc::checkpoint() { if (m_cancel) { throw default_exception("bmc canceled"); @@ -1103,4 +1510,16 @@ namespace datalog { return m_answer; } + void bmc::compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level) { + nonlinear nl(*this); + nl.compile(rules, fmls, level); + } + + expr_ref bmc::compile_query(func_decl* query_pred, unsigned level) { + nonlinear nl(*this); + return nl.compile_query(query_pred, level); + } + }; + +template class rewriter_tpl; diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index 5b6e433cd..06901a160 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -35,83 +35,23 @@ namespace datalog { ast_manager& m; smt_params m_fparams; smt::kernel m_solver; - obj_map m_pred2sort; - obj_map m_sort2pred; - obj_map m_pred2newpred; - obj_map > m_pred2args; - ast_ref_vector m_pinned; rule_set m_rules; func_decl_ref m_query_pred; expr_ref m_answer; volatile bool m_cancel; proof_converter_ref m_pc; - sort_ref m_path_sort; - bv_util m_bv; - unsigned m_bit_width; - - lbool check_query(); - - proof_ref get_proof(model_ref& md, app* trace, app* path); void checkpoint(); - void declare_datatypes(); - - void compile_nonlinear(); - - void mk_rule_vars_nonlinear(rule& r, unsigned rule_id, expr* trace_arg, expr* path_arg, expr_ref_vector& sub); - - expr_ref mk_var_nonlinear(func_decl* pred, sort* s, unsigned idx, expr* path_arg, expr* trace_arg); - - expr_ref mk_arg_nonlinear(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg); - - void mk_subst(rule& r, expr* path, app* trace, expr_ref_vector& sub); + class nonlinear_dt; + class nonlinear; + class qlinear; + class linear; bool is_linear() const; - - lbool check_nonlinear(); - void setup_nonlinear(); - bool check_model_nonlinear(model_ref& md, expr* trace); - void mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path); - func_decl_ref mk_predicate(func_decl* p); - - func_decl_ref mk_rule(func_decl* p, unsigned rule_idx); - - // linear check - lbool check_linear(); - lbool check_linear(unsigned level); - void compile_linear(); - void compile_linear(unsigned level); - void compile_linear(rule& r, unsigned level); - expr_ref mk_level_predicate(symbol const& name, unsigned level); - expr_ref mk_level_predicate(func_decl* p, unsigned level); - expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level); - expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level); - expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level); - void get_model_linear(unsigned level); - void setup_linear(); - void assert_expr(expr* e); - void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub); - - // quantified linear check - void compile_qlinear(); - void setup_qlinear(); - lbool check_qlinear(); - lbool get_model_qlinear(); - sort_ref mk_index_sort(); - var_ref mk_index_var(); - void mk_qrule_vars(datalog::rule const& r, unsigned i, expr_ref_vector& sub); - expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx); - expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current); - expr_ref mk_q_one(); - expr_ref mk_q_num(unsigned i); - expr_ref eval_q(model_ref& model, expr* t, unsigned i); - expr_ref eval_q(model_ref& model, func_decl* f, unsigned i); - func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id); - func_decl_ref mk_q_func_decl(func_decl* f); public: bmc(context& ctx); @@ -131,6 +71,10 @@ namespace datalog { void reset_statistics(); expr_ref get_answer(); + + // direct access to (new) non-linear compiler. + void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level); + expr_ref compile_query(func_decl* query_pred, unsigned level); }; }; diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 7a46228ce..5581732c8 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -715,6 +715,8 @@ namespace datalog { check_positive_predicates(r); break; case BMC_ENGINE: + check_positive_predicates(r); + break; case QBMC_ENGINE: check_existential_tail(r); check_positive_predicates(r); diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index a5259ba8a..880f196a2 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -18,7 +18,8 @@ Revision History: --*/ #include "dl_mk_array_blast.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" + namespace datalog { @@ -54,9 +55,10 @@ namespace datalog { unsigned tsz = r.get_tail_size(); expr_ref_vector conjs(m), new_conjs(m); expr_ref tmp(m); - expr_substitution sub(m); + expr_safe_replace sub(m); uint_set lhs_vars, rhs_vars; bool change = false; + bool inserted = false; for (unsigned i = 0; i < utsz; ++i) { new_conjs.push_back(r.get_tail(i)); @@ -81,6 +83,7 @@ namespace datalog { } else { sub.insert(x, y); + inserted = true; } } else { @@ -89,7 +92,7 @@ namespace datalog { new_conjs.push_back(tmp); } } - if (sub.empty() && !change) { + if (!inserted && !change) { rules.add_rule(&r); return false; } @@ -99,11 +102,9 @@ namespace datalog { r.to_formula(fml1); body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); head = r.get_head(); - scoped_ptr replace = mk_default_expr_replacer(m); - replace->set_substitution(&sub); - (*replace)(body); + sub(body); m_rewriter(body); - (*replace)(head); + sub(head); m_rewriter(head); fml2 = m.mk_implies(body, head); rm.mk_rule(fml2, new_rules, r.name()); diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp index 251988a84..222881bc4 100644 --- a/src/muz_qe/dl_mk_coalesce.cpp +++ b/src/muz_qe/dl_mk_coalesce.cpp @@ -60,7 +60,7 @@ namespace datalog { obj_map indices; bool_rewriter bwr(m); rule_ref r(const_cast(&rl), rm); - sort_ref_vector sorts(m); + ptr_vector sorts; expr_ref_vector revsub(m), conjs(m); rl.get_vars(sorts); revsub.resize(sorts.size()); @@ -72,8 +72,8 @@ namespace datalog { if (is_var(e)) { unsigned v = to_var(e)->get_idx(); SASSERT(v < valid.size()); - if (sorts[v].get()) { - SASSERT(s == sorts[v].get()); + if (sorts[v]) { + SASSERT(s == sorts[v]); if (valid[v]) { revsub[v] = w; valid[v] = false; @@ -92,8 +92,8 @@ namespace datalog { } } for (unsigned i = 0; i < sorts.size(); ++i) { - if (valid[i] && sorts[i].get() && !revsub[i].get()) { - revsub[i] = m.mk_var(m_idx++, sorts[i].get()); + if (valid[i] && sorts[i] && !revsub[i].get()) { + revsub[i] = m.mk_var(m_idx++, sorts[i]); } } var_subst vs(m, false); @@ -112,7 +112,7 @@ namespace datalog { app_ref pred(m), head(m); expr_ref fml1(m), fml2(m), fml(m); app_ref_vector tail(m); - sort_ref_vector sorts1(m), sorts2(m); + ptr_vector sorts1, sorts2; expr_ref_vector conjs1(m), conjs(m); rule_ref res(rm); bool_rewriter bwr(m); diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.cpp b/src/muz_qe/dl_mk_extract_quantifiers2.cpp new file mode 100644 index 000000000..97976a6be --- /dev/null +++ b/src/muz_qe/dl_mk_extract_quantifiers2.cpp @@ -0,0 +1,366 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_extract_quantifiers2.cpp + +Abstract: + + Remove universal quantifiers over interpreted predicates in the body. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-21 + +Revision History: + +--*/ + +#include"dl_mk_extract_quantifiers2.h" +#include"ast_pp.h" +#include"dl_bmc_engine.h" +#include"smt_quantifier.h" +#include"smt_context.h" + +namespace datalog { + + + mk_extract_quantifiers2::mk_extract_quantifiers2(context & ctx) : + rule_transformer::plugin(101, false), + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + m_query_pred(m), + m_quantifiers(m), + m_refs(m) + {} + + mk_extract_quantifiers2::~mk_extract_quantifiers2() { + reset(); + } + + void mk_extract_quantifiers2::set_query(func_decl* q) { + m_query_pred = q; + } + + bool mk_extract_quantifiers2::matches_signature(func_decl* head, expr_ref_vector const& binding) { + unsigned sz = head->get_arity(); + if (sz != binding.size()) { + return false; + } + for (unsigned i = 0; i < sz; ++i) { + if (head->get_domain(i) != m.get_sort(binding[sz-i-1])) { + return false; + } + } + return true; + } + + bool mk_extract_quantifiers2::matches_quantifier(quantifier* q, expr_ref_vector const& binding) { + unsigned sz = q->get_num_decls(); + if (sz != binding.size()) { + return false; + } + for (unsigned i = 0; i < sz; ++i) { + if (q->get_decl_sort(i) != m.get_sort(binding[sz-i-1])) { + return false; + } + } + return true; + } + + bool mk_extract_quantifiers2::mk_abstract_expr(expr_ref& term) { + if (!is_app(term)) { + return false; + } + expr* r; + if (m_map.find(term, r)) { + term = r; + return true; + } + if (to_app(term)->get_family_id() == null_family_id) { + return false; + } + expr_ref_vector args(m); + expr_ref tmp(m); + for (unsigned i = 0; i < to_app(term)->get_num_args(); ++i) { + tmp = to_app(term)->get_arg(i); + if (!mk_abstract_expr(tmp)) { + return false; + } + args.push_back(tmp); + } + tmp = m.mk_app(to_app(term)->get_decl(), args.size(), args.c_ptr()); + m_refs.push_back(tmp); + m_map.insert(term, tmp); + term = tmp; + return true; + } + + bool mk_extract_quantifiers2::mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result) { + for (unsigned i = 0; i < binding.size(); ++i) { + expr_ref tmp(m); + tmp = binding[i]; + if (!mk_abstract_expr(tmp)) { + return false; + } + result.push_back(tmp); + } + return true; + } + + void mk_extract_quantifiers2::mk_abstraction_map(rule& r, expr_ref_vector const& binding) { + m_map.reset(); + unsigned sz = binding.size(); + SASSERT(sz == r.get_decl()->get_arity()); + for (unsigned i = 0; i < sz; ++i) { + m_map.insert(binding[sz-i-1], r.get_head()->get_arg(i)); + SASSERT(m.get_sort(binding[sz-i-1]) == m.get_sort(r.get_head()->get_arg(i))); + } + // todo: also make bindings for variables in rule body. + } + + void mk_extract_quantifiers2::match_bindings(unsigned i, unsigned j, unsigned k) { + expr_ref_vector resb(m); + rule* r = m_qrules[i]; + quantifier* q = m_quantifiers[i].get(); + expr_ref_vector const& ruleb = m_rule_bindings[i][j]; + expr_ref_vector const& quantb = m_quantifier_bindings[i][k]; + mk_abstraction_map(*r, ruleb); + if (!mk_abstract_binding(quantb, resb)) { + return; + } + expr_ref inst(m), tmp(m); + var_shifter shift(m); + + for (unsigned l = 0; l < resb.size(); ++l) { + tmp = resb[l].get(); + shift(tmp, q->get_num_decls(), tmp); + resb[l] = tmp; + } + + instantiate(m, q, resb.c_ptr(), inst); + if (!m_seen.contains(r)) { + m_seen.insert(r, alloc(obj_hashtable)); + } + obj_hashtable& seen = *m_seen.find(r); + if (seen.contains(inst)) { + return; + } + seen.insert(inst); + m_refs.push_back(inst); + if (!m_quantifier_instantiations.contains(r, q)) { + m_quantifier_instantiations.insert(r, q, alloc(expr_ref_vector, m)); + } + expr_ref_vector* vec = 0; + VERIFY(m_quantifier_instantiations.find(r, q, vec)); + vec->push_back(inst); + TRACE("dl", tout << "matched: " << mk_pp(q, m) << "\n" << mk_pp(inst, m) << "\n";); + } + + app_ref mk_extract_quantifiers2::ensure_app(expr* e) { + if (is_app(e)) { + return app_ref(to_app(e), m); + } + else { + return app_ref(m.mk_eq(e, m.mk_true()), m); + } + } + + void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) { + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + bool has_quantifier = false; + expr_ref_vector conjs(m); + for (unsigned i = utsz; i < tsz; ++i) { + conjs.push_back(r.get_tail(i)); + } + datalog::flatten_and(conjs); + for (unsigned j = 0; j < conjs.size(); ++j) { + expr* e = conjs[j].get(); + quantifier* q; + if (rule_manager::is_forall(m, e, q)) { + m_quantifiers.push_back(q); + m_qrules.push_back(&r); + m_rule_bindings.push_back(vector()); + m_quantifier_bindings.push_back(vector()); + has_quantifier = true; + } + } + if (!has_quantifier) { + new_rules.add_rule(&r); + } + } + + void mk_extract_quantifiers2::apply(rule& r, rule_set& new_rules) { + expr_ref_vector tail(m), conjs(m); + expr_ref fml(m); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + for (unsigned i = 0; i < utsz; ++i) { + SASSERT(!r.is_neg_tail(i)); + tail.push_back(r.get_tail(i)); + } + bool has_quantifier = false; + for (unsigned i = utsz; i < tsz; ++i) { + conjs.push_back(r.get_tail(i)); + } + datalog::flatten_and(conjs); + for (unsigned j = 0; j < conjs.size(); ++j) { + expr* e = conjs[j].get(); + quantifier* q; + if (rule_manager::is_forall(m, e, q)) { + expr_ref_vector* ls; + if (m_quantifier_instantiations.find(&r,q,ls)) { + tail.append(*ls); + } + has_quantifier = true; + } + else { + tail.push_back(e); + } + } + if (has_quantifier) { + fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head()); + rule_ref_vector rules(rm); + rm.mk_rule(fml, rules, r.name()); + for (unsigned i = 0; i < rules.size(); ++i) { + new_rules.add_rule(rules[i].get()); + } + } + } + +#if 0 + class mk_extract_quantifiers2::instance_plugin : public smt::quantifier_instance_plugin { + mk_extract_quantifiers2& ex; + ast_manager& m; + expr_ref_vector m_refs; + obj_hashtable m_bindings; + public: + instance_plugin(mk_extract_quantifiers2& ex): ex(ex), m(ex.m), m_refs(m) {} + + virtual void operator()(quantifier* q, unsigned num_bindings, smt::enode*const* bindings) { + expr_ref_vector binding(m); + ptr_vector sorts; + for (unsigned i = 0; i < num_bindings; ++i) { + binding.push_back(bindings[i]->get_owner()); + sorts.push_back(m.get_sort(binding[i].get())); + } + func_decl* f = m.mk_func_decl(symbol("T"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort()); + expr_ref tup(m); + tup = m.mk_app(f, binding.size(), binding.c_ptr()); + if (!m_bindings.contains(tup)) { + m_bindings.insert(tup); + m_refs.push_back(tup); + ex.m_bindings.push_back(binding); + TRACE("dl", tout << "insert\n" << mk_pp(q, m) << "\n" << mk_pp(tup, m) << "\n";); + } + } + }; + +#endif + + void mk_extract_quantifiers2::reset() { + { + obj_pair_map::iterator + it = m_quantifier_instantiations.begin(), + end = m_quantifier_instantiations.end(); + for (; it != end; ++it) { + dealloc(it->get_value()); + } + } + { + obj_map*>::iterator + it = m_seen.begin(), + end = m_seen.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + } + m_quantifier_instantiations.reset(); + m_seen.reset(); + m_has_quantifiers = false; + m_quantifiers.reset(); + m_qrules.reset(); + m_bindings.reset(); + m_rule_bindings.reset(); + m_quantifier_bindings.reset(); + m_refs.reset(); + } + + rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + reset(); + rule_set::iterator it = source.begin(), end = source.end(); + for (; !m_has_quantifiers && it != end; ++it) { + m_has_quantifiers = (*it)->has_quantifiers(); + } + if (!m_has_quantifiers) { + return 0; + } + + rule_set* rules = alloc(rule_set, m_ctx); + it = source.begin(); + for (; it != end; ++it) { + extract(**it, *rules); + } + + bmc bmc(m_ctx); + expr_ref_vector fmls(m); + bmc.compile(source, fmls, 0); // TBD: use cancel_eh to terminate without base-case. + bmc.compile(source, fmls, 1); + bmc.compile(source, fmls, 2); +// bmc.compile(source, fmls, 3); + expr_ref query = bmc.compile_query(m_query_pred, 2); + fmls.push_back(query); + smt_params fparams; + fparams.m_relevancy_lvl = 0; + fparams.m_model = true; + fparams.m_model_compact = true; + fparams.m_mbqi = true; + smt::kernel solver(m, fparams); + TRACE("dl", + for (unsigned i = 0; i < fmls.size(); ++i) { + tout << mk_pp(fmls[i].get(), m) << "\n"; + }); + + for (unsigned i = 0; i < fmls.size(); ++i) { + solver.assert_expr(fmls[i].get()); + } +#if 0 + smt::context& ctx = solver.get_context(); + smt::quantifier_manager* qm = ctx.get_quantifier_manager(); + qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this)); +#endif + lbool res = solver.check(); + + for (unsigned i = 0; i < m_bindings.size(); ++i) { + expr_ref_vector& binding = m_bindings[i]; + for (unsigned j = 0; j < m_qrules.size(); ++j) { + rule* r = m_qrules[j]; + if (matches_signature(r->get_decl(), binding)) { + m_rule_bindings[j].push_back(binding); + } + else if (matches_quantifier(m_quantifiers[j].get(), binding)) { + m_quantifier_bindings[j].push_back(binding); + } + } + } + for (unsigned i = 0; i < m_qrules.size(); ++i) { + for (unsigned j = 0; j < m_rule_bindings[i].size(); ++j) { + for (unsigned k = 0; k < m_quantifier_bindings[i].size(); ++k) { + match_bindings(i, j, k); + } + } + } + it = source.begin(); + for (; it != end; ++it) { + apply(**it, *rules); + } + + return rules; + } + +}; + + diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.h b/src/muz_qe/dl_mk_extract_quantifiers2.h new file mode 100644 index 000000000..30c15b313 --- /dev/null +++ b/src/muz_qe/dl_mk_extract_quantifiers2.h @@ -0,0 +1,91 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_extract_quantifiers2.h + +Abstract: + + Replace universal quantifiers over interpreted predicates in the body + by instantiations mined using bounded model checking search. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-21 + +Revision History: + +--*/ +#ifndef _DL_MK_EXTRACT_QUANTIFIERS2_H_ +#define _DL_MK_EXTRACT_QUANTIFIERS2_H_ + +#include"dl_context.h" +#include"dl_rule_set.h" +#include"dl_rule_transformer.h" +#include"obj_pair_hashtable.h" + +namespace datalog { + + /** + \brief Extract universal quantifiers from rules. + */ + class mk_extract_quantifiers2 : public rule_transformer::plugin { + context& m_ctx; + ast_manager& m; + rule_manager& rm; + func_decl_ref m_query_pred; + quantifier_ref_vector m_quantifiers; + ptr_vector m_qrules; + vectorm_bindings; + vector > m_rule_bindings; + vector > m_quantifier_bindings; + obj_pair_map m_quantifier_instantiations; + obj_map*> m_seen; + + bool m_has_quantifiers; + obj_map m_map; + expr_ref_vector m_refs; + + class instance_plugin; + + void reset(); + + void extract(rule& r, rule_set& new_rules); + + void apply(rule& r, rule_set& new_rules); + + app_ref ensure_app(expr* e); + + bool matches_signature(func_decl* head, expr_ref_vector const& binding); + + bool matches_quantifier(quantifier* q, expr_ref_vector const& binding); + + void match_bindings(unsigned i, unsigned j, unsigned k); + + bool mk_abstract_expr(expr_ref& term); + + bool mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result); + + void mk_abstraction_map(rule& r, expr_ref_vector const& binding); + + public: + /** + \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). + */ + mk_extract_quantifiers2(context & ctx); + + virtual ~mk_extract_quantifiers2(); + + void set_query(func_decl* q); + + rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + + bool has_quantifiers() { return m_has_quantifiers; } + + }; + +}; + +#endif /* _DL_MK_EXTRACT_QUANTIFIERS2_H_ */ + diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index fa532ee6c..24ddd9ba5 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -136,14 +136,14 @@ namespace datalog { expr_ref_vector rule_unifier::get_rule_subst(const rule& r, bool is_tgt) { SASSERT(m_ready); expr_ref_vector result(m); - sort_ref_vector sorts(m); + ptr_vector sorts; expr_ref v(m), w(m); r.get_vars(sorts); for (unsigned i = 0; i < sorts.size(); ++i) { - if (!sorts[i].get()) { + if (!sorts[i]) { sorts[i] = m.mk_bool_sort(); } - v = m.mk_var(i, sorts[i].get()); + v = m.mk_var(i, sorts[i]); m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w); result.push_back(w); } diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index dedd37a78..bd7131fea 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -41,6 +41,7 @@ Revision History: #include"expr_replacer.h" #include"bool_rewriter.h" #include"qe_lite.h" +#include"expr_safe_replace.h" namespace datalog { @@ -130,17 +131,15 @@ namespace datalog { return index; } // replace vars by de-bruijn indices - expr_substitution sub(m); + expr_safe_replace rep(m); for (unsigned i = 0; i < vars.size(); ++i) { app* v = vars[i].get(); if (names) { names->push_back(v->get_decl()->get_name()); } - sub.insert(v, m.mk_var(index++,m.get_sort(v))); + rep.insert(v, m.mk_var(index++,m.get_sort(v))); } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - (*rep)(fml); + rep(fml); return index; } @@ -936,7 +935,7 @@ namespace datalog { } } - void rule::get_vars(sort_ref_vector& sorts) const { + void rule::get_vars(ptr_vector& sorts) const { sorts.reset(); used_vars used; get_used_vars(used); diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index 79a46052c..a9e360344 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -244,7 +244,7 @@ namespace datalog { void norm_vars(rule_manager & rm); - void get_vars(sort_ref_vector& sorts) const; + void get_vars(ptr_vector& sorts) const; void to_formula(expr_ref& result) const; diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 2816a58d4..9233f6314 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -440,7 +440,7 @@ namespace pdr { unsigned ut_size = r.get_uninterpreted_tail_size(); unsigned t_size = r.get_tail_size(); var_subst vs(m, false); - sort_ref_vector vars(m); + ptr_vector vars; uint_set empty_index_set; qe_lite qe(m);