mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-24 13:06:50 +00:00
Code Activity

remove stale experimental code #8063

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-12-12 05:49:05 +00:00
parent 175625f43c
commit f917005ee1
23 changed files with 9 additions and 3918 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/params/sat_params.pyg
View file

@ -75,15 +75,6 @@ def_module_params('sat',
('anf', BOOL, False, 'enable ANF based simplification in-processing'),
('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'),
('anf.exlin', BOOL, False, 'enable extended linear simplification'),
('cut', BOOL, False, 'enable AIG based simplification in-processing'),
('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'),
('cut.aig', BOOL, False, 'extract aigs (and ites) from cluases for cut simplification'),
('cut.lut', BOOL, False, 'extract luts from clauses for cut simplification'),
('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'),
('cut.npn3', BOOL, False, 'extract 3 input functions from clauses for cut simplification'),
('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
('cut.redundancies', BOOL, True, 'integrate redundancy checking of cuts'),
('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'),
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
# - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
# So if the value is 10, at most 1024 cubes will be generated of length 10.

4
src/sat/CMakeLists.txt
View file

@ -1,7 +1,6 @@
z3_add_component(sat
SOURCES
dimacs.cpp
sat_aig_cuts.cpp
sat_aig_finder.cpp
sat_anf_simplifier.cpp
sat_asymm_branch.cpp
@ -12,8 +11,6 @@ z3_add_component(sat
sat_clause_use_list.cpp
sat_cleaner.cpp
sat_config.cpp
sat_cut_simplifier.cpp
sat_cutset.cpp
sat_ddfw_wrapper.cpp
sat_drat.cpp
sat_elim_eqs.cpp
@ -21,7 +18,6 @@ z3_add_component(sat
sat_integrity_checker.cpp
sat_local_search.cpp
sat_lookahead.cpp
sat_lut_finder.cpp
sat_model_converter.cpp
sat_mus.cpp
sat_npn3_finder.cpp

886
src/sat/sat_aig_cuts.cpp
View file

@ -1,886 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_aig_cuts.cpp
Abstract:
Perform cut-set enumeration to identify equivalences.
Author:
Nikolaj Bjorner 2020-01-02
--*/
#include "util/trace.h"
#include "sat/sat_aig_cuts.h"
#include "sat/sat_solver.h"
#include "sat/sat_lut_finder.h"
namespace sat {
aig_cuts::aig_cuts() {
m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
m_empty_cuts.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
m_num_cut_calls = 0;
m_num_cuts = 0;
}
vector<cut_set> const& aig_cuts::operator()() {
if (m_config.m_full) flush_roots();
unsigned_vector node_ids = filter_valid_nodes();
TRACE(cut_simplifier, display(tout););
augment(node_ids);
TRACE(cut_simplifier, display(tout););
++m_num_cut_calls;
return m_cuts;
}
void aig_cuts::augment(unsigned_vector const& ids) {
for (unsigned id : ids) {
if (m_aig[id].empty()) {
continue;
}
IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
for (node const& n : m_aig[id]) {
augment(id, n);
}
#if 0
// augment cuts directly
m_cut_save.reset();
cut_set& cs = m_cuts[id];
for (cut const& c : cs) {
if (c.size() > 1) m_cut_save.push_back(c);
}
for (cut const& c : m_cut_save) {
lut lut(*this, c);
augment_lut(id, lut, cs);
}
#endif
IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "after\n"));
}
}
void aig_cuts::augment(unsigned id, node const& n) {
unsigned nc = n.size();
m_insertions = 0;
cut_set& cs = m_cuts[id];
if (!is_touched(id, n)) {
// no-op
}
else if (n.is_var()) {
SASSERT(!n.sign());
}
else if (n.is_lut()) {
lut lut(*this, n);
augment_lut(id, lut, cs);
}
else if (n.is_ite()) {
augment_ite(id, n, cs);
}
else if (nc == 0) {
augment_aig0(id, n, cs);
}
else if (nc == 1) {
augment_aig1(id, n, cs);
}
else if (nc == 2) {
augment_aig2(id, n, cs);
}
else if (nc <= cut::max_cut_size()) {
augment_aigN(id, n, cs);
}
if (m_insertions > 0) {
touch(id);
}
}
bool aig_cuts::insert_cut(unsigned v, cut const& c, cut_set& cs) {
if (!cs.insert(m_on_cut_add, m_on_cut_del, c)) {
return true;
}
m_num_cuts++;
if (++m_insertions > max_cutset_size(v)) {
return false;
}
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);
}
return true;
}
void aig_cuts::augment_lut(unsigned v, lut const& n, cut_set& cs) {
IF_VERBOSE(4, n.display(verbose_stream() << "augment_lut " << v << " ") << "\n");
literal l1 = n.child(0);
VERIFY(&cs != &lit2cuts(l1));
for (auto const& a : lit2cuts(l1)) {
m_tables[0] = &a;
m_lits[0] = l1;
cut b(a);
augment_lut_rec(v, n, b, 1, cs);
}
}
void aig_cuts::augment_lut_rec(unsigned v, lut const& n, cut& a, unsigned idx, cut_set& cs) {
if (idx < n.size()) {
literal lit = n.child(idx);
VERIFY(&cs != &lit2cuts(lit));
for (auto const& b : lit2cuts(lit)) {
cut ab;
if (!ab.merge(a, b)) continue;
m_tables[idx] = &b;
m_lits[idx] = lit;
augment_lut_rec(v, n, ab, idx + 1, cs);
}
return;
}
for (unsigned i = n.size(); i-- > 0; ) {
m_luts[i] = m_tables[i]->shift_table(a);
}
uint64_t r = 0;
SASSERT(a.size() <= 6);
SASSERT(n.size() <= 6);
for (unsigned j = (1u << a.size()); j-- > 0; ) {
unsigned w = 0;
// when computing the output at position j,
// the i'th bit to index into n.lut() is
// based on the j'th output bit in lut[i]
// m_lits[i].sign() tracks if output bit is negated
for (unsigned i = n.size(); i-- > 0; ) {
w |= (((m_luts[i] >> j) ^ (uint64_t)m_lits[i].sign()) & 1u) << i;
}
r |= ((n.table() >> w) & 1u) << j;
}
a.set_table(r);
IF_VERBOSE(8,
verbose_stream() << "lut: " << v << " - " << a << "\n";
for (unsigned i = 0; i < n.size(); ++i) {
verbose_stream() << m_lits[i] << ": " << *m_tables[i] << "\n";
});
insert_cut(v, a, cs);
}
void aig_cuts::augment_ite(unsigned v, node const& n, cut_set& cs) {
IF_VERBOSE(4, display(verbose_stream() << "augment_ite " << v << " ", n) << "\n");
literal l1 = child(n, 0);
literal l2 = child(n, 1);
literal l3 = child(n, 2);
VERIFY(&cs != &lit2cuts(l1));
VERIFY(&cs != &lit2cuts(l2));
VERIFY(&cs != &lit2cuts(l3));
for (auto const& a : lit2cuts(l1)) {
for (auto const& b : lit2cuts(l2)) {
cut ab;
if (!ab.merge(a, b)) continue;
for (auto const& c : lit2cuts(l3)) {
cut abc;
if (!abc.merge(ab, c)) continue;
uint64_t t1 = a.shift_table(abc);
uint64_t t2 = b.shift_table(abc);
uint64_t t3 = c.shift_table(abc);
if (l1.sign()) t1 = ~t1;
if (l2.sign()) t2 = ~t2;
if (l3.sign()) t3 = ~t3;
abc.set_table((t1 & t2) | ((~t1) & t3));
if (n.sign()) abc.negate();
if (!insert_cut(v, abc, cs)) return;
}
}
}
}
void aig_cuts::augment_aig0(unsigned v, node const& n, cut_set& cs) {
IF_VERBOSE(4, display(verbose_stream() << "augment_unit " << v << " ", n) << "\n");
SASSERT(n.is_and() && n.size() == 0);
reset(cs);
cut c;
c.set_table(n.sign() ? 0x0 : 0x1);
push_back(cs, c);
}
void aig_cuts::augment_aig1(unsigned v, node const& n, cut_set& cs) {
IF_VERBOSE(4, display(verbose_stream() << "augment_aig1 " << v << " ", n) << "\n");
SASSERT(n.is_and());
literal lit = child(n, 0);
VERIFY(&cs != &lit2cuts(lit));
for (auto const& a : lit2cuts(lit)) {
cut c(a);
if (n.sign()) c.negate();
if (!insert_cut(v, c, cs)) return;
}
}
void aig_cuts::augment_aig2(unsigned v, node const& n, cut_set& cs) {
IF_VERBOSE(4, display(verbose_stream() << "augment_aig2 " << v << " ", n) << "\n");
SASSERT(n.is_and() || n.is_xor());
literal l1 = child(n, 0);
literal l2 = child(n, 1);
VERIFY(&cs != &lit2cuts(l1));
VERIFY(&cs != &lit2cuts(l2));
for (auto const& a : lit2cuts(l1)) {
for (auto const& b : lit2cuts(l2)) {
cut c;
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;
}
}
}
void aig_cuts::augment_aigN(unsigned v, node const& n, cut_set& cs) {
IF_VERBOSE(4, display(verbose_stream() << "augment_aigN " << v << " ", n) << "\n");
m_cut_set1.reset(m_on_cut_del);
SASSERT(n.is_and() || n.is_xor());
literal lit = child(n, 0);
for (auto const& a : lit2cuts(lit)) {
cut b(a);
if (lit.sign()) {
b.negate();
}
m_cut_set1.push_back(m_on_cut_add, b);
}
for (unsigned i = 1; i < n.size(); ++i) {
m_cut_set2.reset(m_on_cut_del);
lit = child(n, i);
m_insertions = 0;
for (auto const& a : m_cut_set1) {
for (auto const& b : lit2cuts(lit)) {
cut c;
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:
m_cut_set1.swap(m_cut_set2);
}
m_insertions = 0;
for (auto & cut : m_cut_set1) {
// validate_aigN(v, n, cut);
if (!insert_cut(v, cut, cs)) {
break;
}
}
}
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 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);
}
void aig_cuts::add_var(unsigned v) {
reserve(v);
if (m_aig[v].empty()) {
m_aig[v].push_back(node(v));
init_cut_set(v);
touch(v);
}
}
void aig_cuts::add_node(bool_var v, node const& n) {
for (unsigned i = 0; i < n.size(); ++i) {
reserve(m_literals[i].var());
if (m_aig[m_literals[i].var()].empty()) {
add_var(m_literals[i].var());
}
}
if (m_aig[v].empty() || n.is_const()) {
m_aig[v].reset();
m_aig[v].push_back(n);
on_node_add(v, n);
init_cut_set(v);
if (n.is_const()) {
augment_aig0(v, n, m_cuts[v]);
}
touch(v);
IF_VERBOSE(12, display(verbose_stream() << "add " << v << " == ", n) << "\n");
}
else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
m_literals.shrink(m_literals.size() - n.size());
TRACE(cut_simplifier, tout << "duplicate\n";);
}
SASSERT(!m_aig[v].empty());
}
void aig_cuts::add_node(bool_var v, uint64_t lut, unsigned sz, bool_var const* args) {
TRACE(cut_simplifier, tout << v << " == " << cut::table2string(sz, lut) << " " << bool_var_vector(sz, args) << "\n";);
reserve(v);
unsigned offset = m_literals.size();
node n(lut, sz, offset);
for (unsigned i = 0; i < sz; ++i) {
reserve(args[i]);
m_literals.push_back(literal(args[i], false));
}
add_node(v, n);
}
void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
TRACE(cut_simplifier, tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";);
unsigned v = head.var();
reserve(v);
unsigned offset = m_literals.size();
node n(head.sign(), op, sz, offset);
m_literals.append(sz, args);
for (unsigned i = 0; i < sz; ++i) reserve(args[i].var());
if (op == and_op || op == xor_op) {
std::sort(m_literals.data() + offset, m_literals.data() + offset + sz);
}
add_node(v, n);
}
void aig_cuts::add_cut(bool_var v, uint64_t lut, bool_var_vector const& args) {
// args can be assumed to be sorted
DEBUG_CODE(for (unsigned i = 0; i + 1 < args.size(); ++i) VERIFY(args[i] < args[i+1]););
add_var(v);
for (bool_var w : args) add_var(w);
cut c;
for (bool_var w : args) VERIFY(c.add(w));
c.set_table(lut);
insert_cut(v, c, m_cuts[v]);
}
void aig_cuts::set_root(bool_var v, literal r) {
IF_VERBOSE(10, verbose_stream() << "set-root " << v << " -> " << r << "\n");
m_roots.push_back(std::make_pair(v, r));
}
void aig_cuts::flush_roots() {
if (m_roots.empty()) return;
to_root to_root;
for (unsigned i = m_roots.size(); i-- > 0; ) {
bool_var v = m_roots[i].first;
literal r = m_roots[i].second;
reserve(v);
reserve(r.var());
literal rr = to_root[r.var()];
to_root[v] = r.sign() ? ~rr : rr;
}
for (unsigned i = 0; i < m_aig.size(); ++i) {
// invalidate nodes that have been rooted
if (to_root[i] != literal(i, false)) {
m_aig[i].reset();
reset(m_cuts[i]);
}
else {
unsigned j = 0;
for (node & n : m_aig[i]) {
if (flush_roots(i, to_root, n)) {
m_aig[i][j++] = n;
}
}
m_aig[i].shrink(j);
}
}
for (cut_set& cs : m_cuts) {
flush_roots(to_root, cs);
}
m_roots.reset();
TRACE(cut_simplifier, display(tout););
}
bool aig_cuts::flush_roots(bool_var var, to_root const& to_root, node& n) {
bool changed = false;
for (unsigned i = 0; i < n.size(); ++i) {
literal& lit = m_literals[n.offset() + i];
literal r = to_root[lit.var()];
if (r != lit) {
changed = true;
lit = lit.sign() ? ~r : r;
}
if (lit.var() == var) {
return false;
}
}
if (changed && (n.is_and() || n.is_xor())) {
std::sort(m_literals.data() + n.offset(), m_literals.data() + n.offset() + n.size());
}
return true;
}
void aig_cuts::flush_roots(to_root const& to_root, cut_set& cs) {
for (unsigned j = 0; j < cs.size(); ++j) {
for (unsigned v : cs[j]) {
if (to_root[v] != literal(v, false)) {
evict(cs, j--);
break;
}
}
}
}
lbool aig_cuts::get_value(bool_var v) const {
return (m_aig[v].size() == 1 && m_aig[v][0].is_const()) ?
(m_aig[v][0].sign() ? l_false : l_true) :
l_undef;
}
void aig_cuts::init_cut_set(unsigned id) {
SASSERT(m_aig[id].size() == 1);
SASSERT(m_aig[id][0].is_valid());
auto& cut_set = m_cuts[id];
reset(cut_set);
cut_set.init(m_region, m_config.m_max_cutset_size + 1, id);
push_back(cut_set, cut(id));
}
bool aig_cuts::eq(node const& a, node const& b) {
if (a.is_valid() != b.is_valid()) return false;
if (!a.is_valid()) return true;
if (a.op() != b.op() || a.sign() != b.sign() || a.size() != b.size())
return false;
for (unsigned i = a.size(); i-- > 0; ) {
if (m_literals[a.offset() + i] != m_literals[b.offset() + i])
return false;
}
return true;
}
bool aig_cuts::similar(node const& a, node const& b) {
bool sim = true;
sim = a.is_lut() && !b.is_lut() && a.size() == b.size();
for (unsigned i = a.size(); sim && i-- > 0; ) {
sim = m_literals[a.offset() + i].var() == m_literals[b.offset() + i].var();
}
return sim;
}
bool aig_cuts::insert_aux(unsigned v, node const& n) {
if (!m_config.m_full) return false;
unsigned num_gt = 0, num_eq = 0;
for (node const& n2 : m_aig[v]) {
if (eq(n, n2) || similar(n, n2)) return false;
else if (n.size() < n2.size()) num_gt++;
else if (n.size() == n2.size()) num_eq++;
}
if (m_aig[v].size() < m_config.m_max_aux) {
on_node_add(v, n);
m_aig[v].push_back(n);
touch(v);
return true;
}
if (num_gt > 0) {
unsigned idx = rand() % num_gt;
for (node const& n2 : m_aig[v]) {
if (n.size() < n2.size()) {
if (idx == 0) {
on_node_del(v, m_aig[v][idx]);
on_node_add(v, n);
m_aig[v][idx] = n;
touch(v);
return true;
}
--idx;
}
}
}
if (num_eq > 0) {
unsigned idx = rand() % num_eq;
for (node const& n2 : m_aig[v]) {
if (n.size() == n2.size()) {
if (idx == 0) {
on_node_del(v, m_aig[v][idx]);
on_node_add(v, n);
m_aig[v][idx] = n;
touch(v);
return true;
}
--idx;
}
}
}
return false;
}
unsigned_vector aig_cuts::filter_valid_nodes() const {
unsigned id = 0;
unsigned_vector result;
for (auto& v : m_aig) {
if (!v.empty()) result.push_back(id);
++id;
}
return result;
}
cut_val aig_cuts::eval(node const& n, cut_eval const& env) const {
uint64_t result = 0;
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()].m_f : env[u.var()].m_t;
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()].m_f : env[u.var()].m_t;
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()].m_f : env[u.var()].m_t;
uint64_t vv = v.sign() ? env[v.var()].m_f : env[v.var()].m_t;
uint64_t wv = w.sign() ? env[w.var()].m_f : env[w.var()].m_t;
result = (uv & vv) | ((~uv) & wv);
break;
}
default:
UNREACHABLE();
}
if (n.sign()) result = ~result;
return cut_val(result, ~result);
}
cut_eval aig_cuts::simulate(unsigned num_rounds) {
cut_eval result;
for (unsigned i = 0; i < m_cuts.size(); ++i) {
uint64_t r =
(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 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));
}
}
void aig_cuts::on_node_del(unsigned v, node const& n) {
if (m_on_clause_del) {
node2def(m_on_clause_del, n, literal(v, false));
}
}
void aig_cuts::set_on_clause_add(on_clause_t& on_clause_add) {
m_on_clause_add = on_clause_add;
std::function<void(unsigned v, cut const& c)> _on_cut_add =
[this](unsigned v, cut const& c) { cut2def(m_on_clause_add, c, literal(v, false)); };
m_on_cut_add = _on_cut_add;
}
void aig_cuts::set_on_clause_del(on_clause_t& on_clause_del) {
m_on_clause_del = on_clause_del;
std::function<void(unsigned v, cut const& c)> _on_cut_del =
[this](unsigned v, cut const& c) { cut2def(m_on_clause_del, c, literal(v, false)); };
m_on_cut_del = _on_cut_del;
}
/**
* Encode the cut (variables and truth-table) in a set of clauses.
* r is the result.
*/
void aig_cuts::cut2def(on_clause_t& on_clause, cut const& c, literal r) {
IF_VERBOSE(10, verbose_stream() << "cut2def: " << r << " == " << c << "\n");
VERIFY(r != null_literal);
unsigned sz = c.size();
unsigned num_assigns = 1 << sz;
for (unsigned i = 0; i < num_assigns; ++i) {
m_clause.reset();
for (unsigned j = 0; j < sz; ++j) {
literal lit(c[j], 0 != (i & (1ull << j)));
m_clause.push_back(lit);
}
literal rr = r;
if (0 == (c.table() & (1ull << i))) rr.neg();
m_clause.push_back(rr);
on_clause(m_clause);
}
}
void aig_cuts::node2def(on_clause_t& on_clause, node const& n, literal r) {
IF_VERBOSE(10, display(verbose_stream() << "node2def " << r << " == ", n) << "\n");
SASSERT(on_clause);
literal c, t, e;
if (n.sign()) r.neg();
m_clause.reset();
unsigned num_comb = 0;
switch (n.op()) {
case var_op:
return;
case and_op:
for (unsigned i = 0; i < n.size(); ++i) {
m_clause.push_back(~r);
m_clause.push_back(m_literals[n.offset() + i]);
on_clause(m_clause);
m_clause.reset();
}
for (unsigned i = 0; i < n.size(); ++i) {
m_clause.push_back(~m_literals[n.offset()+i]);
}
m_clause.push_back(r);
on_clause(m_clause);
return;
case ite_op:
// r & c => t, r & ~c => e
// ~r & c => ~t, ~r & ~c => ~e
SASSERT(n.size() == 3);
c = m_literals[n.offset()+0];
t = m_literals[n.offset()+1];
e = m_literals[n.offset()+2];
m_clause.push_back(~r, ~c, t);
on_clause(m_clause);
m_clause.reset();
m_clause.push_back(~r, c, e);
on_clause(m_clause);
m_clause.reset();
m_clause.push_back(r, ~c, ~t);
on_clause(m_clause);
m_clause.reset();
m_clause.push_back(r, c, ~e);
on_clause(m_clause);
return;
case xor_op:
// r = a ^ b ^ c
// <=>
// ~r ^ a ^ b ^ c = 1
if (n.size() > 10) {
throw default_exception("cannot handle large xors");
}
num_comb = (1 << n.size());
for (unsigned i = 0; i < num_comb; ++i) {
bool parity = n.size() % 2 == 1;
m_clause.reset();
for (unsigned j = 0; j < n.size(); ++j) {
literal lit = m_literals[n.offset() + j];
if (0 == (i & (1 << j))) {
lit.neg();
}
else {
parity ^= true;
}
m_clause.push_back(lit);
}
m_clause.push_back(parity ? r : ~r);
TRACE(cut_simplifier, tout << "validate: " << m_clause << "\n";);
on_clause(m_clause);
}
return;
case lut_op:
// r = LUT(v0, v1, v2)
num_comb = (1 << n.size());
for (unsigned i = 0; i < num_comb; ++i) {
m_clause.reset();
for (unsigned j = 0; j < n.size(); ++j) {
literal lit = m_literals[n.offset() + j];
if (0 != (i & (1 << j))) lit.neg();
m_clause.push_back(lit);
}
m_clause.push_back(0 == (n.lut() & (1ull << i)) ? ~r : r);
TRACE(cut_simplifier, tout << n.lut() << " " << m_clause << "\n";);
on_clause(m_clause);
}
return;
default:
UNREACHABLE();
break;
}
}
/**
* compile the truth table from c into clauses that define ~v.
* compile definitions for nodes until all inputs have been covered.
* Assume only the first definition for a node is used for all cuts.
*/
void aig_cuts::cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c) {
bool_vector visited(m_aig.size(), false);
for (unsigned u : c) visited[u] = true;
unsigned_vector todo;
todo.push_back(v);
while (!todo.empty()) {
unsigned u = todo.back();
todo.pop_back();
if (visited[u]) {
continue;
}
visited[u] = true;
node const& n = m_aig[u][0];
node2def(on_clause, n, literal(u, false));
for (unsigned i = 0; i < n.size(); ++i) {
todo.push_back(m_literals[n.offset()+i].var());
}
}
cut2def(on_clause, c, literal(v, true));
}
/**
* simplify a set of cuts by removing don't cares.
*/
void aig_cuts::simplify() {
uint64_t masks[7];
for (unsigned i = 0; i <= 6; ++i) {
masks[i] = cut::effect_mask(i);
}
unsigned dont_cares = 0;
for (cut_set & cs : m_cuts) {
for (cut const& c : cs) {
uint64_t t = c.table();
for (unsigned i = 0; i < std::min(6u, c.size()); ++i) {
uint64_t diff = masks[i] & (t ^ (t >> (1ull << i)));
if (diff == 0ull) {
cut d(c);
d.remove_elem(i);
cs.insert(m_on_cut_add, m_on_cut_del, d);
cs.evict(m_on_cut_del, c);
++dont_cares;
break;
}
}
}
}
IF_VERBOSE(2, verbose_stream() << "#don't cares " << dont_cares << "\n");
}
struct aig_cuts::validator {
aig_cuts& t;
params_ref p;
reslimit lim;
solver s;
unsigned_vector vars;
bool_vector is_var;
validator(aig_cuts& t):t(t),s(p, lim) {
p.set_bool("cut_simplifier", false);
s.updt_params(p);
}
void on_clause(literal_vector const& clause) {
IF_VERBOSE(20, verbose_stream() << clause << "\n");
for (literal lit : clause) {
while (lit.var() >= s.num_vars()) s.mk_var();
is_var.reserve(lit.var() + 1, false);
if (!is_var[lit.var()]) { vars.push_back(lit.var()); is_var[lit.var()] = true; }
}
s.mk_clause(clause);
}
void check() {
lbool r = s.check();
IF_VERBOSE(10, verbose_stream() << "check: " << r << "\n");
if (r == l_true) {
IF_VERBOSE(0,
std::sort(vars.begin(), vars.end());
s.display(verbose_stream());
for (auto v : vars) verbose_stream() << v << " := " << s.get_model()[v] << "\n";
);
UNREACHABLE();
}
}
};
void aig_cuts::validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c) {
validator val(*this);
on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); };
cut2def(on_clause, a, literal(child(n, 0).var(), false));
cut2def(on_clause, b, literal(child(n, 1).var(), false));
cut2def(on_clause, c, literal(v, false));
node2def(on_clause, n, literal(v, true));
val.check();
}
void aig_cuts::validate_aigN(unsigned v, node const& n, cut const& c) {
IF_VERBOSE(10, verbose_stream() << "validate_aigN " << v << " == " << c << "\n");
validator val(*this);
on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); };
for (unsigned i = 0; i < n.size(); ++i) {
unsigned w = m_literals[n.offset() + i].var();
for (cut const& d : m_cuts[w]) {
cut2def(on_clause, d, literal(w, false));
}
}
cut2def(on_clause, c, literal(v, false));
node2def(on_clause, n, literal(v, true));
val.check();
}
std::ostream& aig_cuts::display(std::ostream& out) const {
auto ids = filter_valid_nodes();
for (auto id : ids) {
out << id << " == ";
bool first = true;
for (auto const& n : m_aig[id]) {
if (first) first = false; else out << " ";
display(out, n) << "\n";
}
m_cuts[id].display(out);
}
return out;
}
std::ostream& aig_cuts::display(std::ostream& out, node const& n) const {
out << (n.sign() ? "! " : " ");
switch (n.op()) {
case var_op: out << "var "; break;
case and_op: out << "& "; break;
case xor_op: out << "^ "; break;
case ite_op: out << "? "; break;
default: break;
}
for (unsigned i = 0; i < n.size(); ++i) {
out << m_literals[n.offset() + i] << " ";
}
return out;
}
}

238
src/sat/sat_aig_cuts.h
View file

@ -1,238 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_aig_cuts.h
Abstract:
Extract AIG definitions from clauses.
Perform cut-set enumeration to identify equivalences.
AIG extraction is incremental.
It can be called repeatedly.
Initially, a main aig node is inserted
(from initial clauses or the input
clausification in goal2sat).
Then, auxiliary AIG nodes can be inserted
by walking the current set of main and learned
clauses. AIG nodes with fewer arguments are preferred.
Author:
Nikolaj Bjorner 2020-01-02
--*/
#pragma once
#include "sat/sat_cutset.h"
#include "sat/sat_types.h"
namespace sat {
enum bool_op {
var_op,
and_op,
ite_op,
xor_op,
lut_op,
no_op
};
inline std::ostream& operator<<(std::ostream& out, bool_op op) {
switch (op) {
case var_op: return out << "v";
case and_op: return out << "&";
case ite_op: return out << "?";
case xor_op: return out << "^";
case lut_op: return out << "#";
default: return out << "";
}
}
class aig_cuts {
public:
typedef std::function<void(literal_vector const&)> on_clause_t;
struct config {
unsigned m_max_cutset_size;
unsigned m_max_aux;
unsigned m_max_insertions;
bool m_full;
config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(true) {}
};
private:
// encodes one of var, and, !and, xor, !xor, ite, !ite.
class node {
bool m_sign{ false };
bool_op m_op{ no_op };
uint64_t m_lut{ 0 };
unsigned m_size{ 0 };
unsigned m_offset{ 0 };
public:
node():
m_sign(false), m_op(no_op), m_size(UINT_MAX), m_offset(UINT_MAX) {}
explicit node(unsigned v) :
m_sign(false), m_op(var_op), m_size(0), m_offset(v) {}
explicit node(bool sign, bool_op op, unsigned nc, unsigned o) :
m_sign(sign), m_op(op), m_size(nc), m_offset(o) {}
explicit node(uint64_t lut, unsigned nc, unsigned o):
m_sign(false), m_op(lut_op), m_lut(lut), m_size(nc), m_offset(o) {}
bool is_valid() const { return m_offset != UINT_MAX; }
bool_op op() const { return m_op; }
bool is_var() const { return m_op == var_op; }
bool is_and() const { return m_op == and_op; }
bool is_xor() const { return m_op == xor_op; }
bool is_ite() const { return m_op == ite_op; }
bool is_lut() const { return m_op == lut_op; }
bool is_const() const { return is_and() && size() == 0; }
unsigned var() const { SASSERT(is_var()); return m_offset; }
bool sign() const { return m_sign; }
unsigned size() const { return m_size; }
unsigned offset() const { return m_offset; }
uint64_t lut() const { return m_lut; }
};
random_gen m_rand;
config m_config;
vector<svector<node>> m_aig;
literal_vector m_literals;
region m_region;
cut_set m_cut_set1, m_cut_set2, m_empty_cuts;
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;
svector<std::pair<bool_var, literal>> m_roots;
unsigned m_insertions;
on_clause_t m_on_clause_add, m_on_clause_del;
cut_set::on_update_t m_on_cut_add, m_on_cut_del;
literal_vector m_clause;
cut const* m_tables[6];
uint64_t m_luts[6];
literal m_lits[6];
class to_root {
literal_vector m_to_root;
void reserve(bool_var v) {
while (v >= m_to_root.size()) {
m_to_root.push_back(literal(m_to_root.size(), false));
}
}
public:
literal operator[](bool_var v) const {
return (v < m_to_root.size()) ? m_to_root[v] : literal(v, false);
}
literal& operator[](bool_var v) {
reserve(v);
return m_to_root[v];
}
};
class lut {
aig_cuts& a;
node const* n;
cut const* c;
public:
lut(aig_cuts& a, node const& n) : a(a), n(&n), c(nullptr) {}
lut(aig_cuts& a, cut const& c) : a(a), n(nullptr), c(&c) {}
unsigned size() const { return n ? n->size() : c->size(); }
literal child(unsigned idx) const { return n ? a.child(*n, idx) : a.child(*c, idx); }
uint64_t table() const { return n ? n->lut() : c->table(); }
std::ostream& display(std::ostream& out) const { return n ? a.display(out, *n) : out << *c; }
};
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 v < m_last_touched.size() && 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);
bool eq(node const& a, node const& b);
bool similar(node const& a, node const& b);
unsigned_vector filter_valid_nodes() const;
void augment(unsigned_vector const& ids);
void augment(unsigned id, node const& n);
void augment_ite(unsigned v, node const& n, cut_set& cs);
void augment_aig0(unsigned v, node const& n, cut_set& cs);
void augment_aig1(unsigned v, node const& n, cut_set& cs);
void augment_aig2(unsigned v, node const& n, cut_set& cs);
void augment_aigN(unsigned v, node const& n, cut_set& cs);
void augment_lut(unsigned v, lut const& n, cut_set& cs);
void augment_lut_rec(unsigned v, lut const& n, cut& a, unsigned idx, cut_set& cs);
cut_set const& lit2cuts(literal lit) const { return lit.var() < m_cuts.size() ? m_cuts[lit.var()] : m_empty_cuts; }
bool insert_cut(unsigned v, cut const& c, cut_set& cs);
void flush_roots();
bool flush_roots(bool_var var, to_root const& to_root, node& n);
void flush_roots(to_root const& to_root, cut_set& cs);
cut_val eval(node const& n, cut_eval const& env) const;
lbool get_value(bool_var v) 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]; }
literal child(cut const& n, unsigned idx) const { SASSERT(idx < n.size()); return literal(n[idx], false); }
void on_node_add(unsigned v, node const& n);
void on_node_del(unsigned v, node const& n);
void evict(cut_set& cs, unsigned idx) { cs.evict(m_on_cut_del, idx); }
void reset(cut_set& cs) { cs.reset(m_on_cut_del); }
void push_back(cut_set& cs, cut const& c) { cs.push_back(m_on_cut_add, c); }
void shrink(cut_set& cs, unsigned j) { cs.shrink(m_on_cut_del, j); }
void cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c);
void node2def(on_clause_t& on_clause, node const& n, literal r);
struct validator;
void validate_cut(unsigned v, cut const& c);
void validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c);
void validate_aigN(unsigned v, node const& n, cut const& c);
void add_node(bool_var v, node const& n);
public:
aig_cuts();
void add_var(unsigned v);
void add_node(literal head, bool_op op, unsigned sz, literal const* args);
void add_node(bool_var head, uint64_t lut, unsigned sz, bool_var const* args);
void add_cut(bool_var v, uint64_t lut, bool_var_vector const& args);
void set_root(bool_var v, literal r);
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.reserve(v + 1, 0); 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()();
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.reserve(v + 1, false); m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
cut_eval simulate(unsigned num_rounds);
void simplify();
std::ostream& display(std::ostream& out) const;
};
}

9
src/sat/sat_config.cpp
View file

@ -109,15 +109,6 @@ namespace sat {
m_anf_simplify = p.anf();
m_anf_delay = p.anf_delay();
m_anf_exlin = p.anf_exlin();
m_cut_simplify = p.cut();
m_cut_delay = p.cut_delay();
m_cut_aig = p.cut_aig();
m_cut_lut = p.cut_lut();
m_cut_xor = p.cut_xor();
m_cut_npn3 = p.cut_npn3();
m_cut_dont_cares = p.cut_dont_cares();
m_cut_redundancies = p.cut_redundancies();
m_cut_force = p.cut_force();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_double = p.lookahead_double();
m_lookahead_simplify_bca = p.lookahead_simplify_bca();

9
src/sat/sat_config.h
View file

@ -119,15 +119,6 @@ namespace sat {
bool m_local_search;
local_search_mode m_local_search_mode;
bool m_local_search_dbg_flips;
bool m_cut_simplify;
unsigned m_cut_delay;
bool m_cut_aig;
bool m_cut_lut;
bool m_cut_xor;
bool m_cut_npn3;
bool m_cut_dont_cares;
bool m_cut_redundancies;
bool m_cut_force;
bool m_anf_simplify;
unsigned m_anf_delay;
bool m_anf_exlin;

755
src/sat/sat_cut_simplifier.cpp
View file

@ -1,755 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cut_simplifier.cpp
Abstract:
extract AIG definitions from clauses
Perform cut-set enumeration to identify equivalences.
Author:
Nikolaj Bjorner 2020-01-02
--*/
#include "sat/sat_cut_simplifier.h"
#include "sat/sat_xor_finder.h"
#include "sat/sat_lut_finder.h"
#include "sat/sat_npn3_finder.h"
#include "sat/sat_elim_eqs.h"
namespace sat {
struct cut_simplifier::report {
cut_simplifier& s;
stopwatch m_watch;
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_learned_implies;
report(cut_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.cut-simplifier";
if (nu > 0) verbose_stream() << " :num-units " << nu;
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");
}
};
struct cut_simplifier::validator {
solver& _s;
params_ref p;
literal_vector m_assumptions;
validator(solver& _s, params_ref const& p): _s(_s), p(p) {
}
void validate(unsigned n, literal const* clause) {
validate(literal_vector(n, clause));
}
void validate(literal_vector const& clause) {
if (clause.size() == 2 && clause[0] == ~clause[1]) return;
solver s(p, _s.rlimit());
s.copy(_s, false);
IF_VERBOSE(10, verbose_stream() << "validate: " << clause << "\n");
m_assumptions.reset();
for (literal lit : clause) m_assumptions.push_back(~lit);
lbool r = s.check(clause.size(), m_assumptions.data());
if (r != l_false) {
IF_VERBOSE(0,
verbose_stream() << "not validated: " << clause << "\n";
s.display(verbose_stream()););
UNREACHABLE();
}
}
};
void cut_simplifier::ensure_validator() {
if (!m_validator) {
params_ref p;
p.set_bool("aig", false);
p.set_bool("drat.check_unsat", false);
p.set_sym("drat.file", symbol());
p.set_uint("max_conflicts", 10000);
m_validator = alloc(validator, s, p);
}
}
cut_simplifier::cut_simplifier(solver& _s):
s(_s),
m_trail_size(0),
m_validator(nullptr) {
if (s.get_config().m_drat) {
std::function<void(literal_vector const& clause)> _on_add =
[this](literal_vector const& clause) { s.m_drat.add(clause); };
std::function<void(literal_vector const& clause)> _on_del =
[this](literal_vector const& clause) { s.m_drat.del(clause); };
m_aig_cuts.set_on_clause_add(_on_add);
m_aig_cuts.set_on_clause_del(_on_del);
}
else if (m_config.m_validate_cuts) {
ensure_validator();
std::function<void(literal_vector const& clause)> _on_add =
[this](literal_vector const& clause) {
m_validator->validate(clause);
};
m_aig_cuts.set_on_clause_add(_on_add);
}
}
cut_simplifier::~cut_simplifier() {
dealloc(m_validator);
}
void cut_simplifier::add_and(literal head, unsigned sz, literal const* lits) {
m_aig_cuts.add_node(head, and_op, sz, lits);
for (unsigned i = 0; i < sz; ++i) VERIFY(head.var() != lits[i].var());
m_stats.m_num_ands++;
}
// head == l1 or l2 or l3
// <=>
// ~head == ~l1 and ~l2 and ~l3
void cut_simplifier::add_or(literal head, unsigned sz, literal const* lits) {
m_lits.reset();
m_lits.append(sz, lits);
for (unsigned i = 0; i < sz; ++i) m_lits[i].neg();
m_aig_cuts.add_node(~head, and_op, sz, m_lits.data());
m_stats.m_num_ands++;
}
void cut_simplifier::add_xor(literal head, unsigned sz, literal const* lits) {
m_aig_cuts.add_node(head, xor_op, sz, lits);
m_stats.m_num_xors++;
}
void cut_simplifier::add_ite(literal head, literal c, literal t, literal e) {
literal lits[3] = { c, t, e };
m_aig_cuts.add_node(head, ite_op, 3, lits);
m_stats.m_num_ites++;
}
void cut_simplifier::add_iff(literal head, literal l1, literal l2) {
literal lits[2] = { l1, ~l2 };
m_aig_cuts.add_node(head, xor_op, 2, lits);
m_stats.m_num_xors++;
}
void cut_simplifier::set_root(bool_var v, literal r) {
m_aig_cuts.set_root(v, r);
}
void cut_simplifier::operator()() {
bool force = s.m_config.m_cut_force;
report _report(*this);
TRACE(cut_simplifier, s.display(tout););
unsigned n = 0, i = 0;
++m_stats.m_num_calls;
do {
n = m_stats.m_num_eqs + m_stats.m_num_units;
clauses2aig();
aig2clauses();
++i;
}
while (((force && i < 5) || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
}
/**
\brief extract AIG definitions from clauses
Ensure that they are sorted and variables have unique definitions.
*/
void cut_simplifier::clauses2aig() {
for (; m_config.m_enable_units && m_trail_size < s.init_trail_size(); ++m_trail_size) {
literal lit = s.trail_literal(m_trail_size);
m_aig_cuts.add_node(lit, and_op, 0, nullptr);
}
clause_vector clauses(s.clauses());
if (m_config.m_learned2aig) clauses.append(s.learned());
std::function<void (literal head, literal_vector const& ands)> on_and =
[&,this](literal head, literal_vector const& ands) {
m_aig_cuts.add_node(head, and_op, ands.size(), ands.data());
m_stats.m_xands++;
};
std::function<void (literal head, literal c, literal t, literal e)> on_ite =
[&,this](literal head, literal c, literal t, literal e) {
literal args[3] = { c, t, e };
m_aig_cuts.add_node(head, ite_op, 3, args);
m_stats.m_xites++;
};
if (s.m_config.m_cut_aig) {
aig_finder af(s);
af.set(on_and);
af.set(on_ite);
af(clauses);
}
std::function<void (literal_vector const&)> on_xor =
[&,this](literal_vector const& xors) {
SASSERT(xors.size() > 1);
unsigned max_level = xors.back().var();
unsigned index = xors.size() - 1;
for (unsigned i = index; i-- > 0; ) {
literal l = xors[i];
if (l.var() > max_level) {
max_level = l.var();
index = i;
}
}
// head + t1 + t2 + .. = 1
// <=>
// ~head = t1 + t2 + ..
literal head = ~xors[index];
TRACE(cut_simplifier, tout << xors << "\n";);
unsigned sz = xors.size() - 1;
m_lits.reset();
for (unsigned i = xors.size(); i-- > 0; ) {
if (i != index)
m_lits.push_back(xors[i]);
}
m_aig_cuts.add_node(head, xor_op, sz, m_lits.data());
m_lits.reset();
m_stats.m_xxors++;
};
if (s.m_config.m_cut_xor) {
xor_finder xf(s);
xf.set(on_xor);
xf(clauses);
}
std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut =
[&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
m_stats.m_xluts++;
// m_aig_cuts.add_cut(v, lut, vars);
m_aig_cuts.add_node(v, lut, vars.size(), vars.data());
};
if (s.m_config.m_cut_npn3) {
npn3_finder nf(s);
// TBD: stubs for npn3
// question: perhaps just use a LUT interface?
// nf.set_on_mux
// nf.set_on_maj
// nf.set_on_orand
// nf.set_on_and
// nf.set_on_xor
// nf.set_on_andxor
// nf.set_on_xorand
// nf.set_on_gamble
// nf.set_on_onehot
// nf.set_on_dot
// nf(clauses);
}
if (s.m_config.m_cut_lut) {
lut_finder lf(s);
lf.set(on_lut);
lf(clauses);
}
#if 0
statistics st;
collect_statistics(st);
st.display(std::cout);
exit(0);
#endif
}
void cut_simplifier::aig2clauses() {
vector<cut_set> const& cuts = m_aig_cuts();
m_stats.m_num_cuts = m_aig_cuts.num_cuts();
add_dont_cares(cuts);
cuts2equiv(cuts);
cuts2implies(cuts);
simulate_eqs();
}
void cut_simplifier::cuts2equiv(vector<cut_set> const& cuts) {
map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;
bool new_eq = false;
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());
new_eq = true;
};
for (unsigned i = cuts.size(); i-- > 0; ) {
literal u(i, false);
for (auto& c : cuts[i]) {
unsigned j = 0;
cut nc(c);
nc.negate();
if (m_config.m_enable_units && c.is_true()) {
assign_unit(c, u);
}
else if (m_config.m_enable_units && c.is_false()) {
assign_unit(nc, ~u);
}
else if (cut2id.find(&c, j)) {
literal v(j, false);
assign_equiv(c, u, v);
add_eq(u, v);
}
else if (cut2id.find(&nc, j)) {
literal v(j, true);
assign_equiv(c, u, v);
add_eq(u, v);
}
else {
cut2id.insert(&c, i);
}
}
}
if (new_eq) {
uf2equiv(uf);
}
}
void cut_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);
certify_unit(lit, c);
s.assign_unit(lit);
++m_stats.m_num_units;
}
void cut_simplifier::assign_equiv(cut const& c, literal u, literal v) {
if (u.var() == v.var()) return;
IF_VERBOSE(10, verbose_stream() << u << " " << v << " " << c << "\n";);
TRACE(cut_simplifier, tout << u << " == " << v << "\n";);
certify_equivalence(u, v, c);
validate_eq(u, v);
}
/**
* Convert a union-find over literals into input for eim_eqs.
*/
void cut_simplifier::uf2equiv(union_find<> const& uf) {
union_find_default_ctx ctx;
union_find<> uf2(ctx);
bool new_eq = false;
for (unsigned i = 2*s.num_vars(); i--> 0; ) uf2.mk_var();
// extract equivalences over non-eliminated literals.
for (unsigned idx = 0; idx < uf.get_num_vars(); ++idx) {
if (!uf.is_root(idx) || 1 == uf.size(idx)) continue;
literal root = null_literal;
unsigned first = idx;
do {
literal lit = to_literal(idx);
if (!s.was_eliminated(lit)) {
if (root == null_literal) {
root = lit;
}
else {
uf2.merge(lit.index(), root.index());
new_eq = true;
++m_stats.m_num_eqs;
}
}
idx = uf.next(idx);
}
while (first != idx);
}
for (unsigned i = s.num_vars(); i-- > 0; ) {
literal lit(i, false);
if (uf2.find(lit.index()) == uf2.find((~lit).index())) {
s.set_conflict();
return;
}
}
if (new_eq) {
elim_eqs elim(s);
elim(uf2);
}
}
/**
* Extract binary clauses from cuts.
* A bit encoding of a LUT of u
* that sets a subset of bits for LUT' of v establishes
* that u implies v.
*/
void cut_simplifier::cuts2implies(vector<cut_set> const& cuts) {
if (!m_config.m_learn_implies) return;
vector<vector<std::pair<unsigned, cut const*>>> var_tables;
map<cut const*, unsigned, cut::dom_hash_proc, cut::dom_eq_proc> cut2tables;
unsigned j = 0;
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;
if (!cut2tables.find(&c, j)) {
j = var_tables.size();
var_tables.push_back(vector<std::pair<unsigned, cut const*>>());
cut2tables.insert(&c, j);
}
var_tables[j].push_back(std::make_pair(cs.var(), &c));
}
}
for (unsigned i = 0; i < var_tables.size(); ++i) {
auto const& vt = var_tables[i];
for (unsigned j = 0; j < vt.size(); ++j) {
literal u(vt[j].first, false);
cut const& c1 = *vt[j].second;
cut nc1(c1);
nc1.negate();
uint64_t t1 = c1.table();
uint64_t n1 = nc1.table();
for (unsigned k = j + 1; k < vt.size(); ++k) {
literal v(vt[k].first, false);
cut const& c2 = *vt[k].second;
uint64_t t2 = c2.table();
uint64_t n2 = c2.ntable();
if (t1 == t2 || t1 == n2) {
// already handled
}
else if ((t1 | t2) == t2) {
learn_implies(big, c1, u, v);
}
else if ((t1 | n2) == n2) {
learn_implies(big, c1, u, ~v);
}
else if ((n1 | t2) == t2) {
learn_implies(big, nc1, ~u, v);
}
else if ((n1 | n2) == n2) {
learn_implies(big, nc1, ~u, ~v);
}
}
}
}
}
void cut_simplifier::learn_implies(big& big, cut const& c, literal u, literal v) {
if (u == ~v) {
assign_unit(c, v);
return;
}
if (u == v) {
return;
}
bin_rel q, p(~u, v);
if (m_bins.find(p, q) && q.op != op_code::none)
return;
if (big.connected(u, v))
return;
for (auto const& w : s.get_wlist(u))
if (w.is_binary_clause() && v == w.get_literal())
return;
certify_implies(u, v, c);
s.mk_clause(~u, v, sat::status::redundant());
// m_bins owns reference to ~u or v created by certify_implies
m_bins.insert(p);
++m_stats.m_num_learned_implies;
}
void cut_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<literal> val2lit;
unsigned i = 0, num_eqs = 0;
for (cut_val val : var2val) {
if (!s.was_eliminated(i) && s.value(i) == l_undef) {
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(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++;
}
else {
val2lit.insert(val.m_t, u);
val2lit.insert(val.m_f, ~u);
}
}
++i;
}
IF_VERBOSE(2, verbose_stream() << "(sat.cut-simplifier num simulated eqs " << num_eqs << ")\n");
}
void cut_simplifier::track_binary(bin_rel const& p) {
if (!s.m_config.m_drat)
return;
literal u, v;
p.to_binary(u, v);
track_binary(u, v);
}
void cut_simplifier::untrack_binary(bin_rel const& p) {
if (!s.m_config.m_drat)
return;
literal u, v;
p.to_binary(u, v);
untrack_binary(u, v);
}
void cut_simplifier::track_binary(literal u, literal v) {
if (s.m_config.m_drat) {
s.m_drat.add(u, v, sat::status::redundant());
}
}
void cut_simplifier::untrack_binary(literal u, literal v) {
if (s.m_config.m_drat) {
s.m_drat.del(u, v);
}
}
void cut_simplifier::certify_unit(literal u, cut const& c) {
certify_implies(~u, u, c);
}
/**
* Equivalences modulo cuts are not necessarily DRAT derivable.
* To ensure that there is a DRAT derivation we create all resolvents
* of the LUT clauses until deriving binary u or ~v and ~u or v.
* each resolvent is DRAT derivable because there are two previous lemmas that
* contain complementary literals.
*/
void cut_simplifier::certify_equivalence(literal u, literal v, cut const& c) {
certify_implies(u, v, c);
certify_implies(v, u, c);
}
/**
* certify that u implies v, where c is the cut for u.
* Then every position in c where u is true, it has to be
* the case that v is too.
* Where u is false, v can have any value.
* Thus, for every clause C or u', where u' is u or ~u,
* it follows that C or ~u or v
*/
void cut_simplifier::certify_implies(literal u, literal v, cut const& c) {
if (!s.m_config.m_drat) return;
vector<literal_vector> clauses;
std::function<void(literal_vector const& clause)> on_clause =
[&,this](literal_vector const& clause) {
SASSERT(clause.back().var() == u.var());
clauses.push_back(clause);
clauses.back().back() = ~u;
if (~u != v) clauses.back().push_back(v);
s.m_drat.add(clauses.back());
};
m_aig_cuts.cut2def(on_clause, c, u);
// create all resolvents over C. C is assumed to
// contain all combinations of some set of literals.
unsigned i = 0, sz = clauses.size();
while (sz - i > 1) {
SASSERT((sz & (sz - 1)) == 0 && "sz is a power of 2");
for (; i < sz; ++i) {
auto const& clause = clauses[i];
if (clause[0].sign()) {
literal_vector cl(clause.size() - 1, clause.data() + 1);
clauses.push_back(cl);
s.m_drat.add(cl);
}
}
i = sz;
sz = clauses.size();
}
IF_VERBOSE(10, for (auto const& clause : clauses) verbose_stream() << clause << "\n";);
// once we established equivalence, don't need auxiliary clauses for DRAT.
clauses.pop_back();
for (auto const& clause : clauses) {
s.m_drat.del(clause);
}
}
void cut_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
if (s.m_config.m_cut_dont_cares) {
cuts2bins(cuts);
bins2dont_cares();
dont_cares2cuts(cuts);
}
if (s.m_config.m_cut_redundancies) {
m_aig_cuts.simplify();
}
}
/**
* Collect binary relations between variables that occur in cut sets.
*/
void cut_simplifier::cuts2bins(vector<cut_set> const& cuts) {
svector<bin_rel> dcs;
for (auto const& p : m_bins)
if (p.op != op_code::none)
dcs.push_back(p);
m_bins.reset();
for (auto const& cs : cuts)
for (auto const& c : cs)
for (unsigned i = c.size(); i-- > 0; )
for (unsigned j = i; j-- > 0; )
m_bins.insert(bin_rel(c[j],c[i]));
// don't lose previous don't cares
for (auto const& p : dcs) {
if (m_bins.contains(p)) {
m_bins.insert(p);
}
else {
untrack_binary(p);
}
}
}
/**
* Compute masks for binary relations.
*/
void cut_simplifier::bins2dont_cares() {
big b(s.rand());
b.init(s, true);
for (auto& p : m_bins) {
if (p.op != op_code::none) continue;
literal u(p.u, false), v(p.v, false);
// u -> v, then u & ~v is impossible
if (b.connected(u, v)) {
p.op = op_code::pn;
}
else if (b.connected(u, ~v)) {
p.op = op_code::pp;
}
else if (b.connected(~u, v)) {
p.op = op_code::nn;
}
else if (b.connected(~u, ~v)) {
p.op = op_code::np;
}
if (p.op != op_code::none) {
track_binary(p);
}
}
IF_VERBOSE(2, {
unsigned n = 0; for (auto const& p : m_bins) if (p.op != op_code::none) ++n;
verbose_stream() << n << " / " << m_bins.size() << " don't cares\n";
});
}
/**
* Loop over cuts, if it is possible to add a new don't care combination
* to a cut, then ensure that the variable is "touched" so that it participates
* in the next propagation.
*/
void cut_simplifier::dont_cares2cuts(vector<cut_set> const& cuts) {
for (auto& cs : cuts) {
for (auto const& c : cs) {
if (add_dont_care(c)) {
m_aig_cuts.touch(cs.var());
m_stats.m_num_dont_care_reductions++;
}
}
}
}
/**
* compute masks for position i, j and op-code p.op
* For the don't care combination false, false, the first don't care
* position is 0. If it is true, false, the first don't care position
* is the position that encodes the first occurrence where i is true.
* It is 2^i. Cases for false, true and true, true are similar.
* Don't care positions are spaced apart by 2^{j+1},
* where j is the second variable position.
*/
uint64_t cut_simplifier::op2dont_care(unsigned i, unsigned j, bin_rel const& p) {
SASSERT(i < j && j < 6);
if (p.op == op_code::none) return 0ull;
// first position of mask is offset into output bits contributed by i and j
bool i_is_0 = (p.op == op_code::np || p.op == op_code::nn);
bool j_is_0 = (p.op == op_code::pn || p.op == op_code::nn);
uint64_t first = (i_is_0 ? 0 : (1 << i)) + (j_is_0 ? 0 : (1 << j));
uint64_t inc = 1ull << (j + 1);
uint64_t r = 1ull << first;
while (inc < 64ull) { r |= (r << inc); inc *= 2; }
return r;
}
/**
* Apply obtained dont_cares to cut sets.
* The don't care bits are added to the LUT, so that the
* output is always 1 on don't care combinations.
*/
bool cut_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) {
bin_rel p(c[i], c[j]);
if (m_bins.find(p, p) && p.op != op_code::none) {
dc |= op2dont_care(i, j, p);
}
}
}
return (dc != c.dont_care()) && (c.add_dont_care(dc), true);
}
void cut_simplifier::collect_statistics(statistics& st) const {
st.update("sat-cut.eqs", m_stats.m_num_eqs);
st.update("sat-cut.cuts", m_stats.m_num_cuts);
st.update("sat-cut.ands", m_stats.m_num_ands);
st.update("sat-cut.ites", m_stats.m_num_ites);
st.update("sat-cut.xors", m_stats.m_num_xors);
st.update("sat-cut.xands", m_stats.m_xands);
st.update("sat-cut.xites", m_stats.m_xites);
st.update("sat-cut.xxors", m_stats.m_xxors);
st.update("sat-cut.xluts", m_stats.m_xluts);
st.update("sat-cut.dc-reduce", m_stats.m_num_dont_care_reductions);
}
void cut_simplifier::validate_unit(literal lit) {
if (!m_config.m_validate_lemmas) return;
ensure_validator();
m_validator->validate(1, &lit);
}
void cut_simplifier::validate_eq(literal a, literal b) {
if (!m_config.m_validate_lemmas) return;
ensure_validator();
literal lits1[2] = { a, ~b };
literal lits2[2] = { ~a, b };
m_validator->validate(2, lits1);
m_validator->validate(2, lits2);
}
}

174
src/sat/sat_cut_simplifier.h
View file

@ -1,174 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cut_simplifier.h
Abstract:
extract AIG definitions from clauses
Perform cut-set enumeration to identify equivalences.
Author:
Nikolaj Bjorner 2020-01-02
--*/
#pragma once
#include "util/union_find.h"
#include "sat/sat_aig_finder.h"
#include "sat/sat_aig_cuts.h"
namespace sat {
class cut_simplifier {
public:
struct stats {
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
unsigned m_xxors, m_xands, m_xites, m_xluts; // extrated gates
unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
struct config {
bool m_enable_units; // enable learning units
bool m_enable_dont_cares; // enable applying don't cares to LUTs
bool m_learn_implies; // learn binary clauses
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_simulate_eqs(false) {}
};
private:
struct report;
struct validator;
/**
* collect pairs of literal combinations that are impossible
* base on binary implication graph queries. Apply the masks
* on cut sets so to allow detecting equivalences modulo
* implications.
*
* The encoding is as follows:
* a or b -> op = nn because (~a & ~b) is a don't care
* ~a or b -> op = pn because (a & ~b) is a don't care
* a or ~b -> op = np because (~a & b) is a don't care
* ~a or ~b -> op = pp because (a & b) is a don't care
*
*/
enum class op_code { pp, pn, np, nn, none };
struct bin_rel {
unsigned u, v;
op_code op;
bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(op_code::none) {
if (u > v) std::swap(u, v);
}
// convert binary clause into a bin-rel
bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(op_code::none) {
if (_u.sign() && _v.sign()) op = op_code::pp;
else if (_u.sign()) op = op_code::pn;
else if (_v.sign()) op = op_code::np;
else op = op_code::nn;
if (u > v) {
std::swap(u, v);
if (op == op_code::np) op = op_code::pn;
else if (op == op_code::pn) op = op_code::np;
}
}
bin_rel(): u(UINT_MAX), v(UINT_MAX), op(op_code::none) {}
struct hash {
unsigned operator()(bin_rel const& p) const {
return p.u + 65599*p.v; // Weinberger's should be a bit cheaper mk_mix(p.u, p.v, 1);
}
};
struct eq {
bool operator()(bin_rel const& a, bin_rel const& b) const {
return a.u == b.u && a.v == b.v;
}
};
void to_binary(literal& lu, literal& lv) const {
switch (op) {
case op_code::pp: lu = literal(u, true); lv = literal(v, true); break;
case op_code::pn: lu = literal(u, true); lv = literal(v, false); break;
case op_code::np: lu = literal(u, false); lv = literal(v, true); break;
case op_code::nn: lu = literal(u, false); lv = literal(v, false); break;
default: UNREACHABLE(); break;
}
}
};
solver& s;
stats m_stats;
config m_config;
aig_cuts m_aig_cuts;
unsigned m_trail_size;
literal_vector m_lits;
validator* m_validator;
hashtable<bin_rel, bin_rel::hash, bin_rel::eq> m_bins;
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);
void assign_unit(cut const& c, literal lit);
void assign_equiv(cut const& c, literal u, literal v);
void learn_implies(big& big, cut const& c, literal u, literal v);
void ensure_validator();
void validate_unit(literal lit);
void validate_eq(literal a, literal b);
void certify_unit(literal u, cut const& c);
void certify_implies(literal u, literal v, cut const& c);
void certify_equivalence(literal u, literal v, cut const& c);
void track_binary(literal u, literal v);
void untrack_binary(literal u, literal v);
void track_binary(bin_rel const& p);
void untrack_binary(bin_rel const& p);
void add_dont_cares(vector<cut_set> const& cuts);
void cuts2bins(vector<cut_set> const& cuts);
void bins2dont_cares();
void dont_cares2cuts(vector<cut_set> const& cuts);
bool add_dont_care(cut const & c);
uint64_t op2dont_care(unsigned i, unsigned j, bin_rel const& p);
public:
cut_simplifier(solver& s);
~cut_simplifier();
void operator()();
void collect_statistics(statistics& st) const;
/**
* The clausifier may know that some literal is defined as a
* function of other literals. This API is exposed so that
* the clausifier can instrument the simplifier with an initial
* AIG.
* set_root is issued from the equivalence finder.
*/
void add_and(literal head, unsigned sz, literal const* args);
void add_or(literal head, unsigned sz, literal const* args);
void add_xor(literal head, unsigned sz, literal const* args);
void add_ite(literal head, literal c, literal t, literal e);
void add_iff(literal head, literal l1, literal l2);
void set_root(bool_var v, literal r);
};
}

280
src/sat/sat_cutset.cpp
View file

@ -1,280 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cutset.cpp
Author:
Nikolaj Bjorner 2020-01-02
--*/
#include "util/hashtable.h"
#include "sat/sat_cutset.h"
#include "sat/sat_cutset_compute_shift.h"
#include <memory>
#include <sstream>
namespace sat {
/**
\brief
if c is subsumed by a member in cut_set, then c is not inserted.
otherwise, remove members that c subsumes.
Note that the cut_set maintains invariant that elements don't subsume each-other.
TBD: this is a bottleneck.
Ideas:
- add Bloom filter to is_subset_of operation.
- pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation.
*/
bool cut_set::insert(on_update_t& on_add, on_update_t& on_del, cut const& c) {
unsigned i = 0, k = m_size;
for (; i < k; ++i) {
cut const& a = (*this)[i];
if (a.subset_of(c)) {
return false;
}
if (c.subset_of(a)) {
std::swap(m_cuts[i--], m_cuts[--k]);
}
}
// for DRAT make sure to add new element before removing old cuts
// the new cut may need to be justified relative to the old cut
push_back(on_add, c);
std::swap(m_cuts[i++], m_cuts[m_size-1]);
shrink(on_del, i);
return true;
}
bool cut_set::no_duplicates() const {
hashtable<cut const*, cut::hash_proc, cut::eq_proc> table;
for (auto const& cut : *this) {
VERIFY(!table.contains(&cut));
table.insert(&cut);
}
return true;
}
std::ostream& cut_set::display(std::ostream& out) const {
for (auto const& cut : *this) {
cut.display(out) << "\n";
}
return out;
}
void cut_set::shrink(on_update_t& on_del, unsigned j) {
if (m_var != UINT_MAX && on_del) {
for (unsigned i = j; i < m_size; ++i) {
on_del(m_var, m_cuts[i]);
}
}
m_size = j;
}
void cut_set::push_back(on_update_t& on_add, cut const& c) {
SASSERT(m_max_size > 0);
if (!m_cuts) {
m_cuts = new (*m_region) cut[m_max_size];
}
if (m_size == m_max_size) {
m_max_size *= 2;
cut* new_cuts = new (*m_region) cut[m_max_size];
std::uninitialized_copy(m_cuts, m_cuts + m_size, new_cuts);
m_cuts = new_cuts;
}
if (m_var != UINT_MAX && on_add) on_add(m_var, c);
m_cuts[m_size++] = c;
}
void cut_set::evict(on_update_t& on_del, cut const& c) {
for (unsigned i = 0; i < m_size; ++i) {
if (m_cuts[i] == c) {
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];
}
void cut_set::init(region& r, unsigned max_sz, unsigned v) {
m_var = v;
m_size = 0;
SASSERT(!m_region || m_cuts);
VERIFY(!m_region || m_max_size > 0);
if (!m_region) {
m_max_size = 2; // max_sz;
m_region = &r;
m_cuts = nullptr;
}
}
/**
\brief shift table 'a' by adding elements from 'c'.
a.shift_table(c)
\pre 'a' is a subset of 'c'.
Let 't' be the table for 'a'.
i'th bit in t is function of indices x0*2^0 + x2*2^1 = i
i'th bit in t' is function of indices x0*2^0 + x1*2^1 + x2*2^2 = i
i -> assignment to coefficients in c,
-> assignment to coefficients in a
-> compute j,
-> t'[i] <- t[j]
This is still time consuming:
Ideas:
- pre-compute some shift operations.
- use strides on some common cases.
- what ABC does?
*/
uint64_t cut::shift_table(cut const& c) const {
SASSERT(subset_of(c));
unsigned index = 0;
for (unsigned i = 0, j = 0, x = (*this)[i], y = c[j]; x != UINT_MAX; ) {
if (x == y) {
index |= (1 << j);
x = (*this)[++i];
}
y = c[++j];
}
index |= (1 << c.m_size);
return compute_shift(table(), index);
}
bool cut::operator==(cut const& other) const {
return table() == other.table() && dom_eq(other);
}
unsigned cut::hash() const {
return get_composite_hash(*this, m_size,
[](cut const& c) { return (unsigned)c.table(); },
[](cut const& c, unsigned i) { return c[i]; });
}
unsigned cut::dom_hash() const {
return get_composite_hash(*this, m_size,
[](cut const& c) { return 3; },
[](cut const& c, unsigned i) { return c[i]; });
}
bool cut::dom_eq(cut const& other) const {
if (m_size != other.m_size) return false;
for (unsigned i = 0; i < m_size; ++i) {
if ((*this)[i] != other[i]) return false;
}
return true;
}
/**
* \brief create the masks
* i = 0: 101010101010101
* i = 1: 1100110011001100
* i = 2: 1111000011110000
* i = 3: 111111110000000011111111
*/
uint64_t cut::effect_mask(unsigned i) {
SASSERT(i <= 6);
uint64_t m = 0;
if (i == 6) {
m = ~((uint64_t)0);
}
else {
m = (1ull << (1u << i)) - 1; // i = 0: m = 1
unsigned w = 1u << (i + 1); // i = 0: w = 2
while (w < 64) {
m |= (m << w); // i = 0: m = 1 + 4
w *= 2;
}
}
return m;
}
/**
remove element from cut as it is deemed a don't care
*/
void cut::remove_elem(unsigned i) {
for (unsigned j = i + 1; j < m_size; ++j) {
m_elems[j-1] = m_elems[j];
}
--m_size;
uint64_t m = effect_mask(i);
uint64_t t = 0;
for (unsigned j = 0, offset = 0; j < 64; ++j) {
if (0 != (m & (1ull << j))) {
t |= ((m_table >> j) & 1u) << offset;
++offset;
}
}
m_table = t;
m_dont_care = 0;
unsigned f = 0;
for (unsigned e : *this) {
f |= (1u << (e & 0x1F));
}
m_filter = f;
}
/**
sat-sweep evaluation. Given 64 bits worth of possible values per variable,
find possible values for function table encoded by cut.
*/
cut_val cut::eval(cut_eval const& env) const {
cut_val v;
uint64_t t = table();
uint64_t n = 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]].m_t >> i) & 0x1) << j);
}
v.m_t |= ((t >> offset) & 0x1) << i;
v.m_f |= ((n >> offset) & 0x1) << i;
}
return v;
}
std::ostream& cut::display(std::ostream& out) const {
out << "{";
for (unsigned i = 0; i < m_size; ++i) {
out << (*this)[i];
if (i + 1 < m_size) out << " ";
}
out << "} ";
display_table(out, m_size, table());
return out;
}
std::ostream& cut::display_table(std::ostream& out, unsigned num_input, uint64_t table) {
for (unsigned i = 0; i < (1u << num_input); ++i) {
if (0 != (table & (1ull << i))) out << "1"; else out << "0";
}
return out;
}
std::string cut::table2string(unsigned num_input, uint64_t table) {
std::ostringstream strm;
display_table(strm, num_input, table);
return std::move(strm).str();
}
}

201
src/sat/sat_cutset.h
View file

@ -1,201 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cutset.cpp
Author:
Nikolaj Bjorner 2020-01-02
--*/
#pragma once
#include "util/region.h"
#include "util/debug.h"
#include "util/util.h"
#include "util/lbool.h"
#include "util/vector.h"
#include <algorithm>
#include <cstring>
#include <functional>
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 {
unsigned m_filter;
unsigned m_size;
unsigned m_elems[5];
uint64_t m_table;
mutable uint64_t m_dont_care;
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) {
m_elems[0] = m_elems[1] = m_elems[2] = m_elems[3] = m_elems[4] = 0;
}
cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2), m_dont_care(0) {
m_elems[0] = id;
m_elems[1] = m_elems[2] = m_elems[3] = m_elems[4] = 0;
}
cut_val eval(cut_eval const& env) const;
unsigned size() const { return m_size; }
unsigned filter() const { return m_filter; }
static unsigned max_cut_size() { return 5; }
unsigned const* begin() const { return m_elems; }
unsigned const* end() const { return m_elems + m_size; }
bool add(unsigned i) {
if (m_size >= max_cut_size()) {
return false;
}
else {
m_elems[m_size++] = i;
m_filter |= (1u << (i & 0x1F));
return true;
}
}
void negate() { set_table(~m_table); }
void set_table(uint64_t t) { m_table = t & table_mask(); }
uint64_t table() const { return (m_table | m_dont_care) & table_mask(); }
uint64_t ntable() const { return (~m_table | m_dont_care) & table_mask(); }
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); }
unsigned hash() const;
unsigned dom_hash() const;
bool dom_eq(cut const& other) const;
struct eq_proc {
bool operator()(cut const& a, cut const& b) const { return a == b; }
bool operator()(cut const* a, cut const* b) const { return *a == *b; }
};
struct hash_proc {
unsigned operator()(cut const& a) const { return a.hash(); }
unsigned operator()(cut const* a) const { return a->hash(); }
};
struct dom_eq_proc {
bool operator()(cut const& a, cut const& b) const { return a.dom_eq(b); }
bool operator()(cut const* a, cut const* b) const { return a->dom_eq(*b); }
};
struct dom_hash_proc {
unsigned operator()(cut const& a) const { return a.dom_hash(); }
unsigned operator()(cut const* a) const { return a->dom_hash(); }
};
unsigned operator[](unsigned idx) const {
return (idx >= m_size) ? UINT_MAX : m_elems[idx];
}
uint64_t shift_table(cut const& other) const;
bool merge(cut const& a, cut const& b) {
unsigned i = 0, j = 0;
unsigned x = a[i];
unsigned y = b[j];
while (x != UINT_MAX || y != UINT_MAX) {
if (!add(std::min(x, y))) {
return false;
}
if (x < y) {
x = a[++i];
}
else if (y < x) {
y = b[++j];
}
else {
x = a[++i];
y = b[++j];
}
}
return true;
}
bool subset_of(cut const& other) const {
if (other.m_filter != (m_filter | other.m_filter)) {
return false;
}
unsigned i = 0;
unsigned other_id = other[i];
for (unsigned id : *this) {
while (id > other_id) {
other_id = other[++i];
}
if (id != other_id) return false;
other_id = other[++i];
}
return true;
}
void remove_elem(unsigned i);
static uint64_t effect_mask(unsigned i);
std::ostream& display(std::ostream& out) const;
static std::ostream& display_table(std::ostream& out, unsigned num_input, uint64_t table);
static std::string table2string(unsigned num_input, uint64_t table);
};
class cut_set {
unsigned m_var;
region* m_region;
unsigned m_size;
unsigned m_max_size;
cut * m_cuts;
public:
typedef std::function<void(unsigned v, cut const& c)> on_update_t;
cut_set(): m_var(UINT_MAX), m_region(nullptr), m_size(0), m_max_size(0), m_cuts(nullptr) {}
void init(region& r, unsigned max_sz, unsigned v);
bool insert(on_update_t& on_add, on_update_t& on_del, cut const& c);
bool no_duplicates() const;
unsigned var() const { return m_var; }
unsigned size() const { return m_size; }
cut const * begin() const { return m_cuts; }
cut const * end() const { return m_cuts + m_size; }
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) const { return m_cuts[idx]; }
void shrink(on_update_t& on_del, unsigned j);
void swap(cut_set& other) noexcept {
std::swap(m_var, other.m_var);
std::swap(m_size, other.m_size);
std::swap(m_max_size, other.m_max_size);
std::swap(m_cuts, other.m_cuts);
}
void evict(on_update_t& on_del, unsigned idx);
void evict(on_update_t& on_del, cut const& c);
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, cut const& c) { return c.display(out); }
inline std::ostream& operator<<(std::ostream& out, cut_set const& cs) { return cs.display(out); }
}

939
src/sat/sat_cutset_compute_shift.h
View file

@ -1,939 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cutset_compute_shift.h
Author:
Nikolaj Bjorner 2020-01-02
Notes:
shifts truth table x using 'code'.
code encodes a mapping from bit-positions of the
input truth table encoded with x into bit-positions
in the output truth table.
The truth table covers up to 6 inputs, which fits in 64 bits.
--*/
#pragma once
static uint64_t compute_shift(uint64_t x, unsigned code) {
switch (code) {
#define _x0 (x & 1ull)
#define _x1 _x0
case 1: return _x1;
#define _x2 (_x1 | (_x1 << 1ull))
case 2: return _x2;
#define _x3 (x & 3ull)
#define _x4 _x3
case 3: return _x4;
#define _x5 (_x2 | (_x2 << 2ull))
case 4: return _x5;
#define _x6 (_x4 | (_x4 << 2ull))
case 5: return _x6;
#define _x7 (x & 2ull)
#define _x8 (_x7 << 1ull)
#define _x9 (_x8 | (_x8 << 1ull))
#define _x10 (_x2 | _x9)
case 6: return _x10;
#define _x11 (x & 15ull)
#define _x12 _x11
case 7: return _x12;
#define _x13 (_x5 | (_x5 << 4ull))
case 8: return _x13;
#define _x14 (_x6 | (_x6 << 4ull))
case 9: return _x14;
#define _x15 (_x10 | (_x10 << 4ull))
case 10: return _x15;
#define _x16 (_x12 | (_x12 << 4ull))
case 11: return _x16;
#define _x17 (_x7 << 3ull)
#define _x18 (_x17 | (_x17 << 1ull))
#define _x19 (_x18 | (_x18 << 2ull))
#define _x20 (_x5 | _x19)
case 12: return _x20;
#define _x21 (x & 12ull)
#define _x22 (_x21 << 2ull)
#define _x23 (_x22 | (_x22 << 2ull))
#define _x24 (_x6 | _x23)
case 13: return _x24;
#define _x25 (x & 4ull)
#define _x26 (_x25 << 2ull)
#define _x27 (_x26 | (_x26 << 1ull))
#define _x28 (x & 8ull)
#define _x29 (_x28 << 3ull)
#define _x30 (_x29 | (_x29 << 1ull))
#define _x31 (_x27 | _x30)
#define _x32 (_x10 | _x31)
case 14: return _x32;
#define _x33 (x & 255ull)
#define _x34 _x33
case 15: return _x34;
#define _x35 (_x13 | (_x13 << 8ull))
case 16: return _x35;
#define _x36 (_x14 | (_x14 << 8ull))
case 17: return _x36;
#define _x37 (_x15 | (_x15 << 8ull))
case 18: return _x37;
#define _x38 (_x16 | (_x16 << 8ull))
case 19: return _x38;
#define _x39 (_x20 | (_x20 << 8ull))
case 20: return _x39;
#define _x40 (_x24 | (_x24 << 8ull))
case 21: return _x40;
#define _x41 (_x32 | (_x32 << 8ull))
case 22: return _x41;
#define _x42 (_x34 | (_x34 << 8ull))
case 23: return _x42;
#define _x43 (_x7 << 7ull)
#define _x44 (_x43 | (_x43 << 1ull))
#define _x45 (_x44 | (_x44 << 2ull))
#define _x46 (_x45 | (_x45 << 4ull))
#define _x47 (_x13 | _x46)
case 24: return _x47;
#define _x48 (_x21 << 6ull)
#define _x49 (_x48 | (_x48 << 2ull))
#define _x50 (_x49 | (_x49 << 4ull))
#define _x51 (_x14 | _x50)
case 25: return _x51;
#define _x52 (_x25 << 6ull)
#define _x53 (_x52 | (_x52 << 1ull))
#define _x54 (_x28 << 7ull)
#define _x55 (_x54 | (_x54 << 1ull))
#define _x56 (_x53 | _x55)
#define _x57 (_x56 | (_x56 << 4ull))
#define _x58 (_x15 | _x57)
case 26: return _x58;
#define _x59 (x & 240ull)
#define _x60 (_x59 << 4ull)
#define _x61 (_x60 | (_x60 << 4ull))
#define _x62 (_x16 | _x61)
case 27: return _x62;
#define _x63 (_x53 | (_x53 << 2ull))
#define _x64 (_x28 << 9ull)
#define _x65 (_x64 | (_x64 << 1ull))
#define _x66 (_x65 | (_x65 << 2ull))
#define _x67 (_x63 | _x66)
#define _x68 (_x20 | _x67)
case 28: return _x68;
#define _x69 (x & 48ull)
#define _x70 (_x69 << 4ull)
#define _x71 (_x70 | (_x70 << 2ull))
#define _x72 (x & 192ull)
#define _x73 (_x72 << 6ull)
#define _x74 (_x73 | (_x73 << 2ull))
#define _x75 (_x71 | _x74)
#define _x76 (_x24 | _x75)
case 29: return _x76;
#define _x77 (x & 16ull)
#define _x78 (_x77 << 4ull)
#define _x79 (_x78 | (_x78 << 1ull))
#define _x80 (x & 32ull)
#define _x81 (_x80 << 5ull)
#define _x82 (_x81 | (_x81 << 1ull))
#define _x83 (_x79 | _x82)
#define _x84 (x & 64ull)
#define _x85 (_x84 << 6ull)
#define _x86 (_x85 | (_x85 << 1ull))
#define _x87 (x & 128ull)
#define _x88 (_x87 << 7ull)
#define _x89 (_x88 | (_x88 << 1ull))
#define _x90 (_x86 | _x89)
#define _x91 (_x83 | _x90)
#define _x92 (_x32 | _x91)
case 30: return _x92;
#define _x93 (x & 65535ull)
#define _x94 _x93
case 31: return _x94;
#define _x95 (_x35 | (_x35 << 16ull))
case 32: return _x95;
#define _x96 (_x36 | (_x36 << 16ull))
case 33: return _x96;
#define _x97 (_x37 | (_x37 << 16ull))
case 34: return _x97;
#define _x98 (_x38 | (_x38 << 16ull))
case 35: return _x98;
#define _x99 (_x39 | (_x39 << 16ull))
case 36: return _x99;
#define _x100 (_x40 | (_x40 << 16ull))
case 37: return _x100;
#define _x101 (_x41 | (_x41 << 16ull))
case 38: return _x101;
#define _x102 (_x42 | (_x42 << 16ull))
case 39: return _x102;
#define _x103 (_x47 | (_x47 << 16ull))
case 40: return _x103;
#define _x104 (_x51 | (_x51 << 16ull))
case 41: return _x104;
#define _x105 (_x58 | (_x58 << 16ull))
case 42: return _x105;
#define _x106 (_x62 | (_x62 << 16ull))
case 43: return _x106;
#define _x107 (_x68 | (_x68 << 16ull))
case 44: return _x107;
#define _x108 (_x76 | (_x76 << 16ull))
case 45: return _x108;
#define _x109 (_x92 | (_x92 << 16ull))
case 46: return _x109;
#define _x110 (_x94 | (_x94 << 16ull))
case 47: return _x110;
#define _x111 (_x7 << 15ull)
#define _x112 (_x111 | (_x111 << 1ull))
#define _x113 (_x112 | (_x112 << 2ull))
#define _x114 (_x113 | (_x113 << 4ull))
#define _x115 (_x114 | (_x114 << 8ull))
#define _x116 (_x35 | _x115)
case 48: return _x116;
#define _x117 (_x21 << 14ull)
#define _x118 (_x117 | (_x117 << 2ull))
#define _x119 (_x118 | (_x118 << 4ull))
#define _x120 (_x119 | (_x119 << 8ull))
#define _x121 (_x36 | _x120)
case 49: return _x121;
#define _x122 (_x25 << 14ull)
#define _x123 (_x122 | (_x122 << 1ull))
#define _x124 (_x28 << 15ull)
#define _x125 (_x124 | (_x124 << 1ull))
#define _x126 (_x123 | _x125)
#define _x127 (_x126 | (_x126 << 4ull))
#define _x128 (_x127 | (_x127 << 8ull))
#define _x129 (_x37 | _x128)
case 50: return _x129;
#define _x130 (_x59 << 12ull)
#define _x131 (_x130 | (_x130 << 4ull))
#define _x132 (_x131 | (_x131 << 8ull))
#define _x133 (_x38 | _x132)
case 51: return _x133;
#define _x134 (_x123 | (_x123 << 2ull))
#define _x135 (_x28 << 17ull)
#define _x136 (_x135 | (_x135 << 1ull))
#define _x137 (_x136 | (_x136 << 2ull))
#define _x138 (_x134 | _x137)
#define _x139 (_x138 | (_x138 << 8ull))
#define _x140 (_x39 | _x139)
case 52: return _x140;
#define _x141 (_x69 << 12ull)
#define _x142 (_x141 | (_x141 << 2ull))
#define _x143 (_x72 << 14ull)
#define _x144 (_x143 | (_x143 << 2ull))
#define _x145 (_x142 | _x144)
#define _x146 (_x145 | (_x145 << 8ull))
#define _x147 (_x40 | _x146)
case 53: return _x147;
#define _x148 (_x77 << 12ull)
#define _x149 (_x148 | (_x148 << 1ull))
#define _x150 (_x80 << 13ull)
#define _x151 (_x150 | (_x150 << 1ull))
#define _x152 (_x149 | _x151)
#define _x153 (_x84 << 14ull)
#define _x154 (_x153 | (_x153 << 1ull))
#define _x155 (_x87 << 15ull)
#define _x156 (_x155 | (_x155 << 1ull))
#define _x157 (_x154 | _x156)
#define _x158 (_x152 | _x157)
#define _x159 (_x158 | (_x158 << 8ull))
#define _x160 (_x41 | _x159)
case 54: return _x160;
#define _x161 (x & 65280ull)
#define _x162 (_x161 << 8ull)
#define _x163 (_x162 | (_x162 << 8ull))
#define _x164 (_x42 | _x163)
case 55: return _x164;
#define _x165 (_x134 | (_x134 << 4ull))
#define _x166 (_x28 << 21ull)
#define _x167 (_x166 | (_x166 << 1ull))
#define _x168 (_x167 | (_x167 << 2ull))
#define _x169 (_x168 | (_x168 << 4ull))
#define _x170 (_x165 | _x169)
#define _x171 (_x47 | _x170)
case 56: return _x171;
#define _x172 (_x142 | (_x142 << 4ull))
#define _x173 (_x72 << 18ull)
#define _x174 (_x173 | (_x173 << 2ull))
#define _x175 (_x174 | (_x174 << 4ull))
#define _x176 (_x172 | _x175)
#define _x177 (_x51 | _x176)
case 57: return _x177;
#define _x178 (_x152 | (_x152 << 4ull))
#define _x179 (_x84 << 18ull)
#define _x180 (_x179 | (_x179 << 1ull))
#define _x181 (_x87 << 19ull)
#define _x182 (_x181 | (_x181 << 1ull))
#define _x183 (_x180 | _x182)
#define _x184 (_x183 | (_x183 << 4ull))
#define _x185 (_x178 | _x184)
#define _x186 (_x58 | _x185)
case 58: return _x186;
#define _x187 (x & 3840ull)
#define _x188 (_x187 << 8ull)
#define _x189 (_x188 | (_x188 << 4ull))
#define _x190 (x & 61440ull)
#define _x191 (_x190 << 12ull)
#define _x192 (_x191 | (_x191 << 4ull))
#define _x193 (_x189 | _x192)
#define _x194 (_x62 | _x193)
case 59: return _x194;
#define _x195 (_x149 | (_x149 << 2ull))
#define _x196 (_x80 << 15ull)
#define _x197 (_x196 | (_x196 << 1ull))
#define _x198 (_x197 | (_x197 << 2ull))
#define _x199 (_x195 | _x198)
#define _x200 (_x180 | (_x180 << 2ull))
#define _x201 (_x87 << 21ull)
#define _x202 (_x201 | (_x201 << 1ull))
#define _x203 (_x202 | (_x202 << 2ull))
#define _x204 (_x200 | _x203)
#define _x205 (_x199 | _x204)
#define _x206 (_x68 | _x205)
case 60: return _x206;
#define _x207 (x & 768ull)
#define _x208 (_x207 << 8ull)
#define _x209 (_x208 | (_x208 << 2ull))
#define _x210 (x & 3072ull)
#define _x211 (_x210 << 10ull)
#define _x212 (_x211 | (_x211 << 2ull))
#define _x213 (_x209 | _x212)
#define _x214 (x & 12288ull)
#define _x215 (_x214 << 12ull)
#define _x216 (_x215 | (_x215 << 2ull))
#define _x217 (x & 49152ull)
#define _x218 (_x217 << 14ull)
#define _x219 (_x218 | (_x218 << 2ull))
#define _x220 (_x216 | _x219)
#define _x221 (_x213 | _x220)
#define _x222 (_x76 | _x221)
case 61: return _x222;
#define _x223 (x & 256ull)
#define _x224 (_x223 << 8ull)
#define _x225 (_x224 | (_x224 << 1ull))
#define _x226 (x & 512ull)
#define _x227 (_x226 << 9ull)
#define _x228 (_x227 | (_x227 << 1ull))
#define _x229 (_x225 | _x228)
#define _x230 (x & 1024ull)
#define _x231 (_x230 << 10ull)
#define _x232 (_x231 | (_x231 << 1ull))
#define _x233 (x & 2048ull)
#define _x234 (_x233 << 11ull)
#define _x235 (_x234 | (_x234 << 1ull))
#define _x236 (_x232 | _x235)
#define _x237 (_x229 | _x236)
#define _x238 (x & 4096ull)
#define _x239 (_x238 << 12ull)
#define _x240 (_x239 | (_x239 << 1ull))
#define _x241 (x & 8192ull)
#define _x242 (_x241 << 13ull)
#define _x243 (_x242 | (_x242 << 1ull))
#define _x244 (_x240 | _x243)
#define _x245 (x & 16384ull)
#define _x246 (_x245 << 14ull)
#define _x247 (_x246 | (_x246 << 1ull))
#define _x248 (x & 32768ull)
#define _x249 (_x248 << 15ull)
#define _x250 (_x249 | (_x249 << 1ull))
#define _x251 (_x247 | _x250)
#define _x252 (_x244 | _x251)
#define _x253 (_x237 | _x252)
#define _x254 (_x92 | _x253)
case 62: return _x254;
#define _x255 (x & 4294967295ull)
#define _x256 _x255
case 63: return _x256;
#define _x257 (_x95 | (_x95 << 32ull))
case 64: return _x257;
#define _x258 (_x96 | (_x96 << 32ull))
case 65: return _x258;
#define _x259 (_x97 | (_x97 << 32ull))
case 66: return _x259;
#define _x260 (_x98 | (_x98 << 32ull))
case 67: return _x260;
#define _x261 (_x99 | (_x99 << 32ull))
case 68: return _x261;
#define _x262 (_x100 | (_x100 << 32ull))
case 69: return _x262;
#define _x263 (_x101 | (_x101 << 32ull))
case 70: return _x263;
#define _x264 (_x102 | (_x102 << 32ull))
case 71: return _x264;
#define _x265 (_x103 | (_x103 << 32ull))
case 72: return _x265;
#define _x266 (_x104 | (_x104 << 32ull))
case 73: return _x266;
#define _x267 (_x105 | (_x105 << 32ull))
case 74: return _x267;
#define _x268 (_x106 | (_x106 << 32ull))
case 75: return _x268;
#define _x269 (_x107 | (_x107 << 32ull))
case 76: return _x269;
#define _x270 (_x108 | (_x108 << 32ull))
case 77: return _x270;
#define _x271 (_x109 | (_x109 << 32ull))
case 78: return _x271;
#define _x272 (_x110 | (_x110 << 32ull))
case 79: return _x272;
#define _x273 (_x116 | (_x116 << 32ull))
case 80: return _x273;
#define _x274 (_x121 | (_x121 << 32ull))
case 81: return _x274;
#define _x275 (_x129 | (_x129 << 32ull))
case 82: return _x275;
#define _x276 (_x133 | (_x133 << 32ull))
case 83: return _x276;
#define _x277 (_x140 | (_x140 << 32ull))
case 84: return _x277;
#define _x278 (_x147 | (_x147 << 32ull))
case 85: return _x278;
#define _x279 (_x160 | (_x160 << 32ull))
case 86: return _x279;
#define _x280 (_x164 | (_x164 << 32ull))
case 87: return _x280;
#define _x281 (_x171 | (_x171 << 32ull))
case 88: return _x281;
#define _x282 (_x177 | (_x177 << 32ull))
case 89: return _x282;
#define _x283 (_x186 | (_x186 << 32ull))
case 90: return _x283;
#define _x284 (_x194 | (_x194 << 32ull))
case 91: return _x284;
#define _x285 (_x206 | (_x206 << 32ull))
case 92: return _x285;
#define _x286 (_x222 | (_x222 << 32ull))
case 93: return _x286;
#define _x287 (_x254 | (_x254 << 32ull))
case 94: return _x287;
#define _x288 (_x256 | (_x256 << 32ull))
case 95: return _x288;
#define _x289 (_x7 << 31ull)
#define _x290 (_x289 | (_x289 << 1ull))
#define _x291 (_x290 | (_x290 << 2ull))
#define _x292 (_x291 | (_x291 << 4ull))
#define _x293 (_x292 | (_x292 << 8ull))
#define _x294 (_x293 | (_x293 << 16ull))
#define _x295 (_x95 | _x294)
case 96: return _x295;
#define _x296 (_x21 << 30ull)
#define _x297 (_x296 | (_x296 << 2ull))
#define _x298 (_x297 | (_x297 << 4ull))
#define _x299 (_x298 | (_x298 << 8ull))
#define _x300 (_x299 | (_x299 << 16ull))
#define _x301 (_x96 | _x300)
case 97: return _x301;
#define _x302 (_x25 << 30ull)
#define _x303 (_x302 | (_x302 << 1ull))
#define _x304 (_x28 << 31ull)
#define _x305 (_x304 | (_x304 << 1ull))
#define _x306 (_x303 | _x305)
#define _x307 (_x306 | (_x306 << 4ull))
#define _x308 (_x307 | (_x307 << 8ull))
#define _x309 (_x308 | (_x308 << 16ull))
#define _x310 (_x97 | _x309)
case 98: return _x310;
#define _x311 (_x59 << 28ull)
#define _x312 (_x311 | (_x311 << 4ull))
#define _x313 (_x312 | (_x312 << 8ull))
#define _x314 (_x313 | (_x313 << 16ull))
#define _x315 (_x98 | _x314)
case 99: return _x315;
#define _x316 (_x303 | (_x303 << 2ull))
#define _x317 (_x28 << 33ull)
#define _x318 (_x317 | (_x317 << 1ull))
#define _x319 (_x318 | (_x318 << 2ull))
#define _x320 (_x316 | _x319)
#define _x321 (_x320 | (_x320 << 8ull))
#define _x322 (_x321 | (_x321 << 16ull))
#define _x323 (_x99 | _x322)
case 100: return _x323;
#define _x324 (_x69 << 28ull)
#define _x325 (_x324 | (_x324 << 2ull))
#define _x326 (_x72 << 30ull)
#define _x327 (_x326 | (_x326 << 2ull))
#define _x328 (_x325 | _x327)
#define _x329 (_x328 | (_x328 << 8ull))
#define _x330 (_x329 | (_x329 << 16ull))
#define _x331 (_x100 | _x330)
case 101: return _x331;
#define _x332 (_x77 << 28ull)
#define _x333 (_x332 | (_x332 << 1ull))
#define _x334 (_x80 << 29ull)
#define _x335 (_x334 | (_x334 << 1ull))
#define _x336 (_x333 | _x335)
#define _x337 (_x84 << 30ull)
#define _x338 (_x337 | (_x337 << 1ull))
#define _x339 (_x87 << 31ull)
#define _x340 (_x339 | (_x339 << 1ull))
#define _x341 (_x338 | _x340)
#define _x342 (_x336 | _x341)
#define _x343 (_x342 | (_x342 << 8ull))
#define _x344 (_x343 | (_x343 << 16ull))
#define _x345 (_x101 | _x344)
case 102: return _x345;
#define _x346 (_x161 << 24ull)
#define _x347 (_x346 | (_x346 << 8ull))
#define _x348 (_x347 | (_x347 << 16ull))
#define _x349 (_x102 | _x348)
case 103: return _x349;
#define _x350 (_x316 | (_x316 << 4ull))
#define _x351 (_x28 << 37ull)
#define _x352 (_x351 | (_x351 << 1ull))
#define _x353 (_x352 | (_x352 << 2ull))
#define _x354 (_x353 | (_x353 << 4ull))
#define _x355 (_x350 | _x354)
#define _x356 (_x355 | (_x355 << 16ull))
#define _x357 (_x103 | _x356)
case 104: return _x357;
#define _x358 (_x325 | (_x325 << 4ull))
#define _x359 (_x72 << 34ull)
#define _x360 (_x359 | (_x359 << 2ull))
#define _x361 (_x360 | (_x360 << 4ull))
#define _x362 (_x358 | _x361)
#define _x363 (_x362 | (_x362 << 16ull))
#define _x364 (_x104 | _x363)
case 105: return _x364;
#define _x365 (_x336 | (_x336 << 4ull))
#define _x366 (_x84 << 34ull)
#define _x367 (_x366 | (_x366 << 1ull))
#define _x368 (_x87 << 35ull)
#define _x369 (_x368 | (_x368 << 1ull))
#define _x370 (_x367 | _x369)
#define _x371 (_x370 | (_x370 << 4ull))
#define _x372 (_x365 | _x371)
#define _x373 (_x372 | (_x372 << 16ull))
#define _x374 (_x105 | _x373)
case 106: return _x374;
#define _x375 (_x187 << 24ull)
#define _x376 (_x375 | (_x375 << 4ull))
#define _x377 (_x190 << 28ull)
#define _x378 (_x377 | (_x377 << 4ull))
#define _x379 (_x376 | _x378)
#define _x380 (_x379 | (_x379 << 16ull))
#define _x381 (_x106 | _x380)
case 107: return _x381;
#define _x382 (_x333 | (_x333 << 2ull))
#define _x383 (_x80 << 31ull)
#define _x384 (_x383 | (_x383 << 1ull))
#define _x385 (_x384 | (_x384 << 2ull))
#define _x386 (_x382 | _x385)
#define _x387 (_x367 | (_x367 << 2ull))
#define _x388 (_x87 << 37ull)
#define _x389 (_x388 | (_x388 << 1ull))
#define _x390 (_x389 | (_x389 << 2ull))
#define _x391 (_x387 | _x390)
#define _x392 (_x386 | _x391)
#define _x393 (_x392 | (_x392 << 16ull))
#define _x394 (_x107 | _x393)
case 108: return _x394;
#define _x395 (_x207 << 24ull)
#define _x396 (_x395 | (_x395 << 2ull))
#define _x397 (_x210 << 26ull)
#define _x398 (_x397 | (_x397 << 2ull))
#define _x399 (_x396 | _x398)
#define _x400 (_x214 << 28ull)
#define _x401 (_x400 | (_x400 << 2ull))
#define _x402 (_x217 << 30ull)
#define _x403 (_x402 | (_x402 << 2ull))
#define _x404 (_x401 | _x403)
#define _x405 (_x399 | _x404)
#define _x406 (_x405 | (_x405 << 16ull))
#define _x407 (_x108 | _x406)
case 109: return _x407;
#define _x408 (_x223 << 24ull)
#define _x409 (_x408 | (_x408 << 1ull))
#define _x410 (_x226 << 25ull)
#define _x411 (_x410 | (_x410 << 1ull))
#define _x412 (_x409 | _x411)
#define _x413 (_x230 << 26ull)
#define _x414 (_x413 | (_x413 << 1ull))
#define _x415 (_x233 << 27ull)
#define _x416 (_x415 | (_x415 << 1ull))
#define _x417 (_x414 | _x416)
#define _x418 (_x412 | _x417)
#define _x419 (_x238 << 28ull)
#define _x420 (_x419 | (_x419 << 1ull))
#define _x421 (_x241 << 29ull)
#define _x422 (_x421 | (_x421 << 1ull))
#define _x423 (_x420 | _x422)
#define _x424 (_x245 << 30ull)
#define _x425 (_x424 | (_x424 << 1ull))
#define _x426 (_x248 << 31ull)
#define _x427 (_x426 | (_x426 << 1ull))
#define _x428 (_x425 | _x427)
#define _x429 (_x423 | _x428)
#define _x430 (_x418 | _x429)
#define _x431 (_x430 | (_x430 << 16ull))
#define _x432 (_x109 | _x431)
case 110: return _x432;
#define _x433 (x & 4294901760ull)
#define _x434 (_x433 << 16ull)
#define _x435 (_x434 | (_x434 << 16ull))
#define _x436 (_x110 | _x435)
case 111: return _x436;
#define _x437 (_x350 | (_x350 << 8ull))
#define _x438 (_x28 << 45ull)
#define _x439 (_x438 | (_x438 << 1ull))
#define _x440 (_x439 | (_x439 << 2ull))
#define _x441 (_x440 | (_x440 << 4ull))
#define _x442 (_x441 | (_x441 << 8ull))
#define _x443 (_x437 | _x442)
#define _x444 (_x116 | _x443)
case 112: return _x444;
#define _x445 (_x358 | (_x358 << 8ull))
#define _x446 (_x72 << 42ull)
#define _x447 (_x446 | (_x446 << 2ull))
#define _x448 (_x447 | (_x447 << 4ull))
#define _x449 (_x448 | (_x448 << 8ull))
#define _x450 (_x445 | _x449)
#define _x451 (_x121 | _x450)
case 113: return _x451;
#define _x452 (_x365 | (_x365 << 8ull))
#define _x453 (_x84 << 42ull)
#define _x454 (_x453 | (_x453 << 1ull))
#define _x455 (_x87 << 43ull)
#define _x456 (_x455 | (_x455 << 1ull))
#define _x457 (_x454 | _x456)
#define _x458 (_x457 | (_x457 << 4ull))
#define _x459 (_x458 | (_x458 << 8ull))
#define _x460 (_x452 | _x459)
#define _x461 (_x129 | _x460)
case 114: return _x461;
#define _x462 (_x376 | (_x376 << 8ull))
#define _x463 (_x190 << 36ull)
#define _x464 (_x463 | (_x463 << 4ull))
#define _x465 (_x464 | (_x464 << 8ull))
#define _x466 (_x462 | _x465)
#define _x467 (_x133 | _x466)
case 115: return _x467;
#define _x468 (_x386 | (_x386 << 8ull))
#define _x469 (_x454 | (_x454 << 2ull))
#define _x470 (_x87 << 45ull)
#define _x471 (_x470 | (_x470 << 1ull))
#define _x472 (_x471 | (_x471 << 2ull))
#define _x473 (_x469 | _x472)
#define _x474 (_x473 | (_x473 << 8ull))
#define _x475 (_x468 | _x474)
#define _x476 (_x140 | _x475)
case 116: return _x476;
#define _x477 (_x399 | (_x399 << 8ull))
#define _x478 (_x214 << 36ull)
#define _x479 (_x478 | (_x478 << 2ull))
#define _x480 (_x217 << 38ull)
#define _x481 (_x480 | (_x480 << 2ull))
#define _x482 (_x479 | _x481)
#define _x483 (_x482 | (_x482 << 8ull))
#define _x484 (_x477 | _x483)
#define _x485 (_x147 | _x484)
case 117: return _x485;
#define _x486 (_x418 | (_x418 << 8ull))
#define _x487 (_x238 << 36ull)
#define _x488 (_x487 | (_x487 << 1ull))
#define _x489 (_x241 << 37ull)
#define _x490 (_x489 | (_x489 << 1ull))
#define _x491 (_x488 | _x490)
#define _x492 (_x245 << 38ull)
#define _x493 (_x492 | (_x492 << 1ull))
#define _x494 (_x248 << 39ull)
#define _x495 (_x494 | (_x494 << 1ull))
#define _x496 (_x493 | _x495)
#define _x497 (_x491 | _x496)
#define _x498 (_x497 | (_x497 << 8ull))
#define _x499 (_x486 | _x498)
#define _x500 (_x160 | _x499)
case 118: return _x500;
#define _x501 (x & 16711680ull)
#define _x502 (_x501 << 16ull)
#define _x503 (_x502 | (_x502 << 8ull))
#define _x504 (x & 4278190080ull)
#define _x505 (_x504 << 24ull)
#define _x506 (_x505 | (_x505 << 8ull))
#define _x507 (_x503 | _x506)
#define _x508 (_x164 | _x507)
case 119: return _x508;
#define _x509 (_x382 | (_x382 << 4ull))
#define _x510 (_x80 << 35ull)
#define _x511 (_x510 | (_x510 << 1ull))
#define _x512 (_x511 | (_x511 << 2ull))
#define _x513 (_x512 | (_x512 << 4ull))
#define _x514 (_x509 | _x513)
#define _x515 (_x469 | (_x469 << 4ull))
#define _x516 (_x87 << 49ull)
#define _x517 (_x516 | (_x516 << 1ull))
#define _x518 (_x517 | (_x517 << 2ull))
#define _x519 (_x518 | (_x518 << 4ull))
#define _x520 (_x515 | _x519)
#define _x521 (_x514 | _x520)
#define _x522 (_x171 | _x521)
case 120: return _x522;
#define _x523 (_x396 | (_x396 << 4ull))
#define _x524 (_x210 << 30ull)
#define _x525 (_x524 | (_x524 << 2ull))
#define _x526 (_x525 | (_x525 << 4ull))
#define _x527 (_x523 | _x526)
#define _x528 (_x479 | (_x479 << 4ull))
#define _x529 (_x217 << 42ull)
#define _x530 (_x529 | (_x529 << 2ull))
#define _x531 (_x530 | (_x530 << 4ull))
#define _x532 (_x528 | _x531)
#define _x533 (_x527 | _x532)
#define _x534 (_x177 | _x533)
case 121: return _x534;
#define _x535 (_x412 | (_x412 << 4ull))
#define _x536 (_x230 << 30ull)
#define _x537 (_x536 | (_x536 << 1ull))
#define _x538 (_x233 << 31ull)
#define _x539 (_x538 | (_x538 << 1ull))
#define _x540 (_x537 | _x539)
#define _x541 (_x540 | (_x540 << 4ull))
#define _x542 (_x535 | _x541)
#define _x543 (_x491 | (_x491 << 4ull))
#define _x544 (_x245 << 42ull)
#define _x545 (_x544 | (_x544 << 1ull))
#define _x546 (_x248 << 43ull)
#define _x547 (_x546 | (_x546 << 1ull))
#define _x548 (_x545 | _x547)
#define _x549 (_x548 | (_x548 << 4ull))
#define _x550 (_x543 | _x549)
#define _x551 (_x542 | _x550)
#define _x552 (_x186 | _x551)
case 122: return _x552;
#define _x553 (x & 983040ull)
#define _x554 (_x553 << 16ull)
#define _x555 (_x554 | (_x554 << 4ull))
#define _x556 (x & 15728640ull)
#define _x557 (_x556 << 20ull)
#define _x558 (_x557 | (_x557 << 4ull))
#define _x559 (_x555 | _x558)
#define _x560 (x & 251658240ull)
#define _x561 (_x560 << 24ull)
#define _x562 (_x561 | (_x561 << 4ull))
#define _x563 (x & 4026531840ull)
#define _x564 (_x563 << 28ull)
#define _x565 (_x564 | (_x564 << 4ull))
#define _x566 (_x562 | _x565)
#define _x567 (_x559 | _x566)
#define _x568 (_x194 | _x567)
case 123: return _x568;
#define _x569 (_x409 | (_x409 << 2ull))
#define _x570 (_x226 << 27ull)
#define _x571 (_x570 | (_x570 << 1ull))
#define _x572 (_x571 | (_x571 << 2ull))
#define _x573 (_x569 | _x572)
#define _x574 (_x537 | (_x537 << 2ull))
#define _x575 (_x233 << 33ull)
#define _x576 (_x575 | (_x575 << 1ull))
#define _x577 (_x576 | (_x576 << 2ull))
#define _x578 (_x574 | _x577)
#define _x579 (_x573 | _x578)
#define _x580 (_x488 | (_x488 << 2ull))
#define _x581 (_x241 << 39ull)
#define _x582 (_x581 | (_x581 << 1ull))
#define _x583 (_x582 | (_x582 << 2ull))
#define _x584 (_x580 | _x583)
#define _x585 (_x545 | (_x545 << 2ull))
#define _x586 (_x248 << 45ull)
#define _x587 (_x586 | (_x586 << 1ull))
#define _x588 (_x587 | (_x587 << 2ull))
#define _x589 (_x585 | _x588)
#define _x590 (_x584 | _x589)
#define _x591 (_x579 | _x590)
#define _x592 (_x206 | _x591)
case 124: return _x592;
#define _x593 (x & 196608ull)
#define _x594 (_x593 << 16ull)
#define _x595 (_x594 | (_x594 << 2ull))
#define _x596 (x & 786432ull)
#define _x597 (_x596 << 18ull)
#define _x598 (_x597 | (_x597 << 2ull))
#define _x599 (_x595 | _x598)
#define _x600 (x & 3145728ull)
#define _x601 (_x600 << 20ull)
#define _x602 (_x601 | (_x601 << 2ull))
#define _x603 (x & 12582912ull)
#define _x604 (_x603 << 22ull)
#define _x605 (_x604 | (_x604 << 2ull))
#define _x606 (_x602 | _x605)
#define _x607 (_x599 | _x606)
#define _x608 (x & 50331648ull)
#define _x609 (_x608 << 24ull)
#define _x610 (_x609 | (_x609 << 2ull))
#define _x611 (x & 201326592ull)
#define _x612 (_x611 << 26ull)
#define _x613 (_x612 | (_x612 << 2ull))
#define _x614 (_x610 | _x613)
#define _x615 (x & 805306368ull)
#define _x616 (_x615 << 28ull)
#define _x617 (_x616 | (_x616 << 2ull))
#define _x618 (x & 3221225472ull)
#define _x619 (_x618 << 30ull)
#define _x620 (_x619 | (_x619 << 2ull))
#define _x621 (_x617 | _x620)
#define _x622 (_x614 | _x621)
#define _x623 (_x607 | _x622)
#define _x624 (_x222 | _x623)
case 125: return _x624;
#define _x625 (x & 65536ull)
#define _x626 (_x625 << 16ull)
#define _x627 (_x626 | (_x626 << 1ull))
#define _x628 (x & 131072ull)
#define _x629 (_x628 << 17ull)
#define _x630 (_x629 | (_x629 << 1ull))
#define _x631 (_x627 | _x630)
#define _x632 (x & 262144ull)
#define _x633 (_x632 << 18ull)
#define _x634 (_x633 | (_x633 << 1ull))
#define _x635 (x & 524288ull)
#define _x636 (_x635 << 19ull)
#define _x637 (_x636 | (_x636 << 1ull))
#define _x638 (_x634 | _x637)
#define _x639 (_x631 | _x638)
#define _x640 (x & 1048576ull)
#define _x641 (_x640 << 20ull)
#define _x642 (_x641 | (_x641 << 1ull))
#define _x643 (x & 2097152ull)
#define _x644 (_x643 << 21ull)
#define _x645 (_x644 | (_x644 << 1ull))
#define _x646 (_x642 | _x645)
#define _x647 (x & 4194304ull)
#define _x648 (_x647 << 22ull)
#define _x649 (_x648 | (_x648 << 1ull))
#define _x650 (x & 8388608ull)
#define _x651 (_x650 << 23ull)
#define _x652 (_x651 | (_x651 << 1ull))
#define _x653 (_x649 | _x652)
#define _x654 (_x646 | _x653)
#define _x655 (_x639 | _x654)
#define _x656 (x & 16777216ull)
#define _x657 (_x656 << 24ull)
#define _x658 (_x657 | (_x657 << 1ull))
#define _x659 (x & 33554432ull)
#define _x660 (_x659 << 25ull)
#define _x661 (_x660 | (_x660 << 1ull))
#define _x662 (_x658 | _x661)
#define _x663 (x & 67108864ull)
#define _x664 (_x663 << 26ull)
#define _x665 (_x664 | (_x664 << 1ull))
#define _x666 (x & 134217728ull)
#define _x667 (_x666 << 27ull)
#define _x668 (_x667 | (_x667 << 1ull))
#define _x669 (_x665 | _x668)
#define _x670 (_x662 | _x669)
#define _x671 (x & 268435456ull)
#define _x672 (_x671 << 28ull)
#define _x673 (_x672 | (_x672 << 1ull))
#define _x674 (x & 536870912ull)
#define _x675 (_x674 << 29ull)
#define _x676 (_x675 | (_x675 << 1ull))
#define _x677 (_x673 | _x676)
#define _x678 (x & 1073741824ull)
#define _x679 (_x678 << 30ull)
#define _x680 (_x679 | (_x679 << 1ull))
#define _x681 (x & 2147483648ull)
#define _x682 (_x681 << 31ull)
#define _x683 (_x682 | (_x682 << 1ull))
#define _x684 (_x680 | _x683)
#define _x685 (_x677 | _x684)
#define _x686 (_x670 | _x685)
#define _x687 (_x655 | _x686)
#define _x688 (_x254 | _x687)
case 126: return _x688;
case 127: return x;
default:
UNREACHABLE();
return 0;
}
}
#if 0
def consecutive(S):
for k in range(len(S)-1):
if S[k] + 1 != S[k+1]:
return False
return True
def shift(x, k):
if k == 0:
return x
if k < 0:
return "(%s >> %dull)" % (x,-k)
return "(%s << %dull)" % (x, k)
def hash(r, hashcons):
if r in hashcons:
return hashcons[r]
id = "_x%d" % len(hashcons)
print ("#define %s %s" % (id, r))
hashcons[r] = id
return id
def compile(S, offset, hashcons):
if consecutive(S):
k = S[0]
l = len(S)
if l == 64:
return "x"
mask = ((1 << l)-1) << k
return hash(shift(hash("(x & %dull)" % mask, hashcons), offset - k), hashcons)
l2 = len(S) >> 1
S1 = S[0:l2]
S2 = S[l2:]
if S1 == S2:
r1 = compile(S1, offset, hashcons)
return hash("(%s | (%s << %dull))" % (r1, r1, l2), hashcons)
r1 = compile(S1, offset, hashcons)
r2 = compile(S2, offset + l2, hashcons)
return hash("(%s | %s)" % (r1, r2), hashcons)
def mems2index(mems, bound):
k = 0
i = 0
for m in mems:
if m:
k |= (1 << i)
i += 1
k |= (1 << i)
return k
def precompute(mems, bound, hashcons):
K = 0
j = 0
coeff = {}
deficit = {}
for m in mems:
if m:
coeff[K] = (1 << j)
deficit[K] = j - K
K += 1
j += 1
indices = []
for j in range(1 << len(mems)):
k = 0
for i in range(K):
if 0 != (j & coeff[i]):
k += (1 << i)
indices += [k]
idx = mems2index(mems, bound)
instr = compile(indices, 0, hashcons)
print(" case %d: return %s;" % (idx, instr))
def create_mems(mems, n):
if n == 0:
return ([], mems)
prefix, m1 = create_mems(mems, n - 1)
m2 = [m + [False] for m in m1]
m3 = [m + [True] for m in m1]
return prefix + m1, m2 + m3
def combinations(n, m, hashcons):
prefix, S = create_mems([[]], 6)
mems = prefix + S
for mem in mems:
precompute(mem, m, hashcons)
hashcons = {}
combinations(7, 7, hashcons)
#endif

3
src/sat/sat_drat.h
View file

@ -21,7 +21,8 @@ Notes:
--*/
#pragma once
#include "sat_types.h"
#include "sat/sat_types.h"
#include "sat/sat_clause.h"
namespace sat {
class justification;

3
src/sat/sat_elim_eqs.cpp
View file

@ -229,9 +229,6 @@ namespace sat {
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.m_cut_simplifier)
m_solver.m_cut_simplifier->set_root(v, r);
bool set_root = m_solver.set_root(l, r);
TRACE(elim_eqs, tout << l << " " << r << "\n";);
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !set_root))) {

289
src/sat/sat_lut_finder.cpp
View file

@ -1,289 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_lut_finder.cpp
Abstract:
lut finder
Author:
Nikolaj Bjorner 2020-01-02
Notes:
--*/
#include "sat/sat_lut_finder.h"
#include "sat/sat_solver.h"
namespace sat {
void lut_finder::operator()(clause_vector& clauses) {
m_removed_clauses.reset();
unsigned max_size = m_max_lut_size;
// we better have enough bits in the combination mask to
// handle clauses up to max_size.
// max_size = 5 -> 32 bits
// max_size = 6 -> 64 bits
SASSERT(sizeof(m_combination)*8 >= (1ull << static_cast<uint64_t>(max_size)));
init_clause_filter();
for (unsigned i = 0; i <= 6; ++i) {
m_masks[i] = cut::effect_mask(i);
}
m_var_position.resize(s.num_vars());
for (clause* cp : clauses) {
cp->unmark_used();
}
for (; max_size > 2; --max_size) {
for (clause* cp : clauses) {
clause& c = *cp;
if (c.size() == max_size && !c.was_removed() && !c.is_learned() && !c.was_used()) {
check_lut(c);
}
}
}
m_clause_filters.clear();
for (clause* cp : clauses) cp->unmark_used();
for (clause* cp : m_removed_clauses) cp->mark_used();
std::function<bool(clause*)> not_used = [](clause* cp) { return !cp->was_used(); };
clauses.filter_update(not_used);
}
void lut_finder::check_lut(clause& c) {
SASSERT(c.size() > 2);
unsigned filter = get_clause_filter(c);
s.init_visited();
unsigned mask = 0, i = 0;
m_vars.reset();
m_clause.reset();
for (literal l : c) {
m_clause.push_back(l);
}
// ensure that variables in returned LUT are sorted
std::sort(m_clause.begin(), m_clause.end());
for (literal l : m_clause) {
m_vars.push_back(l.var());
m_var_position[l.var()] = i;
s.mark_visited(l.var());
mask |= (l.sign() << (i++));
}
m_clauses_to_remove.reset();
m_clauses_to_remove.push_back(&c);
m_combination = 0;
m_num_combinations = 0;
set_combination(mask);
c.mark_used();
for (literal l : c) {
for (auto const& cf : m_clause_filters[l.var()]) {
if ((filter == (filter | cf.m_filter)) &&
!cf.m_clause->was_used() &&
extract_lut(*cf.m_clause)) {
add_lut();
return;
}
}
// TBD: replace by BIG
// loop over binary clauses in watch list
for (watched const & w : s.get_wlist(l)) {
if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) {
if (extract_lut(~l, w.get_literal())) {
add_lut();
return;
}
}
}
l.neg();
for (watched const & w : s.get_wlist(l)) {
if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) {
if (extract_lut(~l, w.get_literal())) {
add_lut();
return;
}
}
}
}
}
void lut_finder::add_lut() {
DEBUG_CODE(for (clause* cp : m_clauses_to_remove) VERIFY(cp->was_used()););
m_removed_clauses.append(m_clauses_to_remove);
bool_var v;
uint64_t lut = convert_combination(m_vars, v);
TRACE(aig_simplifier,
for (clause* cp : m_clauses_to_remove) {
tout << *cp << "\n" << v << ": " << m_vars << "\n";
}
display_mask(tout, lut, 1u << m_vars.size()) << "\n";);
m_on_lut(lut, m_vars, v);
}
bool lut_finder::extract_lut(literal l1, literal l2) {
SASSERT(s.m_visited.is_visited(l1.var()));
SASSERT(s.m_visited.is_visited(l2.var()));
m_missing.reset();
unsigned mask = 0;
for (unsigned i = 0; i < m_vars.size(); ++i) {
if (m_vars[i] == l1.var()) {
mask |= (l1.sign() << i);
}
else if (m_vars[i] == l2.var()) {
mask |= (l2.sign() << i);
}
else {
m_missing.push_back(i);
}
}
return update_combinations(mask);
}
bool lut_finder::extract_lut(clause& c2) {
for (literal l : c2) {
if (!s.is_visited(l.var()))
return false;
}
if (c2.size() == m_vars.size()) {
m_clauses_to_remove.push_back(&c2);
c2.mark_used();
}
// insert missing
unsigned mask = 0;
m_missing.reset();
SASSERT(c2.size() <= m_vars.size());
for (unsigned i = 0; i < m_vars.size(); ++i) {
m_clause[i] = null_literal;
}
for (literal l : c2) {
unsigned pos = m_var_position[l.var()];
m_clause[pos] = l;
}
for (unsigned j = 0; j < m_vars.size(); ++j) {
literal lit = m_clause[j];
if (lit == null_literal) {
m_missing.push_back(j);
}
else {
mask |= (m_clause[j].sign() << j);
}
}
return update_combinations(mask);
}
void lut_finder::set_combination(unsigned mask) {
if (!get_combination(mask)) {
m_combination |= (1ull << mask);
m_num_combinations++;
}
}
bool lut_finder::update_combinations(unsigned mask) {
unsigned num_missing = m_missing.size();
for (unsigned k = 0; k < (1ul << num_missing); ++k) {
unsigned mask2 = mask;
for (unsigned i = 0; i < num_missing; ++i) {
if ((k & (1 << i)) != 0) {
mask2 |= 1ul << m_missing[i];
}
}
set_combination(mask2);
}
return lut_is_defined(m_vars.size());
}
bool lut_finder::lut_is_defined(unsigned sz) {
if (m_num_combinations < (1ull << (sz/2)))
return false;
for (unsigned i = sz; i-- > 0; ) {
if (lut_is_defined(i, sz))
return true;
}
return false;
}
/**
* \brief check if all output combinations for variable i are defined.
*/
bool lut_finder::lut_is_defined(unsigned i, unsigned sz) {
uint64_t c = m_combination | (m_combination >> (1ull << (uint64_t)i));
uint64_t m = m_masks[i];
if (sz < 6) m &= ((1ull << (1ull << sz)) - 1);
return (c & m) == m;
}
/**
* find variable where it is defined
* convert bit-mask to truth table for that variable.
* remove variable from vars,
* return truth table.
*/
uint64_t lut_finder::convert_combination(bool_var_vector& vars, bool_var& v) {
SASSERT(lut_is_defined(vars.size()));
unsigned i = 0;
for (i = vars.size(); i-- > 0; ) {
if (lut_is_defined(i, vars.size())) {
break;
}
}
SASSERT(i < vars.size());
v = vars[i];
vars.erase(v);
uint64_t r = 0;
uint64_t m = m_masks[i];
unsigned offset = 0;
// example, if i = 2, then we are examining
// how m_combination evaluates at position xy0uv
// If it evaluates to 0, then it has to evaluate to 1 on position xy1uv
// Offset keeps track of the value of xyuv
//
for (unsigned j = 0; j < 64; ++j) {
if (0 != (m & (1ull << j))) {
if (0 != (m_combination & (1ull << j))) {
r |= 1ull << offset;
}
++offset;
}
}
return r;
}
void lut_finder::init_clause_filter() {
m_clause_filters.reset();
m_clause_filters.resize(s.num_vars());
init_clause_filter(s.m_clauses);
init_clause_filter(s.m_learned);
}
void lut_finder::init_clause_filter(clause_vector& clauses) {
for (clause* cp : clauses) {
clause& c = *cp;
if (c.size() <= m_max_lut_size && s.all_distinct(c)) {
clause_filter cf(get_clause_filter(c), cp);
for (literal l : c) {
m_clause_filters[l.var()].push_back(cf);
}
}
}
}
unsigned lut_finder::get_clause_filter(clause const& c) {
unsigned filter = 0;
for (literal l : c) {
filter |= 1 << ((l.var() % 32));
}
return filter;
}
std::ostream& lut_finder::display_mask(std::ostream& out, uint64_t mask, unsigned sz) const {
for (unsigned i = 0; i < sz; ++i) {
out << ((0 != (((mask >> i)) & 0x1)) ? "1" : "0");
}
return out;
}
}

79
src/sat/sat_lut_finder.h
View file

@ -1,79 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_lut_finder.h
Abstract:
lut finder
Author:
Nikolaj Bjorner 2020-02-03
Notes:
Find LUT with small input fan-ins
--*/
#pragma once
#include "util/params.h"
#include "util/statistics.h"
#include "sat/sat_clause.h"
#include "sat/sat_types.h"
#include "sat/sat_solver.h"
namespace sat {
class lut_finder {
solver& s;
struct clause_filter {
unsigned m_filter;
clause* m_clause;
clause_filter(unsigned f, clause* cp):
m_filter(f), m_clause(cp) {}
};
unsigned m_max_lut_size;
vector<svector<clause_filter>> m_clause_filters; // index of clauses.
uint64_t m_combination; // bit-mask of parities that have been found
unsigned m_num_combinations;
clause_vector m_clauses_to_remove; // remove clauses that become luts
unsigned_vector m_var_position; // position of var in main clause
bool_var_vector m_vars; // reference to variables being tested for LUT
literal_vector m_clause; // reference clause with literals sorted according to main clause
unsigned_vector m_missing; // set of indices not occurring in clause.
uint64_t m_masks[7];
clause_vector m_removed_clauses;
std::function<void (uint64_t, svector<bool_var> const& vars, bool_var v)> m_on_lut;
void set_combination(unsigned mask);
inline bool get_combination(unsigned mask) const { return (m_combination & (1ull << mask)) != 0; }
bool lut_is_defined(unsigned sz);
bool lut_is_defined(unsigned i, unsigned sz);
uint64_t convert_combination(bool_var_vector& vars, bool_var& v);
void check_lut(clause& c);
void add_lut();
bool extract_lut(literal l1, literal l2);
bool extract_lut(clause& c2);
bool update_combinations(unsigned mask);
void init_clause_filter();
void init_clause_filter(clause_vector& clauses);
unsigned get_clause_filter(clause const& c);
std::ostream& display_mask(std::ostream& out, uint64_t mask, unsigned sz) const;
public:
lut_finder(solver& s) : s(s), m_max_lut_size(5) {
memset(m_masks, 0, sizeof(uint64_t)*7);
}
void set(std::function<void (uint64_t, bool_var_vector const&, bool_var)>& f) { m_on_lut = f; }
unsigned max_lut_size() const { return m_max_lut_size; }
void operator()(clause_vector& clauses);
};
}

12
src/sat/sat_solver.cpp
View file

@ -32,7 +32,6 @@ Revision History:
#include "sat/sat_ddfw_wrapper.h"
#include "sat/sat_prob.h"
#include "sat/sat_anf_simplifier.h"
#include "sat/sat_cut_simplifier.h"
#if defined(_MSC_VER) && !defined(_M_ARM) && !defined(_M_ARM64)
# include <xmmintrin.h>
#endif
@ -2105,11 +2104,7 @@ namespace sat {
anf();
anf.collect_statistics(m_aux_stats);
// TBD: throttle anf_delay based on yield
}
if (m_cut_simplifier && m_simplifications > m_config.m_cut_delay && !inconsistent()) {
(*m_cut_simplifier)();
}
}
if (m_config.m_inprocess_out.is_non_empty_string()) {
std::ofstream fout(m_config.m_inprocess_out.str());
@ -3707,7 +3702,6 @@ namespace sat {
SASSERT(new_v + 1 == m_justification.size()); // there are no active variables that have higher values
literal lit = literal(new_v, false);
m_user_scope_literals.push_back(lit);
m_cut_simplifier = nullptr; // for simplicity, wipe it out
if (m_ext)
m_ext->user_push();
TRACE(sat, tout << "user_push: " << lit << "\n";);
@ -3766,9 +3760,6 @@ namespace sat {
m_slow_glue_backup.set_alpha(m_config.m_slow_glue_avg);
m_trail_avg.set_alpha(m_config.m_slow_glue_avg);
if (m_config.m_cut_simplify && !m_cut_simplifier && m_user_scope_literals.empty()) {
m_cut_simplifier = alloc(cut_simplifier, *this);
}
}
void solver::collect_param_descrs(param_descrs & d) {
@ -3788,7 +3779,6 @@ namespace sat {
m_probing.collect_statistics(st);
if (m_ext) m_ext->collect_statistics(st);
if (m_local_search) m_local_search->collect_statistics(st);
if (m_cut_simplifier) m_cut_simplifier->collect_statistics(st);
st.copy(m_aux_stats);
}

4
src/sat/sat_solver.h
View file

@ -39,7 +39,6 @@ Revision History:
#include "sat/sat_simplifier.h"
#include "sat/sat_scc.h"
#include "sat/sat_asymm_branch.h"
#include "sat/sat_cut_simplifier.h"
#include "sat/sat_probing.h"
#include "sat/sat_mus.h"
#include "sat/sat_drat.h"
@ -97,7 +96,6 @@ namespace sat {
config m_config;
stats m_stats;
scoped_ptr<extension> m_ext;
scoped_ptr<cut_simplifier> m_cut_simplifier;
parallel* m_par;
drat m_drat; // DRAT for generating proofs
clause_allocator m_cls_allocator[2];
@ -222,7 +220,6 @@ namespace sat {
friend class scc;
friend class pb::solver;
friend class anf_simplifier;
friend class cut_simplifier;
friend class parallel;
friend class lookahead;
friend class local_search;
@ -450,7 +447,6 @@ namespace sat {
bool is_incremental() const { return m_config.m_incremental; }
extension* get_extension() const override { return m_ext.get(); }
void set_extension(extension* e) override;
cut_simplifier* get_cut_simplifier() override { return m_cut_simplifier.get(); }
bool set_root(literal l, literal r);
void flush_roots();
typedef std::pair<literal, literal> bin_clause;

3
src/sat/sat_solver_core.h
View file

@ -23,7 +23,6 @@ Revision History:
namespace sat {
class cut_simplifier;
class extension;
class solver_core {
@ -58,8 +57,6 @@ namespace sat {
// hooks for extension solver. really just ba_solver atm.
virtual extension* get_extension() const { return nullptr; }
virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); }
virtual cut_simplifier* get_cut_simplifier() { return nullptr; }
};
};

1
src/sat/smt/array_solver.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#pragma once
#include "util/union_find.h"
#include "ast/ast_trail.h"
#include "sat/smt/sat_th.h"
#include "ast/array_decl_plugin.h"

1
src/sat/smt/bv_solver.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#pragma once
#include "util/union_find.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/bv_ackerman.h"
#include "ast/rewriter/bit_blaster/bit_blaster.h"

1
src/sat/smt/dt_solver.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#pragma once
#include "util/union_find.h"
#include "sat/smt/sat_th.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/array_decl_plugin.h"

26
src/sat/tactic/goal2sat.cpp
View file

@ -38,7 +38,6 @@ Notes:
#include "model/model_v2_pp.h"
#include "tactic/tactic.h"
#include "ast/converters/generic_model_converter.h"
#include "sat/sat_cut_simplifier.h"
#include "sat/sat_drat.h"
#include "sat/tactic/goal2sat.h"
#include "sat/smt/pb_solver.h"
@ -76,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
bool m_default_external;
bool m_euf = false;
bool m_top_level = false;
sat::literal_vector aig_lits;
imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
m(_m),
@ -91,10 +89,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
updt_params(p);
}
sat::cut_simplifier* aig() {
return m_solver.get_cut_simplifier();
}
void updt_params(params_ref const & p) {
sat_params sp(p);
m_ite_extra = p.get_bool("ite_extra", true);
@ -440,16 +434,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_result_stack.push_back(~l);
lits = m_result_stack.end() - num - 1;
if (aig()) {
aig_lits.reset();
aig_lits.append(num, lits);
}
// remark: mk_clause may perform destructive updated to lits.
// I have to execute it after the binary mk_clause above.
mk_clause(num+1, lits, mk_tseitin(num+1, lits));
if (aig())
aig()->add_or(l, num, aig_lits.data());
m_solver.set_phase(~l);
m_result_stack.shrink(old_sz);
if (sign)
@ -497,14 +486,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
m_result_stack.push_back(l);
lits = m_result_stack.end() - num - 1;
if (aig()) {
aig_lits.reset();
aig_lits.append(num, lits);
}
mk_clause(num+1, lits, mk_tseitin(num+1, lits));
if (aig()) {
aig()->add_and(l, num, aig_lits.data());
}
mk_clause(num+1, lits, mk_tseitin(num+1, lits));
m_solver.set_phase(l);
if (sign)
l.neg();
@ -546,7 +528,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_clause(~t, ~e, l, mk_tseitin(~t, ~e, l));
mk_clause(t, e, ~l, mk_tseitin(t, e, ~l));
}
if (aig()) aig()->add_ite(l, c, t, e);
if (sign)
l.neg();
@ -645,7 +626,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_clause(~l, ~l1, l2, mk_tseitin(~l, ~l1, l2));
mk_clause(l, l1, l2, mk_tseitin(l, l1, l2));
mk_clause(l, ~l1, ~l2, mk_tseitin(l, ~l1, ~l2));
if (aig()) aig()->add_iff(l, l1, l2);
cache(t, l);
if (sign)

1
src/sat/tactic/sat2goal.cpp
View file

@ -38,7 +38,6 @@ Notes:
#include "model/model_v2_pp.h"
#include "tactic/tactic.h"
#include "ast/converters/generic_model_converter.h"
#include "sat/sat_cut_simplifier.h"
#include "sat/sat_drat.h"
#include "sat/tactic/sat2goal.h"
#include "sat/smt/pb_solver.h"