mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

evaluate with don't cares

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-18 09:17:15 -08:00
parent 321bad2c84
commit 495b88ce99
5 changed files with 47 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/sat/sat_aig_cuts.cpp
View file

@ -86,7 +86,7 @@ namespace sat {
return true; return true;
} }
m_num_cuts++; m_num_cuts++;
if (++m_insertions > m_config.m_max_insertions) { if (++m_insertions > max_cutset_size(v)) {
return false; return false;
} }
while (cs.size() >= max_cutset_size(v)) { while (cs.size() >= max_cutset_size(v)) {
@ -412,7 +412,7 @@ namespace sat {
return result; return result;
} }
uint64_t aig_cuts::eval(node const& n, svector<uint64_t> const& env) const { cut_val aig_cuts::eval(node const& n, cut_eval const& env) const {
uint64_t result; uint64_t result;
switch (n.op()) { switch (n.op()) {
case var_op: case var_op:
@ -422,7 +422,7 @@ namespace sat {
result = ~0ull; result = ~0ull;
for (unsigned i = 0; i < n.size(); ++i) { for (unsigned i = 0; i < n.size(); ++i) {
literal u = m_literals[n.offset() + i]; literal u = m_literals[n.offset() + i];
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
result &= uv; result &= uv;
} }
break; break;
@ -430,7 +430,7 @@ namespace sat {
result = 0ull; result = 0ull;
for (unsigned i = 0; i < n.size(); ++i) { for (unsigned i = 0; i < n.size(); ++i) {
literal u = m_literals[n.offset() + i]; literal u = m_literals[n.offset() + i];
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
result ^= uv; result ^= uv;
} }
break; break;
@ -438,9 +438,9 @@ namespace sat {
literal u = m_literals[n.offset() + 0]; literal u = m_literals[n.offset() + 0];
literal v = m_literals[n.offset() + 1]; literal v = m_literals[n.offset() + 1];
literal w = m_literals[n.offset() + 2]; literal w = m_literals[n.offset() + 2];
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()]; uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
uint64_t vv = v.sign() ? ~env[v.var()] : env[v.var()]; uint64_t vv = v.sign() ? env[v.var()].m_f : env[v.var()].m_t;
uint64_t wv = w.sign() ? ~env[w.var()] : env[w.var()]; uint64_t wv = w.sign() ? env[w.var()].m_f : env[w.var()].m_t;
result = (uv & vv) | ((~uv) & wv); result = (uv & vv) | ((~uv) & wv);
break; break;
} }
@ -448,14 +448,16 @@ namespace sat {
UNREACHABLE(); UNREACHABLE();
} }
if (n.sign()) result = ~result; if (n.sign()) result = ~result;
return result; return cut_val(result, ~result);
} }
svector<uint64_t> aig_cuts::simulate(unsigned num_rounds) { cut_eval aig_cuts::simulate(unsigned num_rounds) {
svector<uint64_t> result; cut_eval result;
for (unsigned i = 0; i < m_cuts.size(); ++i) { for (unsigned i = 0; i < m_cuts.size(); ++i) {
result.push_back((uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) + uint64_t r =
((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull)); (uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) +
((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull);
result.push_back(cut_val(r, ~r));
} }
for (unsigned i = 0; i < num_rounds; ++i) { for (unsigned i = 0; i < num_rounds; ++i) {
for (unsigned j = 0; j < m_cuts.size(); ++j) { for (unsigned j = 0; j < m_cuts.size(); ++j) {

7
src/sat/sat_aig_cuts.h
View file

@ -114,8 +114,6 @@ namespace sat {
bool insert_aux(unsigned v, node const& n); bool insert_aux(unsigned v, node const& n);
void init_cut_set(unsigned id); void init_cut_set(unsigned id);
unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
bool eq(node const& a, node const& b); bool eq(node const& a, node const& b);
unsigned_vector filter_valid_nodes() const; unsigned_vector filter_valid_nodes() const;
@ -133,7 +131,7 @@ namespace sat {
void flush_roots(literal_vector const& to_root, node& n); void flush_roots(literal_vector const& to_root, node& n);
void flush_roots(literal_vector const& to_root, cut_set& cs); void flush_roots(literal_vector const& to_root, cut_set& cs);
uint64_t eval(node const& n, svector<uint64_t> const& env) const; cut_val eval(node const& n, cut_eval const& env) const;
std::ostream& display(std::ostream& out, node const& n) const; std::ostream& display(std::ostream& out, node const& n) const;
@ -166,6 +164,7 @@ namespace sat {
void set_on_clause_del(on_clause_t& on_clause_del); void set_on_clause_del(on_clause_t& on_clause_del);
void inc_max_cutset_size(unsigned v) { m_max_cutset_size[v] += 10; touch(v); } void inc_max_cutset_size(unsigned v) { m_max_cutset_size[v] += 10; touch(v); }
unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
vector<cut_set> const & operator()(); vector<cut_set> const & operator()();
unsigned num_cuts() const { return m_num_cuts; } unsigned num_cuts() const { return m_num_cuts; }
@ -174,7 +173,7 @@ namespace sat {
void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); } void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
svector<uint64_t> simulate(unsigned num_rounds); cut_eval simulate(unsigned num_rounds);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;

20
src/sat/sat_aig_simplifier.cpp
View file

@ -165,7 +165,7 @@ namespace sat {
aig2clauses(); aig2clauses();
++i; ++i;
} }
while (i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units); while (i*i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units);
} }
/** /**
@ -425,17 +425,25 @@ namespace sat {
// Assign higher cutset budgets to equality candidates that come from simulation // Assign higher cutset budgets to equality candidates that come from simulation
// touch them to trigger recomputation of cutsets. // touch them to trigger recomputation of cutsets.
u64_map<unsigned> val2var; u64_map<literal> val2lit;
unsigned i = 0, j = 0, num_eqs = 0; unsigned i = 0, j = 0, num_eqs = 0;
for (uint64_t val : var2val) { for (cut_val val : var2val) {
if (!s.was_eliminated(i) && s.value(i) == l_undef) { if (!s.was_eliminated(i) && s.value(i) == l_undef) {
if (val2var.find(val, j)) { literal u(i, false), v;
if (val2lit.find(val.m_t, v)) {
m_aig_cuts.inc_max_cutset_size(i); m_aig_cuts.inc_max_cutset_size(i);
m_aig_cuts.inc_max_cutset_size(j); m_aig_cuts.inc_max_cutset_size(v.var());
num_eqs++;
}
else if (val2lit.find(val.m_f, v)) {
m_aig_cuts.inc_max_cutset_size(i);
m_aig_cuts.inc_max_cutset_size(v.var());
num_eqs++; num_eqs++;
} }
else { else {
val2var.insert(val, i); val2lit.insert(val.m_t, u);
val2lit.insert(val.m_f, ~u);
} }
} }
++i; ++i;

12
src/sat/sat_cutset.cpp
View file

@ -166,9 +166,10 @@ namespace sat {
sat-sweep evaluation. Given 64 bits worth of possible values per variable, sat-sweep evaluation. Given 64 bits worth of possible values per variable,
find possible values for function table encoded by cut. find possible values for function table encoded by cut.
*/ */
uint64_t cut::eval(svector<uint64_t> const& env) const { cut_val cut::eval(cut_eval const& env) const {
uint64_t result = 0ull; cut_val v;
uint64_t t = table(); uint64_t t = table();
uint64_t n = table();
unsigned sz = size(); unsigned sz = size();
if (sz == 1 && t == 2) { if (sz == 1 && t == 2) {
return env[m_elems[0]]; return env[m_elems[0]];
@ -176,11 +177,12 @@ namespace sat {
for (unsigned i = 0; i < 64; ++i) { for (unsigned i = 0; i < 64; ++i) {
unsigned offset = 0; unsigned offset = 0;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
offset |= (((env[m_elems[j]] >> i) & 0x1) << j); offset |= (((env[m_elems[j]].m_t >> i) & 0x1) << j);
} }
result |= ((t >> offset) & 0x1) << i; v.m_t |= ((t >> offset) & 0x1) << i;
v.m_f |= ((n >> offset) & 0x1) << i;
} }
return result; return v;
} }
std::ostream& cut::display(std::ostream& out) const { std::ostream& cut::display(std::ostream& out) const {

10
src/sat/sat_cutset.h
View file

@ -22,6 +22,14 @@
namespace sat { namespace sat {
struct cut_val {
cut_val():m_t(0ull), m_f(0ull) {}
cut_val(uint64_t t, uint64_t f): m_t(t), m_f(f) {}
uint64_t m_t, m_f;
};
typedef svector<cut_val> cut_eval;
class cut { class cut {
unsigned m_filter; unsigned m_filter;
unsigned m_size; unsigned m_size;
@ -51,7 +59,7 @@ namespace sat {
return *this; return *this;
} }
uint64_t eval(svector<uint64_t> const& env) const; cut_val eval(cut_eval const& env) const;
unsigned size() const { return m_size; } unsigned size() const { return m_size; }