mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix how don't cares are handled
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ba292346ae
commit
0e096c55a9
|
@ -132,7 +132,7 @@ namespace sat {
|
|||
SASSERT(n.is_and() && n.size() == 0);
|
||||
reset(cs);
|
||||
cut c;
|
||||
c.m_table = (n.sign() ? 0x0 : 0x1);
|
||||
c.set_table(n.sign() ? 0x0 : 0x1);
|
||||
push_back(cs, c);
|
||||
}
|
||||
|
||||
|
@ -212,11 +212,6 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
void aig_cuts::replace(unsigned v, cut const& src, cut const& dst) {
|
||||
m_cuts[v].replace(m_on_cut_add, m_on_cut_del, src, dst);
|
||||
touch(v);
|
||||
}
|
||||
|
||||
|
||||
bool aig_cuts::is_touched(node const& n) {
|
||||
for (unsigned i = 0; i < n.size(); ++i) {
|
||||
|
@ -459,7 +454,7 @@ namespace sat {
|
|||
m_clause.push_back(lit);
|
||||
}
|
||||
literal rr = r;
|
||||
if (0 == (c.m_table & (1ull << i))) rr.neg();
|
||||
if (0 == (c.table() & (1ull << i))) rr.neg();
|
||||
m_clause.push_back(rr);
|
||||
on_clause(m_clause);
|
||||
}
|
||||
|
|
|
@ -109,7 +109,6 @@ namespace sat {
|
|||
bool is_touched(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 touch(bool_var v) { m_last_touched[v] = v + 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);
|
||||
|
@ -166,7 +165,7 @@ namespace sat {
|
|||
|
||||
void cut2def(on_clause_t& on_clause, cut const& c, literal r);
|
||||
|
||||
void replace(unsigned v, cut const& src, cut const& dst);
|
||||
void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
|
||||
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
|
|
@ -463,19 +463,14 @@ namespace sat {
|
|||
rep(cut const& s, cut const& d, unsigned v):src(s), dst(d), v(v) {}
|
||||
rep():v(UINT_MAX) {}
|
||||
};
|
||||
vector<rep> to_replace;
|
||||
cut d;
|
||||
for (auto const& cs : cuts) {
|
||||
for (auto& cs : cuts) {
|
||||
for (auto const& c : cs) {
|
||||
if (rewrite_cut(c, d)) {
|
||||
to_replace.push_back(rep(c, d, cs.var()));
|
||||
if (add_dont_care(c)) {
|
||||
m_aig_cuts.touch(cs.var());
|
||||
m_stats.m_num_dont_care_reductions++;
|
||||
}
|
||||
}
|
||||
}
|
||||
for (auto const& p : to_replace) {
|
||||
m_aig_cuts.replace(p.v, p.src, p.dst);
|
||||
}
|
||||
m_stats.m_num_dont_care_reductions += to_replace.size();
|
||||
}
|
||||
|
||||
/*
|
||||
|
@ -497,18 +492,18 @@ namespace sat {
|
|||
/**
|
||||
* apply obtained dont_cares to cut sets.
|
||||
*/
|
||||
bool aig_simplifier::rewrite_cut(cut const& c, cut& d) {
|
||||
bool init = false;
|
||||
bool aig_simplifier::add_dont_care(cut const & c) {
|
||||
uint64_t dc = 0;
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
for (unsigned j = i + 1; j < c.size(); ++j) {
|
||||
var_pair p(c[i], c[j]);
|
||||
if (m_pairs.find(p, p) && p.op != none) {
|
||||
if (!init) { d = c; init = true; }
|
||||
d.set_table(d.m_table | op2dont_care(i, j, p));
|
||||
dc |= op2dont_care(i, j, p);
|
||||
}
|
||||
}
|
||||
}
|
||||
return init && d.m_table != c.m_table;
|
||||
|
||||
return (dc != c.dont_care()) && (c.add_dont_care(dc), true);
|
||||
}
|
||||
|
||||
void aig_simplifier::collect_statistics(statistics& st) const {
|
||||
|
|
|
@ -95,7 +95,7 @@ namespace sat {
|
|||
void cuts2pairs(vector<cut_set> const& cuts);
|
||||
void pairs2dont_cares();
|
||||
void dont_cares2cuts(vector<cut_set> const& cuts);
|
||||
bool rewrite_cut(cut const& c, cut& r);
|
||||
bool add_dont_care(cut const & c);
|
||||
uint64_t op2dont_care(unsigned i, unsigned j, var_pair const& p);
|
||||
|
||||
public:
|
||||
|
|
|
@ -88,17 +88,6 @@ namespace sat {
|
|||
m_cuts[m_size++] = c;
|
||||
}
|
||||
|
||||
void cut_set::replace(on_update_t& on_add, on_update_t& on_del, cut const& src, cut const& dst) {
|
||||
SASSERT(src != dst);
|
||||
insert(on_add, on_del, dst);
|
||||
for (unsigned i = 0; i < size(); ++i) {
|
||||
if (src == (*this)[i]) {
|
||||
evict(on_del, i);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void cut_set::evict(on_update_t& on_del, unsigned idx) {
|
||||
if (m_var != UINT_MAX && on_del) on_del(m_var, m_cuts[idx]);
|
||||
m_cuts[idx] = m_cuts[--m_size];
|
||||
|
@ -146,12 +135,12 @@ namespace sat {
|
|||
y = c[++j];
|
||||
}
|
||||
index |= (1 << c.m_size);
|
||||
return compute_shift(m_table, index);
|
||||
return compute_shift(table(), index);
|
||||
}
|
||||
|
||||
bool cut::operator==(cut const& other) const {
|
||||
if (m_size != other.m_size) return false;
|
||||
if (m_table != other.m_table) return false;
|
||||
if (table() != other.table()) return false;
|
||||
for (unsigned i = 0; i < m_size; ++i) {
|
||||
if ((*this)[i] != other[i]) return false;
|
||||
}
|
||||
|
@ -160,7 +149,7 @@ namespace sat {
|
|||
|
||||
unsigned cut::hash() const {
|
||||
return get_composite_hash(*this, m_size,
|
||||
[](cut const& c) { return (unsigned)c.m_table; },
|
||||
[](cut const& c) { return (unsigned)c.table(); },
|
||||
[](cut const& c, unsigned i) { return c[i]; });
|
||||
}
|
||||
|
||||
|
@ -172,7 +161,7 @@ namespace sat {
|
|||
}
|
||||
out << "} ";
|
||||
for (unsigned i = 0; i < (1u << m_size); ++i) {
|
||||
if (0 != (m_table & (1ull << i))) out << "1"; else out << "0";
|
||||
if (0 != (table() & (1ull << i))) out << "1"; else out << "0";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
|
|
@ -25,11 +25,17 @@ namespace sat {
|
|||
unsigned m_filter;
|
||||
unsigned m_size;
|
||||
unsigned m_elems[4];
|
||||
public:
|
||||
uint64_t m_table;
|
||||
cut(): m_filter(0), m_size(0), m_table(0) {}
|
||||
mutable uint64_t m_dont_care;
|
||||
|
||||
cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2) { m_elems[0] = id; }
|
||||
uint64_t table_mask() const { return (1ull << (1ull << m_size)) - 1ull; }
|
||||
|
||||
public:
|
||||
cut(): m_filter(0), m_size(0), m_table(0), m_dont_care(0) {}
|
||||
|
||||
cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2), m_dont_care(0) {
|
||||
m_elems[0] = id;
|
||||
}
|
||||
|
||||
cut(cut const& other) {
|
||||
*this = other;
|
||||
|
@ -39,6 +45,7 @@ namespace sat {
|
|||
m_filter = other.m_filter;
|
||||
m_size = other.m_size;
|
||||
m_table = other.m_table;
|
||||
m_dont_care = other.m_dont_care;
|
||||
for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i];
|
||||
return *this;
|
||||
}
|
||||
|
@ -62,11 +69,14 @@ namespace sat {
|
|||
}
|
||||
void sort();
|
||||
void negate() { set_table(~m_table); }
|
||||
uint64_t table_mask() const { return (1ull << (1ull << m_size)) - 1ull; }
|
||||
void set_table(uint64_t t) { m_table = t & table_mask(); }
|
||||
uint64_t table() const { return (m_table | m_dont_care) & table_mask(); }
|
||||
|
||||
bool is_true() const { return 0 == (table_mask() & ~m_table); }
|
||||
bool is_false() const { return 0 == (table_mask() & m_table); }
|
||||
uint64_t dont_care() const { return m_dont_care; }
|
||||
void add_dont_care(uint64_t t) const { m_dont_care |= t; }
|
||||
|
||||
bool is_true() const { return 0 == (table_mask() & ~table()); }
|
||||
bool is_false() const { return 0 == (table_mask() & ~m_dont_care & m_table); }
|
||||
|
||||
bool operator==(cut const& other) const;
|
||||
bool operator!=(cut const& other) const { return !(*this == other); }
|
||||
|
@ -157,8 +167,6 @@ namespace sat {
|
|||
}
|
||||
void evict(on_update_t& on_del, unsigned idx);
|
||||
|
||||
void replace(on_update_t& on_add, on_update_t& on_del, cut const& src, cut const& dst);
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue