From e0a41a18c35247f500e921750e82a68800e03849 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Jan 2020 20:47:38 -0800 Subject: [PATCH] add validation to aig_simplifier, start BIG-based masking Signed-off-by: Nikolaj Bjorner --- src/sat/sat_aig_cuts.cpp | 348 +++++++++++++++++++++++++++------ src/sat/sat_aig_cuts.h | 48 ++++- src/sat/sat_aig_simplifier.cpp | 287 +++++++++++++++++++++++---- src/sat/sat_aig_simplifier.h | 49 ++++- src/sat/sat_cutset.cpp | 52 +++-- src/sat/sat_cutset.h | 77 ++++---- src/sat/sat_drat.cpp | 17 +- src/sat/sat_drat.h | 1 + src/sat/sat_elim_eqs.cpp | 5 + src/sat/sat_solver.cpp | 4 +- src/sat/sat_solver.h | 1 + src/sat/tactic/goal2sat.cpp | 5 +- src/util/old_vector.h | 13 +- src/util/symbol.h | 1 + 14 files changed, 741 insertions(+), 167 deletions(-) diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index 2097d2c7a..15bb3f268 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -16,19 +16,20 @@ --*/ #include "sat/sat_aig_cuts.h" +#include "sat/sat_solver.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); + m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX); + m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX); m_num_cut_calls = 0; + m_num_cuts = 0; } vector const& aig_cuts::operator()() { - flush_roots(); + if (true || m_config.m_full) flush_roots(); unsigned_vector node_ids = filter_valid_nodes(); TRACE("aig_simplifier", display(tout);); augment(node_ids); @@ -42,12 +43,11 @@ namespace sat { if (m_aig[id].empty()) { continue; } - bool t = false; + IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n")); for (node const& n : m_aig[id]) { - IF_VERBOSE(3, if (!t && is_touched(n)) { t = true; m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"); }); - augment(id, n); + augment(id, n); } - IF_VERBOSE(3, if (t) m_cuts[id].display(verbose_stream() << "after\n")); + IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "after\n")); } } @@ -62,53 +62,55 @@ namespace sat { SASSERT(!n.sign()); } else if (n.is_ite()) { - augment_ite(n, cs); + augment_ite(id, n, cs); } - else if (nc == 0) { - augment_aig0(n, cs); + else if (nc == 0) { + augment_aig0(id, n, cs); } else if (nc == 1) { - augment_aig1(n, cs); + augment_aig1(id, n, cs); } else if (nc == 2) { - augment_aig2(n, cs); + augment_aig2(id, n, cs); } - else if (nc < m_config.m_max_cut_size) { - augment_aigN(n, cs); + else if (nc <= cut::max_cut_size()) { + augment_aigN(id, n, cs); } if (m_insertions > 0) { touch(id); } } - bool aig_cuts::insert_cut(cut const& c, cut_set& cs) { - if (!cs.insert(c)) { + bool aig_cuts::insert_cut(unsigned v, cut const& c, cut_set& cs) { + if (!cs.insert(&m_on_cut_add, &m_on_cut_del, c)) { return true; } + m_num_cuts++; if (++m_insertions > m_config.m_max_insertions) { return false; } 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); + evict(cs, idx); } return true; } - void aig_cuts::augment_ite(node const& n, cut_set& cs) { + void aig_cuts::augment_ite(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(2, display(verbose_stream() << "augment_ite " << v << " ", n) << "\n"); literal l1 = child(n, 0); literal l2 = child(n, 1); literal l3 = child(n, 2); 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)) { + if (!ab.merge(a, b)) { continue; } for (auto const& c : m_cuts[l3.var()]) { cut abc; - if (!abc.merge(ab, c, m_config.m_max_cut_size)) { + if (!abc.merge(ab, c)) { continue; } uint64_t t1 = a.shift_table(abc); @@ -117,79 +119,84 @@ namespace sat { if (l1.sign()) t1 = ~t1; if (l2.sign()) t2 = ~t2; if (l3.sign()) t3 = ~t3; - abc.set_table((t1 & t2) | (~t1 & 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)) return; + if (!insert_cut(v, abc, cs)) return; } } } } - void aig_cuts::augment_aig0(node const& n, cut_set& cs) { - SASSERT(n.is_and()); - cs.reset(); + void aig_cuts::augment_aig0(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(4, display(verbose_stream() << "augment_unit " << v << " ", n) << "\n"); + SASSERT(n.is_and() && n.size() == 0); + reset(cs); cut c; c.m_table = (n.sign() ? 0x0 : 0x1); - cs.push_back(c); + push_back(cs, c); } - void aig_cuts::augment_aig1(node const& n, cut_set& cs) { + void aig_cuts::augment_aig1(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(4, display(verbose_stream() << "augment_aig1 " << v << " ", n) << "\n"); SASSERT(n.is_and()); literal lit = child(n, 0); for (auto const& a : m_cuts[lit.var()]) { cut c(a); if (n.sign()) c.negate(); - if (!insert_cut(c, cs)) return; + if (!insert_cut(v, c, cs)) return; } } - void aig_cuts::augment_aig2(node const& n, cut_set& cs) { + void aig_cuts::augment_aig2(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(4, display(verbose_stream() << "augment_aig2 " << v << " ", n) << "\n"); SASSERT(n.is_and() || n.is_xor()); literal l1 = child(n, 0); literal l2 = child(n, 1); 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)) { + 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; + uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2); c.set_table(t3); if (n.sign()) c.negate(); - if (!insert_cut(c, cs)) return; + // validate_aig2(a, b, v, n, c); + if (!insert_cut(v, c, cs)) return; } } } } - void aig_cuts::augment_aigN(node const& n, cut_set& cs) { - m_cut_set1.reset(); + void aig_cuts::augment_aigN(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(4, display(verbose_stream() << "augment_aigN " << v << " ", n) << "\n"); + m_cut_set1.reset(nullptr); 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); + cut b(a); if (lit.sign()) { - m_cut_set1.back().negate(); - } + b.negate(); + } + m_cut_set1.push_back(nullptr, b); } for (unsigned i = 1; i < n.size(); ++i) { - m_cut_set2.reset(); - literal lit = child(n, i); + m_cut_set2.reset(nullptr); + lit = child(n, i); m_insertions = 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)) { + 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; + 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(c, m_cut_set2)) goto next_child; + if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child; } } } @@ -198,7 +205,8 @@ namespace sat { } m_insertions = 0; for (auto & cut : m_cut_set1) { - if (!insert_cut(cut, cs)) { + // validate_aigN(v, n, cut); + if (!insert_cut(v, cut, cs)) { break; } } @@ -240,19 +248,22 @@ namespace sat { std::sort(m_literals.c_ptr() + offset, m_literals.c_ptr() + offset + sz); } for (unsigned i = 0; i < sz; ++i) { + reserve(args[i].var()); if (m_aig[args[i].var()].empty()) { add_var(args[i].var()); } } if (m_aig[v].empty() || n.is_const()) { m_aig[v].reset(); - m_aig[v].push_back(n); + m_aig[v].push_back(n); + on_node_add(v, n); init_cut_set(v); if (n.is_const()) { - augment_aig0(n, m_cuts[v]); + augment_aig0(v, n, m_cuts[v]); } touch(v); - IF_VERBOSE(2, display(verbose_stream() << "add " << head.var() << " == ", n) << "\n"); + IF_VERBOSE(12, display(verbose_stream() << "add " << head.var() << " == ", n) << "\n"); + } else if (m_aig[v][0].is_const() || !insert_aux(v, n)) { m_literals.shrink(m_literals.size() - sz); @@ -262,7 +273,7 @@ namespace sat { } void aig_cuts::set_root(bool_var v, literal r) { - IF_VERBOSE(2, verbose_stream() << "set-root " << v << " -> " << r << "\n"); + IF_VERBOSE(10, verbose_stream() << "set-root " << v << " -> " << r << "\n"); m_roots.push_back(std::make_pair(v, r)); } @@ -282,7 +293,7 @@ namespace sat { // invalidate nodes that have been rooted if (to_root[i] != literal(i, false)) { m_aig[i].reset(); - m_cuts[i].reset(); + reset(m_cuts[i]); } else { for (node & n : m_aig[i]) { @@ -312,17 +323,14 @@ namespace sat { } void aig_cuts::flush_roots(literal_vector const& to_root, cut_set& cs) { - unsigned j = 0; - for (cut& c : cs) { - bool has_stale = false; - for (unsigned v : c) { - has_stale |= (to_root[v] != literal(v, false)); - } - if (!has_stale) { - cs[j++] = c; + for (unsigned j = 0; j < cs.size(); ++j) { + for (unsigned v : cs[j]) { + if (to_root[v] != literal(v, false)) { + evict(cs, j--); + break; + } } } - cs.shrink(j); } void aig_cuts::init_cut_set(unsigned id) { @@ -330,9 +338,9 @@ namespace sat { node const& n = m_aig[id][0]; SASSERT(n.is_valid()); auto& cut_set = m_cuts[id]; - cut_set.init(m_region, m_config.m_max_cutset_size + 1); - cut_set.reset(); - cut_set.push_back(cut(id)); + reset(cut_set); + cut_set.init(m_region, m_config.m_max_cutset_size + 1, id); + push_back(cut_set, cut(id)); } bool aig_cuts::eq(node const& a, node const& b) { @@ -346,6 +354,7 @@ namespace sat { } bool aig_cuts::insert_aux(unsigned v, node const& n) { + if (false && !m_config.m_full) return false; unsigned num_gt = 0, num_eq = 0; for (node const& n2 : m_aig[v]) { if (eq(n, n2)) return false; @@ -353,6 +362,7 @@ namespace sat { else if (n.size() == n2.size()) num_eq++; } if (m_aig[v].size() < m_config.m_max_aux) { + on_node_add(v, n); m_aig[v].push_back(n); touch(v); return true; @@ -362,6 +372,8 @@ namespace sat { for (node const& n2 : m_aig[v]) { if (n.size() < n2.size()) { if (idx == 0) { + on_node_del(v, m_aig[v][idx]); + on_node_add(v, n); m_aig[v][idx] = n; touch(v); return true; @@ -375,6 +387,8 @@ namespace sat { for (node const& n2 : m_aig[v]) { if (n.size() == n2.size()) { if (idx == 0) { + on_node_del(v, m_aig[v][idx]); + on_node_add(v, n); m_aig[v][idx] = n; touch(v); return true; @@ -396,6 +410,216 @@ namespace sat { 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)); + } + } + + void aig_cuts::on_node_del(unsigned v, node const& n) { + if (m_on_clause_del) { + node2def(m_on_clause_del, n, literal(v, false)); + } + } + + void aig_cuts::set_on_clause_add(on_clause_t& on_clause_add) { + m_on_clause_add = on_clause_add; + std::function _on_cut_add = + [this](unsigned v, cut const& c) { cut2def(m_on_clause_add, c, literal(v, false)); }; + m_on_cut_add = _on_cut_add; + } + + void aig_cuts::set_on_clause_del(on_clause_t& on_clause_del) { + m_on_clause_del = on_clause_del; + std::function _on_cut_del = + [this](unsigned v, cut const& c) { cut2def(m_on_clause_del, c, literal(v, false)); }; + m_on_cut_del = _on_cut_del; + } + + /** + * Encode the cut (variables and truth-table) in a set of clauses. + * r is the result. + */ + + void aig_cuts::cut2def(on_clause_t& on_clause, cut const& c, literal r) { + IF_VERBOSE(10, verbose_stream() << "cut2def: " << r << " == " << c << "\n"); + VERIFY(r != null_literal); + unsigned sz = c.size(); + unsigned num_assigns = 1 << sz; + for (unsigned i = 0; i < num_assigns; ++i) { + m_clause.reset(); + for (unsigned j = 0; j < sz; ++j) { + literal lit(c[j], 0 != (i & (1ull << j))); + m_clause.push_back(lit); + } + literal rr = r; + if (0 == (c.m_table & (1ull << i))) rr.neg(); + m_clause.push_back(rr); + on_clause(m_clause); + } + } + + void aig_cuts::node2def(on_clause_t& on_clause, node const& n, literal r) { + IF_VERBOSE(10, display(verbose_stream() << "node2def " << r << " == ", n) << "\n"); + SASSERT(on_clause); + literal c, t, e; + if (n.sign()) r.neg(); + m_clause.reset(); + switch (n.op()) { + case var_op: + return; + case and_op: + for (unsigned i = 0; i < n.size(); ++i) { + m_clause.push_back(~r); + m_clause.push_back(m_literals[n.offset() + i]); + on_clause(m_clause); + m_clause.reset(); + } + for (unsigned i = 0; i < n.size(); ++i) { + m_clause.push_back(~m_literals[n.offset()+i]); + } + m_clause.push_back(r); + on_clause(m_clause); + return; + case ite_op: + // r & c => t, r & ~c => e + // ~r & c => ~t, ~r & ~c => ~e + SASSERT(n.size() == 3); + c = m_literals[n.offset()+0]; + t = m_literals[n.offset()+1]; + e = m_literals[n.offset()+2]; + m_clause.push_back(~r, ~c, t); + on_clause(m_clause); + m_clause.reset(); + m_clause.push_back(~r, c, e); + on_clause(m_clause); + m_clause.reset(); + m_clause.push_back(r, ~c, ~t); + on_clause(m_clause); + m_clause.reset(); + m_clause.push_back(r, c, ~e); + on_clause(m_clause); + return; + case xor_op: { + // r = a ^ b ^ c + // <=> + // ~r ^ a ^ b ^ c = 1 + if (n.size() > 10) { + throw default_exception("cannot handle large xors"); + } + unsigned num_comp = (1 << n.size()); + for (unsigned i = 0; i < num_comp; ++i) { + unsigned parity = 0; + m_clause.reset(); + for (unsigned j = 0; j < n.size(); ++j) { + literal lit = m_literals[n.offset() + j]; + if (0 == (i & (1 << j))) { + lit.neg(); + } + else { + ++parity; + } + m_clause.push_back(lit); + } + m_clause.push_back(1 == (parity % 2) ? r : ~r); + on_clause(m_clause); + } + return; + } + default: + UNREACHABLE(); + break; + } + } + + /** + * compile the truth table from c into clauses that define ~v. + * compile definitions for nodes until all inputs have been covered. + * Assume only the first definition for a node is used for all cuts. + */ + void aig_cuts::cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c) { + svector visited(m_aig.size(), false); + for (unsigned u : c) visited[u] = true; + unsigned_vector todo; + todo.push_back(v); + + while (!todo.empty()) { + unsigned u = todo.back(); + todo.pop_back(); + if (visited[u]) { + continue; + } + visited[u] = true; + node const& n = m_aig[u][0]; + node2def(on_clause, n, literal(u, false)); + for (unsigned i = 0; i < n.size(); ++i) { + todo.push_back(m_literals[n.offset()+i].var()); + } + } + cut2def(on_clause, c, literal(v, true)); + } + + struct aig_cuts::validator { + aig_cuts& t; + params_ref p; + reslimit lim; + solver s; + unsigned_vector vars; + svector is_var; + + validator(aig_cuts& t):t(t),s(p, lim) { + p.set_bool("aig_simplifier", false); + s.updt_params(p); + } + + void on_clause(literal_vector const& clause) { + IF_VERBOSE(20, verbose_stream() << clause << "\n"); + for (literal lit : clause) { + while (lit.var() >= s.num_vars()) s.mk_var(); + is_var.reserve(lit.var() + 1, false); + if (!is_var[lit.var()]) { vars.push_back(lit.var()); is_var[lit.var()] = true; } + } + s.mk_clause(clause); + } + + void check() { + lbool r = s.check(); + IF_VERBOSE(10, verbose_stream() << "check: " << r << "\n"); + if (r == l_true) { + std::sort(vars.begin(), vars.end()); + s.display(std::cout); + for (auto v : vars) std::cout << v << " := " << s.get_model()[v] << "\n"; + std::string line; + std::getline(std::cin, line); + } + } + }; + + void aig_cuts::validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c) { + validator val(*this); + on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); }; + cut2def(on_clause, a, literal(child(n, 0).var(), false)); + cut2def(on_clause, b, literal(child(n, 1).var(), false)); + cut2def(on_clause, c, literal(v, false)); + node2def(on_clause, n, literal(v, true)); + val.check(); + } + + void aig_cuts::validate_aigN(unsigned v, node const& n, cut const& c) { + IF_VERBOSE(10, verbose_stream() << "validate_aigN " << v << " == " << c << "\n"); + validator val(*this); + on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); }; + for (unsigned i = 0; i < n.size(); ++i) { + unsigned w = m_literals[n.offset() + i].var(); + for (cut const& d : m_cuts[w]) { + cut2def(on_clause, d, literal(w, false)); + } + } + cut2def(on_clause, c, literal(v, false)); + node2def(on_clause, n, literal(v, true)); + val.check(); + } + std::ostream& aig_cuts::display(std::ostream& out) const { auto ids = filter_valid_nodes(); for (auto id : ids) { diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h index 63f9569f0..2fd1fcfc0 100644 --- a/src/sat/sat_aig_cuts.h +++ b/src/sat/sat_aig_cuts.h @@ -53,14 +53,17 @@ namespace sat { } class aig_cuts { + public: + typedef std::function on_clause_t; 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(5), m_max_insertions(10) {} + bool m_full; + config(): m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10), m_full(false) {} }; + private: // encodes one of var, and, !and, xor, !xor, ite, !ite. class node { @@ -96,8 +99,12 @@ namespace sat { vector m_cuts; unsigned_vector m_last_touched; unsigned m_num_cut_calls; + unsigned m_num_cuts; svector> m_roots; unsigned m_insertions; + on_clause_t m_on_clause_add, m_on_clause_del; + 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(literal lit) const { return is_touched(lit.var()); } @@ -112,13 +119,13 @@ namespace sat { unsigned_vector filter_valid_nodes() const; void augment(unsigned_vector const& ids); void augment(unsigned id, node const& n); - 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); + void augment_ite(unsigned v, node const& n, cut_set& cs); + void augment_aig0(unsigned v, node const& n, cut_set& cs); + void augment_aig1(unsigned v, node const& n, cut_set& cs); + void augment_aig2(unsigned v, node const& n, cut_set& cs); + void augment_aigN(unsigned v, node const& n, cut_set& cs); - bool insert_cut(cut const& c, cut_set& cs); + bool insert_cut(unsigned v, cut const& c, cut_set& cs); void flush_roots(); void flush_roots(literal_vector const& to_root, node& n); @@ -128,15 +135,40 @@ namespace sat { literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; } + void on_node_add(unsigned v, node const& n); + void on_node_del(unsigned v, node const& n); + + void evict(cut_set& cs, unsigned idx) { cs.evict(&m_on_cut_del, idx); } + void reset(cut_set& cs) { cs.reset(&m_on_cut_del); } + void push_back(cut_set& cs, cut const& c) { cs.push_back(&m_on_cut_add, c); } + void shrink(cut_set& cs, unsigned j) { cs.shrink(&m_on_cut_del, j); } + + void cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c); + void node2def(on_clause_t& on_clause, node const& n, literal r); + + struct validator; + void validate_cut(unsigned v, cut const& c); + void validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c); + void validate_aigN(unsigned v, node const& n, cut const& c); + public: + aig_cuts(); void add_var(unsigned v); void add_node(literal head, bool_op op, unsigned sz, literal const* args); void set_root(bool_var v, literal r); + void set_on_clause_add(on_clause_t& on_clause_add); + void set_on_clause_del(on_clause_t& on_clause_del); + vector const & operator()(); + unsigned num_cuts() const { return m_num_cuts; } + + void cut2def(on_clause_t& on_clause, cut const& c, literal r); + std::ostream& display(std::ostream& out) const; + }; } diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp index f09e500ba..edac66071 100644 --- a/src/sat/sat_aig_simplifier.cpp +++ b/src/sat/sat_aig_simplifier.cpp @@ -35,9 +35,9 @@ namespace sat { m_num_cuts = s.m_stats.m_num_cuts; } ~report() { - unsigned ne = s.m_stats.m_num_eqs - m_num_eqs; + 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 nc = s.m_stats.m_num_cuts - m_num_cuts; IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier"; if (ne > 0) verbose_stream() << " :num-eqs " << ne; @@ -47,9 +47,71 @@ namespace sat { } }; - aig_simplifier::aig_simplifier(solver& s): - s(s), - m_trail_size(0) { + struct aig_simplifier::validator { + solver& _s; + params_ref p; + literal_vector m_assumptions; + + validator(solver& _s, params_ref const& p): _s(_s), p(p) { + } + + void validate(unsigned n, literal const* clause) { + validate(literal_vector(n, clause)); + } + + void validate(literal_vector const& clause) { + if (clause.size() == 2 && clause[0] == ~clause[1]) return; + solver s(p, _s.rlimit()); + s.copy(_s, false); + IF_VERBOSE(10, verbose_stream() << "validate: " << clause << "\n"); + m_assumptions.reset(); + for (literal lit : clause) m_assumptions.push_back(~lit); + lbool r = s.check(clause.size(), m_assumptions.c_ptr()); + if (r != l_false) { + std::cout << "not validated: " << clause << "\n"; + s.display(std::cout); + std::string line; + std::getline(std::cin, line); + } + } + }; + + void aig_simplifier::ensure_validator() { + if (!m_validator) { + std::cout << "init validator\n"; + params_ref p; + p.set_bool("aig", false); + p.set_bool("drat.check_unsat", false); + p.set_sym("drat.file", symbol()); + p.set_uint("max_conflicts", 10000); + m_validator = alloc(validator, s, p); + } + } + + aig_simplifier::aig_simplifier(solver& _s): + s(_s), + m_trail_size(0), + m_validator(nullptr) { + if (false) { + ensure_validator(); + std::function _on_add = + [this](literal_vector const& clause) { + std::cout << "add " << clause << "\n"; m_validator->validate(clause); + }; + m_aig_cuts.set_on_clause_add(_on_add); + } + else if (s.get_config().m_drat) { + std::function _on_add = + [this](literal_vector const& clause) { s.m_drat.add(clause); }; + std::function _on_del = + [this](literal_vector const& clause) { s.m_drat.del(clause); }; + m_aig_cuts.set_on_clause_add(_on_add); + m_aig_cuts.set_on_clause_del(_on_del); + } + } + + aig_simplifier::~aig_simplifier() { + dealloc(m_validator); } void aig_simplifier::add_and(literal head, unsigned sz, literal const* lits) { @@ -96,7 +158,7 @@ namespace sat { ++m_stats.m_num_calls; do { n = m_stats.m_num_eqs + m_stats.m_num_units; - clauses2aig(); + if (m_config.m_full || true) clauses2aig(); aig2clauses(); ++i; } @@ -110,7 +172,7 @@ namespace sat { void aig_simplifier::clauses2aig() { // update units - for (; m_trail_size < s.init_trail_size(); ++m_trail_size) { + for (; m_config.m_full && m_trail_size < s.init_trail_size(); ++m_trail_size) { literal lit = s.trail_literal(m_trail_size); m_aig_cuts.add_node(lit, and_op, 0, 0); } @@ -130,7 +192,7 @@ namespace sat { af.set(on_and); af.set(on_ite); clause_vector clauses(s.clauses()); - clauses.append(s.learned()); + if (m_config.m_full || true) clauses.append(s.learned()); af(clauses); std::function on_xor = @@ -165,8 +227,10 @@ namespace sat { void aig_simplifier::aig2clauses() { vector const& cuts = m_aig_cuts(); + m_stats.m_num_cuts = m_aig_cuts.num_cuts(); + map cut2id; - + union_find_default_ctx ctx; union_find<> uf(ctx), uf2(ctx); for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var(); @@ -176,47 +240,60 @@ namespace sat { }; bool new_eq = false; for (unsigned i = cuts.size(); i-- > 0; ) { - m_stats.m_num_cuts += cuts[i].size(); - - for (auto& cut : cuts[i]) { + for (auto& c : cuts[i]) { unsigned j = 0; - if (cut.is_true()) { + if (m_config.m_full && c.is_true()) { if (s.value(i) == l_undef) { - IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, false) << "\n"); - s.assign_unit(literal(i, false)); + literal lit(i, false); + validate_unit(lit); + IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n"); + s.assign_unit(lit); ++m_stats.m_num_units; } break; } - if (cut.is_false()) { + if (m_config.m_full && c.is_false()) { if (s.value(i) == l_undef) { - IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, true) << "\n"); - s.assign_unit(literal(i, true)); + literal lit(i, true); + validate_unit(lit); + IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n"); + s.assign_unit(lit); ++m_stats.m_num_units; } break; } - if (cut2id.find(&cut, j)) { - if (i == j) std::cout << "dup: " << i << "\n"; + if (cut2id.find(&c, j)) { VERIFY(i != j); - literal v(i, false); - literal w(j, false); - add_eq(v, w); - TRACE("aig_simplifier", tout << v << " == " << ~w << "\n";); + literal u(i, false); + literal v(j, false); + IF_VERBOSE(0, + verbose_stream() << u << " " << c << "\n"; + verbose_stream() << v << ": "; + for (cut const& d : cuts[v.var()]) verbose_stream() << d << "\n";); + + certify_equivalence(u, v, c); + //validate_eq(u, v); + add_eq(u, v); + TRACE("aig_simplifier", tout << u << " == " << v << "\n";); new_eq = true; break; } - cut.negate(); - if (cut2id.find(&cut, j)) { - literal v(i, false); - literal w(j, true); - add_eq(v, w); - TRACE("aig_simplifier", tout << v << " == " << w << "\n";); - new_eq = true; - break; + if (true || m_config.m_full) { + cut nc(c); + nc.negate(); + if (cut2id.find(&nc, j)) { + VERIFY(i != j); // maybe possible with don't cares + literal u(i, false); + literal v(j, true); + certify_equivalence(u, v, c); + // validate_eq(u, v); + add_eq(u, v); + TRACE("aig_simplifier", tout << u << " == " << v << "\n";); + new_eq = true; + break; + } } - cut.negate(); - cut2id.insert(&cut, i); + cut2id.insert(&c, i); } } if (!new_eq) { @@ -252,6 +329,134 @@ namespace sat { elim(uf2); } + /** + * Equilvalences modulo cuts are not necessarily DRAT derivable. + * To ensure that there is a DRAT derivation we create all resolvents + * of the LUT clauses until deriving binary u or ~v and ~u or v. + * each resolvent is DRAT derivable because there are two previous lemmas that + * contain complementary literals. + */ + void aig_simplifier::certify_equivalence(literal u, literal v, cut const& c) { + if (!s.m_config.m_drat) return; + + vector clauses; + std::function on_clause = + [&](literal_vector const& clause) { SASSERT(clause.back().var() == u.var()); clauses.push_back(clause); }; + m_aig_cuts.cut2def(on_clause, c, u); + + // create C or u or ~v for each clause C or u + // create C or ~u or v for each clause C or ~u + for (auto& clause : clauses) { + literal w = clause.back(); + SASSERT(w.var() == u.var()); + clause.push_back(w == u ? ~v : v); + s.m_drat.add(clause); + } + // create C or ~u or v for each clause + unsigned i = 0, sz = clauses.size(); + for (; i < sz; ++i) { + literal_vector clause(clauses[i]); + clause[clause.size()-2] = ~clause[clause.size()-2]; + clause[clause.size()-1] = ~clause[clause.size()-1]; + clauses.push_back(clause); + s.m_drat.add(clause); + } + + // create all resolvents over C. C is assumed to + // contain all combinations of some set of literals. + i = 0; sz = clauses.size(); + while (sz - i > 2) { + SASSERT((sz & (sz - 1)) == 0); + for (; i < sz; ++i) { + auto const& clause = clauses[i]; + if (clause[0].sign()) { + literal_vector cl(clause.size() - 1, clause.c_ptr() + 1); + clauses.push_back(cl); + s.m_drat.add(cl); + } + } + i = sz; + sz = clauses.size(); + } + + IF_VERBOSE(10, for (auto const& clause : clauses) verbose_stream() << clause << "\n";); + + // once we established equivalence, don't need auxiliary clauses for DRAT. + for (auto const& clause : clauses) { + if (clause.size() > 2) { + s.m_drat.del(clause); + } + } + } + + /** + * collect pairs of variables that occur in cut sets. + */ + void aig_simplifier::collect_pairs(vector const& cuts) { + m_pairs.reset(); + for (unsigned k = cuts.size(); k-- > 0; ) { + for (auto const& c : cuts[k]) { + for (unsigned i = c.size(); i-- > 0; ) { + for (unsigned j = i; j-- > 0; ) { + m_pairs.insert(var_pair(c[i],c[j])); + } + } + } + } + } + + /** + * compute masks for pairs. + */ + void aig_simplifier::add_masks_to_pairs() { + big b(s.rand()); + b.init(s, true); + for (auto& p : m_pairs) { + literal u(p.u, false), v(p.v, false); + // u -> v, then u & ~v is impossible + if (b.connected(u, v)) { + add_mask(u, ~v, p); + } + else if (b.connected(u, ~v)) { + add_mask(u, v, p); + } + else if (b.connected(~u, v)) { + add_mask(~u, ~v, p); + } + else if (b.connected(~u, ~v)) { + add_mask(~u, v, p); + } + else { + memset(p.masks, 0xFF, var_pair::size()); + } + } + } + + /* + * compute masks for each possible occurrence of u, v within 2-6 elements. + * combinaions relative to u.sign(), v.sign() are impossible. + */ + void aig_simplifier::add_mask(literal u, literal v, var_pair& p) { + unsigned offset = 0; + bool su = u.sign(), sv = v.sign(); + for (unsigned k = 2; k <= 6; ++k) { + for (unsigned i = 0; i < k; ++i) { + for (unsigned j = i + 1; j < k; ++j) { + // convert su, sv, k, i, j into a mask for 2^k bits. + // for outputs + p.masks[offset++] = 0; + } + } + } + } + + /** + * apply obtained masks to cut sets. + */ + void aig_simplifier::apply_masks() { + + } + void aig_simplifier::collect_statistics(statistics& st) const { st.update("sat-aig.eqs", m_stats.m_num_eqs); st.update("sat-aig.cuts", m_stats.m_num_cuts); @@ -259,6 +464,20 @@ namespace sat { st.update("sat-aig.ites", m_stats.m_num_ites); st.update("sat-aig.xors", m_stats.m_num_xors); } + + void aig_simplifier::validate_unit(literal lit) { + ensure_validator(); + m_validator->validate(1, &lit); + } + + void aig_simplifier::validate_eq(literal a, literal b) { + ensure_validator(); + literal lits1[2] = { a, ~b }; + literal lits2[2] = { ~a, b }; + m_validator->validate(2, lits1); + m_validator->validate(2, lits1); + } + } diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h index 4ffacfedc..0ace074b9 100644 --- a/src/sat/sat_aig_simplifier.h +++ b/src/sat/sat_aig_simplifier.h @@ -31,19 +31,64 @@ namespace sat { stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; + struct config { + bool m_full; + config():m_full(false) {} + }; private: + struct report; + struct validator; + solver& s; stats m_stats; + config m_config; aig_cuts m_aig_cuts; unsigned m_trail_size; literal_vector m_lits; + validator* m_validator; - struct report; void clauses2aig(); void aig2clauses(); + void ensure_validator(); + void validate_unit(literal lit); + void validate_eq(literal a, literal b); + void certify_equivalence(literal u, literal v, cut const& c); + + /** + * collect pairs of literal combinations that are impossible + * base on binary implication graph queries. + * Apply the masks on cut sets so to allow detecting + * equivalences modulo implications. + */ + struct var_pair { + unsigned u, v; + uint64_t masks[35]; + static unsigned size() { return sizeof(uint64_t)*35; } + var_pair(unsigned u, unsigned v): u(u), v(v) { + if (u > v) std::swap(u, v); + } + var_pair(): u(UINT_MAX), v(UINT_MAX) {} + + struct hash { + unsigned operator()(var_pair const& p) const { + return mk_mix(p.u, p.v, 1); + } + }; + struct eq { + bool operator()(var_pair const& a, var_pair const& b) const { + return a.u == b.u && a.v == b.v; + } + }; + }; + hashtable m_pairs; + + void collect_pairs(vector const& cuts); + void add_mask(literal u, literal v, var_pair& p); + void add_masks_to_pairs(); + void apply_masks(); public: aig_simplifier(solver& s); - ~aig_simplifier() {} + ~aig_simplifier(); void operator()(); void collect_statistics(statistics& st) const; diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp index 4863c5b92..ca1f4690b 100644 --- a/src/sat/sat_cutset.cpp +++ b/src/sat/sat_cutset.cpp @@ -19,7 +19,6 @@ namespace sat { - /** \brief if c is subsumed by a member in cut_set, then c is not inserted. @@ -32,25 +31,19 @@ namespace sat { - pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation. */ - bool cut_set::insert(cut const& c) { - SASSERT(c.m_size > 0); - unsigned i = 0, j = 0; - for (; i < size(); ++i) { + bool cut_set::insert(on_update_t* on_add, on_update_t* on_del, cut const& c) { + unsigned i = 0, j = 0, k = m_size; + for (; i < k; ++i) { cut const& a = (*this)[i]; if (a.subset_of(c)) { return false; } if (c.subset_of(a)) { - continue; + std::swap(m_cuts[i--], m_cuts[--k]); } - else if (j < i) { - (*this)[j] = a; - } - SASSERT(!(a == c)); - ++j; } - shrink(j); - push_back(c); + shrink(on_del, i); + push_back(on_add, c); return true; } @@ -70,6 +63,37 @@ namespace sat { return out; } + + void cut_set::shrink(on_update_t* on_del, unsigned j) { + if (m_var != UINT_MAX && on_del && *on_del) { + for (unsigned i = j; i < m_size; ++i) { + (*on_del)(m_var, m_cuts[i]); + } + } + m_size = j; + } + + void cut_set::push_back(on_update_t* on_add, cut const& c) { + SASSERT(m_max_size > 0); + if (m_size == m_max_size) { + m_max_size *= 2; + cut* new_cuts = new (*m_region) cut[m_max_size]; + memcpy(new_cuts, m_cuts, sizeof(cut)*m_size); + m_cuts = new_cuts; + } + if (m_var != UINT_MAX && on_add && *on_add) (*on_add)(m_var, c); + m_cuts[m_size++] = c; + } + + void cut_set::init(region& r, unsigned max_sz, unsigned v) { + m_var = v; + m_max_size = max_sz; + SASSERT(!m_region || m_cuts); + if (m_region) return; + m_region = &r; + m_cuts = new (r) cut[max_sz]; + } + /** \brief shift table 'a' by adding elements from 'c'. a.shift_table(c) @@ -127,7 +151,7 @@ namespace sat { out << (*this)[i]; if (i + 1 < m_size) out << " "; } - out << "} t: "; + out << "} "; for (unsigned i = 0; i < (1u << m_size); ++i) { if (0 != (m_table & (1ull << i))) out << "1"; else out << "0"; } diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index 95cf577fc..ca496ed39 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -17,29 +17,41 @@ #include "util/util.h" #include #include +#include namespace sat { - struct cut { - unsigned max_cut_size; + class cut { unsigned m_filter; unsigned m_size; - unsigned m_elems[6]; + unsigned m_elems[4]; + public: uint64_t m_table; - cut(): max_cut_size(6), m_filter(0), m_size(0), m_table(0) {} + cut(): m_filter(0), m_size(0), m_table(0) {} cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2) { m_elems[0] = id; } - cut(cut const& other): m_filter(other.m_filter), m_size(other.m_size), m_table(other.m_table) { - for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i]; + cut(cut const& other) { + *this = other; } + cut& operator=(cut const& other) { + m_filter = other.m_filter; + m_size = other.m_size; + m_table = other.m_table; + for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i]; + return *this; + } + + unsigned size() const { return m_size; } + + static unsigned max_cut_size() { return 4; } + unsigned const* begin() const { return m_elems; } unsigned const* end() const { return m_elems + m_size; } - bool add(unsigned i, unsigned max_sz) { - SASSERT(max_sz <= max_cut_size); - if (m_size >= max_sz) { + bool add(unsigned i) { + if (m_size >= max_cut_size()) { return false; } else { @@ -73,12 +85,12 @@ namespace sat { uint64_t shift_table(cut const& other) const; - bool merge(cut const& a, cut const& b, unsigned max_sz) { + bool merge(cut const& a, cut const& b) { unsigned i = 0, j = 0; unsigned x = a[i]; unsigned y = b[j]; while (x != UINT_MAX || y != UINT_MAX) { - if (!add(std::min(x, y), max_sz)) { + if (!add(std::min(x, y))) { return false; } if (x < y) { @@ -115,41 +127,32 @@ namespace sat { }; class cut_set { + unsigned m_var; region* m_region; unsigned m_size; unsigned m_max_size; cut * m_cuts; public: - cut_set(): m_region(nullptr), m_size(0), m_max_size(0), m_cuts(nullptr) {} - void init(region& r, unsigned sz) { - m_max_size = sz; - SASSERT(!m_region || m_cuts); - if (m_region) return; - m_region = &r; - m_cuts = new (r) cut[sz]; - } - bool insert(cut const& c); + typedef std::function on_update_t; + + cut_set(): m_var(UINT_MAX), m_region(nullptr), m_size(0), m_max_size(0), m_cuts(nullptr) {} + void init(region& r, unsigned max_sz, unsigned v); + bool insert(on_update_t* on_add, on_update_t* on_del, cut const& c); bool no_duplicates() const; unsigned size() const { return m_size; } - cut * begin() const { return m_cuts; } - cut * end() const { return m_cuts + m_size; } - cut & back() { return m_cuts[m_size-1]; } - void push_back(cut const& c) { - SASSERT(c.m_size > 0); - if (m_size == m_max_size) { - m_max_size *= 2; - cut* new_cuts = new (*m_region) cut[m_max_size]; - memcpy(new_cuts, m_cuts, sizeof(cut)*m_size); - m_cuts = new_cuts; - } - m_cuts[m_size++] = c; - } - void reset() { m_size = 0; } - cut & operator[](unsigned idx) { return m_cuts[idx]; } - void shrink(unsigned j) { m_size = j; } + cut const * begin() const { return m_cuts; } + cut const * end() const { return m_cuts + m_size; } + 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]; } + void shrink(on_update_t* on_del, unsigned 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]; } + void evict(on_update_t* on_del, unsigned idx) { if (m_var != UINT_MAX && on_del && *on_del) (*on_del)(m_var, m_cuts[idx]); m_cuts[idx] = m_cuts[--m_size]; } std::ostream& display(std::ostream& out) const; }; + inline std::ostream& operator<<(std::ostream& out, cut const& c) { return c.display(out); } + inline std::ostream& operator<<(std::ostream& out, cut_set const& cs) { return cs.display(out); } + } diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 0beda9d57..bf8c51658 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -399,7 +399,7 @@ namespace sat { } m_units.shrink(num_units); bool ok = m_inconsistent; - IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n"); + // IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n"); m_inconsistent = false; return ok; @@ -465,7 +465,9 @@ namespace sat { if (!is_drup(n, c) && !is_drat(n, c)) { literal_vector lits(n, c); std::cout << "Verification of " << lits << " failed\n"; - s.display(std::cout); + // s.display(std::cout); + std::string line; + std::getline(std::cin, line); SASSERT(false); exit(0); UNREACHABLE(); @@ -756,7 +758,6 @@ namespace sat { } #endif ++m_num_del; - //SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true))); if (m_out) dump(c.size(), c.begin(), status::deleted); if (m_bout) bdump(c.size(), c.begin(), status::deleted); if (m_check) { @@ -764,6 +765,16 @@ namespace sat { append(*c1, status::deleted); } } + + void drat::del(literal_vector const& c) { + ++m_num_del; + if (m_out) dump(c.size(), c.begin(), status::deleted); + if (m_bout) bdump(c.size(), c.begin(), status::deleted); + if (m_check) { + clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), true); + append(*c1, status::deleted); + } + } void drat::check_model(model const& m) { } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 91059703d..17c1868c0 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -98,6 +98,7 @@ namespace sat { bool is_cleaned(clause& c) const; void del(literal l); void del(literal l1, literal l2); + void del(literal_vector const& lits); void del(clause& c); void verify(clause const& c) { verify(c.size(), c.begin()); } diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 06968ec69..20280a772 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -235,6 +235,11 @@ namespace sat { bool root_ok = !m_solver.is_external(v) || set_root; if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) { // cannot really eliminate v, since we have to notify extension of future assignments + if (m_solver.m_config.m_drat && m_solver.m_config.m_drat_file.is_null()) { + std::cout << "DRAT\n"; + m_solver.m_drat.add(~l, r, true); + m_solver.m_drat.add(l, ~r, true); + } m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fac9490c4..c3759739f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1211,7 +1211,7 @@ namespace sat { init_assumptions(num_lits, lits); propagate(false); if (check_inconsistent()) return l_false; - do_cleanup(m_config.m_force_cleanup); + if (m_config.m_force_cleanup) do_cleanup(true); if (m_config.m_unit_walk) { return do_unit_walk(); @@ -1236,7 +1236,7 @@ namespace sat { while (is_sat == l_undef && !should_cancel()) { if (inconsistent()) is_sat = resolve_conflict_core(); else if (should_propagate()) propagate(true); - else if (do_cleanup(false)) continue; + else if (m_conflicts_since_init > 0 && do_cleanup(false)) continue; else if (should_gc()) do_gc(); else if (should_rephase()) do_rephase(); else if (should_reorder()) do_reorder(); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index cdb1142c9..c8ad50241 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -208,6 +208,7 @@ namespace sat { friend class drat; friend class ba_solver; friend class anf_simplifier; + friend class aig_simplifier; friend class parallel; friend class lookahead; friend class local_search; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 73f000193..596179145 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -257,8 +257,6 @@ struct goal2sat::imp { m_cache.insert(t, l); sat::literal * lits = m_result_stack.end() - num; - if (m_aig) m_aig->add_or(l, num, lits); - for (unsigned i = 0; i < num; i++) { mk_clause(~lits[i], l); } @@ -267,6 +265,7 @@ struct goal2sat::imp { // remark: mk_clause may perform destructive updated to lits. // I have to execute it after the binary mk_clause above. mk_clause(num+1, lits); + if (m_aig) m_aig->add_or(l, num, lits); unsigned old_sz = m_result_stack.size() - num - 1; m_result_stack.shrink(old_sz); if (sign) @@ -299,7 +298,6 @@ struct goal2sat::imp { m_cache.insert(t, l); sat::literal * lits = m_result_stack.end() - num; - if (m_aig) m_aig->add_and(l, num, lits); // l => /\ lits for (unsigned i = 0; i < num; i++) { @@ -312,6 +310,7 @@ struct goal2sat::imp { m_result_stack.push_back(l); lits = m_result_stack.end() - num - 1; mk_clause(num+1, lits); + if (m_aig) m_aig->add_and(l, num, lits); unsigned old_sz = m_result_stack.size() - num - 1; m_result_stack.shrink(old_sz); if (sign) diff --git a/src/util/old_vector.h b/src/util/old_vector.h index 47dc88aab..7f214803c 100644 --- a/src/util/old_vector.h +++ b/src/util/old_vector.h @@ -414,20 +414,29 @@ public: reinterpret_cast(m_data)[SIZE_IDX]--; } - void push_back(T const & elem) { + old_vector& push_back(T const & elem) { if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { expand_vector(); } new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); reinterpret_cast(m_data)[SIZE_IDX]++; + return *this; } - void push_back(T && elem) { + template + old_vector& push_back(T const& elem, T elem2, Args ... elems) { + push_back(elem); + push_back(elem2, elems ...); + return *this; + } + + old_vector& push_back(T && elem) { if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { expand_vector(); } new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); reinterpret_cast(m_data)[SIZE_IDX]++; + return *this; } void insert(T const & elem) { diff --git a/src/util/symbol.h b/src/util/symbol.h index f902e80d7..2f2d5eeae 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -70,6 +70,7 @@ public: friend bool operator!=(symbol const & s1, symbol const & s2) { return s1.m_data != s2.m_data; } bool is_numerical() const { return GET_TAG(m_data) == 1; } bool is_null() const { return m_data == nullptr; } + bool is_non_empty_string() const { return !is_null() && !is_numerical() && 0 != bare_str()[0]; } unsigned int get_num() const { SASSERT(is_numerical()); return UNBOXINT(m_data); } std::string str() const; friend bool operator==(symbol const & s1, char const * s2) {