mirror of
https://github.com/Z3Prover/z3
synced 2025-08-18 17:22:15 +00:00
83 lines
2.4 KiB
C++
83 lines
2.4 KiB
C++
#include "sat/sat_bdd.h"
|
|
|
|
namespace sat {
|
|
static void test1() {
|
|
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;
|
|
bdd c2 = v2 && v0 && v1;
|
|
std::cout << c1 << "\n";
|
|
SASSERT(c1 == c2);
|
|
std::cout << "cnf size: " << c1.cnf_size() << "\n";
|
|
|
|
c1 = v0 || v1 || v2;
|
|
c2 = v2 || v1 || v0;
|
|
std::cout << c1 << "\n";
|
|
SASSERT(c1 == c2);
|
|
std::cout << "cnf size: " << c1.cnf_size() << "\n";
|
|
}
|
|
|
|
static void test2() {
|
|
bdd_manager m(20);
|
|
bdd v0 = m.mk_var(0);
|
|
bdd v1 = m.mk_var(1);
|
|
bdd v2 = m.mk_var(2);
|
|
SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1));
|
|
SASSERT(m.mk_ite(v0,v1,v1) == v1);
|
|
SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1));
|
|
SASSERT(m.mk_ite(v1,v0,v0) == v0);
|
|
SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1));
|
|
SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1));
|
|
SASSERT(!(v0 && v1) == (!v0 || !v1));
|
|
SASSERT(!(v0 || v1) == (!v0 && !v1));
|
|
}
|
|
|
|
static void test3() {
|
|
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;
|
|
bdd c2 = m.mk_exists(0, c1);
|
|
std::cout << c1 << "\n";
|
|
std::cout << c2 << "\n";
|
|
SASSERT(c2 == (v1 || v2));
|
|
c2 = m.mk_exists(1, c1);
|
|
SASSERT(c2 == (v0 || v2));
|
|
c2 = m.mk_exists(2, c1);
|
|
SASSERT(c2.is_true());
|
|
SASSERT(m.mk_exists(3, c1) == c1);
|
|
c1 = (v0 && v1) || (v1 && v2) || (!v0 && !v2);
|
|
c2 = m.mk_exists(0, c1);
|
|
SASSERT(c2 == (v1 || (v1 && v2) || !v2));
|
|
c2 = m.mk_exists(1, c1);
|
|
SASSERT(c2 == (v0 || v2 || (!v0 && !v2)));
|
|
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.gc();
|
|
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();
|
|
}
|