From 1101c927c9bbbd9aa684625df15fab5d830e38a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Nov 2017 13:46:02 -0800 Subject: [PATCH] prepare for transitive reduction / hyper-binary clause addition Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 55 ++++++++++++++++++++++------- src/sat/sat_lookahead.cpp | 37 ++++++++++++++----- src/sat/sat_lookahead.h | 4 ++- 3 files changed, 74 insertions(+), 22 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 0fdee0700..1e8cd7182 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -77,7 +77,33 @@ struct pb2bv_rewriter::imp { fmls.push_back(bv.mk_ule(bound, result)); } return result; + } + typedef std::pair ca; + + struct compare_coeffs { + bool operator()(ca const& x, ca const& y) const { + return x.first < y.first; + } + }; + + void sort_args() { + vector cas; + for (unsigned i = 0; i < m_args.size(); ++i) { + cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m))); + } + //for (ca const& ca : cas) std::cout << ca.first << " "; + //std::cout << "\n"; + std::sort(cas.begin(), cas.end(), compare_coeffs()); + //std::cout << "post-sort\n"; + //for (ca const& ca : cas) std::cout << ca.first << " "; + //std::cout << "\n"; + m_coeffs.reset(); + m_args.reset(); + for (ca const& ca : cas) { + m_coeffs.push_back(ca.first); + m_args.push_back(ca.second); + } } // @@ -93,7 +119,10 @@ struct pb2bv_rewriter::imp { // is_le = l_false - >= // template - expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) { + expr_ref mk_le_ge(rational const & k) { + //sort_args(); + unsigned sz = m_args.size(); + expr * const* args = m_args.c_ptr(); TRACE("pb", for (unsigned i = 0; i < sz; ++i) { tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " "; @@ -107,7 +136,7 @@ struct pb2bv_rewriter::imp { tout << k << "\n";); if (k.is_zero()) { if (is_le != l_false) { - return expr_ref(m.mk_not(::mk_or(m, sz, args)), m); + return expr_ref(m.mk_not(::mk_or(m_args)), m); } else { return expr_ref(m.mk_true(), m); @@ -501,25 +530,25 @@ struct pb2bv_rewriter::imp { decl_kind kind = f->get_decl_kind(); rational k = pb.get_k(f); m_coeffs.reset(); + m_args.reset(); for (unsigned i = 0; i < sz; ++i) { m_coeffs.push_back(pb.get_coeff(f, i)); + m_args.push_back(args[i]); } CTRACE("pb", k.is_neg(), tout << expr_ref(m.mk_app(f, sz, args), m) << "\n";); SASSERT(!k.is_neg()); switch (kind) { case OP_PB_GE: case OP_AT_LEAST_K: { - expr_ref_vector nargs(m); - nargs.append(sz, args); - dualize(f, nargs, k); + dualize(f, m_args, k); SASSERT(!k.is_neg()); - return mk_le_ge(sz, nargs.c_ptr(), k); + return mk_le_ge(k); } case OP_PB_LE: case OP_AT_MOST_K: - return mk_le_ge(sz, args, k); + return mk_le_ge(k); case OP_PB_EQ: - return mk_le_ge(sz, args, k); + return mk_le_ge(k); default: UNREACHABLE(); return expr_ref(m.mk_true(), m); @@ -591,21 +620,21 @@ struct pb2bv_rewriter::imp { // skip } else if (au.is_le(f) && is_pb(args[0], args[1])) { - result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + result = mk_le_ge(m_k); } else if (au.is_lt(f) && is_pb(args[0], args[1])) { ++m_k; - result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + result = mk_le_ge(m_k); } else if (au.is_ge(f) && is_pb(args[1], args[0])) { - result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + result = mk_le_ge(m_k); } else if (au.is_gt(f) && is_pb(args[1], args[0])) { ++m_k; - result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + result = mk_le_ge(m_k); } else if (m.is_eq(f) && is_pb(args[0], args[1])) { - result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + result = mk_le_ge(m_k); } else { return false; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 32cc877dd..bc5f9b071 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -233,7 +233,6 @@ namespace sat { if (is_sat()) { return false; } - std::cout << "include newbies\n"; } SASSERT(!m_candidates.empty()); // cut number of candidates down to max_num_cand. @@ -437,8 +436,8 @@ namespace sat { for (binary b : m_ternary[(~l1).index()]) { if (sz-- == 0) break; if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) { - std::cout << b.m_u << " " << b.m_v << "\n"; - std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n"; + IF_VERBOSE(0, verbose_stream() << b.m_u << " " << b.m_v << "\n" + << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";); UNREACHABLE(); } if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u))) @@ -649,6 +648,7 @@ namespace sat { TRACE("sat", display_scc(tout);); } void lookahead::init_scc() { + std::cerr << "init-scc\n"; inc_bstamp(); for (unsigned i = 0; i < m_candidates.size(); ++i) { literal lit(m_candidates[i].m_var, false); @@ -661,6 +661,7 @@ namespace sat { init_arcs(~lit); } m_rank = 0; + m_rank_max = UINT_MAX; m_active = null_literal; m_settled = null_literal; TRACE("sat", display_dfs(tout);); @@ -678,15 +679,19 @@ namespace sat { for (literal u : succ) { SASSERT(u != l); // l => u - if (u.index() > (~l).index() && is_stamped(u)) { + // NB. u.index() > l.index() iff u.index() > (~l).index(). + // since indices for the same boolean variables occupy + // two adjacent numbers. + if (u.index() > l.index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } } for (auto w : m_watches[l.index()]) { + lits.reset(); if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { for (literal u : lits) { - if (u.index() > (~l).index() && is_stamped(u)) { + if (u.index() > l.index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } @@ -695,6 +700,11 @@ namespace sat { } } + void lookahead::add_arc(literal u, literal v) { + auto & lst = m_dfs[u.index()].m_next; + if (lst.empty() || lst.back() != v) lst.push_back(v); + } + void lookahead::get_scc(literal v) { TRACE("scc", tout << v << "\n";); set_parent(v, null_literal); @@ -744,7 +754,7 @@ namespace sat { m_active = get_link(v); literal best = v; double best_rating = get_rating(v); - set_rank(v, UINT_MAX); + set_rank(v, m_rank_max); set_link(v, m_settled); m_settled = t; while (t != v) { if (t == ~v) { @@ -752,7 +762,7 @@ namespace sat { set_conflict(); break; } - set_rank(t, UINT_MAX); + set_rank(t, m_rank_max); set_parent(t, v); double t_rating = get_rating(t); if (t_rating > best_rating) { @@ -763,7 +773,7 @@ namespace sat { } set_parent(v, v); set_vcomp(v, best); - if (get_rank(~v) == UINT_MAX) { + if (maxed_rank(~v)) { set_vcomp(v, ~get_vcomp(get_parent(~v))); } } @@ -2279,6 +2289,17 @@ namespace sat { IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";); elim_eqs elim(m_s); elim(roots, to_elim); + +#if 0 + // TBD: + // Finally create a new graph between parents + // based on the arcs in the the m_dfs[index].m_next structure + // Visit all nodes, assign DFS numbers + // Then prune binary clauses that differ in DFS number more than 1 + // Add binary clauses that have DFS number 1, but no companion binary clause. + // +#endif + } } m_lookahead.reset(); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index e65e7021a..99d5511ea 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -387,6 +387,7 @@ namespace sat { literal m_active; unsigned m_rank; + unsigned m_rank_max; literal m_settled; vector m_dfs; @@ -394,7 +395,7 @@ namespace sat { void init_scc(); void init_dfs_info(literal l); void init_arcs(literal l); - void add_arc(literal u, literal v) { m_dfs[u.index()].m_next.push_back(v); } + void add_arc(literal u, literal v); bool has_arc(literal v) const { return m_dfs[v.index()].m_next.size() > m_dfs[v.index()].m_nextp; } arcs get_arcs(literal v) const { return m_dfs[v.index()].m_next; } literal pop_arc(literal u) { return m_dfs[u.index()].m_next[m_dfs[u.index()].m_nextp++]; } @@ -402,6 +403,7 @@ namespace sat { literal get_next(literal u, unsigned i) const { return m_dfs[u.index()].m_next[i]; } literal get_min(literal v) const { return m_dfs[v.index()].m_min; } unsigned get_rank(literal v) const { return m_dfs[v.index()].m_rank; } + bool maxed_rank(literal v) const { return get_rank(v) >= m_rank_max; } unsigned get_height(literal v) const { return m_dfs[v.index()].m_height; } literal get_parent(literal u) const { return m_dfs[u.index()].m_parent; } literal get_link(literal u) const { return m_dfs[u.index()].m_link; }