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

bug fixes to sorting network

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-11 21:53:12 -07:00
parent e288b7795d
commit 770d0d58fe
2 changed files with 16 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/test/sorting_network.cpp
View file

@ -237,7 +237,7 @@ static void test_sorting_le(unsigned n, unsigned k) {
smt::kernel solver(m, fp);
psort_nw<ast_ext2> sn(ext);
expr_ref result(m);
// k <= B
// B <= k
std::cout << "le " << k << "\n";
solver.push();
result = sn.le(false, k, in.size(), in.c_ptr());
@ -248,12 +248,12 @@ static void test_sorting_le(unsigned n, unsigned k) {
lbool res = solver.check();
SASSERT(res == l_true);
for (unsigned i = 0; i < n - k; ++i) {
solver.assert_expr(m.mk_not(in[i].get()));
for (unsigned i = 0; i < k; ++i) {
solver.assert_expr(in[i].get());
}
res = solver.check();
SASSERT(res == l_true);
solver.assert_expr(m.mk_not(in[n - k].get()));
solver.assert_expr(in[k].get());
res = solver.check();
if (res == l_true) {
TRACE("pb",
@ -284,7 +284,7 @@ void test_sorting_ge(unsigned n, unsigned k) {
smt::kernel solver(m, fp);
psort_nw<ast_ext2> sn(ext);
expr_ref result(m);
// k >= B
// k <= B
std::cout << "ge " << k << "\n";
solver.push();
result = sn.ge(false, k, in.size(), in.c_ptr());
@ -326,14 +326,14 @@ void test_sorting5(unsigned n, unsigned k) {
}
void tst_sorting_network() {
test_sorting1();
test_sorting2();
test_sorting3();
test_sorting4();
test_sorting5(11,4);
test_sorting_eq(11,7);
for (unsigned n = 3; n < 20; n += 2) {
for (unsigned k = 1; k < n; ++k) {
test_sorting5(n, k);
}
}
test_sorting1();
test_sorting2();
test_sorting3();
test_sorting4();
}

6
src/util/sorting_network.h
View file

@ -680,6 +680,12 @@ Notes:
for (unsigned k = 0; k < c; ++k) {
ls.reset();
ls.push_back(ctx.mk_not(out[k]));
if (a <= k) {
add_clause(ctx.mk_not(out[k]), bs[k-a]);
}
if (b <= k) {
add_clause(ctx.mk_not(out[k]), as[k-b]);
}
for (unsigned i = 0; i < std::min(a,k + 1); ++i) {
unsigned j = k - i;
SASSERT(i + j == k);