3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-05 21:51:34 -08:00
parent 2acab46388
commit 63fc62fbe4
6 changed files with 72 additions and 51 deletions

View file

@ -35,15 +35,13 @@ namespace sat {
return false;
}
void aig_finder::find_aigs(clause_vector& clauses) {
if (!m_on_aig) {
return;
}
unsigned j = 0;
for (clause* cp : clauses) {
clause& c = *cp;
if (!find_aig(c)) {
if (!find_aig(*cp)) {
clauses[j++] = cp;
}
}
@ -61,9 +59,7 @@ namespace sat {
for (literal head : c) {
is_aig = true;
for (literal tail : c) {
if (head == tail)
continue;
if (!implies(head, ~tail)) {
if (head != tail && !implies(head, ~tail)) {
is_aig = false;
break;
}
@ -187,25 +183,28 @@ namespace sat {
insert_ternary(*cp);
}
auto try_ite = [&,this](literal x, literal y, literal z, clause& c) {
clause* c1, *c3;
if (has_ternary(y, ~z, ~x, c1)) {
binary b(~y, x, nullptr);
if (!binaries.find(b, b)) {
return false;
}
for (auto p : *b.use_list) {
literal u = p.first;
clause* c2 = p.second;
if (has_ternary(~u, ~x, ~y, c3)) {
c.mark_used();
if (c1) c1->mark_used();
if (c2) c2->mark_used();
if (c3) c3->mark_used();
// DEBUG_CODE(validate_if(~x, ~y, z, u, c, c1, c2, c3););
m_on_if(~x, ~y, z, u);
return true;
}
literal u;
clause* c1, *c2, *c3;
if (!has_ternary(y, ~z, ~x, c1)) {
return false;
}
binary b(~y, x, nullptr);
if (!binaries.find(b, b)) {
return false;
}
for (auto p : *b.use_list) {
u = p.first;
c2 = p.second;
if (!has_ternary(~u, ~x, ~y, c3)) {
continue;
}
c.mark_used();
if (c1) c1->mark_used();
if (c2) c2->mark_used();
if (c3) c3->mark_used();
// DEBUG_CODE(validate_if(~x, ~y, z, u, c, c1, c2, c3););
m_on_if(~x, ~y, z, u);
return true;
}
return false;
};
@ -214,7 +213,7 @@ namespace sat {
clause& c = *cp;
if (c.size() != 3 || c.was_used()) continue;
literal x = c[0], y = c[1], z = c[2];
if (try_ite(x, y, z, c)) continue;
if (try_ite(x, z, y, c)) continue;
if (try_ite(y, x, z, c)) continue;
if (try_ite(z, y, x, c)) continue;
}

View file

@ -176,7 +176,6 @@ namespace sat {
void aig_simplifier::aig2clauses(aig_cuts& aigc) {
vector<cut_set> cuts = aigc.get_cuts(m_config.m_max_cut_size, m_config.m_max_cutset_size);
map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;
literal_vector roots(s.num_vars(), null_literal);
union_find_default_ctx ctx;
union_find<> uf(ctx);
@ -212,23 +211,10 @@ namespace sat {
cut2id.insert(&cut, i);
}
}
if (old_num_eqs == m_stats.m_num_eqs) {
return;
if (old_num_eqs < m_stats.m_num_eqs) {
elim_eqs elim(s);
elim(uf);
}
bool_var_vector to_elim;
for (unsigned i = s.num_vars(); i-- > 0; ) {
literal l1(i, false);
unsigned idx = uf.find(l1.index());
if (idx != l1.index()) {
roots[i] = to_literal(idx);
to_elim.push_back(i);
}
else {
roots[i] = l1;
}
}
elim_eqs elim(s);
elim(roots, to_elim);
}
void aig_simplifier::collect_statistics(statistics& st) const {

View file

@ -15,8 +15,10 @@
--*/
#include "util/union_find.h"
#include "sat/sat_anf_simplifier.h"
#include "sat/sat_solver.h"
#include "sat/sat_elim_eqs.h"
#include "sat/sat_xor_finder.h"
#include "sat/sat_aig_finder.h"
#include "math/grobner/pdd_solver.h"
@ -32,7 +34,7 @@ namespace sat {
IF_VERBOSE(2,
verbose_stream() << " (sat.anf.simplifier"
<< " :num-units " << s.m_stats.m_num_units
<< " :num-eqs " << s.m_stats.m_num_eq
<< " :num-eqs " << s.m_stats.m_num_eqs
<< " :mb " << mem_stat()
<< m_watch << ")\n");
}
@ -61,6 +63,15 @@ namespace sat {
*/
void anf_simplifier::anf2clauses(pdd_solver& solver) {
union_find_default_ctx ctx;
union_find<> uf(ctx);
for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var();
auto add_eq = [&](literal l1, literal l2) {
uf.merge(l1.index(), l2.index());
uf.merge((~l1).index(), (~l2).index());
};
unsigned old_num_eqs = m_stats.m_num_eqs;
for (auto* e : solver.equations()) {
auto const& p = e->poly();
if (p.is_one()) {
@ -80,13 +91,17 @@ namespace sat {
// x + y + c = 0
SASSERT(!p.is_val() && p.hi().is_one() && !p.lo().is_val() && p.lo().hi().is_one() && p.lo().lo().is_val());
literal x(p.var(), false);
literal y(p.lo().var(), p.lo().lo().is_zero());
s.mk_clause(x, y, true);
s.mk_clause(~x, ~y, true);
++m_stats.m_num_eq;
literal y(p.lo().var(), p.lo().lo().is_one());
add_eq(x, y);
++m_stats.m_num_eqs;
TRACE("anf_simplifier", tout << "equivalence " << p << " : " << x << " == " << y << "\n";);
}
}
if (old_num_eqs < m_stats.m_num_eqs) {
elim_eqs elim(s);
elim(uf);
}
}
/**
@ -104,13 +119,13 @@ namespace sat {
void anf_simplifier::anf2phase(pdd_solver& solver) {
if (!m_config.m_anf2phase)
return;
m_eval_ts = 0;
reset_eval();
auto const& eqs = solver.equations();
for (unsigned i = eqs.size(); i-- > 0; ) {
dd::pdd const& p = eqs[i]->poly();
if (!p.is_val() && p.hi().is_one() && s.m_best_phase[p.var()] != eval(p.lo())) {
s.m_best_phase[p.var()] = !s.m_best_phase[p.var()];
++m_stats.m_num_phase_flips;
}
}
}
@ -415,10 +430,11 @@ namespace sat {
void anf_simplifier::save_statistics(pdd_solver& solver) {
solver.collect_statistics(m_st);
m_st.update("sat-anf.units", m_stats.m_num_units);
m_st.update("sat-anf.eqs", m_stats.m_num_eq);
m_st.update("sat-anf.eqs", m_stats.m_num_eqs);
m_st.update("sat-anf.ands", m_stats.m_num_aigs);
m_st.update("sat-anf.ites", m_stats.m_num_ifs);
m_st.update("sat-anf.xors", m_stats.m_num_xors);
m_st.update("sat-anf.phase_flips", m_stats.m_num_phase_flips);
}
}

View file

@ -57,8 +57,9 @@ namespace sat {
struct report;
struct stats {
unsigned m_num_units, m_num_eq;
unsigned m_num_units, m_num_eqs;
unsigned m_num_aigs, m_num_xors, m_num_ifs;
unsigned m_num_phase_flips;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
@ -109,7 +110,7 @@ namespace sat {
public:
anf_simplifier(solver& s) : s(s) {}
anf_simplifier(solver& s) : s(s), m_eval_ts(0) {}
~anf_simplifier() {}
void operator()();

View file

@ -284,4 +284,21 @@ namespace sat {
SASSERT(check_clauses(roots));
TRACE("elim_eqs", tout << "after full cleanup\n"; m_solver.display(tout););
}
void elim_eqs::operator()(union_find<>& uf) {
literal_vector roots(m_solver.num_vars(), null_literal);
bool_var_vector to_elim;
for (unsigned i = m_solver.num_vars(); i-- > 0; ) {
literal l1(i, false);
unsigned idx = uf.find(l1.index());
if (idx != l1.index()) {
roots[i] = to_literal(idx);
to_elim.push_back(i);
}
else {
roots[i] = l1;
}
}
(*this)(roots, to_elim);
}
};

View file

@ -20,6 +20,7 @@ Revision History:
#define SAT_ELIM_EQS_H_
#include "sat/sat_types.h"
#include "util/union_find.h"
namespace sat {
class solver;
@ -44,6 +45,7 @@ namespace sat {
elim_eqs(solver & s);
~elim_eqs();
void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
void operator()(union_find<>& uf);
};
};