mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
add validation to aig_simplifier, start BIG-based masking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
41a00707e1
commit
e0a41a18c3
14 changed files with 741 additions and 167 deletions
|
|
@ -16,19 +16,20 @@
|
|||
--*/
|
||||
|
||||
#include "sat/sat_aig_cuts.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "util/trace.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
aig_cuts::aig_cuts() {
|
||||
m_config.m_max_cut_size = std::min(cut().max_cut_size, m_config.m_max_cut_size);
|
||||
m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1);
|
||||
m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1);
|
||||
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_num_cut_calls = 0;
|
||||
m_num_cuts = 0;
|
||||
}
|
||||
|
||||
vector<cut_set> const& aig_cuts::operator()() {
|
||||
flush_roots();
|
||||
if (true || m_config.m_full) flush_roots();
|
||||
unsigned_vector node_ids = filter_valid_nodes();
|
||||
TRACE("aig_simplifier", display(tout););
|
||||
augment(node_ids);
|
||||
|
|
@ -42,12 +43,11 @@ namespace sat {
|
|||
if (m_aig[id].empty()) {
|
||||
continue;
|
||||
}
|
||||
bool t = false;
|
||||
IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
|
||||
for (node const& n : m_aig[id]) {
|
||||
IF_VERBOSE(3, if (!t && is_touched(n)) { t = true; m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"); });
|
||||
augment(id, n);
|
||||
augment(id, n);
|
||||
}
|
||||
IF_VERBOSE(3, if (t) m_cuts[id].display(verbose_stream() << "after\n"));
|
||||
IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "after\n"));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -62,53 +62,55 @@ namespace sat {
|
|||
SASSERT(!n.sign());
|
||||
}
|
||||
else if (n.is_ite()) {
|
||||
augment_ite(n, cs);
|
||||
augment_ite(id, n, cs);
|
||||
}
|
||||
else if (nc == 0) {
|
||||
augment_aig0(n, cs);
|
||||
else if (nc == 0) {
|
||||
augment_aig0(id, n, cs);
|
||||
}
|
||||
else if (nc == 1) {
|
||||
augment_aig1(n, cs);
|
||||
augment_aig1(id, n, cs);
|
||||
}
|
||||
else if (nc == 2) {
|
||||
augment_aig2(n, cs);
|
||||
augment_aig2(id, n, cs);
|
||||
}
|
||||
else if (nc < m_config.m_max_cut_size) {
|
||||
augment_aigN(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(cut const& c, cut_set& cs) {
|
||||
if (!cs.insert(c)) {
|
||||
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 > m_config.m_max_insertions) {
|
||||
return false;
|
||||
}
|
||||
while (cs.size() >= m_config.m_max_cutset_size) {
|
||||
// never evict the first entry, it is used for the starting point
|
||||
unsigned idx = 1 + (m_rand() % (cs.size() - 1));
|
||||
cs.evict(idx);
|
||||
evict(cs, idx);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void aig_cuts::augment_ite(node const& n, cut_set& cs) {
|
||||
void aig_cuts::augment_ite(unsigned v, node const& n, cut_set& cs) {
|
||||
IF_VERBOSE(2, display(verbose_stream() << "augment_ite " << v << " ", n) << "\n");
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
literal l3 = child(n, 2);
|
||||
for (auto const& a : m_cuts[l1.var()]) {
|
||||
for (auto const& b : m_cuts[l2.var()]) {
|
||||
cut ab;
|
||||
if (!ab.merge(a, b, m_config.m_max_cut_size)) {
|
||||
if (!ab.merge(a, b)) {
|
||||
continue;
|
||||
}
|
||||
for (auto const& c : m_cuts[l3.var()]) {
|
||||
cut abc;
|
||||
if (!abc.merge(ab, c, m_config.m_max_cut_size)) {
|
||||
if (!abc.merge(ab, c)) {
|
||||
continue;
|
||||
}
|
||||
uint64_t t1 = a.shift_table(abc);
|
||||
|
|
@ -117,79 +119,84 @@ namespace sat {
|
|||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
if (l3.sign()) t3 = ~t3;
|
||||
abc.set_table((t1 & t2) | (~t1 & t3));
|
||||
abc.set_table((t1 & t2) | ((~t1) & t3));
|
||||
if (n.sign()) abc.negate();
|
||||
// extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1;
|
||||
if (!insert_cut(abc, cs)) return;
|
||||
if (!insert_cut(v, abc, cs)) return;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig0(node const& n, cut_set& cs) {
|
||||
SASSERT(n.is_and());
|
||||
cs.reset();
|
||||
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.m_table = (n.sign() ? 0x0 : 0x1);
|
||||
cs.push_back(c);
|
||||
push_back(cs, c);
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig1(node const& n, cut_set& cs) {
|
||||
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);
|
||||
for (auto const& a : m_cuts[lit.var()]) {
|
||||
cut c(a);
|
||||
if (n.sign()) c.negate();
|
||||
if (!insert_cut(c, cs)) return;
|
||||
if (!insert_cut(v, c, cs)) return;
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig2(node const& n, cut_set& cs) {
|
||||
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);
|
||||
for (auto const& a : m_cuts[l1.var()]) {
|
||||
for (auto const& b : m_cuts[l2.var()]) {
|
||||
cut c;
|
||||
if (c.merge(a, b, m_config.m_max_cut_size)) {
|
||||
if (c.merge(a, b)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (l1.sign()) t1 = ~t1;
|
||||
if (l2.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2);
|
||||
c.set_table(t3);
|
||||
if (n.sign()) c.negate();
|
||||
if (!insert_cut(c, cs)) return;
|
||||
// validate_aig2(a, b, v, n, c);
|
||||
if (!insert_cut(v, c, cs)) return;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aigN(node const& n, cut_set& cs) {
|
||||
m_cut_set1.reset();
|
||||
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(nullptr);
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal lit = child(n, 0);
|
||||
for (auto const& a : m_cuts[lit.var()]) {
|
||||
m_cut_set1.push_back(a);
|
||||
cut b(a);
|
||||
if (lit.sign()) {
|
||||
m_cut_set1.back().negate();
|
||||
}
|
||||
b.negate();
|
||||
}
|
||||
m_cut_set1.push_back(nullptr, b);
|
||||
}
|
||||
for (unsigned i = 1; i < n.size(); ++i) {
|
||||
m_cut_set2.reset();
|
||||
literal lit = child(n, i);
|
||||
m_cut_set2.reset(nullptr);
|
||||
lit = child(n, i);
|
||||
m_insertions = 0;
|
||||
for (auto const& a : m_cut_set1) {
|
||||
for (auto const& b : m_cuts[lit.var()]) {
|
||||
cut c;
|
||||
if (c.merge(a, b, m_config.m_max_cut_size)) {
|
||||
if (c.merge(a, b)) {
|
||||
uint64_t t1 = a.shift_table(c);
|
||||
uint64_t t2 = b.shift_table(c);
|
||||
if (lit.sign()) t2 = ~t2;
|
||||
uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
|
||||
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(c, m_cut_set2)) goto next_child;
|
||||
if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -198,7 +205,8 @@ namespace sat {
|
|||
}
|
||||
m_insertions = 0;
|
||||
for (auto & cut : m_cut_set1) {
|
||||
if (!insert_cut(cut, cs)) {
|
||||
// validate_aigN(v, n, cut);
|
||||
if (!insert_cut(v, cut, cs)) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -240,19 +248,22 @@ namespace sat {
|
|||
std::sort(m_literals.c_ptr() + offset, m_literals.c_ptr() + offset + sz);
|
||||
}
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
reserve(args[i].var());
|
||||
if (m_aig[args[i].var()].empty()) {
|
||||
add_var(args[i].var());
|
||||
}
|
||||
}
|
||||
if (m_aig[v].empty() || n.is_const()) {
|
||||
m_aig[v].reset();
|
||||
m_aig[v].push_back(n);
|
||||
m_aig[v].push_back(n);
|
||||
on_node_add(v, n);
|
||||
init_cut_set(v);
|
||||
if (n.is_const()) {
|
||||
augment_aig0(n, m_cuts[v]);
|
||||
augment_aig0(v, n, m_cuts[v]);
|
||||
}
|
||||
touch(v);
|
||||
IF_VERBOSE(2, display(verbose_stream() << "add " << head.var() << " == ", n) << "\n");
|
||||
IF_VERBOSE(12, display(verbose_stream() << "add " << head.var() << " == ", n) << "\n");
|
||||
|
||||
}
|
||||
else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
|
||||
m_literals.shrink(m_literals.size() - sz);
|
||||
|
|
@ -262,7 +273,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void aig_cuts::set_root(bool_var v, literal r) {
|
||||
IF_VERBOSE(2, verbose_stream() << "set-root " << v << " -> " << r << "\n");
|
||||
IF_VERBOSE(10, verbose_stream() << "set-root " << v << " -> " << r << "\n");
|
||||
m_roots.push_back(std::make_pair(v, r));
|
||||
}
|
||||
|
||||
|
|
@ -282,7 +293,7 @@ namespace sat {
|
|||
// invalidate nodes that have been rooted
|
||||
if (to_root[i] != literal(i, false)) {
|
||||
m_aig[i].reset();
|
||||
m_cuts[i].reset();
|
||||
reset(m_cuts[i]);
|
||||
}
|
||||
else {
|
||||
for (node & n : m_aig[i]) {
|
||||
|
|
@ -312,17 +323,14 @@ namespace sat {
|
|||
}
|
||||
|
||||
void aig_cuts::flush_roots(literal_vector const& to_root, cut_set& cs) {
|
||||
unsigned j = 0;
|
||||
for (cut& c : cs) {
|
||||
bool has_stale = false;
|
||||
for (unsigned v : c) {
|
||||
has_stale |= (to_root[v] != literal(v, false));
|
||||
}
|
||||
if (!has_stale) {
|
||||
cs[j++] = c;
|
||||
for (unsigned j = 0; j < cs.size(); ++j) {
|
||||
for (unsigned v : cs[j]) {
|
||||
if (to_root[v] != literal(v, false)) {
|
||||
evict(cs, j--);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
cs.shrink(j);
|
||||
}
|
||||
|
||||
void aig_cuts::init_cut_set(unsigned id) {
|
||||
|
|
@ -330,9 +338,9 @@ namespace sat {
|
|||
node const& n = m_aig[id][0];
|
||||
SASSERT(n.is_valid());
|
||||
auto& cut_set = m_cuts[id];
|
||||
cut_set.init(m_region, m_config.m_max_cutset_size + 1);
|
||||
cut_set.reset();
|
||||
cut_set.push_back(cut(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) {
|
||||
|
|
@ -346,6 +354,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool aig_cuts::insert_aux(unsigned v, node const& n) {
|
||||
if (false && !m_config.m_full) return false;
|
||||
unsigned num_gt = 0, num_eq = 0;
|
||||
for (node const& n2 : m_aig[v]) {
|
||||
if (eq(n, n2)) return false;
|
||||
|
|
@ -353,6 +362,7 @@ namespace sat {
|
|||
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;
|
||||
|
|
@ -362,6 +372,8 @@ namespace sat {
|
|||
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;
|
||||
|
|
@ -375,6 +387,8 @@ namespace sat {
|
|||
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;
|
||||
|
|
@ -396,6 +410,216 @@ namespace sat {
|
|||
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.m_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();
|
||||
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");
|
||||
}
|
||||
unsigned num_comp = (1 << n.size());
|
||||
for (unsigned i = 0; i < num_comp; ++i) {
|
||||
unsigned parity = 0;
|
||||
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;
|
||||
}
|
||||
m_clause.push_back(lit);
|
||||
}
|
||||
m_clause.push_back(1 == (parity % 2) ? r : ~r);
|
||||
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) {
|
||||
svector<bool> 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));
|
||||
}
|
||||
|
||||
struct aig_cuts::validator {
|
||||
aig_cuts& t;
|
||||
params_ref p;
|
||||
reslimit lim;
|
||||
solver s;
|
||||
unsigned_vector vars;
|
||||
svector<bool> is_var;
|
||||
|
||||
validator(aig_cuts& t):t(t),s(p, lim) {
|
||||
p.set_bool("aig_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) {
|
||||
std::sort(vars.begin(), vars.end());
|
||||
s.display(std::cout);
|
||||
for (auto v : vars) std::cout << v << " := " << s.get_model()[v] << "\n";
|
||||
std::string line;
|
||||
std::getline(std::cin, line);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
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) {
|
||||
|
|
|
|||
|
|
@ -53,14 +53,17 @@ namespace sat {
|
|||
}
|
||||
|
||||
class aig_cuts {
|
||||
public:
|
||||
typedef std::function<void(literal_vector const&)> on_clause_t;
|
||||
|
||||
struct config {
|
||||
unsigned m_max_cut_size;
|
||||
unsigned m_max_cutset_size;
|
||||
unsigned m_max_aux;
|
||||
unsigned m_max_insertions;
|
||||
config(): m_max_cut_size(4), m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10) {}
|
||||
bool m_full;
|
||||
config(): m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10), m_full(false) {}
|
||||
};
|
||||
private:
|
||||
|
||||
// encodes one of var, and, !and, xor, !xor, ite, !ite.
|
||||
class node {
|
||||
|
|
@ -96,8 +99,12 @@ namespace sat {
|
|||
vector<cut_set> m_cuts;
|
||||
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;
|
||||
|
||||
bool is_touched(node const& n);
|
||||
bool is_touched(literal lit) const { return is_touched(lit.var()); }
|
||||
|
|
@ -112,13 +119,13 @@ namespace sat {
|
|||
unsigned_vector filter_valid_nodes() const;
|
||||
void augment(unsigned_vector const& ids);
|
||||
void augment(unsigned id, node const& n);
|
||||
void augment_ite(node const& n, cut_set& cs);
|
||||
void augment_aig0(node const& n, cut_set& cs);
|
||||
void augment_aig1(node const& n, cut_set& cs);
|
||||
void augment_aig2(node const& n, cut_set& cs);
|
||||
void augment_aigN(node const& n, cut_set& cs);
|
||||
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);
|
||||
|
||||
bool insert_cut(cut const& c, cut_set& cs);
|
||||
bool insert_cut(unsigned v, cut const& c, cut_set& cs);
|
||||
|
||||
void flush_roots();
|
||||
void flush_roots(literal_vector const& to_root, node& n);
|
||||
|
|
@ -128,15 +135,40 @@ namespace sat {
|
|||
|
||||
literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; }
|
||||
|
||||
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);
|
||||
|
||||
public:
|
||||
|
||||
aig_cuts();
|
||||
void add_var(unsigned v);
|
||||
void add_node(literal head, bool_op op, unsigned sz, literal 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);
|
||||
|
||||
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);
|
||||
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,9 +35,9 @@ namespace sat {
|
|||
m_num_cuts = s.m_stats.m_num_cuts;
|
||||
}
|
||||
~report() {
|
||||
unsigned ne = s.m_stats.m_num_eqs - m_num_eqs;
|
||||
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 nc = s.m_stats.m_num_cuts - m_num_cuts;
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "(sat.aig-simplifier";
|
||||
if (ne > 0) verbose_stream() << " :num-eqs " << ne;
|
||||
|
|
@ -47,9 +47,71 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
|
||||
aig_simplifier::aig_simplifier(solver& s):
|
||||
s(s),
|
||||
m_trail_size(0) {
|
||||
struct aig_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.c_ptr());
|
||||
if (r != l_false) {
|
||||
std::cout << "not validated: " << clause << "\n";
|
||||
s.display(std::cout);
|
||||
std::string line;
|
||||
std::getline(std::cin, line);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void aig_simplifier::ensure_validator() {
|
||||
if (!m_validator) {
|
||||
std::cout << "init validator\n";
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
aig_simplifier::aig_simplifier(solver& _s):
|
||||
s(_s),
|
||||
m_trail_size(0),
|
||||
m_validator(nullptr) {
|
||||
if (false) {
|
||||
ensure_validator();
|
||||
std::function<void(literal_vector const& clause)> _on_add =
|
||||
[this](literal_vector const& clause) {
|
||||
std::cout << "add " << clause << "\n"; m_validator->validate(clause);
|
||||
};
|
||||
m_aig_cuts.set_on_clause_add(_on_add);
|
||||
}
|
||||
else 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);
|
||||
}
|
||||
}
|
||||
|
||||
aig_simplifier::~aig_simplifier() {
|
||||
dealloc(m_validator);
|
||||
}
|
||||
|
||||
void aig_simplifier::add_and(literal head, unsigned sz, literal const* lits) {
|
||||
|
|
@ -96,7 +158,7 @@ namespace sat {
|
|||
++m_stats.m_num_calls;
|
||||
do {
|
||||
n = m_stats.m_num_eqs + m_stats.m_num_units;
|
||||
clauses2aig();
|
||||
if (m_config.m_full || true) clauses2aig();
|
||||
aig2clauses();
|
||||
++i;
|
||||
}
|
||||
|
|
@ -110,7 +172,7 @@ namespace sat {
|
|||
void aig_simplifier::clauses2aig() {
|
||||
|
||||
// update units
|
||||
for (; m_trail_size < s.init_trail_size(); ++m_trail_size) {
|
||||
for (; m_config.m_full && 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, 0);
|
||||
}
|
||||
|
|
@ -130,7 +192,7 @@ namespace sat {
|
|||
af.set(on_and);
|
||||
af.set(on_ite);
|
||||
clause_vector clauses(s.clauses());
|
||||
clauses.append(s.learned());
|
||||
if (m_config.m_full || true) clauses.append(s.learned());
|
||||
af(clauses);
|
||||
|
||||
std::function<void (literal_vector const&)> on_xor =
|
||||
|
|
@ -165,8 +227,10 @@ namespace sat {
|
|||
|
||||
void aig_simplifier::aig2clauses() {
|
||||
vector<cut_set> const& cuts = m_aig_cuts();
|
||||
m_stats.m_num_cuts = m_aig_cuts.num_cuts();
|
||||
|
||||
map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;
|
||||
|
||||
|
||||
union_find_default_ctx ctx;
|
||||
union_find<> uf(ctx), uf2(ctx);
|
||||
for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var();
|
||||
|
|
@ -176,47 +240,60 @@ namespace sat {
|
|||
};
|
||||
bool new_eq = false;
|
||||
for (unsigned i = cuts.size(); i-- > 0; ) {
|
||||
m_stats.m_num_cuts += cuts[i].size();
|
||||
|
||||
for (auto& cut : cuts[i]) {
|
||||
for (auto& c : cuts[i]) {
|
||||
unsigned j = 0;
|
||||
if (cut.is_true()) {
|
||||
if (m_config.m_full && c.is_true()) {
|
||||
if (s.value(i) == l_undef) {
|
||||
IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, false) << "\n");
|
||||
s.assign_unit(literal(i, false));
|
||||
literal lit(i, false);
|
||||
validate_unit(lit);
|
||||
IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
|
||||
s.assign_unit(lit);
|
||||
++m_stats.m_num_units;
|
||||
}
|
||||
break;
|
||||
}
|
||||
if (cut.is_false()) {
|
||||
if (m_config.m_full && c.is_false()) {
|
||||
if (s.value(i) == l_undef) {
|
||||
IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, true) << "\n");
|
||||
s.assign_unit(literal(i, true));
|
||||
literal lit(i, true);
|
||||
validate_unit(lit);
|
||||
IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
|
||||
s.assign_unit(lit);
|
||||
++m_stats.m_num_units;
|
||||
}
|
||||
break;
|
||||
}
|
||||
if (cut2id.find(&cut, j)) {
|
||||
if (i == j) std::cout << "dup: " << i << "\n";
|
||||
if (cut2id.find(&c, j)) {
|
||||
VERIFY(i != j);
|
||||
literal v(i, false);
|
||||
literal w(j, false);
|
||||
add_eq(v, w);
|
||||
TRACE("aig_simplifier", tout << v << " == " << ~w << "\n";);
|
||||
literal u(i, false);
|
||||
literal v(j, false);
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << u << " " << c << "\n";
|
||||
verbose_stream() << v << ": ";
|
||||
for (cut const& d : cuts[v.var()]) verbose_stream() << d << "\n";);
|
||||
|
||||
certify_equivalence(u, v, c);
|
||||
//validate_eq(u, v);
|
||||
add_eq(u, v);
|
||||
TRACE("aig_simplifier", tout << u << " == " << v << "\n";);
|
||||
new_eq = true;
|
||||
break;
|
||||
}
|
||||
cut.negate();
|
||||
if (cut2id.find(&cut, j)) {
|
||||
literal v(i, false);
|
||||
literal w(j, true);
|
||||
add_eq(v, w);
|
||||
TRACE("aig_simplifier", tout << v << " == " << w << "\n";);
|
||||
new_eq = true;
|
||||
break;
|
||||
if (true || m_config.m_full) {
|
||||
cut nc(c);
|
||||
nc.negate();
|
||||
if (cut2id.find(&nc, j)) {
|
||||
VERIFY(i != j); // maybe possible with don't cares
|
||||
literal u(i, false);
|
||||
literal v(j, true);
|
||||
certify_equivalence(u, v, c);
|
||||
// validate_eq(u, v);
|
||||
add_eq(u, v);
|
||||
TRACE("aig_simplifier", tout << u << " == " << v << "\n";);
|
||||
new_eq = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
cut.negate();
|
||||
cut2id.insert(&cut, i);
|
||||
cut2id.insert(&c, i);
|
||||
}
|
||||
}
|
||||
if (!new_eq) {
|
||||
|
|
@ -252,6 +329,134 @@ namespace sat {
|
|||
elim(uf2);
|
||||
}
|
||||
|
||||
/**
|
||||
* Equilvalences 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 aig_simplifier::certify_equivalence(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 =
|
||||
[&](literal_vector const& clause) { SASSERT(clause.back().var() == u.var()); clauses.push_back(clause); };
|
||||
m_aig_cuts.cut2def(on_clause, c, u);
|
||||
|
||||
// create C or u or ~v for each clause C or u
|
||||
// create C or ~u or v for each clause C or ~u
|
||||
for (auto& clause : clauses) {
|
||||
literal w = clause.back();
|
||||
SASSERT(w.var() == u.var());
|
||||
clause.push_back(w == u ? ~v : v);
|
||||
s.m_drat.add(clause);
|
||||
}
|
||||
// create C or ~u or v for each clause
|
||||
unsigned i = 0, sz = clauses.size();
|
||||
for (; i < sz; ++i) {
|
||||
literal_vector clause(clauses[i]);
|
||||
clause[clause.size()-2] = ~clause[clause.size()-2];
|
||||
clause[clause.size()-1] = ~clause[clause.size()-1];
|
||||
clauses.push_back(clause);
|
||||
s.m_drat.add(clause);
|
||||
}
|
||||
|
||||
// create all resolvents over C. C is assumed to
|
||||
// contain all combinations of some set of literals.
|
||||
i = 0; sz = clauses.size();
|
||||
while (sz - i > 2) {
|
||||
SASSERT((sz & (sz - 1)) == 0);
|
||||
for (; i < sz; ++i) {
|
||||
auto const& clause = clauses[i];
|
||||
if (clause[0].sign()) {
|
||||
literal_vector cl(clause.size() - 1, clause.c_ptr() + 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.
|
||||
for (auto const& clause : clauses) {
|
||||
if (clause.size() > 2) {
|
||||
s.m_drat.del(clause);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* collect pairs of variables that occur in cut sets.
|
||||
*/
|
||||
void aig_simplifier::collect_pairs(vector<cut_set> const& cuts) {
|
||||
m_pairs.reset();
|
||||
for (unsigned k = cuts.size(); k-- > 0; ) {
|
||||
for (auto const& c : cuts[k]) {
|
||||
for (unsigned i = c.size(); i-- > 0; ) {
|
||||
for (unsigned j = i; j-- > 0; ) {
|
||||
m_pairs.insert(var_pair(c[i],c[j]));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* compute masks for pairs.
|
||||
*/
|
||||
void aig_simplifier::add_masks_to_pairs() {
|
||||
big b(s.rand());
|
||||
b.init(s, true);
|
||||
for (auto& p : m_pairs) {
|
||||
literal u(p.u, false), v(p.v, false);
|
||||
// u -> v, then u & ~v is impossible
|
||||
if (b.connected(u, v)) {
|
||||
add_mask(u, ~v, p);
|
||||
}
|
||||
else if (b.connected(u, ~v)) {
|
||||
add_mask(u, v, p);
|
||||
}
|
||||
else if (b.connected(~u, v)) {
|
||||
add_mask(~u, ~v, p);
|
||||
}
|
||||
else if (b.connected(~u, ~v)) {
|
||||
add_mask(~u, v, p);
|
||||
}
|
||||
else {
|
||||
memset(p.masks, 0xFF, var_pair::size());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* compute masks for each possible occurrence of u, v within 2-6 elements.
|
||||
* combinaions relative to u.sign(), v.sign() are impossible.
|
||||
*/
|
||||
void aig_simplifier::add_mask(literal u, literal v, var_pair& p) {
|
||||
unsigned offset = 0;
|
||||
bool su = u.sign(), sv = v.sign();
|
||||
for (unsigned k = 2; k <= 6; ++k) {
|
||||
for (unsigned i = 0; i < k; ++i) {
|
||||
for (unsigned j = i + 1; j < k; ++j) {
|
||||
// convert su, sv, k, i, j into a mask for 2^k bits.
|
||||
// for outputs
|
||||
p.masks[offset++] = 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* apply obtained masks to cut sets.
|
||||
*/
|
||||
void aig_simplifier::apply_masks() {
|
||||
|
||||
}
|
||||
|
||||
void aig_simplifier::collect_statistics(statistics& st) const {
|
||||
st.update("sat-aig.eqs", m_stats.m_num_eqs);
|
||||
st.update("sat-aig.cuts", m_stats.m_num_cuts);
|
||||
|
|
@ -259,6 +464,20 @@ namespace sat {
|
|||
st.update("sat-aig.ites", m_stats.m_num_ites);
|
||||
st.update("sat-aig.xors", m_stats.m_num_xors);
|
||||
}
|
||||
|
||||
void aig_simplifier::validate_unit(literal lit) {
|
||||
ensure_validator();
|
||||
m_validator->validate(1, &lit);
|
||||
}
|
||||
|
||||
void aig_simplifier::validate_eq(literal a, literal b) {
|
||||
ensure_validator();
|
||||
literal lits1[2] = { a, ~b };
|
||||
literal lits2[2] = { ~a, b };
|
||||
m_validator->validate(2, lits1);
|
||||
m_validator->validate(2, lits1);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -31,19 +31,64 @@ namespace sat {
|
|||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
struct config {
|
||||
bool m_full;
|
||||
config():m_full(false) {}
|
||||
};
|
||||
private:
|
||||
struct report;
|
||||
struct validator;
|
||||
|
||||
solver& s;
|
||||
stats m_stats;
|
||||
config m_config;
|
||||
aig_cuts m_aig_cuts;
|
||||
unsigned m_trail_size;
|
||||
literal_vector m_lits;
|
||||
validator* m_validator;
|
||||
|
||||
struct report;
|
||||
void clauses2aig();
|
||||
void aig2clauses();
|
||||
void ensure_validator();
|
||||
void validate_unit(literal lit);
|
||||
void validate_eq(literal a, literal b);
|
||||
void certify_equivalence(literal u, literal v, cut const& c);
|
||||
|
||||
/**
|
||||
* 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.
|
||||
*/
|
||||
struct var_pair {
|
||||
unsigned u, v;
|
||||
uint64_t masks[35];
|
||||
static unsigned size() { return sizeof(uint64_t)*35; }
|
||||
var_pair(unsigned u, unsigned v): u(u), v(v) {
|
||||
if (u > v) std::swap(u, v);
|
||||
}
|
||||
var_pair(): u(UINT_MAX), v(UINT_MAX) {}
|
||||
|
||||
struct hash {
|
||||
unsigned operator()(var_pair const& p) const {
|
||||
return mk_mix(p.u, p.v, 1);
|
||||
}
|
||||
};
|
||||
struct eq {
|
||||
bool operator()(var_pair const& a, var_pair const& b) const {
|
||||
return a.u == b.u && a.v == b.v;
|
||||
}
|
||||
};
|
||||
};
|
||||
hashtable<var_pair, var_pair::hash, var_pair::eq> m_pairs;
|
||||
|
||||
void collect_pairs(vector<cut_set> const& cuts);
|
||||
void add_mask(literal u, literal v, var_pair& p);
|
||||
void add_masks_to_pairs();
|
||||
void apply_masks();
|
||||
public:
|
||||
aig_simplifier(solver& s);
|
||||
~aig_simplifier() {}
|
||||
~aig_simplifier();
|
||||
void operator()();
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -19,7 +19,6 @@
|
|||
|
||||
namespace sat {
|
||||
|
||||
|
||||
/**
|
||||
\brief
|
||||
if c is subsumed by a member in cut_set, then c is not inserted.
|
||||
|
|
@ -32,25 +31,19 @@ namespace sat {
|
|||
- pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation.
|
||||
*/
|
||||
|
||||
bool cut_set::insert(cut const& c) {
|
||||
SASSERT(c.m_size > 0);
|
||||
unsigned i = 0, j = 0;
|
||||
for (; i < size(); ++i) {
|
||||
bool cut_set::insert(on_update_t* on_add, on_update_t* on_del, cut const& c) {
|
||||
unsigned i = 0, j = 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)) {
|
||||
continue;
|
||||
std::swap(m_cuts[i--], m_cuts[--k]);
|
||||
}
|
||||
else if (j < i) {
|
||||
(*this)[j] = a;
|
||||
}
|
||||
SASSERT(!(a == c));
|
||||
++j;
|
||||
}
|
||||
shrink(j);
|
||||
push_back(c);
|
||||
shrink(on_del, i);
|
||||
push_back(on_add, c);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -70,6 +63,37 @@ namespace sat {
|
|||
return out;
|
||||
}
|
||||
|
||||
|
||||
void cut_set::shrink(on_update_t* on_del, unsigned j) {
|
||||
if (m_var != UINT_MAX && on_del && *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_size == m_max_size) {
|
||||
m_max_size *= 2;
|
||||
cut* new_cuts = new (*m_region) cut[m_max_size];
|
||||
memcpy(new_cuts, m_cuts, sizeof(cut)*m_size);
|
||||
m_cuts = new_cuts;
|
||||
}
|
||||
if (m_var != UINT_MAX && on_add && *on_add) (*on_add)(m_var, c);
|
||||
m_cuts[m_size++] = c;
|
||||
}
|
||||
|
||||
void cut_set::init(region& r, unsigned max_sz, unsigned v) {
|
||||
m_var = v;
|
||||
m_max_size = max_sz;
|
||||
SASSERT(!m_region || m_cuts);
|
||||
if (m_region) return;
|
||||
m_region = &r;
|
||||
m_cuts = new (r) cut[max_sz];
|
||||
}
|
||||
|
||||
/**
|
||||
\brief shift table 'a' by adding elements from 'c'.
|
||||
a.shift_table(c)
|
||||
|
|
@ -127,7 +151,7 @@ namespace sat {
|
|||
out << (*this)[i];
|
||||
if (i + 1 < m_size) out << " ";
|
||||
}
|
||||
out << "} t: ";
|
||||
out << "} ";
|
||||
for (unsigned i = 0; i < (1u << m_size); ++i) {
|
||||
if (0 != (m_table & (1ull << i))) out << "1"; else out << "0";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,29 +17,41 @@
|
|||
#include "util/util.h"
|
||||
#include <algorithm>
|
||||
#include <cstring>
|
||||
#include <functional>
|
||||
|
||||
namespace sat {
|
||||
|
||||
struct cut {
|
||||
unsigned max_cut_size;
|
||||
class cut {
|
||||
unsigned m_filter;
|
||||
unsigned m_size;
|
||||
unsigned m_elems[6];
|
||||
unsigned m_elems[4];
|
||||
public:
|
||||
uint64_t m_table;
|
||||
cut(): max_cut_size(6), m_filter(0), m_size(0), m_table(0) {}
|
||||
cut(): m_filter(0), m_size(0), m_table(0) {}
|
||||
|
||||
cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2) { m_elems[0] = id; }
|
||||
|
||||
cut(cut const& other): m_filter(other.m_filter), m_size(other.m_size), m_table(other.m_table) {
|
||||
for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i];
|
||||
cut(cut const& other) {
|
||||
*this = other;
|
||||
}
|
||||
|
||||
cut& operator=(cut const& other) {
|
||||
m_filter = other.m_filter;
|
||||
m_size = other.m_size;
|
||||
m_table = other.m_table;
|
||||
for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i];
|
||||
return *this;
|
||||
}
|
||||
|
||||
unsigned size() const { return m_size; }
|
||||
|
||||
static unsigned max_cut_size() { return 4; }
|
||||
|
||||
unsigned const* begin() const { return m_elems; }
|
||||
unsigned const* end() const { return m_elems + m_size; }
|
||||
|
||||
bool add(unsigned i, unsigned max_sz) {
|
||||
SASSERT(max_sz <= max_cut_size);
|
||||
if (m_size >= max_sz) {
|
||||
bool add(unsigned i) {
|
||||
if (m_size >= max_cut_size()) {
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
|
|
@ -73,12 +85,12 @@ namespace sat {
|
|||
|
||||
uint64_t shift_table(cut const& other) const;
|
||||
|
||||
bool merge(cut const& a, cut const& b, unsigned max_sz) {
|
||||
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), max_sz)) {
|
||||
if (!add(std::min(x, y))) {
|
||||
return false;
|
||||
}
|
||||
if (x < y) {
|
||||
|
|
@ -115,41 +127,32 @@ namespace sat {
|
|||
};
|
||||
|
||||
class cut_set {
|
||||
unsigned m_var;
|
||||
region* m_region;
|
||||
unsigned m_size;
|
||||
unsigned m_max_size;
|
||||
cut * m_cuts;
|
||||
public:
|
||||
cut_set(): m_region(nullptr), m_size(0), m_max_size(0), m_cuts(nullptr) {}
|
||||
void init(region& r, unsigned sz) {
|
||||
m_max_size = sz;
|
||||
SASSERT(!m_region || m_cuts);
|
||||
if (m_region) return;
|
||||
m_region = &r;
|
||||
m_cuts = new (r) cut[sz];
|
||||
}
|
||||
bool insert(cut const& c);
|
||||
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 size() const { return m_size; }
|
||||
cut * begin() const { return m_cuts; }
|
||||
cut * end() const { return m_cuts + m_size; }
|
||||
cut & back() { return m_cuts[m_size-1]; }
|
||||
void push_back(cut const& c) {
|
||||
SASSERT(c.m_size > 0);
|
||||
if (m_size == m_max_size) {
|
||||
m_max_size *= 2;
|
||||
cut* new_cuts = new (*m_region) cut[m_max_size];
|
||||
memcpy(new_cuts, m_cuts, sizeof(cut)*m_size);
|
||||
m_cuts = new_cuts;
|
||||
}
|
||||
m_cuts[m_size++] = c;
|
||||
}
|
||||
void reset() { m_size = 0; }
|
||||
cut & operator[](unsigned idx) { return m_cuts[idx]; }
|
||||
void shrink(unsigned j) { m_size = j; }
|
||||
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) { return m_cuts[idx]; }
|
||||
void shrink(on_update_t* on_del, unsigned j);
|
||||
void swap(cut_set& other) { std::swap(m_size, other.m_size); std::swap(m_cuts, other.m_cuts); std::swap(m_max_size, other.m_max_size); }
|
||||
void evict(unsigned idx) { m_cuts[idx] = m_cuts[--m_size]; }
|
||||
void evict(on_update_t* on_del, unsigned idx) { if (m_var != UINT_MAX && on_del && *on_del) (*on_del)(m_var, m_cuts[idx]); m_cuts[idx] = m_cuts[--m_size]; }
|
||||
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); }
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -399,7 +399,7 @@ namespace sat {
|
|||
}
|
||||
m_units.shrink(num_units);
|
||||
bool ok = m_inconsistent;
|
||||
IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n");
|
||||
// IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n");
|
||||
m_inconsistent = false;
|
||||
|
||||
return ok;
|
||||
|
|
@ -465,7 +465,9 @@ namespace sat {
|
|||
if (!is_drup(n, c) && !is_drat(n, c)) {
|
||||
literal_vector lits(n, c);
|
||||
std::cout << "Verification of " << lits << " failed\n";
|
||||
s.display(std::cout);
|
||||
// s.display(std::cout);
|
||||
std::string line;
|
||||
std::getline(std::cin, line);
|
||||
SASSERT(false);
|
||||
exit(0);
|
||||
UNREACHABLE();
|
||||
|
|
@ -756,7 +758,6 @@ namespace sat {
|
|||
}
|
||||
#endif
|
||||
++m_num_del;
|
||||
//SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true)));
|
||||
if (m_out) dump(c.size(), c.begin(), status::deleted);
|
||||
if (m_bout) bdump(c.size(), c.begin(), status::deleted);
|
||||
if (m_check) {
|
||||
|
|
@ -764,6 +765,16 @@ namespace sat {
|
|||
append(*c1, status::deleted);
|
||||
}
|
||||
}
|
||||
|
||||
void drat::del(literal_vector const& c) {
|
||||
++m_num_del;
|
||||
if (m_out) dump(c.size(), c.begin(), status::deleted);
|
||||
if (m_bout) bdump(c.size(), c.begin(), status::deleted);
|
||||
if (m_check) {
|
||||
clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), true);
|
||||
append(*c1, status::deleted);
|
||||
}
|
||||
}
|
||||
|
||||
void drat::check_model(model const& m) {
|
||||
}
|
||||
|
|
|
|||
|
|
@ -98,6 +98,7 @@ namespace sat {
|
|||
bool is_cleaned(clause& c) const;
|
||||
void del(literal l);
|
||||
void del(literal l1, literal l2);
|
||||
void del(literal_vector const& lits);
|
||||
void del(clause& c);
|
||||
|
||||
void verify(clause const& c) { verify(c.size(), c.begin()); }
|
||||
|
|
|
|||
|
|
@ -235,6 +235,11 @@ namespace sat {
|
|||
bool root_ok = !m_solver.is_external(v) || set_root;
|
||||
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
|
||||
// cannot really eliminate v, since we have to notify extension of future assignments
|
||||
if (m_solver.m_config.m_drat && m_solver.m_config.m_drat_file.is_null()) {
|
||||
std::cout << "DRAT\n";
|
||||
m_solver.m_drat.add(~l, r, true);
|
||||
m_solver.m_drat.add(l, ~r, true);
|
||||
}
|
||||
m_solver.mk_bin_clause(~l, r, false);
|
||||
m_solver.mk_bin_clause(l, ~r, false);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1211,7 +1211,7 @@ namespace sat {
|
|||
init_assumptions(num_lits, lits);
|
||||
propagate(false);
|
||||
if (check_inconsistent()) return l_false;
|
||||
do_cleanup(m_config.m_force_cleanup);
|
||||
if (m_config.m_force_cleanup) do_cleanup(true);
|
||||
|
||||
if (m_config.m_unit_walk) {
|
||||
return do_unit_walk();
|
||||
|
|
@ -1236,7 +1236,7 @@ namespace sat {
|
|||
while (is_sat == l_undef && !should_cancel()) {
|
||||
if (inconsistent()) is_sat = resolve_conflict_core();
|
||||
else if (should_propagate()) propagate(true);
|
||||
else if (do_cleanup(false)) continue;
|
||||
else if (m_conflicts_since_init > 0 && do_cleanup(false)) continue;
|
||||
else if (should_gc()) do_gc();
|
||||
else if (should_rephase()) do_rephase();
|
||||
else if (should_reorder()) do_reorder();
|
||||
|
|
|
|||
|
|
@ -208,6 +208,7 @@ namespace sat {
|
|||
friend class drat;
|
||||
friend class ba_solver;
|
||||
friend class anf_simplifier;
|
||||
friend class aig_simplifier;
|
||||
friend class parallel;
|
||||
friend class lookahead;
|
||||
friend class local_search;
|
||||
|
|
|
|||
|
|
@ -257,8 +257,6 @@ struct goal2sat::imp {
|
|||
m_cache.insert(t, l);
|
||||
sat::literal * lits = m_result_stack.end() - num;
|
||||
|
||||
if (m_aig) m_aig->add_or(l, num, lits);
|
||||
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
mk_clause(~lits[i], l);
|
||||
}
|
||||
|
|
@ -267,6 +265,7 @@ struct goal2sat::imp {
|
|||
// 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);
|
||||
if (m_aig) m_aig->add_or(l, num, lits);
|
||||
unsigned old_sz = m_result_stack.size() - num - 1;
|
||||
m_result_stack.shrink(old_sz);
|
||||
if (sign)
|
||||
|
|
@ -299,7 +298,6 @@ struct goal2sat::imp {
|
|||
m_cache.insert(t, l);
|
||||
sat::literal * lits = m_result_stack.end() - num;
|
||||
|
||||
if (m_aig) m_aig->add_and(l, num, lits);
|
||||
|
||||
// l => /\ lits
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
|
|
@ -312,6 +310,7 @@ struct goal2sat::imp {
|
|||
m_result_stack.push_back(l);
|
||||
lits = m_result_stack.end() - num - 1;
|
||||
mk_clause(num+1, lits);
|
||||
if (m_aig) m_aig->add_and(l, num, lits);
|
||||
unsigned old_sz = m_result_stack.size() - num - 1;
|
||||
m_result_stack.shrink(old_sz);
|
||||
if (sign)
|
||||
|
|
|
|||
|
|
@ -414,20 +414,29 @@ public:
|
|||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
|
||||
}
|
||||
|
||||
void push_back(T const & elem) {
|
||||
old_vector& push_back(T const & elem) {
|
||||
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
|
||||
expand_vector();
|
||||
}
|
||||
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem);
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
return *this;
|
||||
}
|
||||
|
||||
void push_back(T && elem) {
|
||||
template <typename ...Args>
|
||||
old_vector& push_back(T const& elem, T elem2, Args ... elems) {
|
||||
push_back(elem);
|
||||
push_back(elem2, elems ...);
|
||||
return *this;
|
||||
}
|
||||
|
||||
old_vector& push_back(T && elem) {
|
||||
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
|
||||
expand_vector();
|
||||
}
|
||||
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
return *this;
|
||||
}
|
||||
|
||||
void insert(T const & elem) {
|
||||
|
|
|
|||
|
|
@ -70,6 +70,7 @@ public:
|
|||
friend bool operator!=(symbol const & s1, symbol const & s2) { return s1.m_data != s2.m_data; }
|
||||
bool is_numerical() const { return GET_TAG(m_data) == 1; }
|
||||
bool is_null() const { return m_data == nullptr; }
|
||||
bool is_non_empty_string() const { return !is_null() && !is_numerical() && 0 != bare_str()[0]; }
|
||||
unsigned int get_num() const { SASSERT(is_numerical()); return UNBOXINT(m_data); }
|
||||
std::string str() const;
|
||||
friend bool operator==(symbol const & s1, char const * s2) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue