mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

build fix

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-01 11:23:42 +00:00
parent 84172302a2
commit ed5137ffd2
1 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/test/sorting_network.cpp
View file

@ -22,7 +22,7 @@ struct ast_ext {
ast_ext(ast_manager& m):m(m) {}
typedef expr* T;
typedef expr_ref_vector vector;
T mk_ite(T a, T b, T c) {
T mk_ite(T a, T b, T c) {
return m.mk_ite(a, b, c);
}
T mk_le(T a, T b) {
@ -34,7 +34,7 @@ struct ast_ext {
}
T mk_default() {
return m.mk_false();
}
}
};
@ -164,17 +164,17 @@ struct ast_ext2 {
literal mk_false() { return m.mk_false(); }
literal mk_true() { return m.mk_true(); }
literal mk_max(literal a, literal b) {
return trail(m.mk_or(a, b));
literal mk_max(literal a, literal b) {
return trail(m.mk_or(a, b));
}
literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
literal mk_not(literal a) { if (m.is_not(a,a)) return a;
return trail(m.mk_not(a));
literal mk_not(literal a) { if (m.is_not(a,a)) return a;
return trail(m.mk_not(a));
}
std::ostream& pp(std::ostream& out, literal lit) {
return out << mk_pp(lit, m);
}
literal fresh() {
literal fresh() {
return trail(m.mk_fresh_const("x", m.mk_bool_sort()));
}
void mk_clause(unsigned n, literal const* lits) {
@ -200,7 +200,7 @@ static void test_sorting_eq(unsigned n, unsigned k) {
// equality:
std::cout << "eq " << k << "\n";
solver.push();
result = sn.eq(k, in.size(), in.c_ptr());
result = sn.eq(true, k, in.size(), in.c_ptr());
solver.assert_expr(result);
for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
solver.assert_expr(ext.m_clauses[i].get());
@ -210,7 +210,7 @@ static void test_sorting_eq(unsigned n, unsigned k) {
solver.push();
for (unsigned i = 0; i < k; ++i) {
solver.assert_expr(in[i].get());
solver.assert_expr(in[i].get());
}
res = solver.check();
SASSERT(res == l_true);
@ -256,7 +256,7 @@ static void test_sorting_le(unsigned n, unsigned k) {
SASSERT(res == l_true);
for (unsigned i = 0; i < k; ++i) {
solver.assert_expr(in[i].get());
solver.assert_expr(in[i].get());
}
res = solver.check();
SASSERT(res == l_true);
@ -304,7 +304,7 @@ void test_sorting_ge(unsigned n, unsigned k) {
solver.push();
for (unsigned i = 0; i < n - k; ++i) {
solver.assert_expr(m.mk_not(in[i].get()));
solver.assert_expr(m.mk_not(in[i].get()));
}
res = solver.check();
SASSERT(res == l_true);
@ -350,10 +350,10 @@ void test_at_most_1(unsigned n, bool full) {
for (unsigned i = 0; i < n; ++i) {
in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
}
ast_ext2 ext(m);
psort_nw<ast_ext2> sn(ext);
expr_ref result1(m), result2(m);
expr_ref result1(m), result2(m);
result1 = sn.le(full, 1, in.size(), in.c_ptr());
result2 = naive_at_most1(in);
@ -368,12 +368,12 @@ void test_at_most_1(unsigned n, bool full) {
if (full) {
solver.push();
solver.assert_expr(m.mk_not(m.mk_eq(result1, result2)));
std::cout << result1 << "\n";
res = solver.check();
SASSERT(res == l_false);
solver.pop(1);
}