mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-10-18 08:57:43 -07:00
parent edea879864 80f24c29ab
commit 6155362571
6 changed files with 252 additions and 117 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

145
src/sat/sat_bdd.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include "sat/sat_bdd.h"
#include "util/trace.h"
namespace sat {
@ -48,12 +49,7 @@ namespace sat {
// add variables
for (unsigned i = 0; i < num_vars; ++i) {
m_var2bdd.push_back(make_node(i, false_bdd, true_bdd));
m_var2bdd.push_back(make_node(i, true_bdd, false_bdd));
m_nodes[m_var2bdd[2*i]].m_refcount = max_rc;
m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc;
m_var2level.push_back(i);
m_level2var.push_back(i);
reserve_var(i);
}
}
@ -73,8 +69,8 @@ namespace sat {
return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd;
case bdd_or_op:
return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd;
case bdd_iff_op:
return (a == b) ? true_bdd : false_bdd;
case bdd_xor_op:
return (a == b) ? false_bdd : true_bdd;
default:
return false_bdd;
}
@ -99,7 +95,7 @@ namespace sat {
bdd bdd_manager::mk_false() { return bdd(false_bdd, this); }
bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
bdd bdd_manager::mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
bdd bdd_manager::mk_xor(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_xor_op), this); }
bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); }
bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); }
@ -132,10 +128,10 @@ namespace sat {
if (is_false(b)) return a;
if (is_true(a) || is_true(b)) return true_bdd;
break;
case bdd_iff_op:
if (a == b) return true_bdd;
if (is_true(a)) return b;
if (is_true(b)) return a;
case bdd_xor_op:
if (a == b) return false_bdd;
if (is_false(a)) return b;
if (is_false(b)) return a;
break;
default:
UNREACHABLE();
@ -265,9 +261,9 @@ namespace sat {
goto go_down;
}
go_up:
TRACE("bdd", tout << "sift up " << lvl << "\n";);
while (lvl < max_lvl) {
sift_up(lvl);
++lvl;
sift_up(lvl++);
double cost = current_cost();
if (is_bad_cost(cost, best_cost)) break;
best_cost = std::min(cost, best_cost);
@ -275,22 +271,20 @@ namespace sat {
if (first) {
first = false;
while (lvl != start) {
sift_up(lvl-1);
--lvl;
sift_up(--lvl);
}
goto go_down;
}
else {
while (current_cost() != best_cost) {
sift_up(lvl-1);
--lvl;
sift_up(--lvl);
}
return;
}
go_down:
TRACE("bdd", tout << "sift down " << lvl << "\n";);
while (lvl > 0) {
sift_up(lvl-1);
--lvl;
sift_up(--lvl);
double cost = current_cost();
if (is_bad_cost(cost, best_cost)) break;
best_cost = std::min(cost, best_cost);
@ -298,15 +292,13 @@ namespace sat {
if (first) {
first = false;
while (lvl != start) {
sift_up(lvl);
++lvl;
sift_up(lvl++);
}
goto go_up;
}
else {
while (current_cost() != best_cost) {
sift_up(lvl);
++lvl;
sift_up(lvl++);
}
return;
}
@ -330,30 +322,37 @@ namespace sat {
else {
m_T.push_back(n);
}
TRACE("bdd", tout << "remove " << n << "\n";);
m_node_table.remove(m_nodes[n]);
}
m_level2nodes[lvl + 1].reset();
m_level2nodes[lvl + 1].append(m_T);
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);
}
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);
}
}
m_level2nodes[lvl].reset();
m_level2nodes[lvl].append(m_S);
for (unsigned n : m_S) {
m_nodes[n].m_level = lvl;
m_node_table.insert(m_nodes[n]);
}
std::swap(m_level2nodes[lvl], m_level2nodes[lvl + 1]);
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;
@ -392,6 +391,14 @@ namespace sat {
std::swap(m_level2var[lvl], m_level2var[lvl+1]);
std::swap(m_var2level[v], m_var2level[w]);
m_disable_gc = false;
TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); );
DEBUG_CODE(
for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
for (unsigned n : m_level2nodes[i]) {
bdd_node const& node = m_nodes[n];
SASSERT(node.m_level == i);
}
});
}
void bdd_manager::init_reorder() {
@ -403,18 +410,41 @@ namespace sat {
if (n.is_internal()) continue;
unsigned lvl = n.m_level;
SASSERT(i == m_nodes[i].m_index);
while (m_level2nodes.size() <= lvl) m_level2nodes.push_back(unsigned_vector());
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);
}
TRACE("bdd",
display(tout);
for (unsigned i = 0; i < sz; ++i) {
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";
}
);
}
void bdd_manager::reserve_var(unsigned i) {
while (m_var2level.size() <= i) {
unsigned v = m_var2level.size();
m_var2bdd.push_back(make_node(v, false_bdd, true_bdd));
m_var2bdd.push_back(make_node(v, true_bdd, false_bdd));
m_nodes[m_var2bdd[2*v]].m_refcount = max_rc;
m_nodes[m_var2bdd[2*v+1]].m_refcount = max_rc;
m_var2level.push_back(v);
m_level2var.push_back(v);
}
}
bdd bdd_manager::mk_var(unsigned i) {
reserve_var(i);
return bdd(m_var2bdd[2*i], this);
}
bdd bdd_manager::mk_nvar(unsigned i) {
reserve_var(i);
return bdd(m_var2bdd[2*i+1], this);
}
@ -581,6 +611,29 @@ namespace sat {
return m_count[b.root];
}
unsigned bdd_manager::bdd_size(bdd const& b) {
init_mark();
set_mark(0);
set_mark(1);
unsigned sz = 0;
m_todo.push_back(b.root);
while (!m_todo.empty()) {
BDD r = m_todo.back();
m_todo.pop_back();
if (!is_marked(r)) {
++sz;
set_mark(r);
if (!is_marked(lo(r))) {
m_todo.push_back(lo(r));
}
if (!is_marked(hi(r))) {
m_todo.push_back(hi(r));
}
}
}
return sz;
}
void bdd_manager::alloc_free_nodes(unsigned n) {
for (unsigned i = 0; i < n; ++i) {
m_free_nodes.push_back(m_nodes.size());
@ -678,31 +731,35 @@ namespace sat {
return out;
}
void bdd_manager::well_formed() {
for (unsigned n : m_free_nodes) {
VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0);
}
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;
VERIFY(is_const(lo) || level(lo) < lvl);
VERIFY(is_const(hi) || level(hi) < lvl);
}
}
std::ostream& bdd_manager::display(std::ostream& out) {
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";
}
for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
out << i << " : ";
for (unsigned l : m_level2nodes[i]) out << l << " ";
out << "\n";
}
return out;
}
bdd::bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
bdd::bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); }
bdd::~bdd() { m->dec_ref(root); }
bdd bdd::lo() const { return bdd(m->lo(root), m); }
bdd bdd::hi() const { return bdd(m->hi(root), m); }
unsigned bdd::var() const { return m->var(root); }
bool bdd::is_true() const { return root == bdd_manager::true_bdd; }
bool bdd::is_false() const { return root == bdd_manager::false_bdd; }
bdd bdd::operator!() { return m->mk_not(*this); }
bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); }
bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); }
bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; }
std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); }
std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
double bdd::cnf_size() const { return m->cnf_size(*this); }
double bdd::dnf_size() const { return m->dnf_size(*this); }
}

46
src/sat/sat_bdd.h
View file

@ -35,7 +35,7 @@ namespace sat {
enum bdd_op {
bdd_and_op = 2,
bdd_or_op = 3,
bdd_iff_op = 4,
bdd_xor_op = 4,
bdd_not_op = 5,
bdd_and_proj_op = 6,
bdd_or_proj_op = 7,
@ -149,7 +149,6 @@ namespace sat {
void set_mark(unsigned i) { m_mark[i] = m_mark_level; }
bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
void try_reorder();
void init_reorder();
void sift_up(unsigned level);
void sift_var(unsigned v);
@ -173,10 +172,15 @@ namespace sat {
double dnf_size(bdd const& b) { return count(b, 0); }
double cnf_size(bdd const& b) { return count(b, 1); }
unsigned bdd_size(bdd const& b);
bdd mk_not(bdd b);
bdd mk_and(bdd const& a, bdd const& b);
bdd mk_or(bdd const& a, bdd const& b);
bdd mk_xor(bdd const& a, bdd const& b);
void reserve_var(unsigned v);
void well_formed();
public:
struct mem_out {};
@ -196,39 +200,43 @@ namespace sat {
bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b);
bdd mk_exists(unsigned v, bdd const& b);
bdd mk_forall(unsigned v, bdd const& b);
bdd mk_iff(bdd const& a, bdd const& b);
bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
std::ostream& display(std::ostream& out);
std::ostream& display(std::ostream& out, bdd const& b);
void try_reorder();
};
class bdd {
friend class bdd_manager;
unsigned root;
bdd_manager* m;
bdd(unsigned root, bdd_manager* m);
bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
public:
bdd(bdd & other);
bdd(bdd && other);
bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); }
bdd& operator=(bdd const& other);
~bdd();
bdd lo() const;
bdd hi() const;
unsigned var() const;
bool is_true() const;
bool is_false() const;
bdd operator!();
bdd operator&&(bdd const& other);
bdd operator||(bdd const& other);
~bdd() { m->dec_ref(root); }
bdd lo() const { return bdd(m->lo(root), m); }
bdd hi() const { return bdd(m->hi(root), m); }
unsigned var() const { return m->var(root); }
bool is_true() const { return root == bdd_manager::true_bdd; }
bool is_false() const { return root == bdd_manager::false_bdd; }
bdd operator!() { return m->mk_not(*this); }
bdd operator&&(bdd const& other) { return m->mk_and(*this, other); }
bdd operator||(bdd const& other) { return m->mk_or(*this, other); }
bdd operator^(bdd const& other) { return m->mk_xor(*this, other); }
bdd operator|=(bdd const& other) { return *this = *this || other; }
bdd operator&=(bdd const& other) { return *this = *this && other; }
std::ostream& display(std::ostream& out) const;
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;
double dnf_size() const;
double cnf_size() const { return m->cnf_size(*this); }
double dnf_size() const { return m->dnf_size(*this); }
unsigned bdd_size() const { return m->bdd_size(*this); }
};
std::ostream& operator<<(std::ostream& out, bdd const& b);

22
src/sat/sat_model_converter.cpp
View file

@ -38,16 +38,15 @@ namespace sat {
return *this;
}
void model_converter::process_stack(model & m, literal_vector const& stack) const {
void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
SASSERT(!stack.empty());
unsigned sz = stack.size();
SASSERT(stack[sz - 1] == null_literal);
for (unsigned i = sz - 1; i-- > 0; ) {
literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated
for (unsigned i = sz; i-- > 0; ) {
unsigned csz = stack[i].first;
literal lit = stack[i].second;
bool sat = false;
for (; i > 0 && stack[--i] != null_literal;) {
if (sat) continue;
sat = value_at(stack[i], m) == l_true;
for (unsigned j = 0; !sat && j < csz; ++j) {
sat = value_at(c[j], m) == l_true;
}
if (!sat) {
m[lit.var()] = lit.sign() ? l_false : l_true;
@ -66,6 +65,7 @@ namespace sat {
bool sat = false;
bool var_sign = false;
unsigned index = 0;
literal_vector clause;
for (literal l : it->m_clauses) {
if (l == null_literal) {
// end of clause
@ -74,13 +74,15 @@ namespace sat {
}
elim_stack* s = it->m_elim_stack[index];
if (s) {
process_stack(m, s->stack());
process_stack(m, clause, s->stack());
}
sat = false;
++index;
clause.reset();
continue;
}
clause.push_back(l);
if (sat)
continue;
bool sign = l.sign();
@ -190,13 +192,13 @@ namespace sat {
// TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
}
void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) {
void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) {
SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
SASSERT(m_entries.begin() <= &e);
SASSERT(&e < m_entries.end());
for (literal l : c) e.m_clauses.push_back(l);
e.m_clauses.push_back(null_literal);
e.m_elim_stack.push_back(alloc(elim_stack, elims));
e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
}

12
src/sat/sat_model_converter.h
View file

@ -39,18 +39,20 @@ namespace sat {
class model_converter {
public:
typedef svector<std::pair<unsigned, literal>> elim_stackv;
class elim_stack {
unsigned m_refcount;
literal_vector m_stack;
elim_stackv m_stack;
public:
elim_stack(literal_vector const& stack):
elim_stack(elim_stackv const& stack):
m_refcount(0),
m_stack(stack) {
}
~elim_stack() { }
void inc_ref() { ++m_refcount; }
void dec_ref() { if (0 == --m_refcount) dealloc(this); }
literal_vector const& stack() const { return m_stack; }
elim_stackv const& stack() const { return m_stack; }
};
enum kind { ELIM_VAR = 0, BLOCK_LIT };
@ -74,7 +76,7 @@ namespace sat {
private:
vector<entry> m_entries;
void process_stack(model & m, literal_vector const& stack) const;
void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
public:
model_converter();
@ -86,7 +88,7 @@ namespace sat {
void insert(entry & e, clause const & c);
void insert(entry & e, literal l1, literal l2);
void insert(entry & e, clause_wrapper const & c);
void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack);
void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack);
bool empty() const { return m_entries.empty(); }

128
src/sat/sat_simplifier.cpp
View file

@ -965,6 +965,7 @@ namespace sat {
literal l = m_queue.next();
process(l);
}
cce();
}
//
@ -1027,55 +1028,106 @@ namespace sat {
literal_vector m_covered_clause;
literal_vector m_intersection;
literal_vector m_elim_stack;
sat::model_converter::elim_stackv m_elim_stack;
unsigned m_ala_qhead;
bool cla(literal lit) {
/*
* C \/ l l \/ lit
* -------------------
* C \/ l \/ ~lit
*/
void add_ala() {
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
literal l = m_covered_clause[m_ala_qhead];
for (watched & w : s.get_wlist(~l)) {
if (w.is_binary_clause()) {
literal lit = w.get_literal();
if (!s.is_marked(lit) && !s.is_marked(~lit)) {
//std::cout << "ALA " << ~lit << "\n";
m_covered_clause.push_back(~lit);
s.mark_visited(~lit);
}
}
}
}
}
bool add_cla(literal& blocked) {
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
m_intersection.reset();
if (ri(m_covered_clause[i], m_intersection)) {
blocked = m_covered_clause[i];
return true;
}
for (literal l : m_intersection) {
if (!s.is_marked(l)) {
s.mark_visited(l);
m_covered_clause.push_back(l);
}
}
if (!m_intersection.empty()) {
m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
}
}
return false;
}
bool cla(literal& blocked) {
bool is_tautology = false;
for (literal l : m_covered_clause) s.mark_visited(l);
unsigned num_iterations = 0, sz;
m_elim_stack.reset();
m_ala_qhead = 0;
do {
++num_iterations;
sz = m_covered_clause.size();
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
m_intersection.reset();
if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) {
is_tautology = true;
break;
}
for (literal l : m_intersection) {
if (!s.is_marked(l)) {
s.mark_visited(l);
m_covered_clause.push_back(l);
}
}
if (!m_intersection.empty()) {
m_elim_stack.append(m_covered_clause); // the current clause
m_elim_stack.push_back(m_covered_clause[i]); // the pivot literal
m_elim_stack.push_back(null_literal); // null demarcation
}
do {
++num_iterations;
sz = m_covered_clause.size();
is_tautology = add_cla(blocked);
}
while (m_covered_clause.size() > sz && !is_tautology);
break;
//if (is_tautology) break;
//sz = m_covered_clause.size();
// unsound? add_ala();
}
while (m_covered_clause.size() > sz && !is_tautology);
while (m_covered_clause.size() > sz);
for (literal l : m_covered_clause) s.unmark_visited(l);
if (is_tautology) std::cout << "taut: " << num_iterations << "\n";
// if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
return is_tautology;
}
// perform covered clause elimination.
// first extract the covered literal addition (CLA).
// then check whether the CLA is blocked.
bool cce(clause& c, literal lit) {
bool cce(clause& c, literal& blocked) {
m_covered_clause.reset();
for (literal l : c) m_covered_clause.push_back(l);
return cla(lit);
return cla(blocked);
}
bool cce(literal lit, literal l2) {
bool cce(literal lit, literal l2, literal& blocked) {
m_covered_clause.reset();
m_covered_clause.push_back(lit);
m_covered_clause.push_back(l2);
return cla(lit);
return cla(blocked);
}
void cce() {
m_to_remove.reset();
literal blocked;
for (clause* cp : s.s.m_clauses) {
clause& c = *cp;
if (c.was_removed()) continue;
if (cce(c, blocked)) {
model_converter::entry * new_entry = 0;
block_covered_clause(c, blocked, new_entry);
s.m_num_covered_clauses++;
}
}
for (clause* c : m_to_remove) {
s.remove_clause(*c);
}
m_to_remove.reset();
}
void process(literal l) {
@ -1085,6 +1137,7 @@ namespace sat {
return;
}
literal blocked = null_literal;
m_to_remove.reset();
{
clause_use_list & occs = s.m_use_list.get(l);
@ -1095,14 +1148,10 @@ namespace sat {
SASSERT(c.contains(l));
s.mark_all_but(c, l);
if (all_tautology(l)) {
s.unmark_all(c);
block_clause(c, l, new_entry);
s.m_num_blocked_clauses++;
}
else if (cce(c, l)) {
block_covered_clause(c, l, new_entry);
s.m_num_covered_clauses++;
}
s.unmark_all(c);
it.next();
}
}
@ -1127,8 +1176,9 @@ namespace sat {
block_binary(it, l, new_entry);
s.m_num_blocked_clauses++;
}
else if (cce(l, l2)) {
block_covered_binary(it, l, new_entry);
else if (cce(l, l2, blocked)) {
model_converter::entry * blocked_entry = 0;
block_covered_binary(it, l, blocked, blocked_entry);
s.m_num_covered_clauses++;
}
else {
@ -1163,9 +1213,9 @@ namespace sat {
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
if (new_entry == 0)
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var()));
literal l2 = it->get_literal();
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
s.remove_bin_clause_half(l2, l, it->is_learned());
@ -1173,12 +1223,12 @@ namespace sat {
}
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
prepare_block_binary(it, l, new_entry);
prepare_block_binary(it, l, l, new_entry);
mc.insert(*new_entry, l, it->get_literal());
}
void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
prepare_block_binary(it, l, new_entry);
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
prepare_block_binary(it, l, blocked, new_entry);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}

16
src/test/bdd.cpp
View file

@ -57,10 +57,26 @@ namespace sat {
c2 = m.mk_exists(2, c1);
SASSERT(c2 == ((v0 && v1) || v1 || !v0));
}
void test4() {
bdd_manager m(3);
bdd v0 = m.mk_var(0);
bdd v1 = m.mk_var(1);
bdd v2 = m.mk_var(2);
bdd c1 = (v0 && v2) || v1;
std::cout << "before reorder:\n";
std::cout << c1 << "\n";
std::cout << c1.bdd_size() << "\n";
m.try_reorder();
std::cout << "after reorder:\n";
std::cout << c1 << "\n";
std::cout << c1.bdd_size() << "\n";
}
}
void tst_bdd() {
sat::test1();
sat::test2();
sat::test3();
sat::test4();
}