mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
separate out aig_cuts class, make it fully incremental with eviction strategy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
20618ff3b3
commit
192c6e39c2
|
|
@ -2,6 +2,7 @@ z3_add_component(sat
|
|||
SOURCES
|
||||
ba_solver.cpp
|
||||
dimacs.cpp
|
||||
sat_aig_cuts.cpp
|
||||
sat_aig_finder.cpp
|
||||
sat_aig_simplifier.cpp
|
||||
sat_anf_simplifier.cpp
|
||||
|
|
|
|||
306
src/sat/sat_aig_cuts.cpp
Normal file
306
src/sat/sat_aig_cuts.cpp
Normal file
|
|
@ -0,0 +1,306 @@
|
|||
/*++
|
||||
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 "sat/sat_aig_cuts.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);
|
||||
}
|
||||
|
||||
vector<cut_set> const& aig_cuts::get_cuts() {
|
||||
unsigned_vector node_ids = filter_valid_nodes();
|
||||
augment(node_ids);
|
||||
TRACE("aig_simplifier", display(tout););
|
||||
return m_cuts;
|
||||
}
|
||||
|
||||
void aig_cuts::augment(unsigned_vector const& ids) {
|
||||
for (unsigned id : ids) {
|
||||
cut_set& cs = m_cuts[id];
|
||||
node const& n = m_aig[id];
|
||||
SASSERT(n.is_valid());
|
||||
augment(n, cs);
|
||||
for (node const& n2 : m_aux_aig[id]) {
|
||||
augment(n2, cs);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment(node const& n, cut_set& cs) {
|
||||
unsigned nc = n.num_children();
|
||||
if (n.is_var()) {
|
||||
SASSERT(!n.sign());
|
||||
}
|
||||
else if (n.is_ite()) {
|
||||
augment_ite(n, cs);
|
||||
}
|
||||
else if (nc == 0) {
|
||||
augment_aig0(n, cs);
|
||||
}
|
||||
else if (nc == 1) {
|
||||
augment_aig1(n, cs);
|
||||
}
|
||||
else if (nc == 2) {
|
||||
augment_aig2(n, cs);
|
||||
}
|
||||
else if (nc < m_config.m_max_cut_size) {
|
||||
augment_aigN(n, cs);
|
||||
}
|
||||
}
|
||||
|
||||
bool aig_cuts::insert_cut(cut const& c, cut_set& cs) {
|
||||
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);
|
||||
}
|
||||
return cs.insert(c);
|
||||
}
|
||||
|
||||
void aig_cuts::augment_ite(node const& n, cut_set& cs) {
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
literal l3 = child(n, 2);
|
||||
unsigned round = 0;
|
||||
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)) {
|
||||
continue;
|
||||
}
|
||||
for (auto const& c : m_cuts[l3.var()]) {
|
||||
cut abc;
|
||||
if (!abc.merge(ab, c, m_config.m_max_cut_size)) {
|
||||
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();
|
||||
// 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) && ++round >= m_config.m_max_insertions)
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig0(node const& n, cut_set& cs) {
|
||||
SASSERT(n.is_and());
|
||||
cut c;
|
||||
cs.reset();
|
||||
if (n.sign()) {
|
||||
c.m_table = 0; // constant false
|
||||
}
|
||||
else {
|
||||
c.m_table = 0x3; // constant true
|
||||
}
|
||||
cs.insert(c);
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig1(node const& n, cut_set& cs) {
|
||||
SASSERT(n.is_and());
|
||||
literal lit = child(n, 0);
|
||||
unsigned round = 0;
|
||||
for (auto const& a : m_cuts[lit.var()]) {
|
||||
cut c;
|
||||
c.set_table(a.m_table);
|
||||
if (n.sign()) c.negate();
|
||||
if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions)
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig2(node const& n, cut_set& cs) {
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
unsigned round = 0;
|
||||
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)) {
|
||||
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();
|
||||
if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions)
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aigN(node const& n, cut_set& cs) {
|
||||
m_cut_set1.reset();
|
||||
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);
|
||||
if (lit.sign()) {
|
||||
m_cut_set1.back().negate();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 1; i < n.num_children(); ++i) {
|
||||
m_cut_set2.reset();
|
||||
literal lit = child(n, i);
|
||||
unsigned round = 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)) {
|
||||
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.num_children() && n.sign()) c.negate();
|
||||
if (insert_cut(c, m_cut_set2) && ++round >= m_config.m_max_insertions) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (round >= m_config.m_max_insertions) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_cut_set1.swap(m_cut_set2);
|
||||
}
|
||||
for (auto & cut : m_cut_set1) {
|
||||
insert_cut(cut, cs);
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::reserve(unsigned v) {
|
||||
m_aig.reserve(v + 1);
|
||||
m_cuts.reserve(v + 1);
|
||||
m_aux_aig.reserve(v + 1);
|
||||
}
|
||||
|
||||
void aig_cuts::add_var(unsigned v) {
|
||||
reserve(v);
|
||||
if (!m_aig[v].is_valid()) {
|
||||
m_aig[v] = node(v);
|
||||
init_cut_set(v);
|
||||
}
|
||||
SASSERT(m_aig[v].is_valid());
|
||||
}
|
||||
|
||||
void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
|
||||
TRACE("aig_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) {
|
||||
if (!m_aig[args[i].var()].is_valid()) {
|
||||
add_var(args[i].var());
|
||||
}
|
||||
}
|
||||
if (!m_aig[v].is_valid() || m_aig[v].is_var() || (sz == 0)) {
|
||||
m_aig[v] = n;
|
||||
init_cut_set(v);
|
||||
}
|
||||
else if (eq(n, m_aig[v]) || !insert_aux(v, n)) {
|
||||
m_literals.shrink(m_literals.size() - sz);
|
||||
TRACE("aig_simplifier", tout << "duplicate\n";);
|
||||
}
|
||||
SASSERT(m_aig[v].is_valid());
|
||||
}
|
||||
|
||||
void aig_cuts::init_cut_set(unsigned id) {
|
||||
node const& n = m_aig[id];
|
||||
SASSERT(n.is_valid());
|
||||
auto& cut_set = m_cuts[id];
|
||||
cut_set.init(m_region, m_config.m_max_cutset_size + 1);
|
||||
cut_set.push_back(cut(id)); // TBD: if entry is a constant?
|
||||
m_aux_aig[id].reset();
|
||||
}
|
||||
|
||||
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.num_children() != b.num_children()) return false;
|
||||
for (unsigned i = 0; i < a.num_children(); ++i) {
|
||||
if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool aig_cuts::insert_aux(unsigned v, node const& n) {
|
||||
if (m_aux_aig[v].size() > m_config.m_max_aux) {
|
||||
return false;
|
||||
}
|
||||
for (node const& n2 : m_aux_aig[v]) {
|
||||
if (eq(n, n2)) return false;
|
||||
}
|
||||
m_aux_aig[v].push_back(n);
|
||||
return true;
|
||||
}
|
||||
|
||||
unsigned_vector aig_cuts::filter_valid_nodes() const {
|
||||
unsigned id = 0;
|
||||
unsigned_vector result;
|
||||
for (node const& n : m_aig) {
|
||||
if (n.is_valid()) result.push_back(id);
|
||||
++id;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
std::ostream& aig_cuts::display(std::ostream& out) const {
|
||||
auto ids = filter_valid_nodes();
|
||||
for (auto id : ids) {
|
||||
out << id << " == ";
|
||||
display(out, m_aig[id]) << "\n";
|
||||
for (auto const& n : m_aux_aig[id]) {
|
||||
display(out << " ", n) << "\n";
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& aig_cuts::display(std::ostream& out, node const& n) const {
|
||||
if (n.sign()) out << "! ";
|
||||
switch (n.op()) {
|
||||
case var_op: out << "var "; break;
|
||||
case and_op: out << "and "; break;
|
||||
case xor_op: out << "xor "; break;
|
||||
case ite_op: out << "ite "; break;
|
||||
default: break;
|
||||
}
|
||||
for (unsigned i = 0; i < n.num_children(); ++i) {
|
||||
out << m_literals[n.offset() + i] << " ";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
108
src/sat/sat_aig_cuts.h
Normal file
108
src/sat/sat_aig_cuts.h
Normal file
|
|
@ -0,0 +1,108 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_aig_cuts.h
|
||||
|
||||
Abstract:
|
||||
|
||||
extract AIG definitions from clauses
|
||||
Perform cut-set enumeration to identify equivalences.
|
||||
|
||||
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,
|
||||
no_op
|
||||
};
|
||||
|
||||
class aig_cuts {
|
||||
|
||||
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(3), m_max_insertions(10) {}
|
||||
};
|
||||
|
||||
// encodes one of var, and, !and, xor, !xor, ite, !ite.
|
||||
class node {
|
||||
bool m_sign;
|
||||
bool_op m_op;
|
||||
unsigned m_num_children;
|
||||
unsigned m_offset;
|
||||
public:
|
||||
node(): m_sign(false), m_op(no_op), m_num_children(UINT_MAX), m_offset(UINT_MAX) {}
|
||||
explicit node(unsigned v): m_sign(false), m_op(var_op), m_num_children(UINT_MAX), m_offset(v) {}
|
||||
explicit node(bool negate, bool_op op, unsigned num_children, unsigned offset):
|
||||
m_sign(negate), m_op(op), m_num_children(num_children), m_offset(offset) {}
|
||||
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; }
|
||||
unsigned var() const { SASSERT(is_var()); return m_offset; }
|
||||
bool sign() const { return m_sign; }
|
||||
unsigned num_children() const { SASSERT(!is_var()); return m_num_children; }
|
||||
unsigned offset() const { return m_offset; }
|
||||
};
|
||||
random_gen m_rand;
|
||||
config m_config;
|
||||
svector<node> m_aig; // vector of main aig nodes.
|
||||
vector<svector<node>> m_aux_aig; // vector of auxiliary aig nodes.
|
||||
literal_vector m_literals;
|
||||
region m_region;
|
||||
cut_set m_cut_set1, m_cut_set2;
|
||||
vector<cut_set> m_cuts;
|
||||
|
||||
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);
|
||||
|
||||
unsigned_vector filter_valid_nodes() const;
|
||||
void augment(unsigned_vector const& ids);
|
||||
void augment(node const& n, cut_set& cs);
|
||||
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);
|
||||
|
||||
bool insert_cut(cut const& c, cut_set& cs);
|
||||
|
||||
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.num_children()); return m_literals[n.offset() + idx]; }
|
||||
|
||||
public:
|
||||
aig_cuts();
|
||||
void add_var(unsigned v);
|
||||
void add_node(literal head, bool_op op, unsigned sz, literal const* args);
|
||||
|
||||
vector<cut_set> const & get_cuts();
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -40,7 +40,6 @@ namespace sat {
|
|||
|
||||
aig_simplifier::aig_simplifier(solver& s):
|
||||
s(s),
|
||||
m_aig_cuts(m_config.m_max_cut_size, m_config.m_max_cutset_size),
|
||||
m_trail_size(0) {
|
||||
}
|
||||
|
||||
|
|
@ -95,8 +94,7 @@ namespace sat {
|
|||
literal lit = s.trail_literal(m_trail_size);
|
||||
m_aig_cuts.add_node(lit, and_op, 0, 0);
|
||||
}
|
||||
|
||||
|
||||
|
||||
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.c_ptr());
|
||||
|
|
@ -223,220 +221,5 @@ namespace sat {
|
|||
st.update("sat-aig.xors", m_stats.m_num_xors);
|
||||
}
|
||||
|
||||
aig_cuts::aig_cuts(unsigned max_cut_size, unsigned max_cutset_size) {
|
||||
m_max_cut_size = std::min(cut().max_cut_size, max_cut_size);
|
||||
m_max_cutset_size = max_cutset_size;
|
||||
}
|
||||
|
||||
vector<cut_set> const& aig_cuts::get_cuts() {
|
||||
unsigned_vector node_ids = filter_valid_nodes();
|
||||
m_cut_set1.init(m_region, m_max_cutset_size + 1);
|
||||
m_cut_set2.init(m_region, m_max_cutset_size + 1);
|
||||
augment(node_ids, m_cuts);
|
||||
return m_cuts;
|
||||
}
|
||||
|
||||
void aig_cuts::augment(unsigned_vector const& ids, vector<cut_set>& cuts) {
|
||||
for (unsigned id : ids) {
|
||||
node const& n = m_aig[id];
|
||||
SASSERT(n.is_valid());
|
||||
auto& cut_set = cuts[id];
|
||||
if (n.is_var()) {
|
||||
SASSERT(!n.sign());
|
||||
}
|
||||
else if (n.is_ite()) {
|
||||
augment_ite(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() == 0) {
|
||||
augment_aig0(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() == 1) {
|
||||
augment_aig1(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() == 2) {
|
||||
augment_aig2(n, cut_set, cuts);
|
||||
}
|
||||
else if (n.num_children() < m_max_cut_size && cut_set.size() < m_max_cutset_size) {
|
||||
augment_aigN(n, cut_set, cuts);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_ite(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
literal l3 = child(n, 2);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
cut ab;
|
||||
if (!ab.merge(a, b, m_max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
for (auto const& c : cuts[l3.var()]) {
|
||||
cut abc;
|
||||
if (!abc.merge(ab, c, m_max_cut_size)) {
|
||||
continue;
|
||||
}
|
||||
if (cs.size() >= m_max_cutset_size) break;
|
||||
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();
|
||||
// extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1;
|
||||
cs.insert(abc);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig0(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
SASSERT(n.is_and());
|
||||
cut c;
|
||||
cs.reset();
|
||||
if (n.sign()) {
|
||||
c.m_table = 0; // constant false
|
||||
}
|
||||
else {
|
||||
c.m_table = 0x3; // constant true
|
||||
}
|
||||
cs.insert(c);
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig1(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
SASSERT(n.is_and());
|
||||
literal lit = child(n, 0);
|
||||
for (auto const& a : cuts[lit.var()]) {
|
||||
if (cs.size() >= m_max_cutset_size) break;
|
||||
cut c;
|
||||
c.set_table(a.m_table);
|
||||
if (n.sign()) c.negate();
|
||||
cs.insert(c);
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aig2(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal l1 = child(n, 0);
|
||||
literal l2 = child(n, 1);
|
||||
for (auto const& a : cuts[l1.var()]) {
|
||||
for (auto const& b : cuts[l2.var()]) {
|
||||
if (cs.size() >= m_max_cutset_size) break;
|
||||
cut c;
|
||||
if (c.merge(a, b, m_max_cut_size)) {
|
||||
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();
|
||||
cs.insert(c);
|
||||
}
|
||||
}
|
||||
if (cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::augment_aigN(node const& n, cut_set& cs, vector<cut_set>& cuts) {
|
||||
m_cut_set1.reset();
|
||||
SASSERT(n.is_and() || n.is_xor());
|
||||
literal lit = child(n, 0);
|
||||
for (auto const& a : cuts[lit.var()]) {
|
||||
m_cut_set1.push_back(a);
|
||||
if (lit.sign()) {
|
||||
m_cut_set1.back().negate();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 1; i < n.num_children(); ++i) {
|
||||
m_cut_set2.reset();
|
||||
literal lit = child(n, i);
|
||||
for (auto const& a : m_cut_set1) {
|
||||
for (auto const& b : cuts[lit.var()]) {
|
||||
cut c;
|
||||
if (m_cut_set2.size() + cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
if (c.merge(a, b, m_max_cut_size)) {
|
||||
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.num_children() && n.sign()) c.negate();
|
||||
m_cut_set2.insert(c);
|
||||
}
|
||||
}
|
||||
if (m_cut_set2.size() + cs.size() >= m_max_cutset_size)
|
||||
break;
|
||||
}
|
||||
m_cut_set1.swap(m_cut_set2);
|
||||
}
|
||||
for (auto & cut : m_cut_set1) {
|
||||
cs.insert(cut);
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::add_var(unsigned v) {
|
||||
m_aig.reserve(v + 1);
|
||||
m_cuts.reserve(v + 1);
|
||||
if (!m_aig[v].is_valid()) {
|
||||
m_aig[v] = node(v);
|
||||
init_cut_set(v);
|
||||
}
|
||||
SASSERT(m_aig[v].is_valid());
|
||||
}
|
||||
|
||||
void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
|
||||
TRACE("aig_simplifier", tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";);
|
||||
unsigned v = head.var();
|
||||
m_aig.reserve(v + 1);
|
||||
unsigned offset = m_literals.size();
|
||||
node n(head.sign(), op, sz, offset);
|
||||
m_literals.append(sz, args);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (!m_aig[args[i].var()].is_valid()) {
|
||||
add_var(args[i].var());
|
||||
}
|
||||
}
|
||||
if (!m_aig[v].is_valid() || m_aig[v].is_var() || (sz == 0)) {
|
||||
m_aig[v] = n;
|
||||
init_cut_set(v);
|
||||
}
|
||||
else {
|
||||
insert_aux(v, n);
|
||||
}
|
||||
SASSERT(m_aig[v].is_valid());
|
||||
}
|
||||
|
||||
void aig_cuts::init_cut_set(unsigned id) {
|
||||
node const& n = m_aig[id];
|
||||
SASSERT(n.is_valid());
|
||||
auto& cut_set = m_cuts[id];
|
||||
cut_set.init(m_region, m_max_cutset_size + 1);
|
||||
cut_set.push_back(cut(id)); // TBD: if entry is a constant?
|
||||
if (m_aux_aig.size() < id) {
|
||||
m_aux_aig[id].reset();
|
||||
}
|
||||
}
|
||||
|
||||
void aig_cuts::insert_aux(unsigned v, node const& n) {
|
||||
// TBD: throttle and replacement strategy
|
||||
m_aux_aig.reserve(v + 1);
|
||||
m_aux_aig[v].push_back(n);
|
||||
}
|
||||
|
||||
unsigned_vector aig_cuts::filter_valid_nodes() {
|
||||
unsigned id = 0;
|
||||
unsigned_vector result;
|
||||
for (node const& n : m_aig) {
|
||||
if (n.is_valid()) result.push_back(id);
|
||||
++id;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -19,70 +19,10 @@
|
|||
#pragma once
|
||||
|
||||
#include "sat/sat_aig_finder.h"
|
||||
#include "sat/sat_cutset.h"
|
||||
#include "sat/sat_aig_cuts.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
enum bool_op {
|
||||
var_op,
|
||||
and_op,
|
||||
ite_op,
|
||||
xor_op,
|
||||
no_op
|
||||
};
|
||||
|
||||
class aig_cuts {
|
||||
// encodes one of var, and, !and, xor, !xor, ite, !ite.
|
||||
class node {
|
||||
bool m_sign;
|
||||
bool_op m_op;
|
||||
unsigned m_num_children;
|
||||
unsigned m_offset;
|
||||
public:
|
||||
node(): m_sign(false), m_op(no_op), m_num_children(UINT_MAX), m_offset(UINT_MAX) {}
|
||||
explicit node(unsigned v): m_sign(false), m_op(var_op), m_num_children(UINT_MAX), m_offset(v) {}
|
||||
explicit node(bool negate, bool_op op, unsigned num_children, unsigned offset):
|
||||
m_sign(negate), m_op(op), m_num_children(num_children), m_offset(offset) {}
|
||||
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; }
|
||||
unsigned var() const { SASSERT(is_var()); return m_offset; }
|
||||
bool sign() const { return m_sign; }
|
||||
unsigned num_children() const { SASSERT(!is_var()); return m_num_children; }
|
||||
unsigned offset() const { return m_offset; }
|
||||
};
|
||||
svector<node> m_aig; // vector of main aig nodes.
|
||||
vector<svector<node>> m_aux_aig; // vector of auxiliary aig nodes.
|
||||
literal_vector m_literals;
|
||||
region m_region;
|
||||
unsigned m_max_cut_size;
|
||||
unsigned m_max_cutset_size;
|
||||
cut_set m_cut_set1, m_cut_set2;
|
||||
vector<cut_set> m_cuts;
|
||||
|
||||
void insert_aux(unsigned v, node const& n);
|
||||
void init_cut_set(unsigned id);
|
||||
|
||||
unsigned_vector filter_valid_nodes();
|
||||
void augment(unsigned_vector const& ids, vector<cut_set>& cuts);
|
||||
void augment_ite(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aig0(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aig1(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aig2(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
void augment_aigN(node const& n, cut_set& cs, vector<cut_set>& cuts);
|
||||
|
||||
public:
|
||||
aig_cuts(unsigned max_cut_size, unsigned max_cutset_size);
|
||||
void add_var(unsigned v);
|
||||
void add_node(literal head, bool_op op, unsigned sz, literal const* args);
|
||||
|
||||
literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.num_children()); return m_literals[n.offset() + idx]; }
|
||||
vector<cut_set> const & get_cuts();
|
||||
};
|
||||
|
||||
class aig_simplifier {
|
||||
public:
|
||||
struct stats {
|
||||
|
|
@ -90,15 +30,9 @@ namespace sat {
|
|||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
struct config {
|
||||
unsigned m_max_cut_size;
|
||||
unsigned m_max_cutset_size;
|
||||
config(): m_max_cut_size(4), m_max_cutset_size(10) {}
|
||||
};
|
||||
private:
|
||||
solver& s;
|
||||
stats m_stats;
|
||||
config m_config;
|
||||
solver& s;
|
||||
stats m_stats;
|
||||
aig_cuts m_aig_cuts;
|
||||
unsigned m_trail_size;
|
||||
literal_vector m_lits;
|
||||
|
|
|
|||
|
|
@ -32,12 +32,12 @@ namespace sat {
|
|||
- pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation.
|
||||
*/
|
||||
|
||||
void cut_set::insert(cut const& c) {
|
||||
bool cut_set::insert(cut const& c) {
|
||||
unsigned i = 0, j = 0;
|
||||
for (; i < size(); ++i) {
|
||||
cut const& a = (*this)[i];
|
||||
if (a.subset_of(c)) {
|
||||
return;
|
||||
return false;
|
||||
}
|
||||
if (c.subset_of(a)) {
|
||||
continue;
|
||||
|
|
@ -50,6 +50,7 @@ namespace sat {
|
|||
}
|
||||
shrink(j);
|
||||
push_back(c);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool cut_set::no_duplicates() const {
|
||||
|
|
|
|||
|
|
@ -115,7 +115,7 @@ namespace sat {
|
|||
m_cuts = new (r) cut[sz];
|
||||
m_max_size = sz;
|
||||
}
|
||||
void insert(cut const& c);
|
||||
bool insert(cut const& c);
|
||||
bool no_duplicates() const;
|
||||
unsigned size() const { return m_size; }
|
||||
cut * begin() const { return m_cuts; }
|
||||
|
|
@ -134,6 +134,7 @@ namespace sat {
|
|||
cut & operator[](unsigned idx) { return m_cuts[idx]; }
|
||||
void shrink(unsigned j) { m_size = 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]; }
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1939,8 +1939,6 @@ namespace sat {
|
|||
|
||||
if (m_aig_simplifier && m_simplifications > m_config.m_aig_delay && !inconsistent()) {
|
||||
(*m_aig_simplifier)();
|
||||
m_aig_simplifier->collect_statistics(m_aux_stats);
|
||||
// TBD: throttle aig_delay based on yield
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -3770,6 +3768,7 @@ namespace sat {
|
|||
bool_var new_v = mk_var(true, false);
|
||||
lit = literal(new_v, false);
|
||||
m_user_scope_literals.push_back(lit);
|
||||
m_aig_simplifier = nullptr; // for simplicity, wipe it out
|
||||
TRACE("sat", tout << "user_push: " << lit << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -3922,7 +3921,7 @@ 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_aig_simplify && !m_aig_simplifier) {
|
||||
if (m_config.m_aig_simplify && !m_aig_simplifier && m_user_scope_literals.empty()) {
|
||||
m_aig_simplifier = alloc(aig_simplifier, *this);
|
||||
}
|
||||
}
|
||||
|
|
@ -3944,6 +3943,7 @@ 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_aig_simplifier) m_aig_simplifier->collect_statistics(st);
|
||||
st.copy(m_aux_stats);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue