From 4138e17b3f49d2aad4505128bed9260851cee49e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 31 Mar 2013 16:40:10 -0700 Subject: [PATCH] extract karr invariants as a Datalog relation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_base.h | 1 + src/muz_qe/dl_compiler.cpp | 12 +- src/muz_qe/dl_context.cpp | 4 +- src/muz_qe/dl_interval_relation.cpp | 8 +- src/muz_qe/dl_interval_relation.h | 1 - src/muz_qe/dl_mk_karr_invariants.cpp | 1311 +++++++++++++++++--------- src/muz_qe/dl_mk_karr_invariants.h | 109 ++- src/muz_qe/dl_relation_manager.cpp | 6 + src/muz_qe/dl_relation_manager.h | 1 + src/muz_qe/dl_rule_set.cpp | 160 ++-- src/muz_qe/dl_rule_set.h | 2 + src/muz_qe/hilbert_basis.cpp | 3 +- src/muz_qe/hilbert_basis.h | 5 +- src/muz_qe/rel_context.cpp | 31 +- src/muz_qe/rel_context.h | 2 +- 15 files changed, 1082 insertions(+), 574 deletions(-) diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h index 872bf7565..6c53a4b27 100644 --- a/src/muz_qe/dl_base.h +++ b/src/muz_qe/dl_base.h @@ -233,6 +233,7 @@ namespace datalog { symbol const& get_name() const { return m_name; } + virtual void set_cancel(bool f) {} relation_manager & get_manager() const { return m_manager; } ast_manager& get_ast_manager() const { return datalog::get_ast_manager_from_rel_manager(m_manager); } diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index cc56df4b7..c898f7964 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -1028,21 +1028,23 @@ namespace datalog { func_decl * head_pred = *preds.begin(); const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); + + reg_idx output_delta; - if(!output_deltas.find(head_pred, output_delta)) { + if (!output_deltas.find(head_pred, output_delta)) { output_delta = execution_context::void_register; } rule_vector::const_iterator it = rules.begin(); rule_vector::const_iterator end = rules.end(); - for(; it!=end; ++it) { + for (; it != end; ++it) { rule * r = *it; SASSERT(r->get_head()->get_decl()==head_pred); compile_rule_evaluation(r, input_deltas, output_delta, false, acc); } - if(add_saturation_marks) { + if (add_saturation_marks) { //now the predicate is saturated, so we may mark it as such acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred)); } @@ -1068,7 +1070,7 @@ namespace datalog { for(; sit!=send; ++sit) { func_decl_set & strat_preds = **sit; - if(all_saturated(strat_preds)) { + if (all_saturated(strat_preds)) { //all predicates in stratum are saturated, so no need to compile rules for them continue; } @@ -1084,7 +1086,7 @@ namespace datalog { tout << "\n"; ); - if(is_nonrecursive_stratum(strat_preds)) { + if (is_nonrecursive_stratum(strat_preds)) { //this stratum contains just a single non-recursive rule compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc); } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 71ef7ad20..c667c7775 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -954,6 +954,7 @@ namespace datalog { if (m_pdr.get()) m_pdr->cancel(); if (m_bmc.get()) m_bmc->cancel(); if (m_tab.get()) m_tab->cancel(); + if (m_rel.get()) m_rel->set_cancel(true); } void context::cleanup() { @@ -962,6 +963,7 @@ namespace datalog { if (m_pdr.get()) m_pdr->cleanup(); if (m_bmc.get()) m_bmc->cleanup(); if (m_tab.get()) m_tab->cleanup(); + if (m_rel.get()) m_rel->set_cancel(false); } class context::engine_type_proc { @@ -1231,7 +1233,7 @@ namespace datalog { return m_rel->result_contains_fact(f); } - // TBD: algebraic data-types declarations will not be printed. + // NB: algebraic data-types declarations will not be printed. class free_func_visitor { ast_manager& m; func_decl_set m_funcs; diff --git a/src/muz_qe/dl_interval_relation.cpp b/src/muz_qe/dl_interval_relation.cpp index 150ba1c78..3397f2db0 100644 --- a/src/muz_qe/dl_interval_relation.cpp +++ b/src/muz_qe/dl_interval_relation.cpp @@ -21,6 +21,7 @@ Revision History: #include "optional.h" #include "ast_pp.h" #include "dl_interval_relation.h" +#include "bool_rewriter.h" namespace datalog { @@ -30,8 +31,7 @@ namespace datalog { interval_relation_plugin::interval_relation_plugin(relation_manager& m): relation_plugin(interval_relation_plugin::get_name(), m), m_empty(m_dep), - m_arith(get_ast_manager()), - m_bsimp(get_ast_manager()) { + m_arith(get_ast_manager()) { } bool interval_relation_plugin::can_handle_signature(const relation_signature & sig) { @@ -374,7 +374,6 @@ namespace datalog { void interval_relation::to_formula(expr_ref& fml) const { ast_manager& m = get_plugin().get_ast_manager(); arith_util& arith = get_plugin().m_arith; - basic_simplifier_plugin& bsimp = get_plugin().m_bsimp; expr_ref_vector conjs(m); relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { @@ -405,7 +404,8 @@ namespace datalog { } } } - bsimp.mk_and(conjs.size(), conjs.c_ptr(), fml); + bool_rewriter br(m); + br.mk_and(conjs.size(), conjs.c_ptr(), fml); } diff --git a/src/muz_qe/dl_interval_relation.h b/src/muz_qe/dl_interval_relation.h index 0ff05719e..1a25f430f 100644 --- a/src/muz_qe/dl_interval_relation.h +++ b/src/muz_qe/dl_interval_relation.h @@ -34,7 +34,6 @@ namespace datalog { v_dependency_manager m_dep; interval m_empty; arith_util m_arith; - basic_simplifier_plugin m_bsimp; class join_fn; class project_fn; diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 77b52f2b9..6dca35cdf 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -33,36 +33,35 @@ Revision History: --*/ #include"dl_mk_karr_invariants.h" +#include"expr_safe_replace.h" +#include"bool_rewriter.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()), + m_inner_ctx(m, ctx.get_fparams()), a(m) { + params_ref params; + params.set_sym("default_relation", symbol("karr_relation")); + params.set_sym("engine", symbol("datalog")); + params.set_bool("karr", false); + m_inner_ctx.updt_params(params); } - 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::~mk_karr_invariants() { } - mk_karr_invariants::matrix& mk_karr_invariants::matrix::operator=(matrix const& other) { + matrix& matrix::operator=(matrix const& other) { reset(); append(other); return *this; } - void mk_karr_invariants::matrix::display_row( + void matrix::display_row( std::ostream& out, vector const& row, rational const& b, bool is_eq) { for (unsigned j = 0; j < row.size(); ++j) { out << row[j] << " "; @@ -70,7 +69,7 @@ namespace datalog { out << (is_eq?" = ":" >= ") << -b << "\n"; } - void mk_karr_invariants::matrix::display_ineq( + void matrix::display_ineq( std::ostream& out, vector const& row, rational const& b, bool is_eq) { bool first = true; for (unsigned j = 0; j < row.size(); ++j) { @@ -91,391 +90,31 @@ namespace datalog { out << (is_eq?"= ":">= ") << -b << "\n"; } - void mk_karr_invariants::matrix::display(std::ostream& out) const { + void matrix::display(std::ostream& out) const { for (unsigned i = 0; i < A.size(); ++i) { display_row(out, A[i], b[i], eq[i]); } } - - 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_counter().get_max_rule_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"; - if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back()); - ); - } - // 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); - } - TRACE("dl", M.display(tout << r.get_decl()->get_name() << "\n");); - - 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.push_back(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_verbose", m_hb.display(tout);); - SASSERT(is_sat == l_true); - unsigned basis_size = m_hb.get_basis_size(); - 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_verbose", 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){ - 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); - rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening 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; + expr_ref_vector m_invs; public: - add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m) {} + add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m), m_invs(m) {} - virtual ~add_invariant_model_converter() { - for (unsigned i = 0; i < m_invs.size(); ++i) { - dealloc(m_invs[i]); + virtual ~add_invariant_model_converter() { } + + void add(func_decl* p, expr* inv) { + if (!m.is_true(inv)) { + m_funcs.push_back(p); + m_invs.push_back(inv); } } - 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(); @@ -484,11 +123,9 @@ namespace datalog { 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); + bool_rewriter(m).mk_and(f->get_else(), m_invs[i].get(), body); } } else { @@ -503,7 +140,7 @@ namespace datalog { 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]); + mc->add(translator(m_funcs[i].get()), m_invs[i].get()); } return mc; } @@ -514,7 +151,7 @@ namespace datalog { 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()); + bool_rewriter(m).mk_and(conj.size(), conj.c_ptr(), body); } void mk_body(vector const& row, rational const& b, bool is_eq, expr_ref_vector& conj) { @@ -545,12 +182,10 @@ namespace datalog { conj.push_back(a.mk_ge(lhs, zero)); } } - }; void mk_karr_invariants::cancel() { - rule_transformer::plugin::cancel(); - m_hb.set_cancel(true); + m_inner_ctx.cancel(); } rule_set * mk_karr_invariants::operator()(rule_set const & source) { @@ -564,64 +199,27 @@ namespace datalog { return 0; } } - bool change = true, non_empty = false; - while (!m_ctx.canceled() && 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", - ND.display(tout << "ND\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; - } - } + rel_context& rctx = m_inner_ctx.get_rel_context(); + ptr_vector heads; + m_inner_ctx.ensure_opened(); + it = source.begin(); + for (; it != end; ++it) { + rule_ref r(*it, m_ctx.get_rule_manager()); + m_inner_ctx.add_rule(r); + m_inner_ctx.register_predicate(r->get_decl()); } - - if (!non_empty) { - return 0; + m_inner_ctx.close(); + rule_set::decl2rules::iterator dit = source.begin_grouped_rules(); + rule_set::decl2rules::iterator dend = source.end_grouped_rules(); + for (; dit != dend; ++dit) { + heads.push_back(dit->m_key); } - - if (m_ctx.canceled()) { - 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); - } - }); + m_inner_ctx.rel_query(heads.size(), heads.c_ptr()); rule_set* rules = alloc(rule_set, m_ctx); it = source.begin(); for (; it != end; ++it) { - update_body(*rules, **it); + update_body(rctx, *rules, **it); } if (m_ctx.get_model_converter()) { add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m); @@ -629,9 +227,11 @@ namespace datalog { 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); + expr_ref fml(m); + relation_base* rb = rctx.try_get_relation(p); + if (rb) { + rb->to_formula(fml); + kmc->add(p, fml); } } m_ctx.add_model_converter(kmc); @@ -640,5 +240,824 @@ namespace datalog { return rules; } + void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) { + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + app_ref_vector tail(m); + expr_ref fml(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); + relation_base* rb = rctx.try_get_relation(r.get_decl(i)); + if (rb) { + rb->to_formula(fml); + expr_safe_replace rep(m); + for (unsigned j = 0; j < q->get_arity(); ++j) { + rep.insert(m.mk_var(j, q->get_domain(j)), + r.get_tail(i)->get_arg(j)); + } + rep(fml); + tail.push_back(to_app(fml)); + } + } + 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); + rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening rule. + } + + + + class karr_relation : public relation_base { + friend class karr_relation_plugin; + friend class karr_relation_plugin::filter_equal_fn; + + karr_relation_plugin& m_plugin; + ast_manager& m; + mutable arith_util a; + func_decl_ref m_fn; + mutable bool m_empty; + mutable matrix m_ineqs; + mutable bool m_ineqs_valid; + mutable matrix m_basis; + mutable bool m_basis_valid; + + public: + karr_relation(karr_relation_plugin& p, func_decl* f, relation_signature const& s, bool is_empty): + relation_base(p, s), + m_plugin(p), + m(p.get_ast_manager()), + a(m), + m_fn(f, m), + m_empty(is_empty), + m_ineqs_valid(!is_empty), + m_basis_valid(false) + { + } + + virtual bool empty() const { + return m_empty; + } + + virtual void add_fact(const relation_fact & f) { + SASSERT(m_empty); + SASSERT(!m_basis_valid); + m_empty = false; + m_ineqs_valid = true; + for (unsigned i = 0; i < f.size(); ++i) { + rational n; + if (a.is_numeral(f[i], n) && n.is_int()) { + vector row; + row.resize(f.size()); + row[i] = rational(1); + m_ineqs.A.push_back(row); + m_ineqs.b.push_back(-n); + m_ineqs.eq.push_back(true); + } + } + } + + virtual bool contains_fact(const relation_fact & f) const { + UNREACHABLE(); + return false; + } + + virtual void display(std::ostream & out) const { + if (m_fn) { + out << m_fn->get_name() << "\n"; + } + if (empty()) { + out << "empty\n"; + } + else { + if (m_ineqs_valid) { + m_ineqs.display(out << "ineqs:\n"); + } + if (m_basis_valid) { + m_basis.display(out << "basis:\n"); + } + } + } + + virtual karr_relation * clone() const { + karr_relation* result = alloc(karr_relation, m_plugin, m_fn, get_signature(), m_empty); + result->copy(*this); + return result; + } + + virtual karr_relation * complement(func_decl*) const { + UNREACHABLE(); + return 0; + } + + virtual void to_formula(expr_ref& fml) const { + if (empty()) { + fml = m.mk_false(); + } + else { + matrix const& M = get_ineqs(); + expr_ref_vector conj(m); + for (unsigned i = 0; i < M.size(); ++i) { + to_formula(M.A[i], M.b[i], M.eq[i], conj); + } + bool_rewriter(m).mk_and(conj.size(), conj.c_ptr(), fml); + } + } + + karr_relation_plugin& get_plugin() const { return m_plugin; } + + void filter_interpreted(app* cond) { + rational one(1), mone(-1); + expr* e1, *e2, *en; + var* v, *w; + rational n1, n2; + expr_ref_vector conjs(m); + datalog::flatten_and(cond, conjs); + matrix& M = get_ineqs(); + unsigned num_columns = get_signature().size(); + + 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"; + if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back()); + ); + } + TRACE("dl", display(tout);); + } + + void mk_join(karr_relation const& r1, karr_relation const& r2, + unsigned col_cnt, unsigned const* cols1, unsigned const* cols2) { + if (r1.empty() || r2.empty()) { + m_empty = true; + return; + } + matrix const& M1 = r1.get_ineqs(); + matrix const& M2 = r2.get_ineqs(); + unsigned sig1_size = r1.get_signature().size(); + unsigned sig_size = get_signature().size(); + m_ineqs.reset(); + for (unsigned i = 0; i < M1.size(); ++i) { + vector row; + row.append(M1.A[i]); + row.resize(sig_size); + m_ineqs.A.push_back(row); + m_ineqs.b.push_back(M1.b[i]); + m_ineqs.eq.push_back(M1.eq[i]); + } + for (unsigned i = 0; i < M2.size(); ++i) { + vector row; + row.resize(sig_size); + for (unsigned j = 0; j < M2.A[i].size(); ++j) { + row[sig1_size + j] = M2.A[i][j]; + } + m_ineqs.A.push_back(row); + m_ineqs.b.push_back(M2.b[i]); + m_ineqs.eq.push_back(M2.eq[i]); + } + for (unsigned i = 0; i < col_cnt; ++i) { + vector row; + row.resize(sig_size); + row[cols1[i]] = rational(1); + row[sig1_size + cols2[i]] = rational(-1); + m_ineqs.A.push_back(row); + m_ineqs.b.push_back(rational(0)); + m_ineqs.eq.push_back(true); + } + m_ineqs_valid = true; + m_basis_valid = false; + m_empty = false; + if (r1.m_fn) { + m_fn = r1.m_fn; + } + if (r2.m_fn) { + m_fn = r2.m_fn; + } + } + + void mk_project(karr_relation const& r, unsigned cnt, unsigned const* cols) { + if (r.m_empty) { + m_empty = true; + return; + } + matrix const& M = r.get_basis(); + m_basis.reset(); + for (unsigned i = 0; i < M.size(); ++i) { + vector row; + unsigned k = 0; + for (unsigned j = 0; j < M.A[i].size(); ++j) { + if (k < cnt && j == cols[k]) { + ++k; + } + else { + row.push_back(M.A[i][j]); + } + } + SASSERT(row.size() + cnt == M.A[i].size()); + SASSERT(M.eq[i]); + m_basis.A.push_back(row); + m_basis.b.push_back(M.b[i]); + m_basis.eq.push_back(true); + } + m_basis_valid = true; + m_ineqs_valid = false; + m_empty = false; + m_fn = r.m_fn; + + TRACE("dl", + for (unsigned i = 0; i < cnt; ++i) { + tout << cols[i] << " "; + } + tout << "\n"; + r.display(tout); + display(tout);); + } + + void mk_rename(const karr_relation & r, unsigned col_cnt, const unsigned * cols) { + if (r.empty()) { + m_empty = true; + return; + } + m_ineqs.reset(); + m_basis.reset(); + m_ineqs_valid = r.m_ineqs_valid; + m_basis_valid = r.m_basis_valid; + if (m_ineqs_valid) { + m_ineqs.append(r.m_ineqs); + mk_rename(m_ineqs, col_cnt, cols); + } + if (m_basis_valid) { + m_basis.append(r.m_basis); + mk_rename(m_basis, col_cnt, cols); + } + m_fn = r.m_fn; + TRACE("dl", r.display(tout); display(tout);); + } + + void mk_union(karr_relation const& src, karr_relation* delta) { + if (src.empty()) { + if (delta) { + delta->m_empty = true; + } + return; + } + matrix const& M = src.get_basis(); + if (empty()) { + m_basis = M; + m_basis_valid = true; + m_empty = false; + m_ineqs_valid = false; + if (delta) { + delta->copy(*this); + } + return; + } + matrix& N = get_basis(); + unsigned N_size = N.size(); + for (unsigned i = 0; i < M.size(); ++i) { + bool found = false; + for (unsigned j = 0; !found && j < N_size; ++j) { + found = + same_row(M.A[i], N.A[j]) && + M.b[i] == N.b[j] && + M.eq[i] == N.eq[j]; + } + if (!found) { + N.A.push_back(M.A[i]); + N.b.push_back(M.b[i]); + N.eq.push_back(M.eq[i]); + } + } + m_ineqs_valid = false; + if (N_size != N.size()) { + if (delta) { + delta->copy(*this); + } + } + } + + matrix const& get_basis() const { + init_basis(); + return m_basis; + } + + matrix& get_basis() { + init_basis(); + return m_basis; + } + + matrix const& get_ineqs() const { + init_ineqs(); + return m_ineqs; + } + + matrix & get_ineqs() { + init_ineqs(); + return m_ineqs; + } + + private: + + void copy(karr_relation const& other) { + m_ineqs = other.m_ineqs; + m_basis = other.m_basis; + m_basis_valid = other.m_basis_valid; + m_ineqs_valid = other.m_ineqs_valid; + m_empty = other.m_empty; + } + + bool same_row(vector const& r1, vector const& r2) const { + SASSERT(r1.size() == r2.size()); + for (unsigned i = 0; i < r1.size(); ++i) { + if (r1[i] != r2[i]) { + return false; + } + } + return true; + } + + void mk_rename(matrix& M, unsigned col_cnt, unsigned const* cols) { + for (unsigned j = 0; j < M.size(); ++j) { + vector & row = M.A[j]; + rational tmp = row[cols[0]]; + for (unsigned i = 0; i + 1 < col_cnt; ++i) { + row[cols[i]] = row[cols[i+1]]; + } + row[cols[col_cnt-1]] = tmp; + } + } + + bool 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 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; + } + + void init_ineqs() const { + if (!m_ineqs_valid) { + SASSERT(m_basis_valid); + m_plugin.dualizeH(m_ineqs, m_basis); + m_ineqs_valid = true; + } + } + + void init_basis() const { + if (!m_basis_valid) { + SASSERT(m_ineqs_valid); + if (m_plugin.dualizeI(m_basis, m_ineqs)) { + m_basis_valid = true; + } + else { + m_empty = true; + } + } + } + + void to_formula(vector const& row, rational const& b, bool is_eq, expr_ref_vector& conj) const { + 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)); + } + } + }; + + + karr_relation& karr_relation_plugin::get(relation_base& r) { + return dynamic_cast(r); + } + + karr_relation const & karr_relation_plugin::get(relation_base const& r) { + return dynamic_cast(r); + } + + void karr_relation_plugin::set_cancel(bool f) { + m_hb.set_cancel(f); + } + + relation_base * karr_relation_plugin::mk_empty(const relation_signature & s) { + return alloc(karr_relation, *this, 0, s, true); + } + + relation_base * karr_relation_plugin::mk_full(func_decl* p, const relation_signature & s) { + return alloc(karr_relation, *this, p, s, false); + } + + class karr_relation_plugin::join_fn : public convenient_relation_join_fn { + public: + join_fn(const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt, + const unsigned * cols1, const unsigned * cols2) + : convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2){ + } + + virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) { + karr_relation const& r1 = get(_r1); + karr_relation const& r2 = get(_r2); + karr_relation_plugin& p = r1.get_plugin(); + karr_relation* result = dynamic_cast(p.mk_full(0, get_result_signature())); + result->mk_join(r1, r2, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr()); + return result; + } + }; + + relation_join_fn * karr_relation_plugin::mk_join_fn( + const relation_base & t1, const relation_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { + if (!check_kind(t1) || !check_kind(t2)) { + return 0; + } + return alloc(join_fn, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2); + } + + + class karr_relation_plugin::project_fn : public convenient_relation_project_fn { + public: + project_fn(const relation_signature & orig_sig, unsigned removed_col_cnt, const unsigned * removed_cols) + : convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols) { + } + + virtual relation_base * operator()(const relation_base & _r) { + karr_relation const& r = get(_r); + karr_relation_plugin& p = r.get_plugin(); + karr_relation* result = dynamic_cast(p.mk_full(0, get_result_signature())); + result->mk_project(r, m_removed_cols.size(), m_removed_cols.c_ptr()); + return result; + } + }; + + relation_transformer_fn * karr_relation_plugin::mk_project_fn(const relation_base & r, + unsigned col_cnt, const unsigned * removed_cols) { + return alloc(project_fn, r.get_signature(), col_cnt, removed_cols); + } + + class karr_relation_plugin::rename_fn : public convenient_relation_rename_fn { + public: + rename_fn(karr_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) + : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {} + + virtual relation_base * operator()(const relation_base & _r) { + karr_relation const& r = get(_r); + karr_relation_plugin& p = r.get_plugin(); + karr_relation* result = dynamic_cast(p.mk_full(0, get_result_signature())); + result->mk_rename(r, m_cycle.size(), m_cycle.c_ptr()); + return result; + } + }; + + relation_transformer_fn * karr_relation_plugin::mk_rename_fn(const relation_base & r, + unsigned cycle_len, const unsigned * permutation_cycle) { + if (!check_kind(r)) { + return 0; + } + return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle); + } + + bool karr_relation_plugin::dualizeI(matrix& dst, matrix const& src) { + dst.reset(); + 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 = l_undef; + + try { + is_sat = m_hb.saturate(); + } + catch (...) { + is_sat = l_undef; + } + TRACE("dl_verbose", m_hb.display(tout);); + if (is_sat == l_false) { + return false; + } + if (is_sat == l_undef) { + return 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 && 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); + } + } + return true; + } + + void karr_relation_plugin::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.push_back(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 = l_undef; + try { + is_sat = m_hb.saturate(); + } + catch (...) { + is_sat = l_undef; + } + if (is_sat != l_true) { + return; + } + TRACE("dl_verbose", m_hb.display(tout);); + SASSERT(is_sat == l_true); + unsigned basis_size = m_hb.get_basis_size(); + 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); + } + } + } + + + class karr_relation_plugin::union_fn : public relation_union_fn { + karr_relation_plugin& m_plugin; + public: + union_fn(karr_relation_plugin& p) : + m_plugin(p) { + } + + virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) { + + karr_relation& r = get(_r); + karr_relation const& src = get(_src); + TRACE("dl", r.display(tout << "dst:\n"); src.display(tout << "src:\n");); + + if (_delta) { + karr_relation& d = get(*_delta); + r.mk_union(src, &d); + } + else { + r.mk_union(src, 0); + } + TRACE("dl", r.display(tout << "result:\n");); + } + }; + + relation_union_fn * karr_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, + const relation_base * delta) { + if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { + return 0; + } + return alloc(union_fn, *this); + } + + class karr_relation_plugin::filter_identical_fn : public relation_mutator_fn { + unsigned_vector m_identical_cols; + public: + filter_identical_fn(unsigned col_cnt, const unsigned * identical_cols) + : m_identical_cols(col_cnt, identical_cols) {} + + virtual void operator()(relation_base & _r) { + karr_relation & r = get(_r); + TRACE("dl", r.display(tout << "src:\n");); + r.get_ineqs(); + for (unsigned i = 1; i < m_identical_cols.size(); ++i) { + unsigned c1 = m_identical_cols[0]; + unsigned c2 = m_identical_cols[i]; + vector row; + row.resize(r.get_signature().size()); + row[c1] = rational(1); + row[c2] = rational(-1); + r.m_ineqs.A.push_back(row); + r.m_ineqs.b.push_back(rational(0)); + r.m_ineqs.eq.push_back(true); + r.m_basis_valid = false; + } + TRACE("dl", r.display(tout << "result:\n");); + } + }; + + relation_mutator_fn * karr_relation_plugin::mk_filter_identical_fn( + const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) { + if(!check_kind(t)) { + return 0; + } + return alloc(filter_identical_fn, col_cnt, identical_cols); + } + + + class karr_relation_plugin::filter_equal_fn : public relation_mutator_fn { + unsigned m_col; + rational m_value; + public: + filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col) + : m_col(col) { + arith_util arith(m.get_context().get_manager()); + VERIFY(arith.is_numeral(value, m_value)); + } + + virtual void operator()(relation_base & _r) { + karr_relation & r = get(_r); + karr_relation_plugin & p = r.get_plugin(); + if (m_value.is_int()) { + r.get_ineqs(); + vector row; + row.resize(r.get_signature().size()); + row[m_col] = rational(1); + r.m_ineqs.A.push_back(row); + r.m_ineqs.b.push_back(rational(-1)); + r.m_ineqs.eq.push_back(true); + r.m_basis_valid = false; + } + TRACE("dl", tout << m_value << "\n"; r.display(tout);); + } + }; + + relation_mutator_fn * karr_relation_plugin::mk_filter_equal_fn(const relation_base & r, + const relation_element & value, unsigned col) { + if(check_kind(r)) { + return alloc(filter_equal_fn, get_manager(), value, col); + } + return 0; + } + + + class karr_relation_plugin::filter_interpreted_fn : public relation_mutator_fn { + app_ref m_cond; + public: + filter_interpreted_fn(karr_relation const& t, app* cond): + m_cond(cond, t.get_plugin().get_ast_manager()) { + } + + void operator()(relation_base& t) { + get(t).filter_interpreted(m_cond); + TRACE("dl", tout << mk_pp(m_cond, m_cond.get_manager()) << "\n"; t.display(tout);); + } + }; + + relation_mutator_fn * karr_relation_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { + if (check_kind(t)) { + return alloc(filter_interpreted_fn, get(t), condition); + } + return 0; + } + }; diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 9d611e365..414953e4f 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -30,41 +30,32 @@ namespace datalog { /** \brief Rule transformer that strengthens bodies with invariants. */ + + 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; + static void display_row( + std::ostream& out, vector const& row, rational const& b, bool is_eq); + static void display_ineq( + std::ostream& out, vector const& row, rational const& b, bool is_eq); + }; + 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; - static void display_row( - std::ostream& out, vector const& row, rational const& b, bool is_eq); - static void display_ineq( - std::ostream& out, vector const& row, rational const& b, bool is_eq); - }; class add_invariant_model_converter; - + context& m_ctx; ast_manager& m; rule_manager& rm; + context m_inner_ctx; 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); + void update_body(rel_context& rctx, rule_set& result, rule& r); public: mk_karr_invariants(context & ctx, unsigned priority); @@ -77,6 +68,68 @@ namespace datalog { }; + class karr_relation; + + class karr_relation_plugin : public relation_plugin { + arith_util a; + hilbert_basis m_hb; + + class join_fn; + class project_fn; + class rename_fn; + class union_fn; + class filter_equal_fn; + class filter_identical_fn; + class filter_interpreted_fn; + friend class karr_relation; + public: + karr_relation_plugin(relation_manager& rm): + relation_plugin(karr_relation_plugin::get_name(), rm), + a(get_ast_manager()) + {} + + virtual bool can_handle_signature(const relation_signature & sig) { + for (unsigned i = 0; i < sig.size(); ++i) { + if (a.is_int(sig[i])) { + return true; + } + } + return false; + } + + static symbol get_name() { return symbol("karr_relation"); } + + virtual void set_cancel(bool f); + + virtual relation_base * mk_empty(const relation_signature & s); + + virtual relation_base * mk_full(func_decl* p, const relation_signature & s); + + static karr_relation& get(relation_base& r); + static karr_relation const & get(relation_base const& r); + + virtual relation_join_fn * mk_join_fn( + const relation_base & t1, const relation_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2); + virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, + const unsigned * removed_cols); + virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, + const unsigned * permutation_cycle); + virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, + const relation_base * delta); + virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, + const unsigned * identical_cols); + virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, + unsigned col); + virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + private: + bool dualizeI(matrix& dst, matrix const& src); + void dualizeH(matrix& dst, matrix const& src); + + + }; + + }; #endif /* _DL_MK_KARR_INVARIANTS_H_ */ diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index 3407f8fbe..e001dd1a4 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -468,6 +468,12 @@ namespace datalog { } } + void relation_manager::set_cancel(bool f) { + for (unsigned i = 0; i < m_relation_plugins.size(); ++i) { + m_relation_plugins[i]->set_cancel(f); + } + } + std::string relation_manager::to_nice_string(const relation_element & el) const { uint64 val; std::stringstream stm; diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index ecba3d598..6b350642e 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -223,6 +223,7 @@ namespace datalog { relation_fact & to); + void set_cancel(bool f); // ----------------------------------- diff --git a/src/muz_qe/dl_rule_set.cpp b/src/muz_qe/dl_rule_set.cpp index caecc76ef..f9ae3620d 100644 --- a/src/muz_qe/dl_rule_set.cpp +++ b/src/muz_qe/dl_rule_set.cpp @@ -30,17 +30,17 @@ namespace datalog { rule_dependencies::rule_dependencies(const rule_dependencies & o, bool reversed): m_context(o.m_context) { - if(reversed) { + if (reversed) { iterator oit = o.begin(); iterator oend = o.end(); - for(; oit!=oend; ++oit) { + for (; oit!=oend; ++oit) { func_decl * pred = oit->m_key; item_set & orig_items = *oit->get_value(); ensure_key(pred); item_set::iterator dit = orig_items.begin(); item_set::iterator dend = orig_items.end(); - for(; dit!=dend; ++dit) { + for (; dit!=dend; ++dit) { func_decl * master_pred = *dit; insert(master_pred, pred); } @@ -49,7 +49,7 @@ namespace datalog { else { iterator oit = o.begin(); iterator oend = o.end(); - for(; oit!=oend; ++oit) { + for (; oit!=oend; ++oit) { func_decl * pred = oit->m_key; item_set & orig_items = *oit->get_value(); m_data.insert(pred, alloc(item_set, orig_items)); @@ -73,7 +73,7 @@ namespace datalog { rule_dependencies::item_set & rule_dependencies::ensure_key(func_decl * pred) { deps_type::obj_map_entry * e = m_data.insert_if_not_there2(pred, 0); - if(!e->get_data().m_value) { + if (!e->get_data().m_value) { e->get_data().m_value = alloc(item_set); } return *e->get_data().m_value; @@ -101,12 +101,13 @@ namespace datalog { void rule_dependencies::populate(unsigned n, rule * const * rules) { SASSERT(m_data.empty()); - for(unsigned i=0; iget_decl()->get_name() << "\n";); m_visited.reset(); func_decl * d = r->get_head()->get_decl(); func_decl_set & s = ensure_key(d); @@ -141,7 +142,7 @@ namespace datalog { const rule_dependencies::item_set & rule_dependencies::get_deps(func_decl * f) const { deps_type::obj_map_entry * e = m_data.find_core(f); - if(!e) { + if (!e) { return m_empty_item_set; } SASSERT(e->get_data().get_value()); @@ -152,9 +153,9 @@ namespace datalog { ptr_vector to_remove; iterator pit = begin(); iterator pend = end(); - for(; pit!=pend; ++pit) { + for (; pit!=pend; ++pit) { func_decl * pred = pit->m_key; - if(!allowed.contains(pred)) { + if (!allowed.contains(pred)) { to_remove.insert(pred); continue; } @@ -163,7 +164,7 @@ namespace datalog { } ptr_vector::iterator rit = to_remove.begin(); ptr_vector::iterator rend = to_remove.end(); - for(; rit!=rend; ++rit) { + for (; rit!=rend; ++rit) { remove_m_data_entry(*rit); } } @@ -172,7 +173,7 @@ namespace datalog { remove_m_data_entry(itm); iterator pit = begin(); iterator pend = end(); - for(; pit!=pend; ++pit) { + for (; pit!=pend; ++pit) { item_set & itms = *pit->get_value(); itms.remove(itm); } @@ -181,12 +182,12 @@ namespace datalog { void rule_dependencies::remove(const item_set & to_remove) { item_set::iterator rit = to_remove.begin(); item_set::iterator rend = to_remove.end(); - for(; rit!=rend; ++rit) { + for (; rit!=rend; ++rit) { remove_m_data_entry(*rit); } iterator pit = begin(); iterator pend = end(); - for(; pit!=pend; ++pit) { + for (; pit!=pend; ++pit) { item_set * itms = pit->get_value(); set_difference(*itms, to_remove); } @@ -196,9 +197,9 @@ namespace datalog { unsigned res = 0; iterator pit = begin(); iterator pend = end(); - for(; pit!=pend; ++pit) { + for (; pit!=pend; ++pit) { item_set & itms = *pit->get_value(); - if(itms.contains(f)) { + if (itms.contains(f)) { res++; } } @@ -214,10 +215,10 @@ namespace datalog { iterator pit = begin(); iterator pend = end(); - for(; pit!=pend; ++pit) { + for (; pit!=pend; ++pit) { func_decl * pred = pit->m_key; unsigned deg = in_degree(pred); - if(deg==0) { + if (deg==0) { res.push_back(pred); } else { @@ -225,25 +226,25 @@ namespace datalog { } } - while(curr_indexget_data().m_value; SASSERT(child_deg>0); child_deg--; - if(child_deg==0) { + if (child_deg==0) { res.push_back(child); } } curr_index++; } - if(res.size()m_key; const item_set & deps = *pit->m_value; item_set::iterator dit=deps.begin(); item_set::iterator dend=deps.end(); - if(dit==dend) { + if (dit == dend) { out<get_name()<<" - \n"; } - for(; dit!=dend; ++dit) { + for (; dit != dend; ++dit) { func_decl * dep = *dit; - out<get_name()<<" -> "<get_name()<<"\n"; + out << pred->get_name() << " -> " << dep->get_name() << "\n"; } } } @@ -292,8 +293,8 @@ namespace datalog { m_deps(rs.m_context), m_stratifier(0) { add_rules(rs); - if(rs.m_stratifier) { - TRUSTME(close()); + if (rs.m_stratifier) { + VERIFY(close()); } } @@ -302,7 +303,7 @@ namespace datalog { } void rule_set::reset() { - if(m_stratifier) { + if (m_stratifier) { m_stratifier = 0; } reset_dealloc_values(m_head2rules); @@ -346,18 +347,19 @@ namespace datalog { void rule_set::ensure_closed() { - if(!is_closed()) { - TRUSTME(close()); + if (!is_closed()) { + VERIFY(close()); } } bool rule_set::close() { SASSERT(!is_closed()); //the rule_set is not already closed + m_deps.populate(*this); m_stratifier = alloc(rule_stratifier, m_deps); - if(!stratified_negation()) { + if (!stratified_negation()) { m_stratifier = 0; m_deps.reset(); return false; @@ -391,7 +393,7 @@ namespace datalog { unsigned head_strat = get_predicate_strat(head_decl); SASSERT(head_strat>=neg_strat); //head strat can never be lower than that of a tail - if(head_strat==neg_strat) { + if (head_strat == neg_strat) { return false; } } @@ -415,7 +417,7 @@ namespace datalog { const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const { decl2rules::obj_map_entry * e = m_head2rules.find_core(pred); - if(!e) { + if (!e) { return m_empty_rule_vector; } return *e->get_data().m_value; @@ -443,7 +445,7 @@ namespace datalog { ptr_vector::iterator end2 = rules->end(); for (; it2 != end2; ++it2) { rule * r = *it2; - if(!r->passes_output_thresholds(m_context)) { + if (!r->passes_output_thresholds(m_context)) { continue; } r->display(m_context, out); @@ -468,23 +470,23 @@ namespace datalog { const pred_set_vector & strats = get_strats(); pred_set_vector::const_iterator sit = strats.begin(); pred_set_vector::const_iterator send = strats.end(); - for(; sit!=send; ++sit) { + for (; sit!=send; ++sit) { func_decl_set & strat = **sit; func_decl_set::iterator fit=strat.begin(); func_decl_set::iterator fend=strat.end(); bool non_empty = false; - for(; fit!=fend; ++fit) { + for (; fit!=fend; ++fit) { func_decl * first = *fit; const func_decl_set & deps = m_deps.get_deps(first); func_decl_set::iterator dit=deps.begin(); func_decl_set::iterator dend=deps.end(); - for(; dit!=dend; ++dit) { + for (; dit!=dend; ++dit) { non_empty = true; func_decl * dep = *dit; out<get_name()<<" -> "<get_name()<<"\n"; } } - if(non_empty && sit!=send) { + if (non_empty && sit!=send) { out << "\n"; } } @@ -499,7 +501,7 @@ namespace datalog { rule_stratifier::~rule_stratifier() { comp_vector::iterator it = m_strats.begin(); comp_vector::iterator end = m_strats.end(); - for(; it!=end; ++it) { + for (; it!=end; ++it) { SASSERT(*it); dealloc(*it); } @@ -507,7 +509,7 @@ namespace datalog { unsigned rule_stratifier::get_predicate_strat(func_decl * pred) const { unsigned num; - if(!m_pred_strat_nums.find(pred, num)) { + if (!m_pred_strat_nums.find(pred, num)) { //the number of the predicate is not stored, therefore it did not appear //in the algorithm and therefore it does not depend on anything and nothing //depends on it. So it is safe to assign zero strate to it, although it is @@ -520,19 +522,19 @@ namespace datalog { void rule_stratifier::traverse(T* el) { unsigned p_num; - if(m_preorder_nums.find(el, p_num)) { - if(p_numinsert(s_el); m_component_nums.insert(s_el, comp_num); - } while(s_el!=el); + } while (s_el!=el); m_stack_P.pop_back(); } } } void rule_stratifier::process() { - if(m_deps.empty()) { + if (m_deps.empty()) { return; } //detect strong components rule_dependencies::iterator it = m_deps.begin(); rule_dependencies::iterator end = m_deps.end(); - for(; it!=end; ++it) { + for (; it!=end; ++it) { T * el = it->m_key; //we take a note of the preorder number with which this sweep started m_first_preorder = m_next_preorder; @@ -593,32 +595,32 @@ namespace datalog { //init in_degrees it = m_deps.begin(); end = m_deps.end(); - for(; it!=end; ++it) { + for (; it != end; ++it) { T * el = it->m_key; item_set * out_edges = it->m_value; unsigned el_comp; - TRUSTME( m_component_nums.find(el, el_comp) ); + VERIFY( m_component_nums.find(el, el_comp) ); - item_set::iterator eit=out_edges->begin(); - item_set::iterator eend=out_edges->end(); - for(; eit!=eend; ++eit) { + item_set::iterator eit = out_edges->begin(); + item_set::iterator eend = out_edges->end(); + for (; eit!=eend; ++eit) { T * tgt = *eit; unsigned tgt_comp = m_component_nums.find(tgt); - if(el_comp!=tgt_comp) { + if (el_comp != tgt_comp) { in_degrees[tgt_comp]++; } } } - //We put components whose indegree is zero to m_strats and assign its - //m_components entry to zero. + // We put components whose indegree is zero to m_strats and assign its + // m_components entry to zero. unsigned comp_cnt = m_components.size(); - for(unsigned i=0; ibegin(); item_set::iterator cend=comp->end(); - for(; cit!=cend; ++cit) { + for (; cit!=cend; ++cit) { T * el = *cit; const item_set & deps = m_deps.get_deps(el); item_set::iterator eit=deps.begin(); item_set::iterator eend=deps.end(); - for(; eit!=eend; ++eit) { + for (; eit!=eend; ++eit) { T * tgt = *eit; unsigned tgt_comp; - TRUSTME( m_component_nums.find(tgt, tgt_comp) ); + VERIFY( m_component_nums.find(tgt, tgt_comp) ); //m_components[tgt_comp]==0 means the edge is intra-component. //Otherwise it would go to another component, but it is not possible, since //as m_components[tgt_comp]==0, its indegree has already reached zero. - if(m_components[tgt_comp]) { + if (m_components[tgt_comp]) { SASSERT(in_degrees[tgt_comp]>0); in_degrees[tgt_comp]--; - if(in_degrees[tgt_comp]==0) { + if (in_degrees[tgt_comp]==0) { m_strats.push_back(m_components[tgt_comp]); m_components[tgt_comp] = 0; } } - - traverse(*cit); } } @@ -669,13 +669,12 @@ namespace datalog { SASSERT(m_pred_strat_nums.empty()); unsigned strat_cnt = m_strats.size(); - for(unsigned strat_index=0; strat_indexbegin(); item_set::iterator cend=comp->end(); - for(; cit!=cend; ++cit) { + for (; cit != cend; ++cit) { T * el = *cit; - m_pred_strat_nums.insert(el, strat_index); } } @@ -686,6 +685,21 @@ namespace datalog { m_stack_P.finalize(); m_component_nums.finalize(); m_components.finalize(); + + } + + void rule_stratifier::display(std::ostream& out) const { + m_deps.display(out << "dependencies\n"); + out << "strata\n"; + for (unsigned i = 0; i < m_strats.size(); ++i) { + item_set::iterator it = m_strats[i]->begin(); + item_set::iterator end = m_strats[i]->end(); + for (; it != end; ++it) { + out << (*it)->get_name() << " "; + } + out << "\n"; + } + } }; diff --git a/src/muz_qe/dl_rule_set.h b/src/muz_qe/dl_rule_set.h index 3079c6072..9aa64425c 100644 --- a/src/muz_qe/dl_rule_set.h +++ b/src/muz_qe/dl_rule_set.h @@ -146,6 +146,8 @@ namespace datalog { const comp_vector & get_strats() const { return m_strats; } unsigned get_predicate_strat(func_decl * pred) const; + + void display( std::ostream & out ) const; }; /** diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 7b3e67487..62f091dbc 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -744,7 +744,6 @@ void hilbert_basis::reset() { if (m_passive2) { m_passive2->reset(); } - m_cancel = false; if (m_index) { m_index->reset(1); } @@ -867,7 +866,7 @@ lbool hilbert_basis::saturate() { stopwatch sw; sw.start(); lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]); - IF_VERBOSE(1, + IF_VERBOSE(3, { statistics st; collect_statistics(st); st.display(verbose_stream()); diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index abb59be2d..733b3a2f0 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -37,10 +37,13 @@ typedef vector rational_vector; class hilbert_basis { - static const bool check = false; + static const bool check = true; typedef checked_int64 numeral; typedef vector num_vector; static checked_int64 to_numeral(rational const& r) { + if (!r.is_int64()) { + throw checked_int64::overflow_exception(); + } return checked_int64(r.get_int64()); } static rational to_rational(checked_int64 const& i) { diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index c79acf67f..12045047b 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -27,6 +27,7 @@ Revision History: #include"dl_product_relation.h" #include"dl_bound_relation.h" #include"dl_interval_relation.h" +#include"dl_mk_karr_invariants.h" #include"dl_finite_product_relation.h" #include"dl_sparse_table.h" #include"dl_table.h" @@ -54,6 +55,8 @@ namespace datalog { get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(karr_relation_plugin, get_rmanager())); + } @@ -178,23 +181,23 @@ namespace datalog { return result; } -#define BEGIN_QUERY() \ +#define BEGIN_QUERY() \ rule_set original_rules(m_context.get_rules()); \ - decl_set original_preds; \ - m_context.collect_predicates(original_preds); \ - bool was_closed = m_context.is_closed(); \ - if (was_closed) { \ + decl_set original_preds; \ + m_context.collect_predicates(original_preds); \ + bool was_closed = m_context.is_closed(); \ + if (was_closed) { \ m_context.reopen(); \ - } \ - -#define END_QUERY() \ + } \ + +#define END_QUERY() \ m_context.reopen(); \ m_context.replace_rules(original_rules); \ - restrict_predicates(original_preds); \ - \ - if (was_closed) { \ + restrict_predicates(original_preds); \ + \ + if (was_closed) { \ m_context.close(); \ - } \ + } \ lbool rel_context::query(unsigned num_rels, func_decl * const* rels) { get_rmanager().reset_saturated_marks(); @@ -427,6 +430,10 @@ namespace datalog { get_rmanager().set_predicate_kind(pred, target_kind); } + void rel_context::set_cancel(bool f) { + get_rmanager().set_cancel(f); + } + relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) { relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name); if (!plugin) { diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 2e2b5cd9d..08ee868c0 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -63,7 +63,6 @@ namespace datalog { bool output_profile() const; - lbool query(expr* q); lbool query(unsigned num_rels, func_decl * const* rels); @@ -72,6 +71,7 @@ namespace datalog { void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred); + void set_cancel(bool f); /** \brief Restrict the set of used predicates to \c res.