From ab73c20757c9f57ea708aabac264f019f1b75725 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Mar 2013 17:53:18 -0700 Subject: [PATCH] add Karr linear invariants as transformer Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 62 +-- src/muz_qe/dl_context.h | 6 +- src/muz_qe/dl_mk_array_blast.h | 2 +- src/muz_qe/dl_mk_karr_invariants.cpp | 612 +++++++++++++++++++++++++++ src/muz_qe/dl_mk_karr_invariants.h | 79 ++++ src/muz_qe/dl_rule.cpp | 9 + src/muz_qe/dl_rule.h | 1 + src/muz_qe/dl_rule_transformer.cpp | 39 +- src/muz_qe/dl_rule_transformer.h | 25 +- src/muz_qe/fixedpoint_params.pyg | 1 + src/muz_qe/hilbert_basis.cpp | 1 + src/muz_qe/pdr_context.cpp | 4 + src/muz_qe/pdr_util.cpp | 43 +- src/muz_qe/pdr_util.h | 2 + 14 files changed, 830 insertions(+), 56 deletions(-) create mode 100644 src/muz_qe/dl_mk_karr_invariants.cpp create mode 100644 src/muz_qe/dl_mk_karr_invariants.h diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 7c9d2c965..53231e7b0 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -45,6 +45,7 @@ Revision History: #include"dl_mk_partial_equiv.h" #include"dl_mk_bit_blast.h" #include"dl_mk_array_blast.h" +#include"dl_mk_karr_invariants.h" #include"datatype_decl_plugin.h" #include"expr_abstract.h" @@ -223,6 +224,7 @@ namespace datalog { m_rewriter(m), m_var_subst(m), m_rule_manager(*this), + m_transf(*this), m_trail(*this), m_pinned(m), m_vars(m), @@ -825,23 +827,23 @@ namespace datalog { } void context::transform_rules(model_converter_ref& mc, proof_converter_ref& pc) { - rule_transformer transf(*this); - transf.register_plugin(alloc(mk_filter_rules,*this)); - transf.register_plugin(alloc(mk_simple_joins,*this)); + m_transf.reset(); + m_transf.register_plugin(alloc(mk_filter_rules,*this)); + m_transf.register_plugin(alloc(mk_simple_joins,*this)); if (unbound_compressor()) { - transf.register_plugin(alloc(mk_unbound_compressor,*this)); + m_transf.register_plugin(alloc(mk_unbound_compressor,*this)); } if (similarity_compressor()) { - transf.register_plugin(alloc(mk_similarity_compressor, *this, + m_transf.register_plugin(alloc(mk_similarity_compressor, *this, similarity_compressor_threshold())); } - transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); + m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); - transform_rules(transf, mc, pc); + transform_rules(m_transf, mc, pc); } - + void context::transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc) { SASSERT(m_closed); //we must finish adding rules before we start transforming them TRACE("dl", display_rules(tout);); @@ -862,32 +864,33 @@ namespace datalog { void context::apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc) { ensure_closed(); - datalog::rule_transformer transf(*this); - transf.register_plugin(alloc(datalog::mk_coi_filter, *this)); - transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this)); + m_transf.reset(); + m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this)); + m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 35005)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 35000)); - transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34990)); - transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34980)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 35005)); + m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 35000)); + m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34990)); + m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34980)); //and another round of inlining - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34975)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34970)); - transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34960)); - transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34950)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34975)); + m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34970)); + m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34960)); + m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34950)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34940)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34930)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34920)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34910)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34900)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34940)); + m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34930)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34920)); + m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34910)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34900)); + m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890)); + m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); - transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); - transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); - transform_rules(transf, mc, pc); + m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); + m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); + m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); + transform_rules(m_transf, mc, pc); } void context::collect_params(param_descrs& p) { @@ -928,6 +931,7 @@ namespace datalog { void context::cancel() { m_cancel = true; + m_transf.cancel(); if (m_pdr.get()) m_pdr->cancel(); if (m_bmc.get()) m_bmc->cancel(); if (m_rel.get()) m_rel->cancel(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 98380c9c8..b587daf7f 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -45,11 +45,10 @@ Revision History: #include"proof_converter.h" #include"model2expr.h" #include"smt_params.h" +#include"dl_rule_transformer.h" namespace datalog { - class rule_transformer; - enum execution_result { OK, TIMEOUT, @@ -85,6 +84,7 @@ namespace datalog { th_rewriter m_rewriter; var_subst m_var_subst; rule_manager m_rule_manager; + rule_transformer m_transf; trail_stack m_trail; ast_ref_vector m_pinned; @@ -314,7 +314,7 @@ namespace datalog { void ensure_opened(); void transform_rules(model_converter_ref& mc, proof_converter_ref& pc); - void transform_rules(rule_transformer& trans, model_converter_ref& mc, proof_converter_ref& pc); + void transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc); void replace_rules(rule_set & rs); void apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc); diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h index 1618e4fa8..c0bb39da0 100644 --- a/src/muz_qe/dl_mk_array_blast.h +++ b/src/muz_qe/dl_mk_array_blast.h @@ -49,7 +49,7 @@ namespace datalog { public: /** - \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). + \brief Create rule transformer that removes array stores and selects by ackermannization. */ mk_array_blast(context & ctx, unsigned priority); diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp new file mode 100644 index 000000000..4ed959137 --- /dev/null +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -0,0 +1,612 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_karr_invariants.cpp + +Abstract: + + Extract integer linear invariants. + + The linear invariants are extracted according to Karr's method. + A short description is in + Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation + of Invariants and Intermediate Assertions, in CP 95. + + The algorithm is here adapted to Horn clauses. + The idea is to maintain two data-structures for each recursive relation. + We call them R and RD + - R - set of linear congruences that are true of R. + - RD - the dual basis of of solutions for R. + + RD is updated by accumulating basis vectors for solutions + to R (the homogeneous dual of R) + R is updated from the inhomogeneous dual of RD. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-03-09 + +Revision History: + +--*/ + +#include"dl_mk_karr_invariants.h" + +namespace datalog { + + mk_karr_invariants::mk_karr_invariants(context & ctx, unsigned priority): + rule_transformer::plugin(priority, false), + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + a(m) { + } + + mk_karr_invariants::~mk_karr_invariants() { + obj_map::iterator it = m_constraints.begin(), end = m_constraints.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + it = m_dual_constraints.begin(); + end = m_dual_constraints.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + } + + mk_karr_invariants::matrix& mk_karr_invariants::matrix::operator=(matrix const& other) { + reset(); + append(other); + return *this; + } + + void mk_karr_invariants::matrix::display(std::ostream& out) const { + for (unsigned i = 0; i < A.size(); ++i) { + for (unsigned j = 0; j < A[i].size(); ++j) { + out << A[i][j] << " "; + } + out << (eq[i]?" = ":" >= ") << -b[i] << "\n"; + } + } + + bool mk_karr_invariants::is_linear(expr* e, vector& row, rational& b, rational const& mul) { + if (!a.is_int(e)) { + return false; + } + if (is_var(e)) { + row[to_var(e)->get_idx()] += mul; + return true; + } + if (!is_app(e)) { + return false; + } + rational n; + if (a.is_numeral(e, n)) { + b += mul*n; + return true; + } + if (a.is_add(e)) { + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + if (!is_linear(to_app(e)->get_arg(i), row, b, mul)) { + return false; + } + } + return true; + } + expr* e1, *e2; + if (a.is_sub(e, e1, e2)) { + return is_linear(e1, row, b, mul) && is_linear(e2, row, b, -mul); + } + if (a.is_mul(e, e1, e2) && a.is_numeral(e1, n)) { + return is_linear(e2, row, b, mul*n); + } + if (a.is_mul(e, e1, e2) && a.is_numeral(e2, n)) { + return is_linear(e1, row, b, mul*n); + } + if (a.is_uminus(e, e1)) { + return is_linear(e1, row, b, -mul); + } + return false; + } + + mk_karr_invariants::matrix* mk_karr_invariants::get_constraints(func_decl* p) { + matrix* result = 0; + m_constraints.find(p, result); + return result; + } + + mk_karr_invariants::matrix& mk_karr_invariants::get_dual_constraints(func_decl* p) { + matrix* result = 0; + if (!m_dual_constraints.find(p, result)) { + result = alloc(matrix); + m_dual_constraints.insert(p, result); + } + return *result; + } + + bool mk_karr_invariants::is_eq(expr* e, var*& v, rational& n) { + expr* e1, *e2; + if (!m.is_eq(e, e1, e2)) { + return false; + } + if (!is_var(e1)) { + std::swap(e1, e2); + } + if (!is_var(e1)) { + return false; + } + v = to_var(e1); + if (!a.is_numeral(e2, n)) { + return false; + } + return true; + } + + bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) { + unsigned num_vars = rm.get_var_counter().get_max_var(r)+1; + unsigned arity = r.get_decl()->get_arity(); + unsigned num_columns = arity + num_vars; + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + M.reset(); + + for (unsigned i = 0; i < utsz; ++i) { + matrix const* Mp = get_constraints(r.get_decl(i)); + if (!Mp) { + return false; + } + TRACE("dl", Mp->display(tout << "Intersect\n");); + intersect_matrix(r.get_tail(i), *Mp, num_columns, M); + } + + rational one(1), mone(-1); + expr* e1, *e2, *en; + var* v, *w; + rational n1, n2; + 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 i = 0; i < conjs.size(); ++i) { + expr* e = conjs[i].get(); + rational b(0); + vector row; + row.resize(num_columns, rational(0)); + bool processed = true; + if (m.is_eq(e, e1, e2) && is_linear(e1, row, b, one) && is_linear(e2, row, b, mone)) { + M.A.push_back(row); + M.b.push_back(b); + M.eq.push_back(true); + } + else if ((a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) { + M.A.push_back(row); + M.b.push_back(b); + M.eq.push_back(false); + } + else if ((a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) { + M.A.push_back(row); + M.b.push_back(b + rational(1)); + M.eq.push_back(false); + } + else if (m.is_not(e, en) && (a.is_lt(en, e2, e1) || a.is_gt(en, e1, e2)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) { + M.A.push_back(row); + M.b.push_back(b); + M.eq.push_back(false); + } + else if (m.is_not(e, en) && (a.is_le(en, e2, e1) || a.is_ge(en, e1, e2)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) { + M.A.push_back(row); + M.b.push_back(b + rational(1)); + M.eq.push_back(false); + } + else if (m.is_or(e, e1, e2) && is_eq(e1, v, n1) && is_eq(e2, w, n2) && v == w) { + if (n1 > n2) { + std::swap(n1, n2); + } + SASSERT(n1 <= n2); + row[v->get_idx()] = rational(1); + // v - n1 >= 0 + M.A.push_back(row); + M.b.push_back(-n1); + M.eq.push_back(false); + // -v + n2 >= 0 + row[v->get_idx()] = rational(-1); + M.A.push_back(row); + M.b.push_back(n2); + M.eq.push_back(false); + } + else { + processed = false; + } + TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";); + } + // intersect with the head predicate. + app* head = r.get_head(); + unsigned sz0 = M.A.size(); + for (unsigned i = 0; i < arity; ++i) { + rational n; + expr* arg = head->get_arg(i); + if (!a.is_int(arg)) { + // no-op + } + else if (is_var(arg)) { + vector row; + row.resize(num_columns, rational(0)); + unsigned idx = to_var(arg)->get_idx(); + row[idx] = rational(-1); + row[num_vars + i] = rational(1); + M.A.push_back(row); + M.b.push_back(rational(0)); + M.eq.push_back(true); + } + else if (a.is_numeral(arg, n)) { + vector row; + row.resize(num_columns, rational(0)); + row[num_vars + i] = rational(1); + M.A.push_back(row); + M.b.push_back(-n); + M.eq.push_back(true); + } + else { + UNREACHABLE(); + } + } + if (M.A.size() == sz0) { + return false; + } + + TRACE("dl", M.display(tout << r.get_decl()->get_name() << "\n");); + matrix MD; + dualizeI(MD, M); + M.reset(); + // project for variables in head. + for (unsigned i = 0; i < MD.size(); ++i) { + vector row; + row.append(arity, MD.A[i].c_ptr() + num_vars); + M.A.push_back(row); + M.b.push_back(MD.b[i]); + M.eq.push_back(true); + } + + return true; + } + + void mk_karr_invariants::intersect_matrix(app* p, matrix const& Mp, unsigned num_columns, matrix& M) { + for (unsigned j = 0; j < Mp.size(); ++j) { + rational b = Mp.b[j], n; + vector row; + row.resize(num_columns, rational(0)); + for (unsigned i = 0; i < p->get_num_args(); ++i) { + expr* arg = p->get_arg(i); + if (!a.is_int(arg)) { + // no-op + } + else if (is_var(arg)) { + unsigned idx = to_var(arg)->get_idx(); + row[idx] += Mp.A[j][i]; + } + else if (a.is_numeral(arg, n)) { + b += Mp.A[j][i]*n; + } + else { + UNREACHABLE(); + } + } + M.A.push_back(row); + M.b.push_back(b); + M.eq.push_back(Mp.eq[j]); + } + } + + // treat src as a homogeneous matrix. + void mk_karr_invariants::dualizeH(matrix& dst, matrix const& src) { + dst.reset(); + if (src.size() == 0) { + return; + } + m_hb.reset(); + for (unsigned i = 0; i < src.size(); ++i) { + vector v(src.A[i]); + v.append(src.b[i]); + if (src.eq[i]) { + m_hb.add_eq(v, rational(0)); + } + else { + m_hb.add_ge(v, rational(0)); + } + } + for (unsigned i = 0; i < 1 + src.A[0].size(); ++i) { + m_hb.set_is_int(i); + } + lbool is_sat = m_hb.saturate(); + TRACE("dl", m_hb.display(tout);); + SASSERT(is_sat == l_true); + unsigned basis_size = m_hb.get_basis_size(); + bool first_initial = true; + for (unsigned i = 0; i < basis_size; ++i) { + bool is_initial; + vector soln; + m_hb.get_basis_solution(i, soln, is_initial); + if (!is_initial) { + dst.b.push_back(soln.back()); + dst.eq.push_back(true); + soln.pop_back(); + dst.A.push_back(soln); + } + } + } + + // treat src as an inhomegeneous matrix. + void mk_karr_invariants::dualizeI(matrix& dst, matrix const& src) { + m_hb.reset(); + for (unsigned i = 0; i < src.size(); ++i) { + if (src.eq[i]) { + m_hb.add_eq(src.A[i], -src.b[i]); + } + else { + m_hb.add_ge(src.A[i], -src.b[i]); + } + } + for (unsigned i = 0; !src.A.empty() && i < src.A[0].size(); ++i) { + m_hb.set_is_int(i); + } + lbool is_sat = m_hb.saturate(); + TRACE("dl", m_hb.display(tout);); + SASSERT(is_sat == l_true); + dst.reset(); + unsigned basis_size = m_hb.get_basis_size(); + bool first_initial = true; + for (unsigned i = 0; i < basis_size; ++i) { + bool is_initial; + vector soln; + m_hb.get_basis_solution(i, soln, is_initial); + if (is_initial && first_initial) { + dst.A.push_back(soln); + dst.b.push_back(rational(1)); + dst.eq.push_back(true); + first_initial = false; + } + else if (!is_initial) { + dst.A.push_back(soln); + dst.b.push_back(rational(0)); + dst.eq.push_back(true); + } + } + } + + void mk_karr_invariants::update_body(rule_set& rules, rule& r){ + func_decl* p = r.get_decl(); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + app_ref_vector tail(m); + for (unsigned i = 0; i < tsz; ++i) { + tail.push_back(r.get_tail(i)); + } + for (unsigned i = 0; i < utsz; ++i) { + func_decl* q = r.get_decl(i); + matrix* N = get_constraints(q); + if (!N) { + continue; + } + expr_ref zero(m), lhs(m); + zero = a.mk_numeral(rational(0), true); + for (unsigned j = 0; j < N->size(); ++j) { + rational n; + SASSERT(N->A[j].size() == q->get_arity()); + expr_ref_vector sum(m); + for (unsigned k = 0; k < N->A[j].size(); ++k) { + n = N->A[j][k]; + if (!n.is_zero()) { + expr* arg = r.get_tail(i)->get_arg(k); + sum.push_back(a.mk_mul(a.mk_numeral(n, true), arg)); + } + } + n = N->b[j]; + if (!n.is_zero()) { + sum.push_back(a.mk_numeral(n, true)); + } + lhs = a.mk_add(sum.size(), sum.c_ptr()); + if (N->eq[j]) { + tail.push_back(m.mk_eq(lhs, zero)); + } + else { + tail.push_back(a.mk_ge(lhs, zero)); + } + } + } + rule* new_rule = &r; + if (tail.size() != tsz) { + new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name()); + } + rules.add_rule(new_rule); + } + + class mk_karr_invariants::add_invariant_model_converter : public model_converter { + ast_manager& m; + arith_util a; + func_decl_ref_vector m_funcs; + ptr_vector m_invs; + public: + + add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m) {} + + virtual ~add_invariant_model_converter() { + for (unsigned i = 0; i < m_invs.size(); ++i) { + dealloc(m_invs[i]); + } + } + + void add(func_decl* p, matrix& M) { + m_funcs.push_back(p); + m_invs.push_back(alloc(matrix, M)); + } + + virtual void operator()(model_ref & mr) { + for (unsigned i = 0; i < m_funcs.size(); ++i) { + func_decl* p = m_funcs[i].get(); + func_interp* f = mr->get_func_interp(p); + expr_ref body(m); + unsigned arity = p->get_arity(); + SASSERT(0 < arity); + if (f) { + matrix const& M = *m_invs[i]; + mk_body(M, body); + SASSERT(f->num_entries() == 0); + if (!f->is_partial()) { + body = m.mk_and(f->get_else(), body); + } + } + else { + f = alloc(func_interp, m, arity); + mr->register_decl(p, f); + body = m.mk_false(); // fragile: assume that relation was pruned by being infeasible. + } + f->set_else(body); + } + } + + virtual model_converter * translate(ast_translation & translator) { + add_invariant_model_converter* mc = alloc(add_invariant_model_converter, m); + for (unsigned i = 0; i < m_funcs.size(); ++i) { + mc->add(translator(m_funcs[i].get()), *m_invs[i]); + } + return mc; + } + + private: + void mk_body(matrix const& M, expr_ref& body) { + expr_ref_vector conj(m); + for (unsigned i = 0; i < M.size(); ++i) { + mk_body(M.A[i], M.b[i], M.eq[i], conj); + } + body = m.mk_and(conj.size(), conj.c_ptr()); + } + + void mk_body(vector const& row, rational const& b, bool is_eq, expr_ref_vector& conj) { + expr_ref_vector sum(m); + expr_ref zero(m), lhs(m); + zero = a.mk_numeral(rational(0), true); + + for (unsigned i = 0; i < row.size(); ++i) { + if (row[i].is_zero()) { + continue; + } + var* var = m.mk_var(i, a.mk_int()); + if (row[i].is_one()) { + sum.push_back(var); + } + else { + sum.push_back(a.mk_mul(a.mk_numeral(row[i], true), var)); + } + } + if (!b.is_zero()) { + sum.push_back(a.mk_numeral(b, true)); + } + lhs = a.mk_add(sum.size(), sum.c_ptr()); + if (is_eq) { + conj.push_back(m.mk_eq(lhs, zero)); + } + else { + conj.push_back(a.mk_ge(lhs, zero)); + } + } + + }; + + void mk_karr_invariants::cancel() { + rule_transformer::plugin::cancel(); + m_hb.set_cancel(true); + } + + rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + if (!m_ctx.get_params().karr()) { + return 0; + } + rule_set::iterator it = source.begin(), end = source.end(); + for (; it != end; ++it) { + rule const& r = **it; + if (r.has_negation()) { + return 0; + } + } + bool change = true, non_empty = false; + while (!m_cancel && change) { + change = false; + it = source.begin(); + for (; it != end; ++it) { + rule const& r = **it; + TRACE("dl", r.display(m_ctx, tout);); + matrix MD, P; + if (!get_transition_relation(r, MD)) { + continue; + } + non_empty = true; + func_decl* p = r.get_decl(); + matrix& ND = get_dual_constraints(p); + matrix* N = get_constraints(p); + ND.append(MD); + dualizeH(P, ND); + + TRACE("dl", + MD.display(tout << "MD\n"); + P.display(tout << "P\n");); + + if (!N) { + change = true; + N = alloc(matrix, P); + m_constraints.insert(p, N); + } + else if (P.size() != N->size()) { + change = true; + *N = P; + } + } + } + + if (!non_empty) { + return 0; + } + + if (m_cancel) { + return 0; + } + + TRACE("dl", + rule_set::decl2rules::iterator git = source.begin_grouped_rules(); + rule_set::decl2rules::iterator gend = source.end_grouped_rules(); + for (; git != gend; ++git) { + func_decl* p = git->m_key; + matrix* M = get_constraints(p); + tout << p->get_name() << "\n"; + if (M) { + M->display(tout); + } + }); + + rule_set* rules = alloc(rule_set, m_ctx); + it = source.begin(); + for (; it != end; ++it) { + update_body(*rules, **it); + } + if (mc) { + add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m); + rule_set::decl2rules::iterator git = source.begin_grouped_rules(); + rule_set::decl2rules::iterator gend = source.end_grouped_rules(); + for (; git != gend; ++git) { + func_decl* p = git->m_key; + matrix* M = get_constraints(p); + if (M) { + kmc->add(p, *M); + } + } + mc = concat(mc.get(), kmc); + } + TRACE("dl", rules->display(tout);); + return rules; + } + +}; + diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h new file mode 100644 index 000000000..3b82578a4 --- /dev/null +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -0,0 +1,79 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_karr_invariants.h + +Abstract: + + Extract integer linear invariants. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-03-08 + +Revision History: + +--*/ +#ifndef _DL_MK_KARR_INVARIANTS_H_ +#define _DL_MK_KARR_INVARIANTS_H_ + +#include"dl_context.h" +#include"dl_rule_set.h" +#include"dl_rule_transformer.h" +#include"arith_decl_plugin.h" +#include"hilbert_basis.h" + +namespace datalog { + + /** + \brief Rule transformer that strengthens bodies with invariants. + */ + class mk_karr_invariants : public rule_transformer::plugin { + + struct matrix { + vector > A; + vector b; + svector eq; + unsigned size() const { return A.size(); } + void reset() { A.reset(); b.reset(); eq.reset(); } + matrix& operator=(matrix const& other); + void append(matrix const& other) { A.append(other.A); b.append(other.b); eq.append(other.eq); } + void display(std::ostream& out) const; + }; + class add_invariant_model_converter; + + context& m_ctx; + ast_manager& m; + rule_manager& rm; + arith_util a; + obj_map m_constraints; + obj_map m_dual_constraints; + hilbert_basis m_hb; + + bool is_linear(expr* e, vector& row, rational& b, rational const& mul); + bool is_eq(expr* e, var*& v, rational& n); + bool get_transition_relation(rule const& r, matrix& M); + void intersect_matrix(app* p, matrix const& Mp, unsigned num_columns, matrix& M); + matrix* get_constraints(func_decl* p); + matrix& get_dual_constraints(func_decl* p); + void dualizeH(matrix& dst, matrix const& src); + void dualizeI(matrix& dst, matrix const& src); + void update_body(rule_set& rules, rule& r); + + public: + mk_karr_invariants(context & ctx, unsigned priority); + + virtual ~mk_karr_invariants(); + + virtual void cancel(); + + rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + + }; + +}; + +#endif /* _DL_MK_KARR_INVARIANTS_H_ */ + diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index d34f8a67f..3814d0b62 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -927,6 +927,15 @@ namespace datalog { return exist || univ; } + bool rule::has_negation() const { + for (unsigned i = 0; i < get_uninterpreted_tail_size(); ++i) { + if (is_neg_tail(i)) { + return true; + } + } + return false; + } + void rule::get_used_vars(used_vars& used) const { used.process(get_head()); unsigned sz = get_tail_size(); diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index a9e360344..c01b36162 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -237,6 +237,7 @@ namespace datalog { bool has_uninterpreted_non_predicates(func_decl*& f) const; void has_quantifiers(bool& existential, bool& universal) const; bool has_quantifiers() const; + bool has_negation() const; /** \brief Store in d the (direct) dependencies of the given rule. diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 5f52e0a39..a246d9d61 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -16,40 +16,55 @@ Author: Revision History: --*/ + #include #include #include"dl_context.h" - #include"dl_rule_transformer.h" namespace datalog { rule_transformer::rule_transformer(context & ctx) - : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false) { + : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false), m_cancel(false) { } rule_transformer::~rule_transformer() { - plugin_vector::iterator it=m_plugins.begin(); - plugin_vector::iterator end=m_plugins.end(); + reset(); + } + + void rule_transformer::reset() { + plugin_vector::iterator it = m_plugins.begin(); + plugin_vector::iterator end = m_plugins.end(); for(; it!=end; ++it) { dealloc(*it); } + m_plugins.reset(); + m_dirty = false; + m_cancel = false; + } + + void rule_transformer::cancel() { + m_cancel = true; + plugin_vector::iterator it = m_plugins.begin(); + plugin_vector::iterator end = m_plugins.end(); + for(; it!=end; ++it) { + (*it)->cancel(); + } } struct rule_transformer::plugin_comparator { bool operator()(rule_transformer::plugin * p1, rule_transformer::plugin * p2) { - return p1->get_priority()>p2->get_priority(); + return p1->get_priority() > p2->get_priority(); } }; void rule_transformer::ensure_ordered() { - if (!m_dirty) { - return; + if (m_dirty) { + std::sort(m_plugins.begin(), m_plugins.end(), plugin_comparator()); + m_dirty = false; } - std::sort(m_plugins.begin(), m_plugins.end(), plugin_comparator()); - m_dirty=false; } void rule_transformer::register_plugin(plugin * p) { @@ -67,9 +82,9 @@ namespace datalog { tout<<"init:\n"; rules.display(tout); ); - plugin_vector::iterator it=m_plugins.begin(); - plugin_vector::iterator end=m_plugins.end(); - for(; it!=end; ++it) { + plugin_vector::iterator it = m_plugins.begin(); + plugin_vector::iterator end = m_plugins.end(); + for(; it!=end && !m_cancel; ++it) { plugin & p = **it; rule_set * new_rules = p(rules, mc, pc); diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h index 1cc41a146..cf1a9be75 100644 --- a/src/muz_qe/dl_rule_transformer.h +++ b/src/muz_qe/dl_rule_transformer.h @@ -28,6 +28,8 @@ Revision History: namespace datalog { + class context; + class rule_transformer { public: class plugin; @@ -37,9 +39,10 @@ namespace datalog { typedef svector plugin_vector; struct plugin_comparator; - context & m_context; - rule_manager & m_rule_manager; - bool m_dirty; + context & m_context; + rule_manager & m_rule_manager; + bool m_dirty; + volatile bool m_cancel; svector m_plugins; void ensure_ordered(); @@ -47,6 +50,13 @@ namespace datalog { rule_transformer(context & ctx); ~rule_transformer(); + + /** + \brief Reset all registered transformers. + */ + void reset(); + + void cancel(); /** \brief Add a plugin for rule transformation. @@ -72,6 +82,8 @@ namespace datalog { void attach(rule_transformer & transformer) { m_transformer = &transformer; } protected: + volatile bool m_cancel; + /** \brief Create a plugin object for rule_transformer. @@ -79,7 +91,8 @@ namespace datalog { (higher priority plugins will be applied first). */ plugin(unsigned priority, bool can_destratify_negation = false) : m_priority(priority), - m_can_destratify_negation(can_destratify_negation), m_transformer(0) {} + m_can_destratify_negation(can_destratify_negation), m_transformer(0), m_cancel(false) {} + public: virtual ~plugin() {} @@ -96,8 +109,10 @@ namespace datalog { model_converter_ref& mc, proof_converter_ref& pc) = 0; + virtual void cancel() { m_cancel = true; } + /** - Removes duplicate tails. + Removes duplicate tails. */ static void remove_duplicate_tails(app_ref_vector& tail, svector& tail_neg); diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c2cfadd14..7a3316c56 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -41,6 +41,7 @@ def_module_params('fixedpoint', ('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"), ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"), ('slice', BOOL, True, "PDR: simplify clause set using slicing"), + ('karr', BOOL, False, "Add linear invariants to clauses using Karr's method"), ('coalesce_rules', BOOL, False, "BMC: coalesce rules"), ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index e7c7928a3..9fbd8cc2e 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -686,6 +686,7 @@ void hilbert_basis::reset() { m_passive2->reset(); m_zero.reset(); m_index->reset(); + m_ints.reset(); m_cancel = false; } diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 30665c6e5..8bdff1800 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1425,6 +1425,7 @@ namespace pdr { bool ok = checker.check(pr, side_conditions); if (!ok) { msg << "proof validation failed"; + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); throw default_exception(msg.str()); } for (unsigned i = 0; i < side_conditions.size(); ++i) { @@ -1437,6 +1438,7 @@ namespace pdr { lbool res = solver.check(); if (res != l_false) { msg << "rule validation failed when checking: " << mk_pp(cond, m); + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); throw default_exception(msg.str()); } } @@ -1488,6 +1490,7 @@ namespace pdr { lbool res = solver.check(); if (res != l_false) { msg << "rule validation failed when checking: " << mk_pp(tmp, m); + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); throw default_exception(msg.str()); } } @@ -1595,6 +1598,7 @@ namespace pdr { catch (unknown_exception) { return l_undef; } + UNREACHABLE(); return l_undef; } diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 1ea705e6e..237cf9415 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -32,7 +32,6 @@ Notes: #include "for_each_expr.h" #include "smt_params.h" #include "model.h" -#include "model_v2_pp.h" #include "ref_vector.h" #include "rewriter.h" #include "rewriter_def.h" @@ -42,6 +41,7 @@ Notes: #include "pdr_util.h" #include "arith_decl_plugin.h" #include "expr_replacer.h" +#include "model_smt2_pp.h" namespace pdr { @@ -510,13 +510,24 @@ namespace pdr { set_x(e); } } + + void model_evaluator::eval_exprs(expr_ref_vector& es) { + model_ref mr(m_model); + for (unsigned j = 0; j < es.size(); ++j) { + if (m_array.is_as_array(es[j].get())) { + es[j] = eval(mr, es[j].get()); + } + } + } bool model_evaluator::extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case) { SASSERT(m_array.is_array(a)); + TRACE("pdr", tout << mk_pp(a, m) << "\n";); while (m_array.is_store(a)) { expr_ref_vector store(m); store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); + eval_exprs(store); stores.push_back(store); a = to_app(a)->get_arg(0); } @@ -526,7 +537,7 @@ namespace pdr { return true; } - if (m_array.is_as_array(a)) { + while (m_array.is_as_array(a)) { func_decl* f = m_array.get_as_array_func_decl(to_app(a)); func_interp* g = m_model->get_func_interp(f); unsigned sz = g->num_entries(); @@ -538,20 +549,30 @@ namespace pdr { store.push_back(fe->get_result()); for (unsigned j = 0; j < store.size(); ++j) { if (!is_ground(store[j].get())) { + TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";); return false; } } + eval_exprs(store); stores.push_back(store); } else_case = g->get_else(); if (!else_case) { + TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";); return false; } if (!is_ground(else_case)) { + TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";); return false; } + if (m_array.is_as_array(else_case)) { + model_ref mr(m_model); + else_case = eval(mr, else_case); + } + TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";); return true; } + TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";); return false; } @@ -570,7 +591,8 @@ namespace pdr { } sort* s = m.get_sort(arg1); sort* r = get_array_range(s); - if (!r->is_infinite() && !r->is_very_big()) { + // give up evaluating finite domain/range arrays + if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); set_x(e); return; @@ -591,6 +613,9 @@ namespace pdr { << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";); set_false(e); } + else if (m_array.is_array(else1)) { + eval_array_eq(e, else1, else2); + } else { TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); set_x(e); @@ -614,18 +639,23 @@ namespace pdr { if (w1 == w2) { continue; } - else if (m.is_value(w1) && m.is_value(w2)) { + if (m.is_value(w1) && m.is_value(w2)) { TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n"; tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n"; tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";); set_false(e); - return; + } + else if (m_array.is_array(w1)) { + eval_array_eq(e, w1, w2); + if (is_true(e)) { + continue; + } } else { TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); set_x(e); - return; } + return; } set_true(e); } @@ -869,6 +899,7 @@ namespace pdr { } if (is_x(form)) { IF_VERBOSE(0, verbose_stream() << "formula undetermined in model: " << mk_pp(form, m) << "\n";); + TRACE("pdr", model_smt2_pp(tout, m, *m_model, 0);); has_x = true; } } diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index 220e56b3c..ddbf0d122 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -104,6 +104,8 @@ namespace pdr { bool check_model(ptr_vector const & formulas); bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case); + + void eval_exprs(expr_ref_vector& es); public: model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}