diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index e8bb3c3c7..8a4d79314 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(sat SOURCES ba_solver.cpp dimacs.cpp + sat_aig_cuts.cpp sat_aig_finder.cpp sat_aig_simplifier.cpp sat_anf_simplifier.cpp diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp new file mode 100644 index 000000000..556264524 --- /dev/null +++ b/src/sat/sat_aig_cuts.cpp @@ -0,0 +1,306 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Module Name: + + sat_aig_cuts.cpp + + Abstract: + + Perform cut-set enumeration to identify equivalences. + + Author: + + Nikolaj Bjorner 2020-01-02 + + --*/ + +#include "sat/sat_aig_cuts.h" +#include "util/trace.h" + +namespace sat { + + aig_cuts::aig_cuts() { + m_config.m_max_cut_size = std::min(cut().max_cut_size, m_config.m_max_cut_size); + m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1); + m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1); + } + + vector const& aig_cuts::get_cuts() { + unsigned_vector node_ids = filter_valid_nodes(); + augment(node_ids); + TRACE("aig_simplifier", display(tout);); + return m_cuts; + } + + void aig_cuts::augment(unsigned_vector const& ids) { + for (unsigned id : ids) { + cut_set& cs = m_cuts[id]; + node const& n = m_aig[id]; + SASSERT(n.is_valid()); + augment(n, cs); + for (node const& n2 : m_aux_aig[id]) { + augment(n2, cs); + } + } + } + + void aig_cuts::augment(node const& n, cut_set& cs) { + unsigned nc = n.num_children(); + if (n.is_var()) { + SASSERT(!n.sign()); + } + else if (n.is_ite()) { + augment_ite(n, cs); + } + else if (nc == 0) { + augment_aig0(n, cs); + } + else if (nc == 1) { + augment_aig1(n, cs); + } + else if (nc == 2) { + augment_aig2(n, cs); + } + else if (nc < m_config.m_max_cut_size) { + augment_aigN(n, cs); + } + } + + bool aig_cuts::insert_cut(cut const& c, cut_set& cs) { + while (cs.size() >= m_config.m_max_cutset_size) { + // never evict the first entry, it is used for the starting point + unsigned idx = 1 + (m_rand() % (cs.size() - 1)); + cs.evict(idx); + } + return cs.insert(c); + } + + void aig_cuts::augment_ite(node const& n, cut_set& cs) { + literal l1 = child(n, 0); + literal l2 = child(n, 1); + literal l3 = child(n, 2); + unsigned round = 0; + for (auto const& a : m_cuts[l1.var()]) { + for (auto const& b : m_cuts[l2.var()]) { + cut ab; + if (!ab.merge(a, b, m_config.m_max_cut_size)) { + continue; + } + for (auto const& c : m_cuts[l3.var()]) { + cut abc; + if (!abc.merge(ab, c, m_config.m_max_cut_size)) { + continue; + } + uint64_t t1 = a.shift_table(abc); + uint64_t t2 = b.shift_table(abc); + uint64_t t3 = c.shift_table(abc); + if (l1.sign()) t1 = ~t1; + if (l2.sign()) t2 = ~t2; + if (l3.sign()) t3 = ~t3; + abc.set_table((t1 & t2) | (~t1 & t3)); + if (n.sign()) abc.negate(); + // extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1; + if (insert_cut(abc, cs) && ++round >= m_config.m_max_insertions) + return; + } + } + } + } + + void aig_cuts::augment_aig0(node const& n, cut_set& cs) { + SASSERT(n.is_and()); + cut c; + cs.reset(); + if (n.sign()) { + c.m_table = 0; // constant false + } + else { + c.m_table = 0x3; // constant true + } + cs.insert(c); + } + + void aig_cuts::augment_aig1(node const& n, cut_set& cs) { + SASSERT(n.is_and()); + literal lit = child(n, 0); + unsigned round = 0; + for (auto const& a : m_cuts[lit.var()]) { + cut c; + c.set_table(a.m_table); + if (n.sign()) c.negate(); + if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions) + return; + } + } + + void aig_cuts::augment_aig2(node const& n, cut_set& cs) { + SASSERT(n.is_and() || n.is_xor()); + literal l1 = child(n, 0); + literal l2 = child(n, 1); + unsigned round = 0; + for (auto const& a : m_cuts[l1.var()]) { + for (auto const& b : m_cuts[l2.var()]) { + cut c; + if (c.merge(a, b, m_config.m_max_cut_size)) { + 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(); + if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions) + return; + } + } + } + } + + void aig_cuts::augment_aigN(node const& n, cut_set& cs) { + m_cut_set1.reset(); + SASSERT(n.is_and() || n.is_xor()); + literal lit = child(n, 0); + for (auto const& a : m_cuts[lit.var()]) { + m_cut_set1.push_back(a); + if (lit.sign()) { + m_cut_set1.back().negate(); + } + } + for (unsigned i = 1; i < n.num_children(); ++i) { + m_cut_set2.reset(); + literal lit = child(n, i); + unsigned round = 0; + for (auto const& a : m_cut_set1) { + for (auto const& b : m_cuts[lit.var()]) { + cut c; + if (c.merge(a, b, m_config.m_max_cut_size)) { + 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.num_children() && n.sign()) c.negate(); + if (insert_cut(c, m_cut_set2) && ++round >= m_config.m_max_insertions) { + break; + } + } + } + if (round >= m_config.m_max_insertions) { + break; + } + } + m_cut_set1.swap(m_cut_set2); + } + for (auto & cut : m_cut_set1) { + insert_cut(cut, cs); + } + } + + void aig_cuts::reserve(unsigned v) { + m_aig.reserve(v + 1); + m_cuts.reserve(v + 1); + m_aux_aig.reserve(v + 1); + } + + void aig_cuts::add_var(unsigned v) { + reserve(v); + if (!m_aig[v].is_valid()) { + m_aig[v] = node(v); + init_cut_set(v); + } + SASSERT(m_aig[v].is_valid()); + } + + void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) { + TRACE("aig_simplifier", tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";); + unsigned v = head.var(); + reserve(v); + unsigned offset = m_literals.size(); + node n(head.sign(), op, sz, offset); + m_literals.append(sz, args); + for (unsigned i = 0; i < sz; ++i) { + if (!m_aig[args[i].var()].is_valid()) { + add_var(args[i].var()); + } + } + if (!m_aig[v].is_valid() || m_aig[v].is_var() || (sz == 0)) { + m_aig[v] = n; + init_cut_set(v); + } + else if (eq(n, m_aig[v]) || !insert_aux(v, n)) { + m_literals.shrink(m_literals.size() - sz); + TRACE("aig_simplifier", tout << "duplicate\n";); + } + SASSERT(m_aig[v].is_valid()); + } + + void aig_cuts::init_cut_set(unsigned id) { + node const& n = m_aig[id]; + SASSERT(n.is_valid()); + auto& cut_set = m_cuts[id]; + cut_set.init(m_region, m_config.m_max_cutset_size + 1); + cut_set.push_back(cut(id)); // TBD: if entry is a constant? + m_aux_aig[id].reset(); + } + + bool aig_cuts::eq(node const& a, node const& b) { + if (a.is_valid() != b.is_valid()) return false; + if (!a.is_valid()) return true; + if (a.op() != b.op() || a.sign() != b.sign() || a.num_children() != b.num_children()) return false; + for (unsigned i = 0; i < a.num_children(); ++i) { + if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) return false; + } + return true; + } + + bool aig_cuts::insert_aux(unsigned v, node const& n) { + if (m_aux_aig[v].size() > m_config.m_max_aux) { + return false; + } + for (node const& n2 : m_aux_aig[v]) { + if (eq(n, n2)) return false; + } + m_aux_aig[v].push_back(n); + return true; + } + + unsigned_vector aig_cuts::filter_valid_nodes() const { + unsigned id = 0; + unsigned_vector result; + for (node const& n : m_aig) { + if (n.is_valid()) result.push_back(id); + ++id; + } + return result; + } + + std::ostream& aig_cuts::display(std::ostream& out) const { + auto ids = filter_valid_nodes(); + for (auto id : ids) { + out << id << " == "; + display(out, m_aig[id]) << "\n"; + for (auto const& n : m_aux_aig[id]) { + display(out << " ", n) << "\n"; + } + } + return out; + } + + std::ostream& aig_cuts::display(std::ostream& out, node const& n) const { + if (n.sign()) out << "! "; + switch (n.op()) { + case var_op: out << "var "; break; + case and_op: out << "and "; break; + case xor_op: out << "xor "; break; + case ite_op: out << "ite "; break; + default: break; + } + for (unsigned i = 0; i < n.num_children(); ++i) { + out << m_literals[n.offset() + i] << " "; + } + return out; + } + +} + diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h new file mode 100644 index 000000000..3f6bf49d9 --- /dev/null +++ b/src/sat/sat_aig_cuts.h @@ -0,0 +1,108 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Module Name: + + sat_aig_cuts.h + + Abstract: + + extract AIG definitions from clauses + Perform cut-set enumeration to identify equivalences. + + Author: + + Nikolaj Bjorner 2020-01-02 + + --*/ + +#pragma once + +#include "sat/sat_cutset.h" +#include "sat/sat_types.h" + +namespace sat { + + enum bool_op { + var_op, + and_op, + ite_op, + xor_op, + no_op + }; + + class aig_cuts { + + struct config { + unsigned m_max_cut_size; + unsigned m_max_cutset_size; + unsigned m_max_aux; + unsigned m_max_insertions; + config(): m_max_cut_size(4), m_max_cutset_size(10), m_max_aux(3), m_max_insertions(10) {} + }; + + // encodes one of var, and, !and, xor, !xor, ite, !ite. + class node { + bool m_sign; + bool_op m_op; + unsigned m_num_children; + unsigned m_offset; + public: + node(): m_sign(false), m_op(no_op), m_num_children(UINT_MAX), m_offset(UINT_MAX) {} + explicit node(unsigned v): m_sign(false), m_op(var_op), m_num_children(UINT_MAX), m_offset(v) {} + explicit node(bool negate, bool_op op, unsigned num_children, unsigned offset): + m_sign(negate), m_op(op), m_num_children(num_children), m_offset(offset) {} + bool is_valid() const { return m_offset != UINT_MAX; } + bool_op op() const { return m_op; } + bool is_var() const { return m_op == var_op; } + bool is_and() const { return m_op == and_op; } + bool is_xor() const { return m_op == xor_op; } + bool is_ite() const { return m_op == ite_op; } + unsigned var() const { SASSERT(is_var()); return m_offset; } + bool sign() const { return m_sign; } + unsigned num_children() const { SASSERT(!is_var()); return m_num_children; } + unsigned offset() const { return m_offset; } + }; + random_gen m_rand; + config m_config; + svector m_aig; // vector of main aig nodes. + vector> m_aux_aig; // vector of auxiliary aig nodes. + literal_vector m_literals; + region m_region; + cut_set m_cut_set1, m_cut_set2; + vector m_cuts; + + void reserve(unsigned v); + bool insert_aux(unsigned v, node const& n); + void init_cut_set(unsigned id); + + bool eq(node const& a, node const& b); + + unsigned_vector filter_valid_nodes() const; + void augment(unsigned_vector const& ids); + void augment(node const& n, cut_set& cs); + void augment_ite(node const& n, cut_set& cs); + void augment_aig0(node const& n, cut_set& cs); + void augment_aig1(node const& n, cut_set& cs); + void augment_aig2(node const& n, cut_set& cs); + void augment_aigN(node const& n, cut_set& cs); + + bool insert_cut(cut const& c, cut_set& cs); + + 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.num_children()); return m_literals[n.offset() + idx]; } + + public: + aig_cuts(); + void add_var(unsigned v); + void add_node(literal head, bool_op op, unsigned sz, literal const* args); + + vector const & get_cuts(); + + std::ostream& display(std::ostream& out) const; + }; + +} + + diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp index 73be5e4c9..296e47d15 100644 --- a/src/sat/sat_aig_simplifier.cpp +++ b/src/sat/sat_aig_simplifier.cpp @@ -40,7 +40,6 @@ namespace sat { aig_simplifier::aig_simplifier(solver& s): s(s), - m_aig_cuts(m_config.m_max_cut_size, m_config.m_max_cutset_size), m_trail_size(0) { } @@ -95,8 +94,7 @@ namespace sat { literal lit = s.trail_literal(m_trail_size); m_aig_cuts.add_node(lit, and_op, 0, 0); } - - + std::function on_and = [&,this](literal head, literal_vector const& ands) { m_aig_cuts.add_node(head, and_op, ands.size(), ands.c_ptr()); @@ -223,220 +221,5 @@ namespace sat { st.update("sat-aig.xors", m_stats.m_num_xors); } - aig_cuts::aig_cuts(unsigned max_cut_size, unsigned max_cutset_size) { - m_max_cut_size = std::min(cut().max_cut_size, max_cut_size); - m_max_cutset_size = max_cutset_size; - } - - vector const& aig_cuts::get_cuts() { - unsigned_vector node_ids = filter_valid_nodes(); - m_cut_set1.init(m_region, m_max_cutset_size + 1); - m_cut_set2.init(m_region, m_max_cutset_size + 1); - augment(node_ids, m_cuts); - return m_cuts; - } - - void aig_cuts::augment(unsigned_vector const& ids, vector& cuts) { - for (unsigned id : ids) { - node const& n = m_aig[id]; - SASSERT(n.is_valid()); - auto& cut_set = cuts[id]; - if (n.is_var()) { - SASSERT(!n.sign()); - } - else if (n.is_ite()) { - augment_ite(n, cut_set, cuts); - } - else if (n.num_children() == 0) { - augment_aig0(n, cut_set, cuts); - } - else if (n.num_children() == 1) { - augment_aig1(n, cut_set, cuts); - } - else if (n.num_children() == 2) { - augment_aig2(n, cut_set, cuts); - } - else if (n.num_children() < m_max_cut_size && cut_set.size() < m_max_cutset_size) { - augment_aigN(n, cut_set, cuts); - } - } - } - - void aig_cuts::augment_ite(node const& n, cut_set& cs, vector& cuts) { - literal l1 = child(n, 0); - literal l2 = child(n, 1); - literal l3 = child(n, 2); - for (auto const& a : cuts[l1.var()]) { - for (auto const& b : cuts[l2.var()]) { - cut ab; - if (!ab.merge(a, b, m_max_cut_size)) { - continue; - } - for (auto const& c : cuts[l3.var()]) { - cut abc; - if (!abc.merge(ab, c, m_max_cut_size)) { - continue; - } - if (cs.size() >= m_max_cutset_size) break; - uint64_t t1 = a.shift_table(abc); - uint64_t t2 = b.shift_table(abc); - uint64_t t3 = c.shift_table(abc); - if (l1.sign()) t1 = ~t1; - if (l2.sign()) t2 = ~t2; - if (l3.sign()) t3 = ~t3; - abc.set_table((t1 & t2) | (~t1 & t3)); - if (n.sign()) abc.negate(); - // extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1; - cs.insert(abc); - } - } - } - } - - void aig_cuts::augment_aig0(node const& n, cut_set& cs, vector& cuts) { - SASSERT(n.is_and()); - cut c; - cs.reset(); - if (n.sign()) { - c.m_table = 0; // constant false - } - else { - c.m_table = 0x3; // constant true - } - cs.insert(c); - } - - void aig_cuts::augment_aig1(node const& n, cut_set& cs, vector& cuts) { - SASSERT(n.is_and()); - literal lit = child(n, 0); - for (auto const& a : cuts[lit.var()]) { - if (cs.size() >= m_max_cutset_size) break; - cut c; - c.set_table(a.m_table); - if (n.sign()) c.negate(); - cs.insert(c); - } - } - - void aig_cuts::augment_aig2(node const& n, cut_set& cs, vector& cuts) { - SASSERT(n.is_and() || n.is_xor()); - literal l1 = child(n, 0); - literal l2 = child(n, 1); - for (auto const& a : cuts[l1.var()]) { - for (auto const& b : cuts[l2.var()]) { - if (cs.size() >= m_max_cutset_size) break; - cut c; - if (c.merge(a, b, m_max_cut_size)) { - 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(); - cs.insert(c); - } - } - if (cs.size() >= m_max_cutset_size) - break; - } - } - - void aig_cuts::augment_aigN(node const& n, cut_set& cs, vector& cuts) { - m_cut_set1.reset(); - SASSERT(n.is_and() || n.is_xor()); - literal lit = child(n, 0); - for (auto const& a : cuts[lit.var()]) { - m_cut_set1.push_back(a); - if (lit.sign()) { - m_cut_set1.back().negate(); - } - } - for (unsigned i = 1; i < n.num_children(); ++i) { - m_cut_set2.reset(); - literal lit = child(n, i); - for (auto const& a : m_cut_set1) { - for (auto const& b : cuts[lit.var()]) { - cut c; - if (m_cut_set2.size() + cs.size() >= m_max_cutset_size) - break; - if (c.merge(a, b, m_max_cut_size)) { - 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.num_children() && n.sign()) c.negate(); - m_cut_set2.insert(c); - } - } - if (m_cut_set2.size() + cs.size() >= m_max_cutset_size) - break; - } - m_cut_set1.swap(m_cut_set2); - } - for (auto & cut : m_cut_set1) { - cs.insert(cut); - } - } - - void aig_cuts::add_var(unsigned v) { - m_aig.reserve(v + 1); - m_cuts.reserve(v + 1); - if (!m_aig[v].is_valid()) { - m_aig[v] = node(v); - init_cut_set(v); - } - SASSERT(m_aig[v].is_valid()); - } - - void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) { - TRACE("aig_simplifier", tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";); - unsigned v = head.var(); - m_aig.reserve(v + 1); - unsigned offset = m_literals.size(); - node n(head.sign(), op, sz, offset); - m_literals.append(sz, args); - for (unsigned i = 0; i < sz; ++i) { - if (!m_aig[args[i].var()].is_valid()) { - add_var(args[i].var()); - } - } - if (!m_aig[v].is_valid() || m_aig[v].is_var() || (sz == 0)) { - m_aig[v] = n; - init_cut_set(v); - } - else { - insert_aux(v, n); - } - SASSERT(m_aig[v].is_valid()); - } - - void aig_cuts::init_cut_set(unsigned id) { - node const& n = m_aig[id]; - SASSERT(n.is_valid()); - auto& cut_set = m_cuts[id]; - cut_set.init(m_region, m_max_cutset_size + 1); - cut_set.push_back(cut(id)); // TBD: if entry is a constant? - if (m_aux_aig.size() < id) { - m_aux_aig[id].reset(); - } - } - - void aig_cuts::insert_aux(unsigned v, node const& n) { - // TBD: throttle and replacement strategy - m_aux_aig.reserve(v + 1); - m_aux_aig[v].push_back(n); - } - - unsigned_vector aig_cuts::filter_valid_nodes() { - unsigned id = 0; - unsigned_vector result; - for (node const& n : m_aig) { - if (n.is_valid()) result.push_back(id); - ++id; - } - return result; - } } diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h index dbd8e9aaf..58962941d 100644 --- a/src/sat/sat_aig_simplifier.h +++ b/src/sat/sat_aig_simplifier.h @@ -19,70 +19,10 @@ #pragma once #include "sat/sat_aig_finder.h" -#include "sat/sat_cutset.h" +#include "sat/sat_aig_cuts.h" namespace sat { - enum bool_op { - var_op, - and_op, - ite_op, - xor_op, - no_op - }; - - class aig_cuts { - // encodes one of var, and, !and, xor, !xor, ite, !ite. - class node { - bool m_sign; - bool_op m_op; - unsigned m_num_children; - unsigned m_offset; - public: - node(): m_sign(false), m_op(no_op), m_num_children(UINT_MAX), m_offset(UINT_MAX) {} - explicit node(unsigned v): m_sign(false), m_op(var_op), m_num_children(UINT_MAX), m_offset(v) {} - explicit node(bool negate, bool_op op, unsigned num_children, unsigned offset): - m_sign(negate), m_op(op), m_num_children(num_children), m_offset(offset) {} - bool is_valid() const { return m_offset != UINT_MAX; } - bool_op op() const { return m_op; } - bool is_var() const { return m_op == var_op; } - bool is_and() const { return m_op == and_op; } - bool is_xor() const { return m_op == xor_op; } - bool is_ite() const { return m_op == ite_op; } - unsigned var() const { SASSERT(is_var()); return m_offset; } - bool sign() const { return m_sign; } - unsigned num_children() const { SASSERT(!is_var()); return m_num_children; } - unsigned offset() const { return m_offset; } - }; - svector m_aig; // vector of main aig nodes. - vector> m_aux_aig; // vector of auxiliary aig nodes. - literal_vector m_literals; - region m_region; - unsigned m_max_cut_size; - unsigned m_max_cutset_size; - cut_set m_cut_set1, m_cut_set2; - vector m_cuts; - - void insert_aux(unsigned v, node const& n); - void init_cut_set(unsigned id); - - unsigned_vector filter_valid_nodes(); - void augment(unsigned_vector const& ids, vector& cuts); - void augment_ite(node const& n, cut_set& cs, vector& cuts); - void augment_aig0(node const& n, cut_set& cs, vector& cuts); - void augment_aig1(node const& n, cut_set& cs, vector& cuts); - void augment_aig2(node const& n, cut_set& cs, vector& cuts); - void augment_aigN(node const& n, cut_set& cs, vector& cuts); - - public: - aig_cuts(unsigned max_cut_size, unsigned max_cutset_size); - void add_var(unsigned v); - void add_node(literal head, bool_op op, unsigned sz, literal const* args); - - literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.num_children()); return m_literals[n.offset() + idx]; } - vector const & get_cuts(); - }; - class aig_simplifier { public: struct stats { @@ -90,15 +30,9 @@ namespace sat { stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; - struct config { - unsigned m_max_cut_size; - unsigned m_max_cutset_size; - config(): m_max_cut_size(4), m_max_cutset_size(10) {} - }; private: - solver& s; - stats m_stats; - config m_config; + solver& s; + stats m_stats; aig_cuts m_aig_cuts; unsigned m_trail_size; literal_vector m_lits; diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp index ab5005862..e23c2b866 100644 --- a/src/sat/sat_cutset.cpp +++ b/src/sat/sat_cutset.cpp @@ -32,12 +32,12 @@ namespace sat { - pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation. */ - void cut_set::insert(cut const& c) { + bool cut_set::insert(cut const& c) { unsigned i = 0, j = 0; for (; i < size(); ++i) { cut const& a = (*this)[i]; if (a.subset_of(c)) { - return; + return false; } if (c.subset_of(a)) { continue; @@ -50,6 +50,7 @@ namespace sat { } shrink(j); push_back(c); + return true; } bool cut_set::no_duplicates() const { diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index 1ed343f64..6da26a7d8 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -115,7 +115,7 @@ namespace sat { m_cuts = new (r) cut[sz]; m_max_size = sz; } - void insert(cut const& c); + bool insert(cut const& c); bool no_duplicates() const; unsigned size() const { return m_size; } cut * begin() const { return m_cuts; } @@ -134,6 +134,7 @@ namespace sat { cut & operator[](unsigned idx) { return m_cuts[idx]; } void shrink(unsigned j) { m_size = j; } void swap(cut_set& other) { std::swap(m_size, other.m_size); std::swap(m_cuts, other.m_cuts); std::swap(m_max_size, other.m_max_size); } + void evict(unsigned idx) { m_cuts[idx] = m_cuts[--m_size]; } }; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3b6123108..fac9490c4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1939,8 +1939,6 @@ namespace sat { if (m_aig_simplifier && m_simplifications > m_config.m_aig_delay && !inconsistent()) { (*m_aig_simplifier)(); - m_aig_simplifier->collect_statistics(m_aux_stats); - // TBD: throttle aig_delay based on yield } } @@ -3770,6 +3768,7 @@ namespace sat { bool_var new_v = mk_var(true, false); lit = literal(new_v, false); m_user_scope_literals.push_back(lit); + m_aig_simplifier = nullptr; // for simplicity, wipe it out TRACE("sat", tout << "user_push: " << lit << "\n";); } @@ -3922,7 +3921,7 @@ namespace sat { m_slow_glue_backup.set_alpha(m_config.m_slow_glue_avg); m_trail_avg.set_alpha(m_config.m_slow_glue_avg); - if (m_config.m_aig_simplify && !m_aig_simplifier) { + if (m_config.m_aig_simplify && !m_aig_simplifier && m_user_scope_literals.empty()) { m_aig_simplifier = alloc(aig_simplifier, *this); } } @@ -3944,6 +3943,7 @@ namespace sat { m_probing.collect_statistics(st); if (m_ext) m_ext->collect_statistics(st); if (m_local_search) m_local_search->collect_statistics(st); + if (m_aig_simplifier) m_aig_simplifier->collect_statistics(st); st.copy(m_aux_stats); }