mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

test sup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-01 10:33:25 -07:00
parent 5edc939b85
commit 05bcf0bed7
2 changed files with 45 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/dd/dd_fdd.cpp
View file

@ -215,10 +215,9 @@ namespace dd {
} }
SASSERT(!lo[idx]); SASSERT(!lo[idx]);
trail.reverse();
lo[idx] = true; lo[idx] = true;
unsigned v = m_pos2var[idx]; unsigned v = m_pos2var[idx];
b = trail[idx].cofactor(m->mk_var(v)); b = trail[lo.size() - idx - 1].cofactor(m->mk_var(v));
for (unsigned i = idx; i-- > 0; ) { for (unsigned i = idx; i-- > 0; ) {
SASSERT(!b.is_true()); SASSERT(!b.is_true());
if (b.is_false()) { if (b.is_false()) {
@ -279,12 +278,10 @@ namespace dd {
} }
SASSERT(hi[idx]); SASSERT(hi[idx]);
trail.reverse();
hi[idx] = false; hi[idx] = false;
unsigned v = m_pos2var[idx]; unsigned v = m_pos2var[idx];
b = trail[idx].cofactor(m->mk_nvar(v)); b = trail[hi.size() - idx - 1].cofactor(m->mk_nvar(v));
// Check logic, TBD
for (unsigned i = idx; i-- > 0; ) { for (unsigned i = idx; i-- > 0; ) {
SASSERT(!b.is_true()); SASSERT(!b.is_true());
if (b.is_false()) { if (b.is_false()) {
@ -292,11 +289,11 @@ namespace dd {
hi[j] = true; hi[j] = true;
break; break;
} }
hi[i] = b.lo().is_true(); hi[i] = !b.hi().is_true();
if (hi[i]) if (!hi[i])
b = b.hi();
else
b = b.lo(); b = b.lo();
else
b = b.hi();
} }
inc(hi); inc(hi);

40
src/test/bdd.cpp
View file

@ -446,6 +446,14 @@ public:
} }
} }
static void dec(bool_vector& x) {
for (auto& b : x) {
b = !b;
if (!b)
break;
}
}
static unsigned value(bool_vector const& x) { static unsigned value(bool_vector const& x) {
unsigned p = 1; unsigned p = 1;
unsigned v = 0; unsigned v = 0;
@ -463,15 +471,42 @@ public:
bddv const& x = x_dom.var(); bddv const& x = x_dom.var();
bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33); bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33);
bool_vector lo(10, false); bool_vector lo(10, false);
for (unsigned i = 0; i < 30; ++i) { for (unsigned i = 0; i < 20; ++i) {
unsigned v = value(lo);
bool found = x_dom.sup(c, lo); bool found = x_dom.sup(c, lo);
std::cout << found << ": " << value(lo) << "\n"; std::cout << found << ": " << v << " - " << value(lo) << "\n";
if (found) if (found)
std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n"; std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n";
c = !c;
inc(lo); inc(lo);
} }
} }
static void test_inf() {
std::cout << "test_inf\n";
bdd_manager m(20);
fdd const x_dom(m, 10);
bddv const& x = x_dom.var();
bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33);
bool_vector hi(10, true);
for (unsigned i = 0; i < 10; ++i) {
bool found = x_dom.inf(c, hi);
std::cout << found << ": " << value(hi) << "\n";
if (found) {
std::cout << x_dom.inf(c, hi) << ": " << value(hi) << "\n";
SASSERT(value(hi) == 0 || value(hi) == 1 || value(hi) == 5 || value(hi) == 6 ||
value(hi) == 10 || value(hi) == 11 ||
value(hi) == 13 || value(hi) == 14 ||
value(hi) == 28 || value(hi) == 29 ||
value(hi) == 33 || value(hi) == 34 || value(hi) == 1023);
}
c = !c;
dec(hi);
}
}
}; };
} }
@ -494,5 +529,6 @@ void tst_bdd() {
dd::test_bdd::test_fdd_twovars(); dd::test_bdd::test_fdd_twovars();
dd::test_bdd::test_fdd_find_hint(); dd::test_bdd::test_fdd_find_hint();
dd::test_bdd::test_cofactor(); dd::test_bdd::test_cofactor();
dd::test_bdd::test_inf();
dd::test_bdd::test_sup(); dd::test_bdd::test_sup();
} }