diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp
index 3125b2a3a..e44bf7944 100644
--- a/src/sat/sat_bdd.cpp
+++ b/src/sat/sat_bdd.cpp
@@ -23,6 +23,8 @@ Revision History:
namespace sat {
bdd_manager::bdd_manager(unsigned num_vars) {
+ m_cost_metric = bdd_cost;
+ m_cost_bdd = 0;
for (BDD a = 0; a < 2; ++a) {
for (BDD b = 0; b < 2; ++b) {
for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) {
@@ -58,6 +60,7 @@ namespace sat {
m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
}
for (auto* e : m_op_cache) {
+ VERIFY(e != m_spare_entry);
m_alloc.deallocate(sizeof(*e), e);
}
}
@@ -78,16 +81,21 @@ namespace sat {
bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) {
bool first = true;
+ SASSERT(well_formed());
while (true) {
try {
return apply_rec(arg1, arg2, op);
}
catch (mem_out) {
+ throw;
+#if 0
try_reorder();
if (!first) throw;
first = false;
+#endif
}
}
+ SASSERT(well_formed());
}
@@ -101,17 +109,20 @@ namespace sat {
bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) {
+ // std::cout << a << " " << b << " " << c << " " << e1 << " " << e2 << "\n";
if (e1 != e2) {
+ VERIFY(e2->m_result != -1);
push_entry(e1);
- if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) {
- return true;
- }
- e1 = const_cast<op_entry*>(e2);
+ e1 = nullptr;
+ return true;
+ }
+ else {
+ e1->m_bdd1 = a;
+ e1->m_bdd2 = b;
+ e1->m_op = c;
+ VERIFY(e1->m_result == -1);
+ return false;
}
- e1->m_bdd1 = a;
- e1->m_bdd2 = b;
- e1->m_op = c;
- return false;
}
bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) {
@@ -143,8 +154,10 @@ namespace sat {
op_entry * e1 = pop_entry(a, b, op);
op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
if (check_result(e1, e2, a, b, op)) {
+ SASSERT(!m_free_nodes.contains(e2->m_result));
return e2->m_result;
}
+ // VERIFY(well_formed());
BDD r;
if (level(a) == level(b)) {
push(apply_rec(lo(a), lo(b), op));
@@ -163,6 +176,8 @@ namespace sat {
}
pop(2);
e1->m_result = r;
+ // VERIFY(well_formed());
+ SASSERT(!m_free_nodes.contains(r));
return r;
}
@@ -190,6 +205,7 @@ namespace sat {
else {
void * mem = m_alloc.allocate(sizeof(op_entry));
result = new (mem) op_entry(l, r, op);
+ // std::cout << "alloc: " << result << "\n";
}
result->m_result = -1;
return result;
@@ -200,16 +216,22 @@ namespace sat {
m_spare_entry = e;
}
- bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) {
+ bdd_manager::BDD bdd_manager::make_node(unsigned lvl, BDD l, BDD h) {
m_is_new_node = false;
- if (l == r) {
+ if (l == h) {
return l;
}
+ if (!is_const(l) && level(l) >= lvl) {
+ display(std::cout << l << " level: " << level(l) << " lvl: " << lvl << "\n");
+ }
+ VERIFY(is_const(l) || level(l) < lvl);
+ VERIFY(is_const(h) || level(h) < lvl);
- bdd_node n(level, l, r);
+ bdd_node n(lvl, l, h);
node_table::entry* e = m_node_table.insert_if_not_there2(n);
if (e->get_data().m_index != 0) {
- return e->get_data().m_index;
+ unsigned result = e->get_data().m_index;
+ return result;
}
e->get_data().m_refcount = 0;
bool do_gc = m_free_nodes.empty();
@@ -226,25 +248,50 @@ namespace sat {
}
SASSERT(!m_free_nodes.empty());
- e->get_data().m_index = m_free_nodes.back();
- m_nodes[e->get_data().m_index] = e->get_data();
- m_free_nodes.pop_back();
- m_is_new_node = true;
- return e->get_data().m_index;
+ unsigned result = m_free_nodes.back();
+ m_free_nodes.pop_back();
+ e->get_data().m_index = result;
+ m_nodes[result] = e->get_data();
+ m_is_new_node = true;
+ SASSERT(!m_free_nodes.contains(result));
+ SASSERT(m_nodes[result].m_index == result);
+ return result;
}
+ void bdd_manager::try_cnf_reorder(bdd const& b) {
+ m_cost_bdd = b.root;
+ m_cost_metric = cnf_cost;
+ try_reorder();
+ m_cost_metric = bdd_cost;
+ m_cost_bdd = 0;
+ }
+
void bdd_manager::try_reorder() {
+ gc();
+ for (auto* e : m_op_cache) {
+ m_alloc.deallocate(sizeof(*e), e);
+ }
+ m_op_cache.reset();
init_reorder();
for (unsigned i = 0; i < m_var2level.size(); ++i) {
sift_var(i);
}
+ SASSERT(m_op_cache.empty());
+ SASSERT(well_formed());
}
double bdd_manager::current_cost() {
-#if 0
-
-#endif
- return m_nodes.size() - m_free_nodes.size();
+ switch (m_cost_metric) {
+ case bdd_cost:
+ return m_nodes.size() - m_free_nodes.size();
+ case cnf_cost:
+ return cnf_size(m_cost_bdd);
+ case dnf_cost:
+ return dnf_size(m_cost_bdd);
+ default:
+ UNREACHABLE();
+ return 0;
+ }
}
bool bdd_manager::is_bad_cost(double current_cost, double best_cost) const {
@@ -306,9 +353,11 @@ namespace sat {
void bdd_manager::sift_up(unsigned lvl) {
if (m_level2nodes[lvl].empty()) return;
+ // VERIFY(well_formed());
// exchange level and level + 1.
m_S.reset();
m_T.reset();
+ m_to_free.reset();
m_disable_gc = true;
for (unsigned n : m_level2nodes[lvl + 1]) {
@@ -320,6 +369,8 @@ namespace sat {
m_S.push_back(n);
}
else {
+ reorder_decref(l);
+ reorder_decref(h);
m_T.push_back(n);
}
TRACE("bdd", tout << "remove " << n << "\n";);
@@ -331,14 +382,12 @@ namespace sat {
for (unsigned n : m_level2nodes[lvl]) {
bdd_node& node = m_nodes[n];
m_node_table.remove(node);
- if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) {
- TRACE("bdd", tout << "free " << n << "\n";);
- node.set_internal();
- m_free_nodes.push_back(n);
+ node.m_level = lvl + 1;
+ if (m_reorder_rc[n] == 0) {
+ m_to_free.push_back(n);
}
else {
TRACE("bdd", tout << "set level " << n << " to " << lvl + 1 << "\n";);
- node.m_level = lvl + 1;
m_node_table.insert(node);
m_level2nodes[lvl + 1].push_back(n);
}
@@ -352,19 +401,18 @@ namespace sat {
}
for (unsigned n : m_T) {
- TRACE("bdd", tout << "transform " << n << "\n";);
BDD l = lo(n);
BDD h = hi(n);
if (l == 0 && h == 0) continue;
BDD a, b, c, d;
- if (level(l) == lvl) {
+ if (level(l) == lvl + 1) {
a = lo(l);
b = hi(l);
}
else {
a = b = l;
}
- if (level(h) == lvl) {
+ if (level(h) == lvl + 1) {
c = lo(h);
d = hi(h);
}
@@ -375,15 +423,22 @@ namespace sat {
unsigned ac = make_node(lvl, a, c);
if (is_new_node()) {
m_level2nodes[lvl].push_back(ac);
- m_max_parent.setx(ac, lvl + 1, 0);
+ m_reorder_rc.reserve(ac+1);
+ reorder_incref(a);
+ reorder_incref(c);
}
unsigned bd = make_node(lvl, b, d);
if (is_new_node()) {
m_level2nodes[lvl].push_back(bd);
- m_max_parent.setx(bd, lvl + 1, 0);
+ m_reorder_rc.reserve(bd+1);
+ reorder_incref(b);
+ reorder_incref(d);
}
m_nodes[n].m_lo = ac;
m_nodes[n].m_hi = bd;
+ reorder_incref(ac);
+ reorder_incref(bd);
+ TRACE("bdd", tout << "transform " << n << " " << " " << a << " " << b << " " << c << " " << d << " " << ac << " " << bd << "\n";);
m_node_table.insert(m_nodes[n]);
}
unsigned v = m_level2var[lvl];
@@ -391,6 +446,30 @@ namespace sat {
std::swap(m_level2var[lvl], m_level2var[lvl+1]);
std::swap(m_var2level[v], m_var2level[w]);
m_disable_gc = false;
+
+ // add orphaned nodes to free-list
+ for (unsigned i = 0; i < m_to_free.size(); ++i) {
+ unsigned n = m_to_free[i];
+ bdd_node& node = m_nodes[n];
+ if (!node.is_internal()) {
+ VERIFY(!m_free_nodes.contains(n));
+ VERIFY(node.m_refcount == 0);
+ m_free_nodes.push_back(n);
+ m_node_table.remove(node);
+ BDD l = lo(n);
+ BDD h = hi(n);
+ node.set_internal();
+
+ reorder_decref(l);
+ if (!m_nodes[l].is_internal() && m_reorder_rc[l] == 0) {
+ m_to_free.push_back(l);
+ }
+ reorder_decref(h);
+ if (!m_nodes[h].is_internal() && m_reorder_rc[h] == 0) {
+ m_to_free.push_back(h);
+ }
+ }
+ }
TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); );
DEBUG_CODE(
for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
@@ -399,12 +478,24 @@ namespace sat {
SASSERT(node.m_level == i);
}
});
+
+ TRACE("bdd",
+ for (unsigned i = 0; i < m_nodes.size(); ++i) {
+ if (m_reorder_rc[i] != 0) {
+ tout << i << " " << m_reorder_rc[i] << "\n";
+ }});
+
+ // VERIFY(well_formed());
}
void bdd_manager::init_reorder() {
m_level2nodes.reset();
unsigned sz = m_nodes.size();
- m_max_parent.fill(sz, 0);
+ m_reorder_rc.fill(sz, 0);
+ for (unsigned i = 0; i < sz; ++i) {
+ if (m_nodes[i].m_refcount > 0)
+ m_reorder_rc[i] = UINT_MAX;
+ }
for (unsigned i = 0; i < sz; ++i) {
bdd_node const& n = m_nodes[i];
if (n.is_internal()) continue;
@@ -412,8 +503,8 @@ namespace sat {
SASSERT(i == m_nodes[i].m_index);
m_level2nodes.reserve(lvl + 1);
m_level2nodes[lvl].push_back(i);
- m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], lvl);
- m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], lvl);
+ reorder_incref(n.m_lo);
+ reorder_incref(n.m_hi);
}
TRACE("bdd",
display(tout);
@@ -421,11 +512,19 @@ namespace sat {
bdd_node const& n = m_nodes[i];
if (n.is_internal()) continue;
unsigned lvl = n.m_level;
- tout << "lvl: " << lvl << " parent: " << m_max_parent[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n";
+ tout << i << " lvl: " << lvl << " rc: " << m_reorder_rc[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n";
}
);
}
+ void bdd_manager::reorder_incref(unsigned n) {
+ if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]++;
+ }
+
+ void bdd_manager::reorder_decref(unsigned n) {
+ if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]--;
+ }
+
void bdd_manager::reserve_var(unsigned i) {
while (m_var2level.size() <= i) {
unsigned v = m_var2level.size();
@@ -455,9 +554,12 @@ namespace sat {
return bdd(mk_not_rec(b.root), this);
}
catch (mem_out) {
+ throw;
+#if 0
try_reorder();
if (!first) throw;
first = false;
+#endif
}
}
}
@@ -532,12 +634,13 @@ namespace sat {
push(mk_ite_rec(a1, b1, c1));
push(mk_ite_rec(a2, b2, c2));
r = make_node(lvl, read(2), read(1));
- pop(2);
+ pop(2);
e1->m_result = r;
return r;
}
bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) {
+ // VERIFY(well_formed());
return bdd(mk_quant(n, vars, b.root, bdd_or_op), this);
}
@@ -570,9 +673,11 @@ namespace sat {
bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op;
op_entry * e1 = pop_entry(a, b, q_op);
op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
- if (check_result(e1, e2, a, b, q_op))
+ if (check_result(e1, e2, a, b, q_op)) {
r = e2->m_result;
+ }
else {
+ VERIFY(e1->m_result == -1);
push(mk_quant_rec(l, lo(b), op));
push(mk_quant_rec(l, hi(b), op));
r = make_node(lvl, read(2), read(1));
@@ -580,26 +685,29 @@ namespace sat {
e1->m_result = r;
}
}
+ VERIFY(r != UINT_MAX);
return r;
}
- double bdd_manager::count(bdd const& b, unsigned z) {
+ double bdd_manager::count(BDD b, unsigned z) {
init_mark();
m_count.resize(m_nodes.size());
m_count[0] = z;
m_count[1] = 1-z;
set_mark(0);
set_mark(1);
- m_todo.push_back(b.root);
+ m_todo.push_back(b);
while (!m_todo.empty()) {
BDD r = m_todo.back();
if (is_marked(r)) {
m_todo.pop_back();
}
else if (!is_marked(lo(r))) {
+ VERIFY (is_const(r) || r != lo(r));
m_todo.push_back(lo(r));
}
else if (!is_marked(hi(r))) {
+ VERIFY (is_const(r) || r != hi(r));
m_todo.push_back(hi(r));
}
else {
@@ -608,7 +716,7 @@ namespace sat {
m_todo.pop_back();
}
}
- return m_count[b.root];
+ return m_count[b];
}
unsigned bdd_manager::bdd_size(bdd const& b) {
@@ -644,8 +752,8 @@ namespace sat {
}
void bdd_manager::gc() {
+ m_free_nodes.reset();
IF_VERBOSE(3, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";);
- SASSERT(m_free_nodes.empty());
svector<bool> reachable(m_nodes.size(), false);
for (unsigned i = m_bdd_stack.size(); i-- > 0; ) {
reachable[m_bdd_stack[i]] = true;
@@ -674,6 +782,7 @@ namespace sat {
for (unsigned i = m_nodes.size(); i-- > 2; ) {
if (!reachable[i]) {
m_nodes[i].set_internal();
+ VERIFY(m_nodes[i].m_refcount == 0);
m_free_nodes.push_back(i);
}
}
@@ -681,10 +790,25 @@ namespace sat {
std::sort(m_free_nodes.begin(), m_free_nodes.end());
m_free_nodes.reverse();
- for (auto* e : m_op_cache) {
- m_alloc.deallocate(sizeof(*e), e);
+ ptr_vector<op_entry> to_delete, to_keep;
+ for (auto* e : m_op_cache) {
+ // std::cout << "check: " << e << "\n";
+ if (!reachable[e->m_bdd1] || !reachable[e->m_bdd2] || !reachable[e->m_op] || (e->m_result != -1 && !reachable[e->m_result])) {
+ to_delete.push_back(e);
+ }
+ else {
+ to_keep.push_back(e);
+ }
}
m_op_cache.reset();
+ for (op_entry* e : to_delete) {
+ // std::cout << "erase: " << e << "\n";
+ m_alloc.deallocate(sizeof(*e), e);
+ }
+ for (op_entry* e : to_keep) {
+ m_op_cache.insert(e);
+ }
+
m_node_table.reset();
// re-populate node cache
for (unsigned i = m_nodes.size(); i-- > 2; ) {
@@ -693,6 +817,7 @@ namespace sat {
m_node_table.insert(m_nodes[i]);
}
}
+ SASSERT(well_formed());
}
void bdd_manager::init_mark() {
@@ -707,6 +832,7 @@ namespace sat {
std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) {
init_mark();
m_todo.push_back(b.root);
+ m_reorder_rc.reserve(m_nodes.size());
while (!m_todo.empty()) {
BDD r = m_todo.back();
if (is_marked(r)) {
@@ -723,7 +849,7 @@ namespace sat {
m_todo.push_back(hi(r));
}
else {
- out << r << " : " << var(r) << " " << lo(r) << " " << hi(r) << "\n";
+ out << r << " : " << var(r) << " @ " << level(r) << " " << lo(r) << " " << hi(r) << " " << m_reorder_rc[r] << "\n";
set_mark(r);
m_todo.pop_back();
}
@@ -731,30 +857,52 @@ namespace sat {
return out;
}
- void bdd_manager::well_formed() {
+ bool bdd_manager::well_formed() {
for (unsigned n : m_free_nodes) {
- VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0);
+ if (!(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0)) {
+ std::cout << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n";
+ display(std::cout);
+ UNREACHABLE();
+ }
}
for (bdd_node const& n : m_nodes) {
if (n.is_internal()) continue;
unsigned lvl = n.m_level;
BDD lo = n.m_lo;
BDD hi = n.m_hi;
+ if (!is_const(lo) && level(lo) >= lvl) {
+ std::cout << n.m_index << " lo: " << lo << "\n";
+ display(std::cout);
+ }
VERIFY(is_const(lo) || level(lo) < lvl);
+ if (!is_const(hi) && level(hi) >= lvl) {
+ std::cout << n.m_index << " hi: " << hi << "\n";
+ display(std::cout);
+ }
VERIFY(is_const(hi) || level(hi) < lvl);
+ if (!is_const(lo) && m_nodes[lo].is_internal()) {
+ std::cout << n.m_index << " lo: " << lo << "\n";
+ display(std::cout);
+ }
+ if (!is_const(hi) && m_nodes[hi].is_internal()) {
+ std::cout << n.m_index << " hi: " << hi << "\n";
+ display(std::cout);
+ }
+ VERIFY(is_const(lo) || !m_nodes[lo].is_internal());
+ VERIFY(is_const(hi) || !m_nodes[hi].is_internal());
}
+ return true;
}
std::ostream& bdd_manager::display(std::ostream& out) {
+ m_reorder_rc.reserve(m_nodes.size());
for (unsigned i = 0; i < m_nodes.size(); ++i) {
bdd_node const& n = m_nodes[i];
if (n.is_internal()) continue;
- out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n";
+ out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << " rc " << m_reorder_rc[i] << "\n";
}
for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
- out << i << " : ";
- for (unsigned l : m_level2nodes[i]) out << l << " ";
- out << "\n";
+ out << "level: " << i << " : " << m_level2nodes[i] << "\n";
}
return out;
}
diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h
index 41e45c822..41d1115b9 100644
--- a/src/sat/sat_bdd.h
+++ b/src/sat/sat_bdd.h
@@ -50,7 +50,7 @@ namespace sat {
m_hi(hi),
m_index(0)
{}
- bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {}
+ bdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {}
unsigned m_refcount : 10;
unsigned m_level : 22;
BDD m_lo;
@@ -58,7 +58,13 @@ namespace sat {
unsigned m_index;
unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); }
bool is_internal() const { return m_lo == 0 && m_hi == 0; }
- void set_internal() { m_lo = m_hi = 0; }
+ void set_internal() { m_lo = 0; m_hi = 0; }
+ };
+
+ enum cost_metric {
+ cnf_cost,
+ dnf_cost,
+ bdd_cost
};
struct hash_node {
@@ -94,7 +100,7 @@ namespace sat {
struct eq_entry {
bool operator()(op_entry * a, op_entry * b) const {
- return a->hash() == b->hash();
+ return a->m_bdd1 == b->m_bdd2 && a->m_bdd2 == b->m_bdd2 && a->m_op == b->m_op;
}
};
@@ -117,9 +123,11 @@ namespace sat {
bool m_disable_gc;
bool m_is_new_node;
unsigned m_max_num_bdd_nodes;
- unsigned_vector m_S, m_T; // used for reordering
+ unsigned_vector m_S, m_T, m_to_free; // used for reordering
vector<unsigned_vector> m_level2nodes;
- unsigned_vector m_max_parent;
+ unsigned_vector m_reorder_rc;
+ cost_metric m_cost_metric;
+ BDD m_cost_bdd;
BDD make_node(unsigned level, BDD l, BDD r);
bool is_new_node() const { return m_is_new_node; }
@@ -141,15 +149,16 @@ namespace sat {
void push_entry(op_entry* e);
bool check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c);
- double count(bdd const& b, unsigned z);
+ double count(BDD b, unsigned z);
- void gc();
void alloc_free_nodes(unsigned n);
void init_mark();
void set_mark(unsigned i) { m_mark[i] = m_mark_level; }
bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
void init_reorder();
+ void reorder_incref(unsigned n);
+ void reorder_decref(unsigned n);
void sift_up(unsigned level);
void sift_var(unsigned v);
double current_cost();
@@ -166,12 +175,12 @@ namespace sat {
inline unsigned var(BDD b) const { return m_level2var[level(b)]; }
inline BDD lo(BDD b) const { return m_nodes[b].m_lo; }
inline BDD hi(BDD b) const { return m_nodes[b].m_hi; }
- inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; }
- inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; }
+ inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; VERIFY(!m_free_nodes.contains(b)); }
+ inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; VERIFY(!m_free_nodes.contains(b)); }
inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; }
- double dnf_size(bdd const& b) { return count(b, 0); }
- double cnf_size(bdd const& b) { return count(b, 1); }
+ double dnf_size(BDD b) { return count(b, 0); }
+ double cnf_size(BDD b) { return count(b, 1); }
unsigned bdd_size(bdd const& b);
bdd mk_not(bdd b);
@@ -180,7 +189,7 @@ namespace sat {
bdd mk_xor(bdd const& a, bdd const& b);
void reserve_var(unsigned v);
- void well_formed();
+ bool well_formed();
public:
struct mem_out {};
@@ -205,7 +214,9 @@ namespace sat {
std::ostream& display(std::ostream& out);
std::ostream& display(std::ostream& out, bdd const& b);
+ void gc();
void try_reorder();
+ void try_cnf_reorder(bdd const& b);
};
class bdd {
@@ -234,8 +245,8 @@ namespace sat {
std::ostream& display(std::ostream& out) const { return m->display(out, *this); }
bool operator==(bdd const& other) const { return root == other.root; }
bool operator!=(bdd const& other) const { return root != other.root; }
- double cnf_size() const { return m->cnf_size(*this); }
- double dnf_size() const { return m->dnf_size(*this); }
+ double cnf_size() const { return m->cnf_size(root); }
+ double dnf_size() const { return m->dnf_size(root); }
unsigned bdd_size() const { return m->bdd_size(*this); }
};
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 6edc125ea..99c15c247 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -26,6 +26,7 @@ namespace sat{
elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) {
m_mark_lim = 0;
m_max_literals = 11;
+ m_miss = 0;
}
bool elim_vars::operator()(bool_var v) {
@@ -57,10 +58,11 @@ namespace sat{
double sz1 = b1.cnf_size();
if (sz1 > 2*clause_size) {
return false;
- }
+ }
if (sz1 <= clause_size) {
return elim_var(v, b1);
}
+
m_vars.reverse();
bdd b2 = elim_var(v);
double sz2 = b2.cnf_size();
@@ -73,6 +75,11 @@ namespace sat{
if (sz3 <= clause_size) {
return elim_var(v, b3);
}
+#if 0
+ m.try_cnf_reorder(b3);
+ sz3 = b3.cnf_size();
+ if (sz3 <= clause_size) ++m_miss;
+#endif
return false;
}
diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h
index 8893bbc40..e4843c41c 100644
--- a/src/sat/sat_elim_vars.h
+++ b/src/sat/sat_elim_vars.h
@@ -40,6 +40,7 @@ namespace sat {
unsigned m_mark_lim;
unsigned_vector m_var2index;
unsigned_vector m_occ;
+ unsigned m_miss;
unsigned m_max_literals;
@@ -61,6 +62,7 @@ namespace sat {
public:
elim_vars(simplifier& s);
bool operator()(bool_var v);
+ unsigned miss() const { return m_miss; }
};
};
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 5c039f664..be698fc46 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -412,11 +412,17 @@ namespace sat {
for (literal l1 : m_trail) {
SASSERT(is_true(l1));
for (literal l2 : m_binary[l1.index()]) {
+ VERIFY(is_true(l2));
if (is_undef(l2)) return true;
}
unsigned sz = m_ternary_count[(~l1).index()];
for (binary b : m_ternary[(~l1).index()]) {
if (sz-- == 0) break;
+ if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) {
+ std::cout << b.m_u << " " << b.m_v << "\n";
+ std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";
+ UNREACHABLE();
+ }
if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
return true;
}
@@ -424,6 +430,7 @@ namespace sat {
for (nary * n : m_nary_clauses) {
if (n->size() == 1 && !is_true(n->get_head())) {
for (literal lit : *n) {
+ VERIFY(!is_undef(lit));
if (is_undef(lit)) return true;
}
}
@@ -1743,74 +1750,10 @@ namespace sat {
bool lookahead::check_autarky(literal l, unsigned level) {
return false;
-#if 0
- // no propagations are allowed to reduce clauses.
- for (nary * cp : m_nary[(~l).index()]) {
- clause& c = *cp;
- unsigned sz = c.size();
- bool found = false;
- for (unsigned i = 0; !found && i < sz; ++i) {
- found = is_true(c[i]);
- if (found) {
- TRACE("sat", tout << c[i] << " is true in " << c << "\n";);
- }
- }
- IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";);
- if (!found) return false;
- }
- //
- // bail out if there is a pending binary propagation.
- // In general, we would have to check, recursively that
- // a binary propagation does not create reduced clauses.
- //
- literal_vector const& lits = m_binary[l.index()];
- TRACE("sat", tout << l << ": " << lits << "\n";);
- for (unsigned i = 0; i < lits.size(); ++i) {
- literal l2 = lits[i];
- if (is_true(l2)) continue;
- SASSERT(!is_false(l2));
- return false;
- }
-
- return true;
-#endif
}
-
- void lookahead::update_lookahead_reward(literal l, unsigned level) {
- if (m_lookahead_reward == 0) {
- if (!check_autarky(l, level)) {
- // skip
- }
- else if (get_lookahead_reward(l) == 0) {
- ++m_stats.m_autarky_propagations;
- IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
-
- TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
- << " "
- << (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
- lookahead_backtrack();
- assign(l);
- propagate();
- }
- else {
- ++m_stats.m_autarky_equivalences;
- // l => p is known, but p => l is possibly not.
- // add p => l.
- // justification: any consequence of l
- // that is not a consequence of p does not
- // reduce the clauses.
- literal p = get_parent(l);
- SASSERT(p != null_literal);
- if (m_stamp[p.var()] > m_stamp[l.var()]) {
- TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout););
- IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";);
- add_binary(~l, p);
- set_level(l, p);
- }
- }
- }
- else {
+ void lookahead::update_lookahead_reward(literal l, unsigned level) {
+ if (m_lookahead_reward != 0) {
inc_lookahead_reward(l, m_lookahead_reward);
}
}
@@ -1852,7 +1795,6 @@ namespace sat {
literal last_changed = null_literal;
unsigned num_iterations = 0;
while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
- change = false;
num_iterations++;
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
literal lit = m_lookahead[i].m_lit;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index d30485254..64a4ef63e 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -247,6 +247,7 @@ namespace sat {
inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); }
inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
+ unsigned get_level(literal d) const { return m_stamp[d.var()]; }
lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; }
// set the level within a scope of the search.
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b967ade06..b1f0431cc 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1657,6 +1657,7 @@ namespace sat {
bool_var_vector vars;
order_vars_for_elim(vars);
sat::elim_vars elim_bdd(*this);
+ unsigned bdd_vars = 0;
for (bool_var v : vars) {
checkpoint();
@@ -1665,10 +1666,13 @@ namespace sat {
if (try_eliminate(v)) {
m_num_elim_vars++;
}
- else if (elim_bdd(v)) {
+ else if (false && elim_bdd(v)) {
m_num_elim_vars++;
+ ++bdd_vars;
}
}
+ std::cout << "bdd elim: " << bdd_vars << "\n";
+ std::cout << "bdd miss: " << elim_bdd.miss() << "\n";
m_pos_cls.finalize();
m_neg_cls.finalize();
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
index b60522740..ea5a0bc34 100644
--- a/src/test/bdd.cpp
+++ b/src/test/bdd.cpp
@@ -67,6 +67,7 @@ namespace sat {
std::cout << "before reorder:\n";
std::cout << c1 << "\n";
std::cout << c1.bdd_size() << "\n";
+ m.gc();
m.try_reorder();
std::cout << "after reorder:\n";
std::cout << c1 << "\n";
diff --git a/src/util/vector.h b/src/util/vector.h
index c60585512..f068481db 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -472,6 +472,11 @@ typedef svector<char> char_vector;
typedef svector<signed char> signed_char_vector;
typedef svector<double> double_vector;
+inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) {
+ for (unsigned u : v) out << u << " ";
+ return out;
+}
+
template<typename Hash, typename Vec>
struct vector_hash_tpl {
Hash m_hash;