mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 13:58:45 +00:00
adding bdd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4f7147dd78
commit
64ea473bc7
|
|
@ -3,6 +3,7 @@ z3_add_component(sat
|
|||
ba_solver.cpp
|
||||
dimacs.cpp
|
||||
sat_asymm_branch.cpp
|
||||
sat_bdd.cpp
|
||||
sat_clause.cpp
|
||||
sat_clause_set.cpp
|
||||
sat_clause_use_list.cpp
|
||||
|
|
|
|||
260
src/sat/sat_bdd.cpp
Normal file
260
src/sat/sat_bdd.cpp
Normal file
|
|
@ -0,0 +1,260 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_bdd.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Simple BDD package modeled after BuDDy, which is modeled after CUDD.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2017-10-13
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/sat_bdd.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
bdd_manager::bdd_manager(unsigned num_vars, unsigned cache_size) {
|
||||
for (BDD a = 0; a < 2; ++a) {
|
||||
for (BDD b = 0; b < 2; ++b) {
|
||||
for (unsigned op = bdd_and_op; op < bdd_no_op; ++op) {
|
||||
unsigned index = a + 2*b + 4*op;
|
||||
m_apply_const.reserve(index+1);
|
||||
m_apply_const[index] = apply_const(a, b, static_cast<bdd_op>(op));
|
||||
}
|
||||
}
|
||||
}
|
||||
// add two dummy nodes for true_bdd and false_bdd
|
||||
m_nodes.push_back(bdd_node(0,0,0));
|
||||
m_nodes.push_back(bdd_node(0,0,0));
|
||||
m_nodes[0].m_refcount = max_rc;
|
||||
m_nodes[1].m_refcount = max_rc;
|
||||
|
||||
// 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);
|
||||
}
|
||||
|
||||
m_spare_entry = nullptr;
|
||||
}
|
||||
|
||||
bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) {
|
||||
switch (op) {
|
||||
case bdd_and_op:
|
||||
return (a == 1 && b == 1) ? 1 : 0;
|
||||
case bdd_or_op:
|
||||
return (a == 1 || b == 1) ? 1 : 0;
|
||||
case bdd_iff_op:
|
||||
return (a == b) ? 1 : 0;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) {
|
||||
return apply_rec(arg1, arg2, op);
|
||||
}
|
||||
|
||||
bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) {
|
||||
switch (op) {
|
||||
case bdd_and_op:
|
||||
if (a == b) return a;
|
||||
if (is_false(a) || is_false(b)) return false_bdd;
|
||||
if (is_true(a)) return b;
|
||||
if (is_true(b)) return a;
|
||||
break;
|
||||
case bdd_or_op:
|
||||
if (a == b) return a;
|
||||
if (is_false(a)) return b;
|
||||
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;
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
if (is_const(a) && is_const(b)) {
|
||||
return m_apply_const[a + 2*b + 4*op];
|
||||
}
|
||||
cache_entry * e1 = pop_entry(hash2(a, b, op));
|
||||
cache_entry const* e2 = m_cache.insert_if_not_there(e1);
|
||||
if (e2->m_op == op && e2->m_bdd1 == a && e2->m_bdd2 == b) {
|
||||
push_entry(e1);
|
||||
return e2->m_result;
|
||||
}
|
||||
BDD r;
|
||||
if (level(a) == level(b)) {
|
||||
push(apply_rec(lo(a), lo(b), op));
|
||||
push(apply_rec(hi(a), hi(b), op));
|
||||
r = make_node(level(a), read(2), read(1));
|
||||
}
|
||||
else if (level(a) < level(b)) {
|
||||
push(apply_rec(lo(a), b, op));
|
||||
push(apply_rec(hi(a), b, op));
|
||||
r = make_node(level(a), read(2), read(1));
|
||||
}
|
||||
else {
|
||||
push(apply_rec(a, lo(b), op));
|
||||
push(apply_rec(a, hi(b), op));
|
||||
r = make_node(level(b), read(2), read(1));
|
||||
}
|
||||
e1->m_result = r;
|
||||
e1->m_bdd1 = a;
|
||||
e1->m_bdd2 = b;
|
||||
e1->m_op = op;
|
||||
return r;
|
||||
}
|
||||
|
||||
void bdd_manager::push(BDD b) {
|
||||
m_bdd_stack.push_back(b);
|
||||
}
|
||||
|
||||
void bdd_manager::pop(unsigned num_scopes) {
|
||||
m_bdd_stack.shrink(m_bdd_stack.size() - num_scopes);
|
||||
}
|
||||
|
||||
bdd_manager::BDD bdd_manager::read(unsigned index) {
|
||||
return m_bdd_stack[m_bdd_stack.size() - index];
|
||||
}
|
||||
|
||||
|
||||
bdd_manager::cache_entry* bdd_manager::pop_entry(unsigned hash) {
|
||||
cache_entry* result = 0;
|
||||
if (m_spare_entry) {
|
||||
result = m_spare_entry;
|
||||
m_spare_entry = 0;
|
||||
result->m_hash = hash;
|
||||
}
|
||||
else {
|
||||
void * mem = m_alloc.allocate(sizeof(cache_entry));
|
||||
result = new (mem) cache_entry(hash);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
void bdd_manager::push_entry(cache_entry* e) {
|
||||
SASSERT(!m_spare_entry);
|
||||
m_spare_entry = e;
|
||||
}
|
||||
|
||||
|
||||
bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) {
|
||||
if (l == r) {
|
||||
return l;
|
||||
}
|
||||
#if 0
|
||||
// TBD
|
||||
unsigned hash = node_hash(level, l, r);
|
||||
bdd result = m_
|
||||
#endif
|
||||
int sz = m_nodes.size();
|
||||
m_nodes.push_back(bdd_node(level, l, r));
|
||||
return sz;
|
||||
}
|
||||
|
||||
#if 0
|
||||
void bdd_manager::bdd_reorder(int) {
|
||||
|
||||
}
|
||||
#endif
|
||||
|
||||
bdd bdd_manager::mk_var(unsigned i) {
|
||||
return bdd(m_var2bdd[2*i+1], this);
|
||||
}
|
||||
|
||||
bdd bdd_manager::mk_nvar(unsigned i) {
|
||||
return bdd(m_var2bdd[2*i+1], this);
|
||||
}
|
||||
|
||||
unsigned bdd_manager::hash2(BDD a, BDD b, bdd_op op) const {
|
||||
return mk_mix(a, b, op);
|
||||
}
|
||||
|
||||
bdd bdd_manager::mk_not(bdd b) {
|
||||
return bdd(mk_not_rec(b.root), this);
|
||||
}
|
||||
|
||||
bdd_manager::BDD bdd_manager::mk_not_rec(BDD b) {
|
||||
if (is_true(b)) return false_bdd;
|
||||
if (is_false(b)) return true_bdd;
|
||||
cache_entry* e1 = pop_entry(hash1(b, bdd_not_op));
|
||||
cache_entry const* e2 = m_cache.insert_if_not_there(e1);
|
||||
if (e2->m_bdd1 == b && e2->m_op == bdd_not_op) {
|
||||
push_entry(e1);
|
||||
return e2->m_result;
|
||||
}
|
||||
push(mk_not_rec(lo(b)));
|
||||
push(mk_not_rec(hi(b)));
|
||||
BDD r = make_node(level(b), read(2), read(1));
|
||||
pop(2);
|
||||
e1->m_bdd1 = b;
|
||||
e1->m_bdd2 = b;
|
||||
e1->m_op = bdd_not_op;
|
||||
e1->m_result = r;
|
||||
return r;
|
||||
}
|
||||
|
||||
#if 0
|
||||
bdd bdd_manager::mk_exists(bdd vars, bdd b) {
|
||||
|
||||
}
|
||||
|
||||
bdd bdd_manager::mk_forall(bdd vars, bdd b) {
|
||||
|
||||
}
|
||||
|
||||
bdd bdd_manager::mk_ite(bdd c, bdd t, bdd e) {
|
||||
|
||||
}
|
||||
|
||||
double bdd_manager::path_count(bdd b) {
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
std::ostream& bdd_manager::display(std::ostream& out, bdd b) {
|
||||
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& bdd_manager::display(std::ostream& out) {
|
||||
|
||||
return out;
|
||||
}
|
||||
|
||||
bdd::bdd(int 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() {
|
||||
m->dec_ref(root);
|
||||
}
|
||||
|
||||
#if 0
|
||||
#endif
|
||||
|
||||
}
|
||||
170
src/sat/sat_bdd.h
Normal file
170
src/sat/sat_bdd.h
Normal file
|
|
@ -0,0 +1,170 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_bdd
|
||||
|
||||
Abstract:
|
||||
|
||||
Simple BDD package modeled after BuDDy, which is modeled after CUDD.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2017-10-13
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef SAT_BDD_H_
|
||||
#define SAT_BDD_H_
|
||||
|
||||
#include "util/vector.h"
|
||||
#include "util/map.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
struct bdd_pair {
|
||||
int* m_bdd;
|
||||
int m_last;
|
||||
int m_id;
|
||||
bdd_pair* m_next;
|
||||
};
|
||||
|
||||
class bdd_manager;
|
||||
|
||||
class bdd {
|
||||
friend class bdd_manager;
|
||||
int root;
|
||||
bdd_manager* m;
|
||||
bdd(int root, bdd_manager* m);
|
||||
public:
|
||||
bdd(bdd & other);
|
||||
~bdd();
|
||||
// bdd operator!() { return m->mk_not(*this); }
|
||||
};
|
||||
|
||||
class bdd_manager {
|
||||
friend bdd;
|
||||
|
||||
typedef int BDD;
|
||||
|
||||
enum bdd_op {
|
||||
bdd_and_op = 0,
|
||||
bdd_or_op,
|
||||
bdd_iff_op,
|
||||
bdd_not_op,
|
||||
bdd_no_op
|
||||
};
|
||||
|
||||
struct bdd_node {
|
||||
bdd_node(unsigned level, int lo, int hi):
|
||||
m_refcount(0),
|
||||
m_level(level),
|
||||
m_lo(lo),
|
||||
m_hi(hi)
|
||||
{}
|
||||
unsigned m_refcount : 10;
|
||||
unsigned m_level : 22;
|
||||
int m_lo;
|
||||
int m_hi;
|
||||
//unsigned m_hash;
|
||||
//unsigned m_next;
|
||||
};
|
||||
|
||||
struct cache_entry {
|
||||
cache_entry(unsigned hash):
|
||||
m_bdd1(0),
|
||||
m_bdd2(0),
|
||||
m_op(bdd_no_op),
|
||||
m_result(0),
|
||||
m_hash(hash)
|
||||
{}
|
||||
|
||||
BDD m_bdd1;
|
||||
BDD m_bdd2;
|
||||
bdd_op m_op;
|
||||
BDD m_result;
|
||||
unsigned m_hash;
|
||||
};
|
||||
|
||||
struct hash_entry {
|
||||
unsigned operator()(cache_entry* e) const { return e->m_hash; }
|
||||
};
|
||||
|
||||
struct eq_entry {
|
||||
bool operator()(cache_entry * a, cache_entry * b) const {
|
||||
return a->m_hash == b->m_hash;
|
||||
}
|
||||
};
|
||||
|
||||
svector<bdd_node> m_nodes;
|
||||
ptr_hashtable<cache_entry, hash_entry, eq_entry> m_cache;
|
||||
unsigned_vector m_apply_const;
|
||||
svector<BDD> m_bdd_stack;
|
||||
cache_entry* m_spare_entry;
|
||||
svector<BDD> m_var2bdd;
|
||||
unsigned_vector m_var2level, m_level2var;
|
||||
small_object_allocator m_alloc;
|
||||
|
||||
BDD make_node(unsigned level, BDD l, BDD r);
|
||||
|
||||
BDD apply_const(BDD a, BDD b, bdd_op op);
|
||||
BDD apply(BDD arg1, BDD arg2, bdd_op op);
|
||||
BDD apply_rec(BDD arg1, BDD arg2, bdd_op op);
|
||||
|
||||
void push(BDD b);
|
||||
void pop(unsigned num_scopes);
|
||||
BDD read(unsigned index);
|
||||
|
||||
cache_entry* pop_entry(unsigned hash);
|
||||
void push_entry(cache_entry* e);
|
||||
|
||||
// void bdd_reorder(int);
|
||||
|
||||
BDD mk_not_rec(BDD b);
|
||||
|
||||
unsigned hash1(BDD b, bdd_op op) const { return hash2(b, b, op); }
|
||||
unsigned hash2(BDD a, BDD b, bdd_op op) const;
|
||||
unsigned hash3(BDD a, BDD b, BDD c, bdd_op op) const;
|
||||
|
||||
static const BDD false_bdd = 0;
|
||||
static const BDD true_bdd = 1;
|
||||
static const unsigned max_rc = (1 << 10) - 1;
|
||||
|
||||
inline bool is_true(BDD b) const { return b == true_bdd; }
|
||||
inline bool is_false(BDD b) const { return b == false_bdd; }
|
||||
inline bool is_const(BDD b) const { return 0 <= b && b <= 1; }
|
||||
|
||||
unsigned level(BDD b) const { return m_nodes[b].m_level; }
|
||||
BDD lo(BDD b) const { return m_nodes[b].m_lo; }
|
||||
BDD hi(BDD b) const { return m_nodes[b].m_hi; }
|
||||
void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; }
|
||||
void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc && m_nodes[b].m_refcount > 0) m_nodes[b].m_refcount--; }
|
||||
|
||||
BDD mk_true() { return 1; }
|
||||
BDD mk_false() { return 0; }
|
||||
|
||||
public:
|
||||
bdd_manager(unsigned nodes, unsigned cache_size);
|
||||
|
||||
bdd mk_var(unsigned i);
|
||||
bdd mk_nvar(unsigned i);
|
||||
|
||||
bdd mk_not(bdd b);
|
||||
bdd mk_exist(bdd vars, bdd b);
|
||||
bdd mk_forall(bdd vars, bdd b);
|
||||
bdd mk_and(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
|
||||
bdd mk_or(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
|
||||
bdd mk_iff(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
|
||||
bdd mk_ite(bdd c, bdd t, bdd e);
|
||||
|
||||
double path_count(bdd b);
|
||||
|
||||
std::ostream& display(std::ostream& out, bdd b);
|
||||
std::ostream& display(std::ostream& out);
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -39,6 +39,7 @@ def_module_params('sat',
|
|||
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
|
||||
('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
|
||||
('lookahead_search', BOOL, False, 'use lookahead solver'),
|
||||
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
|
||||
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
|
||||
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
|
||||
('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
|
||||
|
|
|
|||
Loading…
Reference in a new issue