From 22f1c6448a9e2a68020864a902cc2d8cb2e6a746 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Jan 2020 22:43:18 -0800 Subject: [PATCH] add option to increase thresholds based on simulated equality Signed-off-by: Nikolaj Bjorner --- src/sat/sat_aig_cuts.cpp | 111 ++++++++++++++++++++++++++------- src/sat/sat_aig_cuts.h | 12 +++- src/sat/sat_aig_simplifier.cpp | 39 ++++++++++-- src/sat/sat_aig_simplifier.h | 7 ++- src/sat/sat_cutset.cpp | 21 +++++++ src/sat/sat_cutset.h | 11 ++-- 6 files changed, 166 insertions(+), 35 deletions(-) diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index bd2f0fb64..de1d91f3c 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -55,7 +55,7 @@ namespace sat { unsigned nc = n.size(); m_insertions = 0; cut_set& cs = m_cuts[id]; - if (!is_touched(n)) { + if (!is_touched(id, n)) { // no-op } else if (n.is_var()) { @@ -89,7 +89,7 @@ namespace sat { if (++m_insertions > m_config.m_max_insertions) { return false; } - while (cs.size() >= m_config.m_max_cutset_size) { + while (cs.size() >= max_cutset_size(v)) { // never evict the first entry, it is used for the starting point unsigned idx = 1 + (m_rand() % (cs.size() - 1)); evict(cs, idx); @@ -155,17 +155,18 @@ namespace sat { for (auto const& a : m_cuts[l1.var()]) { for (auto const& b : m_cuts[l2.var()]) { cut c; - if (c.merge(a, b)) { - uint64_t t1 = a.shift_table(c); - uint64_t t2 = b.shift_table(c); - if (l1.sign()) t1 = ~t1; - if (l2.sign()) t2 = ~t2; - uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2); - c.set_table(t3); - if (n.sign()) c.negate(); - // validate_aig2(a, b, v, n, c); - if (!insert_cut(v, c, cs)) return; + if (!c.merge(a, b)) { + continue; } + uint64_t t1 = a.shift_table(c); + uint64_t t2 = b.shift_table(c); + if (l1.sign()) t1 = ~t1; + if (l2.sign()) t2 = ~t2; + uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2); + c.set_table(t3); + if (n.sign()) c.negate(); + // validate_aig2(a, b, v, n, c); + if (!insert_cut(v, c, cs)) return; } } } @@ -189,15 +190,16 @@ namespace sat { for (auto const& a : m_cut_set1) { for (auto const& b : m_cuts[lit.var()]) { cut c; - if (c.merge(a, b)) { - uint64_t t1 = a.shift_table(c); - uint64_t t2 = b.shift_table(c); - if (lit.sign()) t2 = ~t2; - uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2); - c.set_table(t3); - if (i + 1 == n.size() && n.sign()) c.negate(); - if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child; + if (!c.merge(a, b)) { + continue; } + uint64_t t1 = a.shift_table(c); + uint64_t t2 = b.shift_table(c); + if (lit.sign()) t2 = ~t2; + uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2); + c.set_table(t3); + if (i + 1 == n.size() && n.sign()) c.negate(); + if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child; } } next_child: @@ -212,20 +214,20 @@ namespace sat { } } - - bool aig_cuts::is_touched(node const& n) { + bool aig_cuts::is_touched(bool_var v, node const& n) { for (unsigned i = 0; i < n.size(); ++i) { literal lit = m_literals[n.offset() + i]; if (is_touched(lit)) { return true; } } - return false; + return is_touched(v); } void aig_cuts::reserve(unsigned v) { m_aig.reserve(v + 1); m_cuts.reserve(v + 1); + m_max_cutset_size.reserve(v + 1, m_config.m_max_cutset_size); m_last_touched.reserve(v + 1, 0); } @@ -410,6 +412,69 @@ namespace sat { return result; } + uint64_t aig_cuts::eval(node const& n, svector const& env) const { + uint64_t result; + switch (n.op()) { + case var_op: + UNREACHABLE(); + break; + case and_op: + result = ~0ull; + for (unsigned i = 0; i < n.size(); ++i) { + literal u = m_literals[n.offset() + i]; + uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; + result &= uv; + } + break; + case xor_op: + result = 0ull; + for (unsigned i = 0; i < n.size(); ++i) { + literal u = m_literals[n.offset() + i]; + uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; + result ^= uv; + } + break; + case ite_op: { + literal u = m_literals[n.offset() + 0]; + literal v = m_literals[n.offset() + 1]; + literal w = m_literals[n.offset() + 2]; + uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; + uint64_t vv = v.sign() ? ~env[v.var()] : env[v.var()]; + uint64_t wv = w.sign() ? ~env[w.var()] : env[w.var()]; + result = (uv & vv) | ((~uv) & wv); + break; + } + default: + UNREACHABLE(); + } + if (n.sign()) result = ~result; + return result; + } + + svector aig_cuts::simulate(unsigned num_rounds) { + svector result; + for (unsigned i = 0; i < m_cuts.size(); ++i) { + result.push_back((uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) + + ((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull)); + } + for (unsigned i = 0; i < num_rounds; ++i) { + for (unsigned j = 0; j < m_cuts.size(); ++j) { + cut_set const& cs = m_cuts[j]; + if (cs.size() <= 1) { + if (!m_aig[j].empty() && !m_aig[j][0].is_var()) { + result[j] = eval(m_aig[j][0], result); + } + } + else if (cs.size() > 1) { + cut const& c = cs[1 + (m_rand() % (cs.size() - 1))]; + result[j] = c.eval(result); + } + } + } + return result; + } + + void aig_cuts::on_node_add(unsigned v, node const& n) { if (m_on_clause_add) { node2def(m_on_clause_add, n, literal(v, false)); diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h index 879241737..11d413498 100644 --- a/src/sat/sat_aig_cuts.h +++ b/src/sat/sat_aig_cuts.h @@ -61,7 +61,7 @@ namespace sat { unsigned m_max_aux; unsigned m_max_insertions; bool m_full; - config(): m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10), m_full(false) {} + config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(false) {} }; private: @@ -97,6 +97,7 @@ namespace sat { region m_region; cut_set m_cut_set1, m_cut_set2; vector m_cuts; + unsigned_vector m_max_cutset_size; unsigned_vector m_last_touched; unsigned m_num_cut_calls; unsigned m_num_cuts; @@ -106,13 +107,15 @@ namespace sat { cut_set::on_update_t m_on_cut_add, m_on_cut_del; literal_vector m_clause; - bool is_touched(node const& n); + bool is_touched(bool_var v, node const& n); bool is_touched(literal lit) const { return is_touched(lit.var()); } bool is_touched(bool_var v) const { return m_last_touched[v] + m_aig.size() >= m_num_cut_calls * m_aig.size(); } void reserve(unsigned v); bool insert_aux(unsigned v, node const& n); void init_cut_set(unsigned id); + unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; } + bool eq(node const& a, node const& b); unsigned_vector filter_valid_nodes() const; @@ -130,6 +133,8 @@ namespace sat { void flush_roots(literal_vector const& to_root, node& n); void flush_roots(literal_vector const& to_root, cut_set& cs); + uint64_t eval(node const& n, svector const& env) const; + std::ostream& display(std::ostream& out, node const& n) const; literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; } @@ -160,6 +165,8 @@ namespace sat { void set_on_clause_add(on_clause_t& on_clause_add); void set_on_clause_del(on_clause_t& on_clause_del); + void inc_max_cutset_size(unsigned v) { m_max_cutset_size[v] += 10; touch(v); } + vector const & operator()(); unsigned num_cuts() const { return m_num_cuts; } @@ -167,6 +174,7 @@ namespace sat { void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); } + svector simulate(unsigned num_rounds); std::ostream& display(std::ostream& out) const; diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp index 5380816c6..6027e2f8f 100644 --- a/src/sat/sat_aig_simplifier.cpp +++ b/src/sat/sat_aig_simplifier.cpp @@ -25,23 +25,26 @@ namespace sat { struct aig_simplifier::report { aig_simplifier& s; stopwatch m_watch; - unsigned m_num_eqs, m_num_units, m_num_cuts; + unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_learned_implies; report(aig_simplifier& s): s(s) { m_watch.start(); m_num_eqs = s.m_stats.m_num_eqs; m_num_units = s.m_stats.m_num_units; m_num_cuts = s.m_stats.m_num_cuts; + m_num_learned_implies = s.m_stats.m_num_learned_implies; } ~report() { unsigned ne = s.m_stats.m_num_eqs - m_num_eqs; unsigned nu = s.m_stats.m_num_units - m_num_units; unsigned nc = s.m_stats.m_num_cuts - m_num_cuts; + unsigned ni = s.m_stats.m_num_learned_implies - m_num_learned_implies; IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier"; - if (ne > 0) verbose_stream() << " :num-eqs " << ne; if (nu > 0) verbose_stream() << " :num-units " << nu; - if (nc > 0) verbose_stream() << " :num-cuts " << nc; + if (ne > 0) verbose_stream() << " :num-eqs " << ne; + if (ni > 0) verbose_stream() << " :num-bin " << ni; + if (nc > 0) verbose_stream() << " :num-cuts " << nc; verbose_stream() << " :mb " << mem_stat() << m_watch << ")\n"); } }; @@ -231,6 +234,7 @@ namespace sat { add_dont_cares(cuts); cuts2equiv(cuts); cuts2implies(cuts); + simulate_eqs(); } void aig_simplifier::cuts2equiv(vector const& cuts) { @@ -281,8 +285,8 @@ namespace sat { void aig_simplifier::assign_unit(cut const& c, literal lit) { if (s.value(lit) != l_undef) return; + IF_VERBOSE(10, verbose_stream() << "new unit " << lit << "\n"); validate_unit(lit); - IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n"); s.assign_unit(lit); certify_unit(lit, c); ++m_stats.m_num_units; @@ -345,6 +349,8 @@ namespace sat { big big(s.rand()); big.init(s, true); for (auto const& cs : cuts) { + if (s.was_eliminated(cs.var())) + continue; for (auto const& c : cs) { if (c.is_false() || c.is_true()) continue; @@ -410,6 +416,31 @@ namespace sat { s.mk_clause(~u, v, true); // m_bins owns reference to ~u or v created by certify_implies m_bins.insert(p); + ++m_stats.m_num_learned_implies; + } + + void aig_simplifier::simulate_eqs() { + if (!m_config.m_simulate_eqs) return; + auto var2val = m_aig_cuts.simulate(4); + + // Assign higher cutset budgets to equality candidates that come from simulation + // touch them to trigger recomputation of cutsets. + u64_map val2var; + unsigned i = 0, j = 0, num_eqs = 0; + for (uint64_t val : var2val) { + if (!s.was_eliminated(i) && s.value(i) == l_undef) { + if (val2var.find(val, j)) { + m_aig_cuts.inc_max_cutset_size(i); + m_aig_cuts.inc_max_cutset_size(j); + num_eqs++; + } + else { + val2var.insert(val, i); + } + } + ++i; + } + IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier num simulated eqs " << num_eqs << ")\n"); } void aig_simplifier::track_binary(bin_rel const& p) { diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h index 74328f623..7f523fd2f 100644 --- a/src/sat/sat_aig_simplifier.h +++ b/src/sat/sat_aig_simplifier.h @@ -28,7 +28,7 @@ namespace sat { public: struct stats { unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites; - unsigned m_num_calls, m_num_dont_care_reductions; + unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -39,13 +39,15 @@ namespace sat { bool m_learned2aig; // add learned clauses to AIGs used by cut-set enumeration bool m_validate_cuts; // enable direct validation of generated cuts bool m_validate_lemmas; // enable direct validation of learned lemmas + bool m_simulate_eqs; // use symbolic simulation to control size of cutsets. config(): m_enable_units(true), m_enable_dont_cares(true), m_learn_implies(false), m_learned2aig(true), m_validate_cuts(false), - m_validate_lemmas(false) {} + m_validate_lemmas(false), + m_simulate_eqs(true) {} }; private: struct report; @@ -120,6 +122,7 @@ namespace sat { void clauses2aig(); void aig2clauses(); + void simulate_eqs(); void cuts2equiv(vector const& cuts); void cuts2implies(vector const& cuts); void uf2equiv(union_find<> const& uf); diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp index 407301b12..460eb4411 100644 --- a/src/sat/sat_cutset.cpp +++ b/src/sat/sat_cutset.cpp @@ -161,6 +161,27 @@ namespace sat { } return true; } + + /** + sat-sweep evaluation. Given 64 bits worth of possible values per variable, + find possible values for function table encoded by cut. + */ + uint64_t cut::eval(svector const& env) const { + uint64_t result = 0ull; + uint64_t t = table(); + unsigned sz = size(); + if (sz == 1 && t == 2) { + return env[m_elems[0]]; + } + for (unsigned i = 0; i < 64; ++i) { + unsigned offset = 0; + for (unsigned j = 0; j < sz; ++j) { + offset |= (((env[m_elems[j]] >> i) & 0x1) << j); + } + result |= ((t >> offset) & 0x1) << i; + } + return result; + } std::ostream& cut::display(std::ostream& out) const { out << "{"; diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index ac43279f8..eb138e170 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -15,6 +15,7 @@ #include "util/region.h" #include "util/debug.h" #include "util/util.h" +#include "util/vector.h" #include #include #include @@ -24,7 +25,7 @@ namespace sat { class cut { unsigned m_filter; unsigned m_size; - unsigned m_elems[4]; + unsigned m_elems[5]; uint64_t m_table; mutable uint64_t m_dont_care; @@ -50,9 +51,11 @@ namespace sat { return *this; } + uint64_t eval(svector const& env) const; + unsigned size() const { return m_size; } - static unsigned max_cut_size() { return 4; } + static unsigned max_cut_size() { return 5; } unsigned const* begin() const { return m_elems; } unsigned const* end() const { return m_elems + m_size; } @@ -113,7 +116,7 @@ namespace sat { unsigned x = a[i]; unsigned y = b[j]; while (x != UINT_MAX || y != UINT_MAX) { - if (!add(std::min(x, y))) { + if (!add(std::min(x, y))) { return false; } if (x < y) { @@ -169,7 +172,7 @@ namespace sat { cut const & back() { return m_cuts[m_size-1]; } void push_back(on_update_t& on_add, cut const& c); void reset(on_update_t& on_del) { shrink(on_del, 0); } - cut const & operator[](unsigned idx) { return m_cuts[idx]; } + cut const & operator[](unsigned idx) const { return m_cuts[idx]; } void shrink(on_update_t& on_del, unsigned j); void swap(cut_set& other) { std::swap(m_var, other.m_var);