diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 91d967e76..14fc0dcce 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -49,8 +49,9 @@ namespace dd { m_nodes.reset(); m_free_nodes.reset(); m_pdd_stack.reset(); - m_mpq_table.reset(); m_values.reset(); + m_free_values.reset(); + m_mpq_table.reset(); init_nodes(level2var); } diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp index 9763acb53..c64d93b95 100644 --- a/src/sat/sat_aig_simplifier.cpp +++ b/src/sat/sat_aig_simplifier.cpp @@ -83,12 +83,12 @@ namespace sat { std::function on_xor = [&,this](literal_vector const& xors) { SASSERT(xors.size() > 1); - unsigned max_level = s.def_level(xors.back().var()); + unsigned max_level = xors.back().var(); unsigned index = xors.size() - 1; for (unsigned i = index; i-- > 0; ) { literal l = xors[i]; - if (s.def_level(l.var()) > max_level) { - max_level = s.def_level(l.var()); + if (l.var() > max_level) { + max_level = l.var(); index = i; } } @@ -227,109 +227,138 @@ namespace sat { vector aig_cuts::get_cuts(unsigned max_cut_size, unsigned max_cutset_size) { unsigned_vector sorted = top_sort(); - vector cuts; - cuts.resize(m_aig.size()); - max_cut_size = std::min(cut().max_cut_size, max_cut_size); - cut_set cut_set2; - cut_set2.init(m_region, max_cutset_size + 1); + vector cuts(m_aig.size()); + m_max_cut_size = std::min(cut().max_cut_size, max_cut_size); + m_max_cutset_size = max_cutset_size; + m_cut_set1.init(m_region, m_max_cutset_size + 1); + m_cut_set2.init(m_region, m_max_cutset_size + 1); + + unsigned j = 0; for (unsigned id : sorted) { node const& n = m_aig[id]; - if (!n.is_valid()) { - continue; + if (n.is_valid()) { + auto& cut_set = cuts[id]; + cut_set.init(m_region, m_max_cutset_size + 1); + cut_set.push_back(cut(id)); + sorted[j++] = id; } + } + sorted.shrink(j); + augment(sorted, cuts); + return 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]; - cut_set.init(m_region, max_cutset_size + 1); if (n.is_var()) { SASSERT(!n.sign()); } else if (n.is_ite()) { - 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, max_cut_size)) { - continue; - } - for (auto const& c : cuts[l3.var()]) { - cut abc; - if (!abc.merge(ab, c, max_cut_size)) { - continue; - } - if (cut_set.size() >= 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; - cut_set.insert(abc); - } - } - } + augment_ite(n, cut_set, cuts); } else if (n.num_children() == 2) { - 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 (cut_set.size() >= max_cutset_size) break; - cut c; - if (c.merge(a, b, 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(); - cut_set.insert(c); - } - } - if (cut_set.size() >= max_cutset_size) break; - } + augment_aig2(n, cut_set, cuts); } - else if (n.num_children() < max_cut_size) { - SASSERT(n.is_and() || n.is_xor()); - literal lit = child(n, 0); - for (auto const& a : cuts[lit.var()]) { - cut_set.push_back(a); - if (lit.sign()) { - cut_set.back().negate(); - } - } - for (unsigned i = 1; i < n.num_children(); ++i) { - cut_set2.reset(); - literal lit = child(n, i); - for (auto const& a : cut_set) { - for (auto const& b : cuts[lit.var()]) { - cut c; - if (cut_set2.size() >= max_cutset_size) - break; - if (c.merge(a, b, 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(); - cut_set2.insert(c); - } - } - if (cut_set2.size() >= max_cutset_size) - break; - } - cut_set.swap(cut_set2); - } + else if (n.num_children() < m_max_cut_size && cut_set.size() < m_max_cutset_size) { + augment_aigN(n, cut_set, cuts); } - cut_set.push_back(cut(id)); } - return 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_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) { diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h index 4cde99d5d..3800f3ac8 100644 --- a/src/sat/sat_aig_simplifier.h +++ b/src/sat/sat_aig_simplifier.h @@ -32,7 +32,7 @@ namespace sat { }; class aig_cuts { - // encodes one of var, n1 & n2 & .. & nk, !(n1 & n2 & .. & nk) + // encodes one of var, and, !and, xor, !xor, ite, !ite. class node { bool m_sign; bool_op m_op; @@ -54,11 +54,20 @@ namespace sat { unsigned num_children() const { SASSERT(!is_var()); return m_num_children; } unsigned offset() const { return m_offset; } }; - svector m_aig; // vector of aig nodes. + 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; unsigned_vector top_sort(); + void augment(unsigned_vector const& ids, vector& cuts); + void augment_ite(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: void add_var(unsigned v); void add_node(literal head, bool_op op, unsigned sz, literal const* args); diff --git a/src/sat/sat_anf_simplifier.cpp b/src/sat/sat_anf_simplifier.cpp index a2a39cb3b..db1a3347e 100644 --- a/src/sat/sat_anf_simplifier.cpp +++ b/src/sat/sat_anf_simplifier.cpp @@ -353,7 +353,7 @@ namespace sat { /** assign levels to variables. - use s.def_level as a primary source for the level of a variable. + use variable id as a primary source for the level of a variable. secondarily, sort variables randomly (each variable is assigned a random, unique, id). */ @@ -365,7 +365,7 @@ namespace sat { for (unsigned i = 0; i < nv; ++i) var2id[i] = i; shuffle(var2id.size(), var2id.c_ptr(), s.rand()); for (unsigned i = 0; i < nv; ++i) id2var[var2id[i]] = i; - for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(s.def_level(i), var2id[i]); + for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(i, var2id[i]); std::sort(vl.begin(), vl.end()); for (unsigned i = 0; i < nv; ++i) l2v[i] = id2var[vl[i].second]; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 823508fff..85a37b121 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -151,7 +151,6 @@ namespace sat { m_phase[v] = src.m_phase[v]; m_best_phase[v] = src.m_best_phase[v]; m_prev_phase[v] = src.m_prev_phase[v]; - m_level[v] = src.m_level[v]; // inherit activity: m_activity[v] = src.m_activity[v]; @@ -239,7 +238,7 @@ namespace sat { // // ----------------------- - bool_var solver::mk_var(bool ext, bool dvar, unsigned level) { + bool_var solver::mk_var(bool ext, bool dvar) { m_model_is_current = false; m_stats.m_mk_var++; bool_var v = m_justification.size(); @@ -251,7 +250,6 @@ namespace sat { m_decision.push_back(dvar); m_eliminated.push_back(false); m_external.push_back(ext); - m_level.push_back(level); m_touched.push_back(0); m_activity.push_back(0); m_mark.push_back(false); @@ -3859,7 +3857,6 @@ namespace sat { m_decision.shrink(v); m_eliminated.shrink(v); m_external.shrink(v); - m_level.shrink(v); m_touched.shrink(v); m_activity.shrink(v); m_mark.shrink(v); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a67caeecf..98edec401 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -122,7 +122,6 @@ namespace sat { svector m_lit_mark; svector m_eliminated; svector m_external; - unsigned_vector m_level; unsigned_vector m_touched; unsigned m_touch_index; literal_vector m_replay_assign; @@ -248,9 +247,9 @@ namespace sat { // // ----------------------- void add_clause(unsigned num_lits, literal * lits, bool learned) override { mk_clause(num_lits, lits, learned); } - bool_var add_var(bool ext, unsigned level = 0) override { return mk_var(ext, true, level); } + bool_var add_var(bool ext) override { return mk_var(ext, true); } - bool_var mk_var(bool ext = false, bool dvar = true, unsigned level = 0); + bool_var mk_var(bool ext = false, bool dvar = true); clause* mk_clause(literal_vector const& lits, bool learned = false) { return mk_clause(lits.size(), lits.c_ptr(), learned); } clause* mk_clause(unsigned num_lits, literal * lits, bool learned = false); @@ -335,7 +334,6 @@ namespace sat { bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } - unsigned def_level(bool_var v) const { return m_level[v]; } unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 3bcd4f143..b3c43ea6a 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -63,9 +63,7 @@ namespace sat { add_clause(3, lits, is_redundant); } // create boolean variable, tagged as external (= true) or internal (can be eliminated). - // the level indicates the depth in an ast the variable comes from. - // variables of higher levels are outputs gates relative to lower levels - virtual bool_var add_var(bool ext, unsigned level = 0) = 0; + virtual bool_var add_var(bool ext) = 0; // update parameters virtual void updt_params(params_ref const& p) {} diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7eb24a6a5..a3e6b857c 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -121,7 +121,7 @@ struct goal2sat::imp { sat::literal mk_true() { if (m_true == sat::null_literal) { // create fake variable to represent true; - m_true = sat::literal(m_solver.add_var(false, 0), false); + m_true = sat::literal(m_solver.add_var(false), false); mk_clause(m_true); // v is true } return m_true; @@ -140,7 +140,7 @@ struct goal2sat::imp { } else { bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); - sat::bool_var v = m_solver.add_var(ext, get_depth(t)); + sat::bool_var v = m_solver.add_var(ext); m_map.insert(t, v); l = sat::literal(v, sign); TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << "\n";); @@ -248,7 +248,7 @@ struct goal2sat::imp { } else { SASSERT(num <= m_result_stack.size()); - sat::bool_var k = m_solver.add_var(false, get_depth(t)); + sat::bool_var k = m_solver.add_var(false); sat::literal l(k, false); m_cache.insert(t, l); sat::literal * lits = m_result_stack.end() - num; @@ -287,7 +287,7 @@ struct goal2sat::imp { } else { SASSERT(num <= m_result_stack.size()); - sat::bool_var k = m_solver.add_var(false, get_depth(t)); + sat::bool_var k = m_solver.add_var(false); sat::literal l(k, false); m_cache.insert(t, l); // l => /\ lits @@ -330,7 +330,7 @@ struct goal2sat::imp { m_result_stack.reset(); } else { - sat::bool_var k = m_solver.add_var(false, get_depth(n)); + sat::bool_var k = m_solver.add_var(false); sat::literal l(k, false); m_cache.insert(n, l); mk_clause(~l, ~c, t); @@ -367,7 +367,7 @@ struct goal2sat::imp { m_result_stack.reset(); } else { - sat::bool_var k = m_solver.add_var(false, get_depth(t)); + sat::bool_var k = m_solver.add_var(false); sat::literal l(k, false); m_cache.insert(t, l); mk_clause(~l, l1, ~l2); @@ -391,7 +391,7 @@ struct goal2sat::imp { return; } sat::literal_vector lits; - sat::bool_var v = m_solver.add_var(true, get_depth(t)); + sat::bool_var v = m_solver.add_var(true); lits.push_back(sat::literal(v, true)); convert_pb_args(num, lits); // ensure that = is converted to xor @@ -473,7 +473,7 @@ struct goal2sat::imp { m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); } else { - sat::bool_var v = m_solver.add_var(true, get_depth(t)); + sat::bool_var v = m_solver.add_var(true); sat::literal lit(v, sign); m_ext->add_pb_ge(v, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); @@ -504,7 +504,7 @@ struct goal2sat::imp { m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); } else { - sat::bool_var v = m_solver.add_var(true, get_depth(t)); + sat::bool_var v = m_solver.add_var(true); sat::literal lit(v, sign); m_ext->add_pb_ge(v, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); @@ -518,8 +518,8 @@ struct goal2sat::imp { svector wlits; convert_pb_args(t, wlits); bool base_assert = (root && !sign && m_solver.num_user_scopes() == 0); - sat::bool_var v1 = base_assert ? sat::null_bool_var : m_solver.add_var(true, get_depth(t)); - sat::bool_var v2 = base_assert ? sat::null_bool_var : m_solver.add_var(true, get_depth(t)); + sat::bool_var v1 = base_assert ? sat::null_bool_var : m_solver.add_var(true); + sat::bool_var v2 = base_assert ? sat::null_bool_var : m_solver.add_var(true); m_ext->add_pb_ge(v1, wlits, k.get_unsigned()); k.neg(); for (wliteral& wl : wlits) { @@ -533,7 +533,7 @@ struct goal2sat::imp { } else { sat::literal l1(v1, false), l2(v2, false); - sat::bool_var v = m_solver.add_var(false, get_depth(t)); + sat::bool_var v = m_solver.add_var(false); sat::literal l(v, false); mk_clause(~l, l1); mk_clause(~l, l2); @@ -558,7 +558,7 @@ struct goal2sat::imp { m_ext->add_at_least(sat::null_bool_var, lits, k2); } else { - sat::bool_var v = m_solver.add_var(true, get_depth(t)); + sat::bool_var v = m_solver.add_var(true); sat::literal lit(v, false); m_ext->add_at_least(v, lits, k.get_unsigned()); m_cache.insert(t, lit); @@ -585,7 +585,7 @@ struct goal2sat::imp { m_ext->add_at_least(sat::null_bool_var, lits, k2); } else { - sat::bool_var v = m_solver.add_var(true, get_depth(t)); + sat::bool_var v = m_solver.add_var(true); sat::literal lit(v, false); m_ext->add_at_least(v, lits, k2); m_cache.insert(t, lit); @@ -598,8 +598,8 @@ struct goal2sat::imp { SASSERT(k.is_unsigned()); sat::literal_vector lits; convert_pb_args(t->get_num_args(), lits); - sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true, get_depth(t)); - sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true, get_depth(t)); + sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true); + sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.add_var(true); m_ext->add_at_least(v1, lits, k.get_unsigned()); for (sat::literal& l : lits) { l.neg(); @@ -612,7 +612,7 @@ struct goal2sat::imp { } else { sat::literal l1(v1, false), l2(v2, false); - sat::bool_var v = m_solver.add_var(false, get_depth(t)); + sat::bool_var v = m_solver.add_var(false); sat::literal l(v, false); mk_clause(~l, l1); mk_clause(~l, l2);