From 44a79d05c84776ab8881395ad0b7d1b7010eef93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Feb 2020 06:45:15 -0800 Subject: [PATCH] debugging cuts Signed-off-by: Nikolaj Bjorner --- src/sat/sat_aig_cuts.cpp | 26 ++++++++++++++++++++++---- src/sat/sat_aig_cuts.h | 2 +- src/sat/sat_cut_simplifier.cpp | 3 ++- src/smt/theory_array.cpp | 2 +- 4 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index 36d5f3c9a..1d87953ab 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -103,6 +103,7 @@ namespace sat { void aig_cuts::augment_lut(unsigned v, node const& n, cut_set& cs) { IF_VERBOSE(4, display(verbose_stream() << "augment_lut " << v << " ", n) << "\n"); literal l1 = child(n, 0); + VERIFY(&cs != &m_cuts[l1.var()]); for (auto const& a : m_cuts[l1.var()]) { m_tables[0] = &a; cut b(a); @@ -112,6 +113,7 @@ namespace sat { void aig_cuts::augment_lut_rec(unsigned v, node const& n, cut& a, unsigned idx, cut_set& cs) { if (idx < n.size()) { + VERIFY(&cs != &m_cuts[child(n, idx).var()]); for (auto const& b : m_cuts[child(n, idx).var()]) { cut ab; if (ab.merge(a, b)) { @@ -185,6 +187,7 @@ namespace sat { IF_VERBOSE(4, display(verbose_stream() << "augment_aig1 " << v << " ", n) << "\n"); SASSERT(n.is_and()); literal lit = child(n, 0); + VERIFY(&cs != &m_cuts[lit.var()]); for (auto const& a : m_cuts[lit.var()]) { cut c(a); if (n.sign()) c.negate(); @@ -197,6 +200,11 @@ namespace sat { SASSERT(n.is_and() || n.is_xor()); literal l1 = child(n, 0); literal l2 = child(n, 1); + if (&cs == &m_cuts[l2.var()]) { + IF_VERBOSE(0, display(verbose_stream() << "augment_aig2 " << v << " ", n) << "\n"); + } + VERIFY(&cs != &m_cuts[l1.var()]); + VERIFY(&cs != &m_cuts[l2.var()]); for (auto const& a : m_cuts[l1.var()]) { for (auto const& b : m_cuts[l2.var()]) { cut c; @@ -362,6 +370,7 @@ namespace sat { literal r = m_roots[i].second; literal rr = to_root[r.var()]; to_root[v] = r.sign() ? ~rr : rr; + if (rr != r) std::cout << v << " -> " << to_root[v] << "\n"; } for (unsigned i = 0; i < m_aig.size(); ++i) { // invalidate nodes that have been rooted @@ -370,9 +379,13 @@ namespace sat { reset(m_cuts[i]); } else { + unsigned j = 0; for (node & n : m_aig[i]) { - flush_roots(to_root, n); + if (flush_roots(i, to_root, n)) { + m_aig[i][j++] = n; + } } + m_aig[i].shrink(j); } } for (cut_set& cs : m_cuts) { @@ -382,18 +395,23 @@ namespace sat { TRACE("aig_simplifier", display(tout);); } - void aig_cuts::flush_roots(literal_vector const& to_root, node& n) { + bool aig_cuts::flush_roots(bool_var var, literal_vector const& to_root, node& n) { bool changed = false; for (unsigned i = 0; i < n.size(); ++i) { literal& lit = m_literals[n.offset() + i]; - if (to_root[lit.var()] != lit) { + literal r = to_root[lit.var()]; + if (r != lit) { changed = true; - lit = lit.sign() ? ~to_root[lit.var()] : to_root[lit.var()]; + lit = lit.sign() ? ~r : r; + } + if (lit.var() == var) { + return false; } } if (changed && (n.is_and() || n.is_xor())) { std::sort(m_literals.c_ptr() + n.offset(), m_literals.c_ptr() + n.offset() + n.size()); } + return true; } void aig_cuts::flush_roots(literal_vector const& to_root, cut_set& cs) { diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h index c7ca473a0..9496b1264 100644 --- a/src/sat/sat_aig_cuts.h +++ b/src/sat/sat_aig_cuts.h @@ -140,7 +140,7 @@ namespace sat { bool insert_cut(unsigned v, cut const& c, cut_set& cs); void flush_roots(); - void flush_roots(literal_vector const& to_root, node& n); + bool flush_roots(bool_var var, literal_vector const& to_root, node& n); void flush_roots(literal_vector const& to_root, cut_set& cs); cut_val eval(node const& n, cut_eval const& env) const; diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp index 167503cc1..935ca0b58 100644 --- a/src/sat/sat_cut_simplifier.cpp +++ b/src/sat/sat_cut_simplifier.cpp @@ -119,6 +119,7 @@ namespace sat { void cut_simplifier::add_and(literal head, unsigned sz, literal const* lits) { m_aig_cuts.add_node(head, and_op, sz, lits); + for (unsigned i = 0; i < sz; ++i) VERIFY(head.var() != lits[i].var()); m_stats.m_num_ands++; } @@ -310,8 +311,8 @@ namespace sat { return; IF_VERBOSE(10, verbose_stream() << "new unit " << lit << "\n"); validate_unit(lit); - s.assign_unit(lit); certify_unit(lit, c); + s.assign_unit(lit); ++m_stats.m_num_units; } diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 65095e5b3..9e341bb78 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -331,11 +331,11 @@ namespace smt { if (!is_store(n) && !is_select(n)) return; context & ctx = get_context(); + if (!ctx.e_internalized(n)) ctx.internalize(n, false); enode * arg = ctx.get_enode(n->get_arg(0)); theory_var v_arg = arg->get_th_var(get_id()); SASSERT(v_arg != null_theory_var); - if (!ctx.e_internalized(n)) ctx.internalize(n, false); enode* e = ctx.get_enode(n); if (is_select(n)) { add_parent_select(v_arg, e);