mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
add option to increase thresholds based on simulated equality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
93d1091ad9
commit
22f1c6448a
6 changed files with 166 additions and 35 deletions
|
|
@ -55,7 +55,7 @@ namespace sat {
|
|||
unsigned nc = n.size();
|
||||
m_insertions = 0;
|
||||
cut_set& cs = m_cuts[id];
|
||||
if (!is_touched(n)) {
|
||||
if (!is_touched(id, n)) {
|
||||
// no-op
|
||||
}
|
||||
else if (n.is_var()) {
|
||||
|
|
@ -89,7 +89,7 @@ namespace sat {
|
|||
if (++m_insertions > m_config.m_max_insertions) {
|
||||
return false;
|
||||
}
|
||||
while (cs.size() >= m_config.m_max_cutset_size) {
|
||||
while (cs.size() >= max_cutset_size(v)) {
|
||||
// never evict the first entry, it is used for the starting point
|
||||
unsigned idx = 1 + (m_rand() % (cs.size() - 1));
|
||||
evict(cs, idx);
|
||||
|
|
@ -155,17 +155,18 @@ namespace sat {
|
|||
for (auto const& a : m_cuts[l1.var()]) {
|
||||
for (auto const& b : m_cuts[l2.var()]) {
|
||||
cut c;
|
||||
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);
|
||||
c.set_table(t3);
|
||||
if (n.sign()) c.negate();
|
||||
// validate_aig2(a, b, v, n, c);
|
||||
if (!insert_cut(v, c, cs)) return;
|
||||
if (!c.merge(a, b)) {
|
||||
continue;
|
||||
}
|
||||
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();
|
||||
// validate_aig2(a, b, v, n, c);
|
||||
if (!insert_cut(v, c, cs)) return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -189,15 +190,16 @@ namespace sat {
|
|||
for (auto const& a : m_cut_set1) {
|
||||
for (auto const& b : m_cuts[lit.var()]) {
|
||||
cut c;
|
||||
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);
|
||||
c.set_table(t3);
|
||||
if (i + 1 == n.size() && n.sign()) c.negate();
|
||||
if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child;
|
||||
if (!c.merge(a, b)) {
|
||||
continue;
|
||||
}
|
||||
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.size() && n.sign()) c.negate();
|
||||
if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child;
|
||||
}
|
||||
}
|
||||
next_child:
|
||||
|
|
@ -212,20 +214,20 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
bool aig_cuts::is_touched(node const& n) {
|
||||
bool aig_cuts::is_touched(bool_var v, node const& n) {
|
||||
for (unsigned i = 0; i < n.size(); ++i) {
|
||||
literal lit = m_literals[n.offset() + i];
|
||||
if (is_touched(lit)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
return is_touched(v);
|
||||
}
|
||||
|
||||
void aig_cuts::reserve(unsigned v) {
|
||||
m_aig.reserve(v + 1);
|
||||
m_cuts.reserve(v + 1);
|
||||
m_max_cutset_size.reserve(v + 1, m_config.m_max_cutset_size);
|
||||
m_last_touched.reserve(v + 1, 0);
|
||||
}
|
||||
|
||||
|
|
@ -410,6 +412,69 @@ namespace sat {
|
|||
return result;
|
||||
}
|
||||
|
||||
uint64_t aig_cuts::eval(node const& n, svector<uint64_t> const& env) const {
|
||||
uint64_t result;
|
||||
switch (n.op()) {
|
||||
case var_op:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
case and_op:
|
||||
result = ~0ull;
|
||||
for (unsigned i = 0; i < n.size(); ++i) {
|
||||
literal u = m_literals[n.offset() + i];
|
||||
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
|
||||
result &= uv;
|
||||
}
|
||||
break;
|
||||
case xor_op:
|
||||
result = 0ull;
|
||||
for (unsigned i = 0; i < n.size(); ++i) {
|
||||
literal u = m_literals[n.offset() + i];
|
||||
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
|
||||
result ^= uv;
|
||||
}
|
||||
break;
|
||||
case ite_op: {
|
||||
literal u = m_literals[n.offset() + 0];
|
||||
literal v = m_literals[n.offset() + 1];
|
||||
literal w = m_literals[n.offset() + 2];
|
||||
uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
|
||||
uint64_t vv = v.sign() ? ~env[v.var()] : env[v.var()];
|
||||
uint64_t wv = w.sign() ? ~env[w.var()] : env[w.var()];
|
||||
result = (uv & vv) | ((~uv) & wv);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
if (n.sign()) result = ~result;
|
||||
return result;
|
||||
}
|
||||
|
||||
svector<uint64_t> aig_cuts::simulate(unsigned num_rounds) {
|
||||
svector<uint64_t> result;
|
||||
for (unsigned i = 0; i < m_cuts.size(); ++i) {
|
||||
result.push_back((uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) +
|
||||
((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull));
|
||||
}
|
||||
for (unsigned i = 0; i < num_rounds; ++i) {
|
||||
for (unsigned j = 0; j < m_cuts.size(); ++j) {
|
||||
cut_set const& cs = m_cuts[j];
|
||||
if (cs.size() <= 1) {
|
||||
if (!m_aig[j].empty() && !m_aig[j][0].is_var()) {
|
||||
result[j] = eval(m_aig[j][0], result);
|
||||
}
|
||||
}
|
||||
else if (cs.size() > 1) {
|
||||
cut const& c = cs[1 + (m_rand() % (cs.size() - 1))];
|
||||
result[j] = c.eval(result);
|
||||
}
|
||||
}
|
||||
}
|
||||
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));
|
||||
|
|
|
|||
|
|
@ -61,7 +61,7 @@ namespace sat {
|
|||
unsigned m_max_aux;
|
||||
unsigned m_max_insertions;
|
||||
bool m_full;
|
||||
config(): m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10), m_full(false) {}
|
||||
config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(false) {}
|
||||
};
|
||||
private:
|
||||
|
||||
|
|
@ -97,6 +97,7 @@ namespace sat {
|
|||
region m_region;
|
||||
cut_set m_cut_set1, m_cut_set2;
|
||||
vector<cut_set> m_cuts;
|
||||
unsigned_vector m_max_cutset_size;
|
||||
unsigned_vector m_last_touched;
|
||||
unsigned m_num_cut_calls;
|
||||
unsigned m_num_cuts;
|
||||
|
|
@ -106,13 +107,15 @@ namespace sat {
|
|||
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(bool_var v, 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 reserve(unsigned v);
|
||||
bool insert_aux(unsigned v, node const& n);
|
||||
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);
|
||||
|
||||
unsigned_vector filter_valid_nodes() const;
|
||||
|
|
@ -130,6 +133,8 @@ namespace sat {
|
|||
void flush_roots(literal_vector const& to_root, node& n);
|
||||
void flush_roots(literal_vector const& to_root, cut_set& cs);
|
||||
|
||||
uint64_t eval(node const& n, svector<uint64_t> const& env) const;
|
||||
|
||||
std::ostream& display(std::ostream& out, node const& n) const;
|
||||
|
||||
literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; }
|
||||
|
|
@ -160,6 +165,8 @@ namespace sat {
|
|||
void set_on_clause_add(on_clause_t& on_clause_add);
|
||||
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); }
|
||||
|
||||
vector<cut_set> const & operator()();
|
||||
unsigned num_cuts() const { return m_num_cuts; }
|
||||
|
||||
|
|
@ -167,6 +174,7 @@ namespace sat {
|
|||
|
||||
void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
|
||||
|
||||
svector<uint64_t> simulate(unsigned num_rounds);
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -25,23 +25,26 @@ namespace sat {
|
|||
struct aig_simplifier::report {
|
||||
aig_simplifier& s;
|
||||
stopwatch m_watch;
|
||||
unsigned m_num_eqs, m_num_units, m_num_cuts;
|
||||
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_learned_implies;
|
||||
|
||||
report(aig_simplifier& s): s(s) {
|
||||
m_watch.start();
|
||||
m_num_eqs = s.m_stats.m_num_eqs;
|
||||
m_num_units = s.m_stats.m_num_units;
|
||||
m_num_cuts = s.m_stats.m_num_cuts;
|
||||
m_num_learned_implies = s.m_stats.m_num_learned_implies;
|
||||
}
|
||||
~report() {
|
||||
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 ni = s.m_stats.m_num_learned_implies - m_num_learned_implies;
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "(sat.aig-simplifier";
|
||||
if (ne > 0) verbose_stream() << " :num-eqs " << ne;
|
||||
if (nu > 0) verbose_stream() << " :num-units " << nu;
|
||||
if (nc > 0) verbose_stream() << " :num-cuts " << nc;
|
||||
if (ne > 0) verbose_stream() << " :num-eqs " << ne;
|
||||
if (ni > 0) verbose_stream() << " :num-bin " << ni;
|
||||
if (nc > 0) verbose_stream() << " :num-cuts " << nc;
|
||||
verbose_stream() << " :mb " << mem_stat() << m_watch << ")\n");
|
||||
}
|
||||
};
|
||||
|
|
@ -231,6 +234,7 @@ namespace sat {
|
|||
add_dont_cares(cuts);
|
||||
cuts2equiv(cuts);
|
||||
cuts2implies(cuts);
|
||||
simulate_eqs();
|
||||
}
|
||||
|
||||
void aig_simplifier::cuts2equiv(vector<cut_set> const& cuts) {
|
||||
|
|
@ -281,8 +285,8 @@ namespace sat {
|
|||
void aig_simplifier::assign_unit(cut const& c, literal lit) {
|
||||
if (s.value(lit) != l_undef)
|
||||
return;
|
||||
IF_VERBOSE(10, verbose_stream() << "new unit " << lit << "\n");
|
||||
validate_unit(lit);
|
||||
IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
|
||||
s.assign_unit(lit);
|
||||
certify_unit(lit, c);
|
||||
++m_stats.m_num_units;
|
||||
|
|
@ -345,6 +349,8 @@ namespace sat {
|
|||
big big(s.rand());
|
||||
big.init(s, true);
|
||||
for (auto const& cs : cuts) {
|
||||
if (s.was_eliminated(cs.var()))
|
||||
continue;
|
||||
for (auto const& c : cs) {
|
||||
if (c.is_false() || c.is_true())
|
||||
continue;
|
||||
|
|
@ -410,6 +416,31 @@ namespace sat {
|
|||
s.mk_clause(~u, v, true);
|
||||
// m_bins owns reference to ~u or v created by certify_implies
|
||||
m_bins.insert(p);
|
||||
++m_stats.m_num_learned_implies;
|
||||
}
|
||||
|
||||
void aig_simplifier::simulate_eqs() {
|
||||
if (!m_config.m_simulate_eqs) return;
|
||||
auto var2val = m_aig_cuts.simulate(4);
|
||||
|
||||
// Assign higher cutset budgets to equality candidates that come from simulation
|
||||
// touch them to trigger recomputation of cutsets.
|
||||
u64_map<unsigned> val2var;
|
||||
unsigned i = 0, j = 0, num_eqs = 0;
|
||||
for (uint64_t val : var2val) {
|
||||
if (!s.was_eliminated(i) && s.value(i) == l_undef) {
|
||||
if (val2var.find(val, j)) {
|
||||
m_aig_cuts.inc_max_cutset_size(i);
|
||||
m_aig_cuts.inc_max_cutset_size(j);
|
||||
num_eqs++;
|
||||
}
|
||||
else {
|
||||
val2var.insert(val, i);
|
||||
}
|
||||
}
|
||||
++i;
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier num simulated eqs " << num_eqs << ")\n");
|
||||
}
|
||||
|
||||
void aig_simplifier::track_binary(bin_rel const& p) {
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ namespace sat {
|
|||
public:
|
||||
struct stats {
|
||||
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
|
||||
unsigned m_num_calls, m_num_dont_care_reductions;
|
||||
unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
|
@ -39,13 +39,15 @@ namespace sat {
|
|||
bool m_learned2aig; // add learned clauses to AIGs used by cut-set enumeration
|
||||
bool m_validate_cuts; // enable direct validation of generated cuts
|
||||
bool m_validate_lemmas; // enable direct validation of learned lemmas
|
||||
bool m_simulate_eqs; // use symbolic simulation to control size of cutsets.
|
||||
config():
|
||||
m_enable_units(true),
|
||||
m_enable_dont_cares(true),
|
||||
m_learn_implies(false),
|
||||
m_learned2aig(true),
|
||||
m_validate_cuts(false),
|
||||
m_validate_lemmas(false) {}
|
||||
m_validate_lemmas(false),
|
||||
m_simulate_eqs(true) {}
|
||||
};
|
||||
private:
|
||||
struct report;
|
||||
|
|
@ -120,6 +122,7 @@ namespace sat {
|
|||
|
||||
void clauses2aig();
|
||||
void aig2clauses();
|
||||
void simulate_eqs();
|
||||
void cuts2equiv(vector<cut_set> const& cuts);
|
||||
void cuts2implies(vector<cut_set> const& cuts);
|
||||
void uf2equiv(union_find<> const& uf);
|
||||
|
|
|
|||
|
|
@ -161,6 +161,27 @@ namespace sat {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
sat-sweep evaluation. Given 64 bits worth of possible values per variable,
|
||||
find possible values for function table encoded by cut.
|
||||
*/
|
||||
uint64_t cut::eval(svector<uint64_t> const& env) const {
|
||||
uint64_t result = 0ull;
|
||||
uint64_t t = table();
|
||||
unsigned sz = size();
|
||||
if (sz == 1 && t == 2) {
|
||||
return env[m_elems[0]];
|
||||
}
|
||||
for (unsigned i = 0; i < 64; ++i) {
|
||||
unsigned offset = 0;
|
||||
for (unsigned j = 0; j < sz; ++j) {
|
||||
offset |= (((env[m_elems[j]] >> i) & 0x1) << j);
|
||||
}
|
||||
result |= ((t >> offset) & 0x1) << i;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
std::ostream& cut::display(std::ostream& out) const {
|
||||
out << "{";
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@
|
|||
#include "util/region.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/util.h"
|
||||
#include "util/vector.h"
|
||||
#include <algorithm>
|
||||
#include <cstring>
|
||||
#include <functional>
|
||||
|
|
@ -24,7 +25,7 @@ namespace sat {
|
|||
class cut {
|
||||
unsigned m_filter;
|
||||
unsigned m_size;
|
||||
unsigned m_elems[4];
|
||||
unsigned m_elems[5];
|
||||
uint64_t m_table;
|
||||
mutable uint64_t m_dont_care;
|
||||
|
||||
|
|
@ -50,9 +51,11 @@ namespace sat {
|
|||
return *this;
|
||||
}
|
||||
|
||||
uint64_t eval(svector<uint64_t> const& env) const;
|
||||
|
||||
unsigned size() const { return m_size; }
|
||||
|
||||
static unsigned max_cut_size() { return 4; }
|
||||
static unsigned max_cut_size() { return 5; }
|
||||
|
||||
unsigned const* begin() const { return m_elems; }
|
||||
unsigned const* end() const { return m_elems + m_size; }
|
||||
|
|
@ -113,7 +116,7 @@ namespace sat {
|
|||
unsigned x = a[i];
|
||||
unsigned y = b[j];
|
||||
while (x != UINT_MAX || y != UINT_MAX) {
|
||||
if (!add(std::min(x, y))) {
|
||||
if (!add(std::min(x, y))) {
|
||||
return false;
|
||||
}
|
||||
if (x < y) {
|
||||
|
|
@ -169,7 +172,7 @@ namespace sat {
|
|||
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]; }
|
||||
cut const & operator[](unsigned idx) const { return m_cuts[idx]; }
|
||||
void shrink(on_update_t& on_del, unsigned j);
|
||||
void swap(cut_set& other) {
|
||||
std::swap(m_var, other.m_var);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue