Skip to content

Commit

Permalink
add option to increase thresholds based on simulated equality
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jan 17, 2020
1 parent 93d1091 commit 22f1c64
Show file tree
Hide file tree
Showing 6 changed files with 166 additions and 35 deletions.
111 changes: 88 additions & 23 deletions src/sat/sat_aig_cuts.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()) {
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
}
}
}
Expand All @@ -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:
Expand All @@ -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);
}

Expand Down Expand Up @@ -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));
Expand Down
12 changes: 10 additions & 2 deletions src/sat/sat_aig_cuts.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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]; }
Expand Down Expand Up @@ -160,13 +165,16 @@ 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; }

void cut2def(on_clause_t& on_clause, cut const& c, literal r);

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;

Expand Down
39 changes: 35 additions & 4 deletions src/sat/sat_aig_simplifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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");
}
};
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down
7 changes: 5 additions & 2 deletions src/sat/sat_aig_simplifier.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)); }
};
Expand All @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
21 changes: 21 additions & 0 deletions src/sat/sat_cutset.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 << "{";
Expand Down
Loading

0 comments on commit 22f1c64

Please sign in to comment.