From 6ed266e4dee0cc0526a6f28340e779b620e4785b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Mar 2013 08:53:46 -0700 Subject: [PATCH] debugging karr invariants Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_array_blast.cpp | 11 +-- src/muz_qe/dl_mk_array_blast.h | 2 + src/muz_qe/dl_mk_bit_blast.cpp | 4 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 43 +++++------ src/muz_qe/dl_mk_karr_invariants.cpp | 67 ++++++++++++----- src/muz_qe/dl_mk_karr_invariants.h | 6 +- src/muz_qe/dl_rule_set.h | 2 +- src/muz_qe/dl_rule_transformer.cpp | 6 +- src/muz_qe/dl_rule_transformer.h | 8 +-- src/muz_qe/fdd.cpp | 17 ++--- src/muz_qe/hilbert_basis.cpp | 6 +- src/test/hilbert_basis.cpp | 12 ++++ src/test/karr.cpp | 80 +++++++++++++++++++++ 13 files changed, 196 insertions(+), 68 deletions(-) diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index 048269c5a..adf08662a 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -30,7 +30,8 @@ namespace datalog { m(ctx.get_manager()), a(m), rm(ctx.get_rule_manager()), - m_rewriter(m, m_params){ + m_rewriter(m, m_params), + m_simplifier(ctx) { m_params.set_bool("expand_select_store",true); m_rewriter.updt_params(m_params); } @@ -202,9 +203,11 @@ namespace datalog { SASSERT(new_rules.size() == 1); TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n");); - - rules.add_rule(new_rules[0].get()); - rm.mk_rule_rewrite_proof(r, *new_rules[0].get()); + rule_ref new_rule(rm); + if (m_simplifier.transform_rule(new_rules[0].get(), new_rule)) { + rules.add_rule(new_rule.get()); + rm.mk_rule_rewrite_proof(r, *new_rule.get()); + } return true; } diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h index 94eb64601..4680821a2 100644 --- a/src/muz_qe/dl_mk_array_blast.h +++ b/src/muz_qe/dl_mk_array_blast.h @@ -22,6 +22,7 @@ Revision History: #include"dl_context.h" #include"dl_rule_set.h" #include"dl_rule_transformer.h" +#include"dl_mk_interp_tail_simplifier.h" #include "equiv_proof_converter.h" #include "array_decl_plugin.h" @@ -37,6 +38,7 @@ namespace datalog { rule_manager& rm; params_ref m_params; th_rewriter m_rewriter; + mk_interp_tail_simplifier m_simplifier; typedef obj_map defs_t; diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 338eed0b4..9dfd9deba 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -223,7 +223,9 @@ namespace datalog { expr_ref fml1(m), fml2(m), fml3(m); rule_ref r2(m_context.get_rule_manager()); // We need to simplify rule before bit-blasting. - m_simplifier.transform_rule(r, r2); + if (!m_simplifier.transform_rule(r, r2)) { + r2 = r; + } r2->to_formula(fml1); m_blaster(fml1, fml2, pr); m_rewriter(fml2, fml3); diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index a48b7b32f..35fd630f9 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -469,7 +469,7 @@ namespace datalog { start: unsigned u_len = r->get_uninterpreted_tail_size(); unsigned len = r->get_tail_size(); - if (u_len==len) { + if (u_len == len) { res = r; return true; } @@ -504,34 +504,29 @@ namespace datalog { expr_ref simp_res(m); simplify_expr(itail.get(), simp_res); - modified |= itail.get()!=simp_res.get(); - - if (is_app(simp_res.get())) { - itail = to_app(simp_res.get()); - } - else if (m.is_bool(simp_res)) { - itail = m.mk_eq(simp_res, m.mk_true()); - } - else { - throw default_exception("simplification resulted in non-boolean non-function"); - } - - if (m.is_false(itail.get())) { - //the tail member is never true, so we may delete the rule + modified |= itail.get() != simp_res.get(); + + if (m.is_false(simp_res)) { TRACE("dl", r->display(m_context, tout << "rule is infeasible\n");); return false; } - if (!m.is_true(itail.get())) { - //if the simplified tail is not a tautology, we add it to the rule - tail.push_back(itail); - tail_neg.push_back(false); - } - else { - modified = true; - } + SASSERT(m.is_bool(simp_res)); - SASSERT(tail.size() == tail_neg.size()); if (modified) { + expr_ref_vector conjs(m); + flatten_and(simp_res, conjs); + for (unsigned i = 0; i < conjs.size(); ++i) { + expr* e = conjs[i].get(); + if (is_app(e)) { + tail.push_back(to_app(e)); + } + else { + tail.push_back(m.mk_eq(e, m.mk_true())); + } + tail_neg.push_back(false); + } + + SASSERT(tail.size() == tail_neg.size()); res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); res->set_accounting_parent_object(m_context, r); } diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index d44b31979..013923045 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -62,12 +62,38 @@ namespace datalog { return *this; } + void mk_karr_invariants::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] << " "; + } + out << (is_eq?" = ":" >= ") << -b << "\n"; + } + + void mk_karr_invariants::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) { + if (!row[j].is_zero()) { + if (!first && row[j].is_pos()) { + out << "+ "; + } + if (row[j].is_minus_one()) { + out << "- "; + } + if (row[j] > rational(1) || row[j] < rational(-1)) { + out << row[j] << "*"; + } + out << "x" << j << " "; + first = false; + } + } + out << (is_eq?"= ":">= ") << -b << "\n"; + } + 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"; + display_row(out, A[i], b[i], eq[i]); } } @@ -182,24 +208,28 @@ namespace datalog { 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)) { + 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)) { + 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.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)) { + 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)) { + 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.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) { @@ -221,7 +251,9 @@ namespace datalog { else { processed = false; } - TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";); + 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(); @@ -270,6 +302,7 @@ namespace datalog { 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; } @@ -322,7 +355,7 @@ namespace datalog { m_hb.set_is_int(i); } lbool is_sat = m_hb.saturate(); - TRACE("dl", m_hb.display(tout);); + 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) { @@ -353,7 +386,7 @@ namespace datalog { m_hb.set_is_int(i); } lbool is_sat = m_hb.saturate(); - TRACE("dl", m_hb.display(tout);); + TRACE("dl_verbose", m_hb.display(tout);); SASSERT(is_sat == l_true); dst.reset(); unsigned basis_size = m_hb.get_basis_size(); @@ -532,7 +565,7 @@ namespace datalog { } } bool change = true, non_empty = false; - while (!m_cancel && change) { + while (!m_ctx.canceled() && change) { change = false; it = source.begin(); for (; it != end; ++it) { @@ -550,8 +583,8 @@ namespace datalog { dualizeH(P, ND); TRACE("dl", - MD.display(tout << "MD\n"); - P.display(tout << "P\n");); + ND.display(tout << "ND\n"); + P.display(tout << "P\n");); if (!N) { change = true; @@ -569,7 +602,7 @@ namespace datalog { return 0; } - if (m_cancel) { + if (m_ctx.canceled()) { return 0; } diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 7cd26d495..d70fb374b 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -41,6 +41,10 @@ namespace datalog { 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; @@ -67,7 +71,7 @@ namespace datalog { virtual ~mk_karr_invariants(); - virtual void cancel(); + virtual void cancel(); rule_set * operator()(rule_set const & source, model_converter_ref& mc); diff --git a/src/muz_qe/dl_rule_set.h b/src/muz_qe/dl_rule_set.h index fdbbf7626..3079c6072 100644 --- a/src/muz_qe/dl_rule_set.h +++ b/src/muz_qe/dl_rule_set.h @@ -46,7 +46,7 @@ namespace datalog { ast_mark m_visited; - //we need to take care with removing to aviod memory leaks + //we need to take care with removing to avoid memory leaks void remove_m_data_entry(func_decl * key); //sometimes we need to return reference to an empty set, diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 5ecbf2b45..7e0e951e1 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -26,7 +26,7 @@ Revision History: namespace datalog { rule_transformer::rule_transformer(context & ctx) - : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false), m_cancel(false) { + : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false) { } @@ -42,11 +42,9 @@ namespace datalog { } 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) { @@ -84,7 +82,7 @@ namespace datalog { ); plugin_vector::iterator it = m_plugins.begin(); plugin_vector::iterator end = m_plugins.end(); - for(; it!=end && !m_cancel; ++it) { + for(; it!=end && !m_context.canceled(); ++it) { plugin & p = **it; rule_set * new_rules = p(rules, mc); diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h index 3b2140caf..87ff10fb0 100644 --- a/src/muz_qe/dl_rule_transformer.h +++ b/src/muz_qe/dl_rule_transformer.h @@ -41,7 +41,6 @@ namespace datalog { context & m_context; rule_manager & m_rule_manager; bool m_dirty; - volatile bool m_cancel; svector m_plugins; void ensure_ordered(); @@ -81,7 +80,6 @@ namespace datalog { void attach(rule_transformer & transformer) { m_transformer = &transformer; } protected: - volatile bool m_cancel; /** \brief Create a plugin object for rule_transformer. @@ -90,7 +88,7 @@ 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_cancel(false) {} + m_can_destratify_negation(can_destratify_negation), m_transformer(0) {} public: virtual ~plugin() {} @@ -98,6 +96,8 @@ namespace datalog { unsigned get_priority() { return m_priority; } bool can_destratify_negation() const { return m_can_destratify_negation; } + virtual void cancel() {} + /** \brief Return \c rule_set object with containing transformed rules or 0 if no transformation was done. @@ -107,8 +107,6 @@ namespace datalog { virtual rule_set * operator()(rule_set const & source, model_converter_ref& mc) = 0; - virtual void cancel() { m_cancel = true; } - /** Removes duplicate tails. */ diff --git a/src/muz_qe/fdd.cpp b/src/muz_qe/fdd.cpp index afb5206cc..6c3bc0974 100644 --- a/src/muz_qe/fdd.cpp +++ b/src/muz_qe/fdd.cpp @@ -97,14 +97,14 @@ node_id manager::mk_node(unsigned var, node_id lo, node_id hi) { inc_ref(hi); } - TRACE("mtdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";); + TRACE("fdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";); return result; } void manager::inc_ref(node_id n) { - TRACE("mtdd", tout << "incref: " << n << "\n";); + TRACE("fdd", tout << "incref: " << n << "\n";); if (!is_leaf(n)) { m_nodes[n].inc_ref(); } @@ -126,6 +126,7 @@ void manager::setup_keys(Key const* keys) { void manager::insert(Key const* keys) { setup_keys(keys); + m_insert_cache.reset(); node_id result = insert_sign(m_num_idx + m_num_keys, m_root); inc_ref(result); dec_ref(m_root); @@ -161,7 +162,7 @@ node_id manager::insert_sign(unsigned idx, node_id n) { node_id manager::insert(unsigned idx, node_id n) { node_id result; SASSERT(0 <= idx && idx <= m_num_idx); - TRACE("mtdd", tout << "insert: " << idx << " " << n << "\n";); + TRACE("fdd", tout << "insert: " << idx << " " << n << "\n";); if (is_leaf(n)) { while (idx > 0) { --idx; @@ -176,9 +177,8 @@ node_id manager::insert(unsigned idx, node_id n) { --idx; config c(m_dont_cares, idx, n); - insert_cache::key_data & kd = m_insert_cache.insert_if_not_there2(c, 0)->get_data(); - if (kd.m_value != 0) { - return kd.m_value; + if (m_insert_cache.find(c, result)) { + return result; } node nd = m_nodes[n]; @@ -209,7 +209,7 @@ node_id manager::insert(unsigned idx, node_id n) { } result = mk_node(idx, lo, hi); } - kd.m_value = result; + m_insert_cache.insert(c, result); return result; } @@ -263,11 +263,12 @@ bool manager::find_le(Key const* keys) { SASSERT(idx > 0); --idx; while (nc.var() < idx) { - if (idx2bit(idx)) { + if (idx2bit(idx) && is_dont_care(idx2key(idx))) { set_dont_care(idx2key(idx)); } --idx; } + SASSERT(nc.var() == idx); if (is_dont_care(idx2key(idx)) || idx2bit(idx)) { n = nc.hi(); } diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 221e9a706..69b8765a7 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -290,7 +290,7 @@ public: } void display(std::ostream& out) const { - // m_fdd.display(out); + m_fdd.display(out); } @@ -302,8 +302,8 @@ class hilbert_basis::index { // for positive weights a shared value index. // typedef value_index1 value_index; - // typedef value_index2 value_index; - typedef value_index3 value_index; + typedef value_index2 value_index; + // typedef value_index3 value_index; struct stats { unsigned m_num_find; diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index a5f554e5e..2f58cc3c8 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -514,6 +514,15 @@ static void tst16() { saturate_basis(hb); } +static void tst17() { + hilbert_basis hb; + hb.add_eq(vec(1, 0), R(0)); + hb.add_eq(vec(-1, 0), R(0)); + hb.add_eq(vec(0, 2), R(0)); + hb.add_eq(vec(0, -2), R(0)); + saturate_basis(hb); + +} void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; @@ -522,6 +531,9 @@ void tst_hilbert_basis() { g_use_ordered_support = true; + tst17(); + return; + if (true) { tst1(); tst2(); diff --git a/src/test/karr.cpp b/src/test/karr.cpp index 3ac427a88..8770eac94 100644 --- a/src/test/karr.cpp +++ b/src/test/karr.cpp @@ -165,6 +165,28 @@ namespace karr { return v; } + static vector V(int i, int j, int k, int l, int m) { + vector v; + v.push_back(rational(i)); + v.push_back(rational(j)); + v.push_back(rational(k)); + v.push_back(rational(l)); + v.push_back(rational(m)); + return v; + } + + static vector V(int i, int j, int k, int l, int x, int y, int z) { + vector v; + v.push_back(rational(i)); + v.push_back(rational(j)); + v.push_back(rational(k)); + v.push_back(rational(l)); + v.push_back(rational(x)); + v.push_back(rational(y)); + v.push_back(rational(z)); + return v; + } + #define R(_x_) rational(_x_) @@ -206,8 +228,66 @@ namespace karr { e2.display(std::cout << "e2\n"); } + void tst2() { + /** + 0 0 0 0 0 0 0 = 0 + 0 0 0 0 0 0 0 = 0 + 0 0 0 0 0 0 0 = 0 + 0 0 0 0 0 0 0 = 0 + 0 0 0 0 1 0 0 = 0 + 0 0 0 0 -1 0 0 = 0 + 0 1 0 0 0 0 0 = 0 + 0 -1 0 0 0 0 0 = 0 + 0 0 0 2 0 0 0 = 0 + 0 0 0 -2 0 0 0 = 0 + */ + + matrix ND; + ND.A.push_back(V(0,0,0,0,1,0,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,0,0,0,-1,0,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,1,0,0,0,0,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,-1,0,0,0,0,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,0,0,2,0,0,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,0,0,-2,0,0,0)); ND.b.push_back(R(0)); + + ND.display(std::cout << "ND\n"); + + matrix N; + dualizeH(N, ND); + + N.display(std::cout << "N\n"); + + + } + + void tst3() { + /** + 0 0 0 0 1 0 0 = 0 + 0 0 0 0 -1 0 0 = 0 + 0 1 0 0 0 0 0 = 0 + 0 -1 0 0 0 0 0 = 0 + 0 0 0 2 0 0 0 = 0 + 0 0 0 -2 0 0 0 = 0 + */ + + matrix ND; + ND.A.push_back(V(1,0)); ND.b.push_back(R(0)); + ND.A.push_back(V(0,2)); ND.b.push_back(R(0)); + + ND.display(std::cout << "ND\n"); + + matrix N; + dualizeH(N, ND); + + N.display(std::cout << "N\n"); + + + } + }; void tst_karr() { + karr::tst3(); + return; karr::tst1(); }