mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

add cofactoring functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-30 09:11:42 -07:00
parent 1defbc8aa4
commit b019477378
3 changed files with 67 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/math/dd/dd_bdd.cpp
View file

@ -145,6 +145,13 @@ namespace dd {
if (is_true(a)) return mk_not_rec(b);
if (is_true(b)) return mk_not_rec(a);
break;
case bdd_cofactor_op:
if (a == b) return a;
if (is_const(a)) return a;
if (level(a) == level(b))
SASSERT(!is_const(b));
break;
default:
UNREACHABLE();
break;
@ -573,7 +580,47 @@ namespace dd {
e1->m_result = r;
return r;
}
/**
* co-factor a using b.
* b must be a variable bdd (it can be generalized to a cube)
*/
bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) {
bool first = true;
scoped_push _sp(*this);
SASSERT(!is_const(b) && is_const(lo(b)) && is_const(hi(b)));
while (true) {
try {
return bdd(mk_cofactor_rec(a.root, b.root), this);
}
catch (const mem_out &) {
if (!first) throw;
try_reorder();
first = false;
}
}
}
bdd_manager::BDD bdd_manager::mk_cofactor_rec(BDD a, BDD b) {
if (is_const(a)) return a;
unsigned la = level(a), lb = level(b);
if (la < lb) return a;
if (la == lb) return is_true(hi(b)) ? hi(a) : lo(a);
op_entry* e1 = pop_entry(a, b, bdd_cofactor_op);
op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
if (check_result(e1, e2, a, b, bdd_cofactor_op))
return e2->m_result;
SASSERT(la > lb);
push(mk_cofactor_rec(lo(a), b));
push(mk_cofactor_rec(hi(a), b));
BDD r = make_node(la, read(2), read(1));
pop(2);
e1->m_result = r;
return r;
}
bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) {
bool first = true;
scoped_push _sp(*this);
@ -589,6 +636,7 @@ namespace dd {
}
}
bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) {
if (is_true(a)) return b;
if (is_false(a)) return c;

6
src/math/dd/dd_bdd.h
View file

@ -45,7 +45,8 @@ namespace dd {
bdd_not_op = 5,
bdd_and_proj_op = 6,
bdd_or_proj_op = 7,
bdd_no_op = 8,
bdd_cofactor_op = 8,
bdd_no_op = 9,
};
struct bdd_node {
@ -146,6 +147,7 @@ namespace dd {
BDD mk_not_rec(BDD b);
BDD mk_ite_rec(BDD a, BDD b, BDD c);
BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op);
BDD mk_cofactor_rec(BDD a, BDD b);
void push(BDD b);
void pop(unsigned num_scopes);
@ -193,6 +195,7 @@ namespace dd {
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);
bdd mk_cofactor(bdd const& a, bdd const& b);
void reserve_var(unsigned v);
bool well_formed();
@ -292,6 +295,7 @@ namespace dd {
bdd operator^(bdd const& other) const { return m->mk_xor(*this, other); }
bdd operator|=(bdd const& other) { return *this = *this || other; }
bdd operator&=(bdd const& other) { return *this = *this && other; }
bdd cofactor(bdd const& cube) { return m->mk_cofactor(*this, cube); }
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; }

14
src/test/bdd.cpp
View file

@ -425,6 +425,19 @@ public:
SASSERT_EQ(x_dom.find_hint(s358 && (x == rational(4)), rational(5), r), find_t::empty);
}
static void test_cofactor() {
std::cout << "test_cofactor\n";
bdd_manager m(20);
bdd v0 = m.mk_var(0);
bdd v1 = m.mk_var(1);
bdd v2 = m.mk_var(2);
bdd c1 = v0 && v1 && v2;
SASSERT(c1.cofactor(v0) == (v1 && v2));
SASSERT(c1.cofactor(v1) == (v0 && v2));
SASSERT(c1.cofactor(v2) == (v0 && v1));
SASSERT(c1.cofactor(!v1) == m.mk_false());
}
};
}
@ -446,4 +459,5 @@ void tst_bdd() {
dd::test_bdd::test_fdd_reorder();
dd::test_bdd::test_fdd_twovars();
dd::test_bdd::test_fdd_find_hint();
dd::test_bdd::test_cofactor();
}