diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index af7270825..076d7ec73 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -54,7 +54,7 @@ static void tst1() { std::cout << "p: " << p << "\n"; am.isolate_roots(p, rs1); display_anums(std::cout, rs1); - SASSERT(rs1.size() == 1); + ENSURE(rs1.size() == 1); std::cout.flush(); p = (x^2) - 2; @@ -62,7 +62,7 @@ static void tst1() { rs1.reset(); am.isolate_roots(p, rs1); display_anums(std::cout, rs1); - SASSERT(rs1.size() == 2); + ENSURE(rs1.size() == 2); scoped_anum sqrt2(am); am.set(sqrt2, rs1[1]); @@ -88,7 +88,7 @@ static void tst1() { rs1.reset(); am.isolate_roots(p, rs1); display_anums(std::cout, rs1); - SASSERT(rs1.size() == 3); + ENSURE(rs1.size() == 3); scoped_anum gauss(am); am.set(gauss, rs1[1]); @@ -104,7 +104,7 @@ static void tst1() { rs1.reset(); am.isolate_roots(p, rs1); display_anums(std::cout, rs1); - SASSERT(rs1.size() == 4); + ENSURE(rs1.size() == 4); scoped_anum hidden_sqrt2(am); am.set(hidden_sqrt2, rs1[2]); @@ -116,8 +116,8 @@ static void tst1() { std::cout << "sqrt(2)^4: " << (sqrt2^4) << "\n"; - SASSERT(is_int(power(sqrt2, 4))); - SASSERT(power(sqrt2, 4) == 4); + ENSURE(is_int(power(sqrt2, 4))); + ENSURE(power(sqrt2, 4) == 4); scoped_anum sqrt2_gauss(am); am.add(sqrt2, gauss, sqrt2_gauss); @@ -242,9 +242,9 @@ static void tst_wilkinson() { std::cout << "p: " << p << "\n"; am.isolate_roots(p, rs1); display_anums(std::cout, rs1); - SASSERT(rs1.size() == 20); + ENSURE(rs1.size() == 20); for (unsigned i = 0; i < rs1.size(); i++) { - SASSERT(am.is_int(rs1[i])); + ENSURE(am.is_int(rs1[i])); } } @@ -328,9 +328,9 @@ static void tst_eval_sign(polynomial_ref const & p, anum_manager & am, std::cout << "x1 -> "; am.display_root(std::cout, v1); std::cout << "\n"; std::cout << "x2 -> "; am.display_root(std::cout, v2); std::cout << "\n"; int s = am.eval_sign_at(p, x2v); - SASSERT((s == 0) == (expected == 0)); - SASSERT((s < 0) == (expected < 0)); - SASSERT((s > 0) == (expected > 0)); + ENSURE((s == 0) == (expected == 0)); + ENSURE((s < 0) == (expected < 0)); + ENSURE((s > 0) == (expected > 0)); std::cout << "sign: " << s << "\n"; } @@ -399,7 +399,7 @@ static void tst_isolate_roots(polynomial_ref const & p, anum_manager & am, scoped_anum_vector roots(am); svector signs; am.isolate_roots(p, x2v, roots, signs); - SASSERT(roots.size() + 1 == signs.size()); + ENSURE(roots.size() + 1 == signs.size()); std::cout << "roots:\n"; for (unsigned i = 0; i < roots.size(); i++) { am.display_root(std::cout, roots[i]); std::cout << " "; am.display_decimal(std::cout, roots[i]); std::cout << "\n"; diff --git a/src/test/api.cpp b/src/test/api.cpp index 667d10bc5..f691a8701 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -101,7 +101,7 @@ static void test_mk_distinct() { Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32); Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) }; Z3_ast d = Z3_mk_distinct(ctx, 2, args); - SASSERT(cb_called); + ENSURE(cb_called); Z3_del_config(cfg); Z3_del_context(ctx); diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp index 5ed7c3501..6bdb11d48 100644 --- a/src/test/arith_rewriter.cpp +++ b/src/test/arith_rewriter.cpp @@ -27,7 +27,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(assert " << str << ")\n"; std::istringstream is(buffer.str()); VERIFY(parse_smt2_commands(ctx, is)); - SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + ENSURE(ctx.begin_assertions() != ctx.end_assertions()); result = *ctx.begin_assertions(); return result; } diff --git a/src/test/ast.cpp b/src/test/ast.cpp index b59e2a612..20a1007a4 100644 --- a/src/test/ast.cpp +++ b/src/test/ast.cpp @@ -29,21 +29,21 @@ static void tst1() { expr_ref i1(m.mk_app(fid, OP_AND, a.get(), c.get()), m); expr_ref i2(m.mk_app(fid, OP_AND, a.get(), c.get()), m); expr_ref i3(m.mk_app(fid, OP_OR, a.get(), c.get()), m); - SASSERT(i1.get() == i2.get()); - SASSERT(i1.get() != i3.get()); + ENSURE(i1.get() == i2.get()); + ENSURE(i1.get() != i3.get()); // TODO use smart pointers to track references // ast_manager m; // ast_ref n1(m.mk_numeral(rational(2,3)), m); // ast_ref n2(m.mk_numeral(rational(2,3)), m); -// SASSERT(n1 == n2); +// ENSURE(n1 == n2); // ast_ref n3(m.mk_numeral(rational(1,2)), m); -// SASSERT(n1 != n3); +// ENSURE(n1 != n3); // ast_ref v1 (m.mk_var(1), m); // ast_ref v2 (m.mk_var(2), m); // ast_ref v3 (m.mk_var(1), m); -// SASSERT(v1 != v2); -// SASSERT(v1 == v3); +// ENSURE(v1 != v2); +// ENSURE(v1 == v3); // TRACE("ast", tout << "reseting v1\n";); // v1.reset(); // TRACE("ast", tout << "overwriting v3\n";); @@ -59,7 +59,7 @@ static void tst1() { // ast_ref foo_x(m.mk_const(foo_decl.get(), x.get()), m); // ast_ref foo_foo_x(m.mk_const(foo_decl.get(), foo_x.get()), m); // ast_ref foo_foo_x2(m.mk_const(foo_decl.get(), m.mk_const(foo_decl.get(), m.mk_const(x_decl.get()))), m); -// SASSERT(foo_foo_x2 == foo_foo_x); +// ENSURE(foo_foo_x2 == foo_foo_x); } static void tst2() { @@ -70,13 +70,13 @@ static void tst2() { // m_nodes.push_back(m.mk_numeral(rational(1,2))); // m_nodes.push_back(m.mk_var(2)); // m_nodes[1] = m.mk_var(3); -// SASSERT(m_nodes[1]->kind() == AST_VAR); -// SASSERT(m_nodes.get(1)->kind() == AST_VAR); +// ENSURE(m_nodes[1]->kind() == AST_VAR); +// ENSURE(m_nodes.get(1)->kind() == AST_VAR); // m_nodes.pop_back(); -// SASSERT(m_nodes.size() == 2); -// SASSERT(!m_nodes.empty()); +// ENSURE(m_nodes.size() == 2); +// ENSURE(!m_nodes.empty()); // m_nodes.set(1, m.mk_var(4)); -// SASSERT(&(m_nodes.get_manager()) == &m); +// ENSURE(&(m_nodes.get_manager()) == &m); } static void tst3() { @@ -95,16 +95,16 @@ static void tst4() { // #ifdef Z3DEBUG // int r; // #endif -// SASSERT(!wm1.find(n1, r)); +// ENSURE(!wm1.find(n1, r)); // wm1.insert(n2, 10); -// SASSERT(!wm1.find(n1, r)); -// SASSERT(wm1.find(n2, r) && r == 10); +// ENSURE(!wm1.find(n1, r)); +// ENSURE(wm1.find(n2, r) && r == 10); // wm1.insert(n2, 20); -// SASSERT(!wm1.find(n1, r)); -// SASSERT(wm1.find(n2, r) && r == 20); +// ENSURE(!wm1.find(n1, r)); +// ENSURE(wm1.find(n2, r) && r == 20); // wm1.insert(n1, 0); -// SASSERT(wm1.find(n1, r) && r == 0); -// SASSERT(wm1.find(n2, r) && r == 20); +// ENSURE(wm1.find(n1, r) && r == 0); +// ENSURE(wm1.find(n2, r) && r == 20); } static void tst5() { @@ -119,13 +119,13 @@ static void tst5() { m.push_back(arr1, a2); m.pop_back(arr1, arr2); m.set(arr2, 0, a2, arr3); - SASSERT(m.size(arr1) == 2); - SASSERT(m.size(arr2) == 1); - SASSERT(m.size(arr3) == 1); - SASSERT(m.get(arr1, 0) == a1); - SASSERT(m.get(arr1, 1) == a2); - SASSERT(m.get(arr2, 0) == a1); - SASSERT(m.get(arr3, 0) == a2); + ENSURE(m.size(arr1) == 2); + ENSURE(m.size(arr2) == 1); + ENSURE(m.size(arr3) == 1); + ENSURE(m.get(arr1, 0) == a1); + ENSURE(m.get(arr1, 1) == a2); + ENSURE(m.get(arr2, 0) == a1); + ENSURE(m.get(arr3, 0) == a2); m.del(arr1); m.del(arr2); m.del(arr3); diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index 6f83bb328..46a39747d 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -31,30 +31,30 @@ static void tst1() { bool val = (rand()%2) != 0; v1.push_back(val); v2.push_back(val); - SASSERT(v1.size() == v2.size()); + ENSURE(v1.size() == v2.size()); } else if (op <= 3) { - SASSERT(v1.size() == v2.size()); + ENSURE(v1.size() == v2.size()); if (v1.size() > 0) { bool val = (rand()%2) != 0; unsigned idx = rand()%v1.size(); - SASSERT(v1.get(idx) == v2[idx]); + ENSURE(v1.get(idx) == v2[idx]); v1.set(idx, val); v2[idx] = val; - SASSERT(v1.get(idx) == v2[idx]); + ENSURE(v1.get(idx) == v2[idx]); } } else if (op <= 4) { - SASSERT(v1.size() == v2.size()); + ENSURE(v1.size() == v2.size()); if (v1.size() > 0) { unsigned idx = rand()%v1.size(); VERIFY(v1.get(idx) == v2[idx]); } } else if (op <= 5) { - SASSERT(v1.size() == v2.size()); + ENSURE(v1.size() == v2.size()); for (unsigned j = 0; j < v1.size(); j++) { - SASSERT(v1.get(j) == v2[j]); + ENSURE(v1.get(j) == v2[j]); } } } @@ -66,11 +66,11 @@ static void tst2() { b.push_back(false); b.push_back(true); b.resize(30); - SASSERT(b.get(0) == true); - SASSERT(b.get(1) == false); - SASSERT(b.get(2) == true); - SASSERT(b.get(3) == false); - SASSERT(b.get(29) == false); + ENSURE(b.get(0) == true); + ENSURE(b.get(1) == false); + ENSURE(b.get(2) == true); + ENSURE(b.get(3) == false); + ENSURE(b.get(29) == false); } static void tst_shift() { @@ -116,14 +116,14 @@ static void tst_or() { std::cout << b1 << "\n"; std::cout << b2 << "\n"; b1 |= b2; - SASSERT(b1.size() == 10); + ENSURE(b1.size() == 10); std::cout << b1 << "\n"; - SASSERT(b1 != b2); - SASSERT(b1 != b2); + ENSURE(b1 != b2); + ENSURE(b1 != b2); b1.unset(4); - SASSERT(b1 == b2); + ENSURE(b1 == b2); b1.unset(3); - SASSERT(b1 != b2); + ENSURE(b1 != b2); } { bit_vector b1; @@ -133,9 +133,9 @@ static void tst_or() { b1.set(0); b2.set(4); b1 |= b2; - SASSERT(b1 != b2); + ENSURE(b1 != b2); b2.set(0); - SASSERT(b1 == b2); + ENSURE(b1 == b2); std::cout << "-----\n"; std::cout << b1 << "\n"; } @@ -149,9 +149,9 @@ static void tst_or() { b2.set(3); b2.resize(5); b1 |= b2; - SASSERT(!b1.get(8)); - SASSERT(b1.get(5)); - SASSERT(b1.get(3)); + ENSURE(!b1.get(8)); + ENSURE(b1.get(5)); + ENSURE(b1.get(3)); } { bit_vector b1; @@ -166,17 +166,17 @@ static void tst_or() { b2.set(80); b1.set(4); b2.set(4); - SASSERT(b1!=b2); + ENSURE(b1!=b2); b2.resize(123); - SASSERT(b1!=b2); + ENSURE(b1!=b2); b1.resize(120); b2.resize(120); - SASSERT(b1==b2); + ENSURE(b1==b2); b1.unset(80); b1.unset(100); - SASSERT(b1!=b2); + ENSURE(b1!=b2); b1 |= b2; - SASSERT(b1 == b2); + ENSURE(b1 == b2); } { bit_vector b1; @@ -188,8 +188,8 @@ static void tst_or() { b2.set(1); b1.set(0); b1 |= b2; - SASSERT(b1.size() == 10); - SASSERT(b1.get(8) && b1.get(4) && b1.get(1) && b1.get(0) && !b1.get(9)); + ENSURE(b1.size() == 10); + ENSURE(b1.get(8) && b1.get(4) && b1.get(1) && b1.get(0) && !b1.get(9)); } { bit_vector b1; @@ -201,7 +201,7 @@ static void tst_or() { b2.set(8); b2.set(0); b1 |= b2; - SASSERT(b1.get(1) && b1.get(5) && b1.get(8) && b1.get(0) && !b1.get(11)); + ENSURE(b1.get(1) && b1.get(5) && b1.get(8) && b1.get(0) && !b1.get(11)); std::cout << "b1(size32): " << b1 << "\n"; } } @@ -218,8 +218,8 @@ static void tst_and() { std::cout << "------\nb1: " << b1 << "\n"; b1 &= b2; std::cout << "------\nb1: " << b1 << "\n"; - SASSERT(!b1.get(4)); - SASSERT(b1.get(2)); + ENSURE(!b1.get(4)); + ENSURE(b1.get(2)); } { bit_vector b1; @@ -234,7 +234,7 @@ static void tst_and() { b2.set(127); b2.set(5); b1 &= b2; - SASSERT(!b1.get(240) && !b1.get(232) && !b1.get(128) && b1.get(127) && !b1.get(8) && !b1.get(5)); + ENSURE(!b1.get(240) && !b1.get(232) && !b1.get(128) && b1.get(127) && !b1.get(8) && !b1.get(5)); } } @@ -243,17 +243,17 @@ static void tst_crash() { bit_vector b; b.push_back(true); b.resize(64); - SASSERT(!b.get(63)); - SASSERT(b.get(0)); - SASSERT(!b.get(1)); + ENSURE(!b.get(63)); + ENSURE(b.get(0)); + ENSURE(!b.get(1)); } { bit_vector b; b.push_back(false); b.resize(64, true); - SASSERT(b.get(63)); - SASSERT(!b.get(0)); - SASSERT(b.get(1)); + ENSURE(b.get(63)); + ENSURE(!b.get(0)); + ENSURE(b.get(1)); } } @@ -264,12 +264,12 @@ static void tst_bv_reset() { b.reset(); b.resize(sz, bit); for (unsigned i = 0; i < sz; ++i) { - SASSERT(bit == b.get(i)); + ENSURE(bit == b.get(i)); } for (unsigned sz2 = sz; sz2 < sz+10; ++sz2) { b.resize(sz2, !bit); for (unsigned i = sz; i < sz2; ++i) { - SASSERT(bit != b.get(i)); + ENSURE(bit != b.get(i)); } } bit = !bit; @@ -283,19 +283,19 @@ static void tst_eq() { b3.resize(32); b1.set(3, true); - SASSERT(b1 != b2); - SASSERT(!(b1 == b2)); - SASSERT(b2 == b3); + ENSURE(b1 != b2); + ENSURE(!(b1 == b2)); + ENSURE(b2 == b3); b3.set(3, true); - SASSERT(b1 == b3); - SASSERT(!(b1 != b3)); + ENSURE(b1 == b3); + ENSURE(!(b1 != b3)); b2.set(31, true); b3.set(31); b3.unset(3); - SASSERT(b2 == b3); - SASSERT(!(b2 != b3)); + ENSURE(b2 == b3); + ENSURE(!(b2 != b3)); } void tst_bit_vector() { diff --git a/src/test/bits.cpp b/src/test/bits.cpp index f32871a5a..ba75ea0b4 100644 --- a/src/test/bits.cpp +++ b/src/test/bits.cpp @@ -27,11 +27,11 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k, if (trace) std::cout << " for sz = " << sz << std::endl; shl(src_sz, src, k, sz, actual_dst.c_ptr()); - SASSERT(!has_one_at_first_k_bits(sz, actual_dst.c_ptr(), k)); + ENSURE(!has_one_at_first_k_bits(sz, actual_dst.c_ptr(), k)); for (unsigned i = 0; i < sz; i++) { if (trace && dst[i] != actual_dst[i]) std::cout << "UNEXPECTED RESULT at [" << i << "]: " << actual_dst[i] << ", expected: " << dst[i] << "\n"; - SASSERT(dst[i] == actual_dst[i]); + ENSURE(dst[i] == actual_dst[i]); } if (sz == src_sz) { unsigned nz1 = nlz(sz, src); @@ -52,7 +52,7 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k, if (trace && src[i] != new_src[i]) { std::cout << "shr BUG, inverting shl, at bit[" << i << "], " << new_src[i] << ", expected: " << src[i] << std::endl; } - SASSERT(src[i] == new_src[i]); + ENSURE(src[i] == new_src[i]); } } } @@ -65,7 +65,7 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k, for (unsigned i = 0; i < dst_sz; i++) { if (trace && dst[i] != actual_dst[i]) std::cout << "UNEXPECTED RESULT at [" << i << "]: " << actual_dst[i] << ", expected: " << dst[i] << "\n"; - SASSERT(dst[i] == actual_dst[i]); + ENSURE(dst[i] == actual_dst[i]); } if (src_sz <= dst_sz) { if (trace) @@ -74,7 +74,7 @@ static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k, for (unsigned i = 0; i < src_sz; i++) { if (trace && src[i] != dst[i]) std::cout << "UNEXPECTED RESULT at [" << i << "]: " << src[i] << ", expected: " << dst[i] << "\n"; - SASSERT(src[i] == actual_dst[i]); + ENSURE(src[i] == actual_dst[i]); } } } @@ -134,7 +134,7 @@ static void tst_shr(unsigned src_sz, unsigned const * src, unsigned k, for (unsigned i = 0; i < src_sz; i++) { if (trace && dst[i] != actual_dst[i]) std::cout << "UNEXPECTED RESULT at [" << i << "]: " << actual_dst[i] << ", expected: " << dst[i] << "\n"; - SASSERT(dst[i] == actual_dst[i]); + ENSURE(dst[i] == actual_dst[i]); } } @@ -172,7 +172,7 @@ static void tst_shl_rand(unsynch_mpz_manager & m, unsigned sz, unsigned k, bool m.mul2k(max, 32); while (!m.is_zero(_dst)) { m.mod(_dst, max, tmp); - SASSERT(m.is_uint64(tmp) && m.get_uint64(tmp) < UINT_MAX); + ENSURE(m.is_uint64(tmp) && m.get_uint64(tmp) < UINT_MAX); dst.push_back(static_cast(m.get_uint64(tmp))); m.div(_dst, max, _dst); } diff --git a/src/test/buffer.cpp b/src/test/buffer.cpp index a23fb3c74..f4b7f0c99 100644 --- a/src/test/buffer.cpp +++ b/src/test/buffer.cpp @@ -24,22 +24,22 @@ template class ptr_scoped_buffer; static void tst1() { ptr_scoped_buffer b; - SASSERT(b.empty()); + ENSURE(b.empty()); b.push_back(alloc(point, 10, 20)); - SASSERT(!b.empty()); + ENSURE(!b.empty()); point * p1 = alloc(point, 30, 20); b.push_back(p1); - SASSERT(b.get(1) == p1); + ENSURE(b.get(1) == p1); b.push_back(alloc(point, 40, 20)); - SASSERT(b.size() == 3); + ENSURE(b.size() == 3); b.pop_back(); - SASSERT(b.get(0) != p1); - SASSERT(b.get(1) == p1); + ENSURE(b.get(0) != p1); + ENSURE(b.get(1) == p1); point * p2 = alloc(point, 30, 20); - SASSERT(b.get(0) != p2); + ENSURE(b.get(0) != p2); b.set(0, p2); - SASSERT(b.get(0) == p2); - SASSERT(b.size() == 2); + ENSURE(b.get(0) == p2); + ENSURE(b.size() == 2); b.push_back(alloc(point, 40, 40)); } diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index 69b97a9cc..42952706b 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -30,7 +30,7 @@ class tst_bv_simplifier_plugin_cls { if (!m_bv_util.is_numeral(e, r, bv_size0)) { UNREACHABLE(); } - SASSERT(bv_size == bv_size0); + ENSURE(bv_size == bv_size0); } unsigned u32(expr* e) { @@ -109,26 +109,26 @@ public: ar = m_manager.mk_app(m_fid, OP_BNEG, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((0-a) == u32(e.get())); + ENSURE((0-a) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNOT, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~a) == u32(e.get())); + ENSURE((~a) == u32(e.get())); parameter params[2] = { parameter(32), parameter(32) }; ar = m_manager.mk_app(m_fid, OP_SIGN_EXT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((int64)(int)a) == i64(e.get())); + ENSURE(((int64)(int)a) == i64(e.get())); ar = m_manager.mk_app(m_fid, OP_ZERO_EXT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((uint64)a) == u64(e.get())); + ENSURE(((uint64)a) == u64(e.get())); params[0] = parameter(7); params[1] = parameter(0); ar = m_manager.mk_app(m_fid, OP_EXTRACT, 2, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((unsigned char)a) == u8(e.get())); + ENSURE(((unsigned char)a) == u8(e.get())); params[0] = parameter(2); ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es); @@ -137,21 +137,21 @@ public: ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a != 0) == bit2bool(e.get())); + ENSURE((a != 0) == bit2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BREDAND, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a == 0xFFFFFFFF) == bit2bool(e.get())); + ENSURE((a == 0xFFFFFFFF) == bit2bool(e.get())); params[0] = parameter(8); ar = m_manager.mk_app(m_fid, OP_ROTATE_LEFT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a << 8) | (a >> 24)) == u32(e.get())); + ENSURE(((a << 8) | (a >> 24)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_ROTATE_RIGHT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a >> 8) | (a << 24)) == u32(e.get())); + ENSURE(((a >> 8) | (a << 24)) == u32(e.get())); params[0] = parameter(m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT)); ar = m_manager.mk_app(m_fid, OP_BV2INT, 1, params, 1, es); @@ -159,7 +159,7 @@ public: params[0] = parameter(32); ar = m_manager.mk_app(m_fid, OP_INT2BV, 1, params, 1, es2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(a == u32(e.get())); + ENSURE(a == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BIT0); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); diff --git a/src/test/chashtable.cpp b/src/test/chashtable.cpp index 7d55fe01f..c9750b95e 100644 --- a/src/test/chashtable.cpp +++ b/src/test/chashtable.cpp @@ -37,16 +37,16 @@ static void display(T const & beg, T const & end) { static void tst1() { int_table t; t.insert(10); - SASSERT(t.contains(10)); + ENSURE(t.contains(10)); t.insert(20); - SASSERT(t.contains(20)); + ENSURE(t.contains(20)); t.insert(30); - SASSERT(t.contains(30)); - SASSERT(t.size() == 3); + ENSURE(t.contains(30)); + ENSURE(t.size() == 3); display(t.begin(), t.end()); t.erase(20); - SASSERT(!t.contains(20)); - SASSERT(t.size() == 2); + ENSURE(!t.contains(20)); + ENSURE(t.size() == 2); } struct dummy_hash { @@ -61,54 +61,54 @@ static void tst2() { dint_table t; t.insert(10); t.insert(12); - SASSERT(t.used_slots() == 1); + ENSURE(t.used_slots() == 1); display(t.begin(), t.end()); t.insert(13); display(t.begin(), t.end()); - SASSERT(t.used_slots() == 2); + ENSURE(t.used_slots() == 2); t.insert(14); - SASSERT(t.used_slots() == 2); - SASSERT(t.size() == 4); + ENSURE(t.used_slots() == 2); + ENSURE(t.size() == 4); display(t.begin(), t.end()); t.erase(12); - SASSERT(!t.contains(12)); - SASSERT(t.size() == 3); - SASSERT(t.contains(10)); - SASSERT(!t.contains(12)); - SASSERT(t.contains(14)); - SASSERT(t.contains(13)); + ENSURE(!t.contains(12)); + ENSURE(t.size() == 3); + ENSURE(t.contains(10)); + ENSURE(!t.contains(12)); + ENSURE(t.contains(14)); + ENSURE(t.contains(13)); t.insert(16); - SASSERT(t.size() == 4); + ENSURE(t.size() == 4); t.insert(18); - SASSERT(t.size() == 5); - SASSERT(t.used_slots() == 2); + ENSURE(t.size() == 5); + ENSURE(t.used_slots() == 2); display(t.begin(), t.end()); t.erase(10); display(t.begin(), t.end()); - SASSERT(!t.contains(10)); - SASSERT(!t.contains(12)); - SASSERT(t.contains(14)); - SASSERT(t.contains(13)); - SASSERT(t.contains(16)); - SASSERT(t.contains(18)); + ENSURE(!t.contains(10)); + ENSURE(!t.contains(12)); + ENSURE(t.contains(14)); + ENSURE(t.contains(13)); + ENSURE(t.contains(16)); + ENSURE(t.contains(18)); } static void tst3() { dint_table t; t.insert(10); t.insert(12); - SASSERT(t.used_slots() == 1); - SASSERT(t.contains(10)); - SASSERT(t.contains(12)); + ENSURE(t.used_slots() == 1); + ENSURE(t.contains(10)); + ENSURE(t.contains(12)); t.erase(12); t.erase(10); - SASSERT(t.size() == 0); - SASSERT(t.empty()); - SASSERT(t.used_slots() == 0); + ENSURE(t.size() == 0); + ENSURE(t.empty()); + ENSURE(t.used_slots() == 0); t.insert(10); - SASSERT(t.used_slots() == 1); - SASSERT(t.contains(10)); - SASSERT(t.size() == 1); + ENSURE(t.used_slots() == 1); + ENSURE(t.contains(10)); + ENSURE(t.size() == 1); } typedef int_hashtable > int_set; @@ -123,29 +123,29 @@ static void tst4(unsigned num, unsigned N) { TRACE("chashtable", tout << "erase " << v << "\n";); s.erase(v); t.erase(v); - SASSERT(!t.contains(v)); + ENSURE(!t.contains(v)); } else { TRACE("chashtable", tout << "insert " << v << "\n";); s.insert(v); t.insert(v); - SASSERT(t.contains(v)); + ENSURE(t.contains(v)); } - SASSERT(s.size() == t.size()); - SASSERT(s.empty() == t.empty()); + ENSURE(s.size() == t.size()); + ENSURE(s.empty() == t.empty()); } std::cout << "size: " << s.size() << " " << t.size() << "\n"; int_set::iterator it1 = s.begin(); int_set::iterator end1 = s.end(); for(; it1 != end1; ++it1) { - SASSERT(t.contains(*it1)); + ENSURE(t.contains(*it1)); } typename T::iterator it2 = t.begin(); typename T::iterator end2 = t.end(); for(; it2 != end2; ++it2) { - SASSERT(s.contains(*it2)); - SASSERT(t.contains(*it2)); + ENSURE(s.contains(*it2)); + ENSURE(t.contains(*it2)); } } @@ -164,10 +164,10 @@ static void tst5() { static void tst6() { int_map m; m.insert(10, 4); - SASSERT(m.contains(10)); + ENSURE(m.contains(10)); DEBUG_CODE({ int r; - SASSERT(m.find(10, r) && r == 4); + ENSURE(m.find(10, r) && r == 4); }); } diff --git a/src/test/diff_logic.cpp b/src/test/diff_logic.cpp index 70345c2d6..3a1ec198d 100644 --- a/src/test/diff_logic.cpp +++ b/src/test/diff_logic.cpp @@ -70,20 +70,20 @@ static void tst2() { g.init_var(3); g.init_var(4); smt::literal d; - SASSERT(g.enable_edge(g.add_edge(1, 2, rational(-1), l1))); - SASSERT(g.get_edge_weight(1, 2, w, d) && w == rational(-1)); - SASSERT(!g.get_edge_weight(2, 3, w, d)); - SASSERT(g.enable_edge(g.add_edge(2, 3, rational(-2), l2))); - SASSERT(g.enable_edge(g.add_edge(1, 4, rational(1), l3))); - SASSERT(g.get_edge_weight(1, 2, w, d) && w == rational(-1)); - SASSERT(g.get_edge_weight(1, 4, w, d) && w == rational(1)); - SASSERT(!g.get_edge_weight(1, 3, w, d)); - SASSERT(g.enable_edge(g.add_edge(2, 4, rational(10), l6))); - SASSERT(g.is_feasible()); + ENSURE(g.enable_edge(g.add_edge(1, 2, rational(-1), l1))); + ENSURE(g.get_edge_weight(1, 2, w, d) && w == rational(-1)); + ENSURE(!g.get_edge_weight(2, 3, w, d)); + ENSURE(g.enable_edge(g.add_edge(2, 3, rational(-2), l2))); + ENSURE(g.enable_edge(g.add_edge(1, 4, rational(1), l3))); + ENSURE(g.get_edge_weight(1, 2, w, d) && w == rational(-1)); + ENSURE(g.get_edge_weight(1, 4, w, d) && w == rational(1)); + ENSURE(!g.get_edge_weight(1, 3, w, d)); + ENSURE(g.enable_edge(g.add_edge(2, 4, rational(10), l6))); + ENSURE(g.is_feasible()); g.push(); - SASSERT(g.enable_edge(g.add_edge(3, 0, rational(2), l4))); - SASSERT(!g.enable_edge(g.add_edge(0, 1, rational(-1), l5))); - SASSERT(!g.is_feasible()); + ENSURE(g.enable_edge(g.add_edge(3, 0, rational(2), l4))); + ENSURE(!g.enable_edge(g.add_edge(0, 1, rational(-1), l5))); + ENSURE(!g.is_feasible()); TRACE("diff_logic", g.display(tout);); struct proc { svector found; @@ -96,22 +96,22 @@ static void tst2() { }; proc p; g.traverse_neg_cycle(true, p); - SASSERT(p.found[0] == false); - SASSERT(p.found[1] == true); - SASSERT(p.found[2] == true); - SASSERT(p.found[3] == false); - SASSERT(p.found[4] == true); - SASSERT(p.found[5] == true); - SASSERT(p.found[6] == false); + ENSURE(p.found[0] == false); + ENSURE(p.found[1] == true); + ENSURE(p.found[2] == true); + ENSURE(p.found[3] == false); + ENSURE(p.found[4] == true); + ENSURE(p.found[5] == true); + ENSURE(p.found[6] == false); g.pop(1); - SASSERT(g.is_feasible()); + ENSURE(g.is_feasible()); TRACE("diff_logic", g.display(tout);); } static int add_edge(dlg& g, dl_var src, dl_var dst, int weight, unsigned lit) { int id = g.add_edge(src, dst, rational(weight), smt::literal(lit)); bool ok = g.enable_edge(id); - SASSERT(ok); + ENSURE(ok); return id; } @@ -147,7 +147,7 @@ static void tst3() { for (unsigned i = 0; i < subsumed.size(); ++i) { std::cout << "subsumed: " << subsumed[i] << "\n"; - SASSERT(e38 == subsumed[i]); + ENSURE(e38 == subsumed[i]); tst_dl_functor tst_fn; diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index 8a62dcb7d..8d60cd883 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -51,12 +51,12 @@ static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, cha dealloc(p); func_decl * pred = ctx.try_get_predicate_decl(symbol(pred_name)); - SASSERT(pred); - SASSERT(pred->get_arity()==1); + ENSURE(pred); + ENSURE(pred->get_arity()==1); app_ref query_app(m.mk_app(pred, m.mk_var(0, pred->get_domain()[0])), m); lbool status = ctx.query(query_app); - SASSERT(status != l_undef); + ENSURE(status != l_undef); return status; } @@ -77,9 +77,9 @@ static void dl_context_simple_query_test(params_ref & params) { app_ref c_1(decl_util.mk_constant(1, res1->get_signature()[0]), m); relation_fact f(m); f.push_back(c_0); - SASSERT(res1->contains_fact(f)); + ENSURE(res1->contains_fact(f)); f[0]=c_1; - SASSERT(!res1->contains_fact(f)); + ENSURE(!res1->contains_fact(f)); #endif } diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index c375587fb..84ffd548a 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -37,12 +37,12 @@ namespace datalog { sparse_table_plugin & plugin = static_cast(*rctx.get_rmanager().get_table_plugin(symbol("sparse"))); - SASSERT(&plugin); + ENSURE(&plugin); table_signature sig2; sig2.push_back(2); sig2.push_back(2); sig2.set_functional_columns(1); - SASSERT(plugin.can_handle_signature(sig2)); + ENSURE(plugin.can_handle_signature(sig2)); table_fact f00; f00.push_back(0); @@ -56,32 +56,32 @@ namespace datalog { { table_aptr t0 = plugin.mk_empty(sig2); - SASSERT(t0->empty()); + ENSURE(t0->empty()); t0->add_fact(f00); - SASSERT(!t0->empty()); - SASSERT(t0->get_size_estimate_rows()==1); + ENSURE(!t0->empty()); + ENSURE(t0->get_size_estimate_rows()==1); t0->add_fact(f01); - SASSERT(t0->get_size_estimate_rows()==1); + ENSURE(t0->get_size_estimate_rows()==1); t0->add_fact(f11); - SASSERT(t0->get_size_estimate_rows()==2); + ENSURE(t0->get_size_estimate_rows()==2); unsigned rem_cols0[]={0}; scoped_ptr project0 = rmgr.mk_project_fn(*t0, 1, rem_cols0); table_aptr t1 = (*project0)(*t0); - SASSERT(t1->get_size_estimate_rows()==2); - SASSERT(t1->get_signature().functional_columns()==0); //project on non-functional column cancels functional + ENSURE(t1->get_size_estimate_rows()==2); + ENSURE(t1->get_signature().functional_columns()==0); //project on non-functional column cancels functional unsigned rem_cols1[]={1}; scoped_ptr project1 = rmgr.mk_project_fn(*t0, 1, rem_cols1); table_aptr t2 = (*project1)(*t0); - SASSERT(t2->get_size_estimate_rows()==2); + ENSURE(t2->get_size_estimate_rows()==2); idx_set acc; collector_of_reduced * reducer = alloc(collector_of_reduced, acc); scoped_ptr rproject = rmgr.mk_project_with_reduce_fn(*t0, 1, rem_cols0, reducer); table_aptr rt = (*rproject)(*t0); - SASSERT(acc.num_elems()==1); - SASSERT(rt->get_size_estimate_rows()==1); + ENSURE(acc.num_elems()==1); + ENSURE(rt->get_size_estimate_rows()==1); } { table_aptr t0 = plugin.mk_empty(sig2); @@ -90,44 +90,44 @@ namespace datalog { unsigned join_cols[]={1}; scoped_ptr join0 = rmgr.mk_join_fn(*t0, *t0, 1, join_cols, join_cols); table_aptr t1 = (*join0)(*t0, *t0); - SASSERT(t1->get_signature().size()==4); - SASSERT(t1->get_signature().functional_columns()==2); + ENSURE(t1->get_signature().size()==4); + ENSURE(t1->get_signature().functional_columns()==2); table_fact f0011; f0011.push_back(0); f0011.push_back(0); f0011.push_back(1); f0011.push_back(1); - SASSERT(t1->contains_fact(f0011)); + ENSURE(t1->contains_fact(f0011)); table_fact f0111 = f0011; f0111[1] = 1; - SASSERT(!t1->contains_fact(f0111)); + ENSURE(!t1->contains_fact(f0111)); } { table_aptr t0 = plugin.mk_empty(sig2); t0->display(std::cout<<"0:"); - SASSERT(t0->get_signature().functional_columns()==1); + ENSURE(t0->get_signature().functional_columns()==1); table_fact aux_fact; aux_fact = f01; TRUSTME( t0->suggest_fact(aux_fact) ); t0->display(std::cout<<"1:"); - SASSERT(t0->contains_fact(f01)); - SASSERT(aux_fact[1]==1); + ENSURE(t0->contains_fact(f01)); + ENSURE(aux_fact[1]==1); aux_fact = f00; TRUSTME( !t0->suggest_fact(aux_fact) ); t0->display(std::cout<<"2:"); - SASSERT(t0->contains_fact(f01)); - SASSERT(!t0->contains_fact(f00)); - SASSERT(aux_fact[1]==1); + ENSURE(t0->contains_fact(f01)); + ENSURE(!t0->contains_fact(f00)); + ENSURE(aux_fact[1]==1); t0->ensure_fact(f00); t0->display(std::cout<<"3:"); - SASSERT(t0->contains_fact(f00)); - SASSERT(!t0->contains_fact(f01)); + ENSURE(t0->contains_fact(f00)); + ENSURE(!t0->contains_fact(f01)); } } @@ -140,7 +140,7 @@ namespace datalog { relation_manager & rmgr = ctx.get_rel_context()->get_rmanager(); relation_plugin & rel_plugin = *rmgr.get_relation_plugin(params.get_sym("default_relation", symbol("sparse"))); - SASSERT(&rel_plugin); + ENSURE(&rel_plugin); finite_product_relation_plugin plg(rel_plugin, rmgr); sort_ref byte_srt_ref(dl_util.mk_sort(symbol("BYTE"), 256), m); @@ -194,9 +194,9 @@ namespace datalog { scoped_rel r2 = r1->clone(); scoped_rel r3 = r2->clone(); - SASSERT(!r1->contains_fact(f77)); + ENSURE(!r1->contains_fact(f77)); r1->add_fact(f77); - SASSERT(r1->contains_fact(f77)); + ENSURE(r1->contains_fact(f77)); r2->add_fact(f79); r3->add_fact(f99); @@ -207,34 +207,34 @@ namespace datalog { r2->display( std::cout << "r2 1\n"); r4->display( std::cout << "r4 0\n"); - SASSERT(!r4->contains_fact(f77)); - SASSERT(r4->contains_fact(f79)); + ENSURE(!r4->contains_fact(f77)); + ENSURE(r4->contains_fact(f79)); r4->add_fact(f77); r4->display( std::cout << "r4 1\n"); - SASSERT(r4->contains_fact(f77)); - SASSERT(r4->contains_fact(f79)); + ENSURE(r4->contains_fact(f77)); + ENSURE(r4->contains_fact(f79)); r4->add_fact(f99); r4->display( std::cout << "r4 2\n"); - SASSERT(r4->contains_fact(f99)); + ENSURE(r4->contains_fact(f99)); std::cout << "------ testing union ------\n"; r2->display( std::cout << "r2\n"); scoped_ptr union_op = rmgr.mk_union_fn(*r1, *r2, r3.get()); - SASSERT(union_op); + ENSURE(union_op); (*union_op)(*r1, *r2, r3.get()); r1->display( std::cout << "r1\n"); r2->display( std::cout << "r2\n"); r3->display( std::cout << "r3\n"); - SASSERT(r1->contains_fact(f77)); - SASSERT(r1->contains_fact(f79)); - SASSERT(!r1->contains_fact(f99)); + ENSURE(r1->contains_fact(f77)); + ENSURE(r1->contains_fact(f79)); + ENSURE(!r1->contains_fact(f99)); - SASSERT(!r3->contains_fact(f77)); - SASSERT(r3->contains_fact(f79)); - SASSERT(r3->contains_fact(f99)); + ENSURE(!r3->contains_fact(f77)); + ENSURE(r3->contains_fact(f79)); + ENSURE(r3->contains_fact(f99)); std::cout << "------ testing join ------\n"; @@ -264,9 +264,9 @@ namespace datalog { jr_rr->display( std::cout << "rr\n"); - SASSERT(!jr_tt->contains_fact(f7797)); - SASSERT(jr_tr->contains_fact(f7797)); - SASSERT(jr_rr->contains_fact(f7797)); + ENSURE(!jr_tt->contains_fact(f7797)); + ENSURE(jr_tr->contains_fact(f7797)); + ENSURE(jr_rr->contains_fact(f7797)); std::cout << "------ testing project ------\n"; @@ -288,17 +288,17 @@ namespace datalog { scoped_rel sr_2r = (*proj_2r)(*r31); scoped_rel sr_1t = (*proj_1t)(*r31); - SASSERT(sr_1r->contains_fact(f79)); - SASSERT(sr_1r->contains_fact(f97)); - SASSERT(!sr_1r->contains_fact(f77)); + ENSURE(sr_1r->contains_fact(f79)); + ENSURE(sr_1r->contains_fact(f97)); + ENSURE(!sr_1r->contains_fact(f77)); - SASSERT(sr_2r->contains_fact(f7)); - SASSERT(sr_2r->contains_fact(f9)); + ENSURE(sr_2r->contains_fact(f7)); + ENSURE(sr_2r->contains_fact(f9)); - SASSERT(sr_1t->contains_fact(f79)); - SASSERT(!sr_1t->contains_fact(f97)); - SASSERT(sr_1t->contains_fact(f77)); - SASSERT(sr_1t->contains_fact(f99)); + ENSURE(sr_1t->contains_fact(f79)); + ENSURE(!sr_1t->contains_fact(f97)); + ENSURE(sr_1t->contains_fact(f77)); + ENSURE(sr_1t->contains_fact(f99)); std::cout << "------ testing filter_interpreted ------\n"; @@ -314,8 +314,8 @@ namespace datalog { scoped_ptr i_filter = rmgr.mk_filter_interpreted_fn(*r41, cond); (*i_filter)(*r41); - SASSERT(r41->contains_fact(f7797)); - SASSERT(!r41->contains_fact(f7997)); + ENSURE(r41->contains_fact(f7797)); + ENSURE(!r41->contains_fact(f7997)); std::cout << "------ testing filter_by_negation ------\n"; @@ -334,9 +334,9 @@ namespace datalog { nf_r31_cols, nf_r1_cols); (*neg_filter)(*r31, *r1); - SASSERT(!r31->contains_fact(f779)); - SASSERT(r31->contains_fact(f977)); - SASSERT(r31->contains_fact(f799)); + ENSURE(!r31->contains_fact(f779)); + ENSURE(r31->contains_fact(f977)); + ENSURE(r31->contains_fact(f799)); } diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index e69f1fb13..eaa26cdbb 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -23,7 +23,7 @@ void dl_query_ask_ground_query(context & ctx, func_decl * pred, relation_fact & lbool is_sat = ctx.query(query); std::cerr << "@@ query should succeed: " << should_be_successful << "\n"; - SASSERT(is_sat != l_undef); + ENSURE(is_sat != l_undef); if((is_sat != l_true) == should_be_successful) { std::cerr<<"wrong ground query answer!\n"; UNREACHABLE(); @@ -80,13 +80,13 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, func_decl * pred_b = *it; std::cerr << "Checking queries on relation " << pred_b->get_name() << "\n"; func_decl * pred_q = ctx_q.try_get_predicate_decl(symbol(pred_b->get_name().bare_str())); - SASSERT(pred_q); + ENSURE(pred_q); relation_base & rel_b = ctx_b.get_rel_context()->get_relation(pred_b); relation_signature sig_b = rel_b.get_signature(); relation_signature sig_q = ctx_q.get_rel_context()->get_relation(pred_q).get_signature(); - SASSERT(sig_b.size()==sig_q.size()); + ENSURE(sig_b.size()==sig_q.size()); std::cerr << "Queries on random facts...\n"; relation_fact f_b(m); @@ -164,7 +164,7 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) { const unsigned attempts = 10; func_decl * v_pred = ctx.try_get_predicate_decl(symbol("V")); - SASSERT(v_pred); + ENSURE(v_pred); sort * var_sort = v_pred->get_domain(0); uint64 var_sz; @@ -180,7 +180,7 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) { app_ref query_lit(m.mk_app(v_pred, q_args.c_ptr()), m); lbool is_sat = ctx.query(query_lit); - SASSERT(is_sat != l_undef); + ENSURE(is_sat != l_undef); bool found = is_sat == l_true; std::cerr<<"query finished: "<get_rmanager(); m.register_plugin(alloc(interval_relation_plugin, m)); interval_relation_plugin& ip = dynamic_cast(*m.get_relation_plugin(symbol("interval_relation"))); - SASSERT(&ip); + ENSURE(&ip); relation_signature sig; sort* int_sort = autil.mk_int(); @@ -38,8 +38,8 @@ namespace datalog { i1.display(std::cout); i2.display(std::cout); - SASSERT(i1.empty()); - SASSERT(!i2.empty()); + ENSURE(i1.empty()); + ENSURE(!i2.empty()); app_ref cond1(ast_m), cond2(ast_m), cond3(ast_m); app_ref cond4(ast_m), cond5(ast_m), cond6(ast_m); @@ -84,11 +84,11 @@ namespace datalog { fact1.push_back(autil.mk_numeral(rational(4), true)); fact1.push_back(autil.mk_numeral(rational(4), true)); fact1.push_back(autil.mk_numeral(rational(5), true)); - SASSERT(i2.contains_fact(fact1)); + ENSURE(i2.contains_fact(fact1)); fact1[0] = autil.mk_numeral(rational(-1), true); - SASSERT(i2.contains_fact(fact1)); + ENSURE(i2.contains_fact(fact1)); fact1[0] = autil.mk_numeral(rational(1), true); - SASSERT(!i2.contains_fact(fact1)); + ENSURE(!i2.contains_fact(fact1)); relation_base* i5 = (*ren1)(i2); i2.display(std::cout << "Orig\n"); @@ -97,7 +97,7 @@ namespace datalog { (*filterCond1)(i2); i2.display(std::cout); // empty - SASSERT(i2.empty()); + ENSURE(i2.empty()); relation_base* i4 = (*proj2)(*i3); i4->display(std::cout); @@ -128,7 +128,7 @@ namespace datalog { relation_manager & m = ctx.get_rel_context()->get_rmanager(); m.register_plugin(alloc(bound_relation_plugin, m)); bound_relation_plugin& br = dynamic_cast(*m.get_relation_plugin(symbol("bound_relation"))); - SASSERT(&br); + ENSURE(&br); relation_signature sig; sort* int_sort = autil.mk_int(); @@ -142,8 +142,8 @@ namespace datalog { i1.display(std::cout << "empty:\n"); i2.display(std::cout << "full:\n"); - SASSERT(i1.empty()); - SASSERT(!i2.empty()); + ENSURE(i1.empty()); + ENSURE(!i2.empty()); app_ref cond1(ast_m), cond2(ast_m), cond3(ast_m); app_ref cond4(ast_m), cond5(ast_m), cond6(ast_m); @@ -201,7 +201,7 @@ namespace datalog { relation_base* i5 = (*ren1)(i2); i5->display(std::cout); - //SASSERT(i2.empty()); + //ENSURE(i2.empty()); relation_base* i4 = (*proj2)(*i3); i4->display(std::cout); diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index 62eec34bc..f9ccb3116 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -12,7 +12,7 @@ typedef datalog::table_base* (*mk_table_fn)(datalog::relation_manager& m, datalo static datalog::table_base* mk_bv_table(datalog::relation_manager& m, datalog::table_signature& sig) { datalog::table_plugin * p = m.get_table_plugin(symbol("bitvector")); - SASSERT(p); + ENSURE(p); return p->mk_empty(sig); } @@ -57,12 +57,12 @@ static void test_table(mk_table_fn mk_table) { std::cout << "\n"; } - SASSERT(table.contains_fact(row1)); - SASSERT(table.contains_fact(row2)); - SASSERT(!table.contains_fact(row3)); + ENSURE(table.contains_fact(row1)); + ENSURE(table.contains_fact(row2)); + ENSURE(!table.contains_fact(row3)); #if 0 table.remove_facts(1, &row1); - SASSERT(!table.contains_fact(row1)); + ENSURE(!table.contains_fact(row1)); #endif table.add_fact(row1); diff --git a/src/test/dl_util.cpp b/src/test/dl_util.cpp index 02e40bbd9..44b95934e 100644 --- a/src/test/dl_util.cpp +++ b/src/test/dl_util.cpp @@ -22,7 +22,7 @@ void dl_util_two_array_sort() { datalog::sort_two_arrays(num, a1, a2); for(unsigned i=0; i result; // VERIFY(!m.intersect(*d1,*d0, result)); // m.subtract(*d1,*d0, result); - SASSERT(result.empty()); + ENSURE(result.empty()); dX = m.allocateX(); m.display(std::cout, *d0) << "\n"; m.display(std::cout, *dX) << "\n"; - SASSERT(m.contains(*dX,*d1)); - SASSERT(m.contains(*dX,*d0)); - SASSERT(!m.contains(*d0,*d1)); - SASSERT(!m.contains(*d1,*d0)); + ENSURE(m.contains(*dX,*d1)); + ENSURE(m.contains(*dX,*d0)); + ENSURE(!m.contains(*d0,*d1)); + ENSURE(!m.contains(*d1,*d0)); d1->neg().push_back(m.tbvm().allocate0()); @@ -88,14 +88,14 @@ static void tst_doc1(unsigned n) { doc_ref d1_2(m1, m1.allocate1()); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; - SASSERT(m1.equals(*d1_1,*d1_2)); + ENSURE(m1.equals(*d1_1,*d1_2)); m.set(*d1,2,BIT_x); m.set(*d1,4,BIT_x); d1_1 = m.project(m1, to_delete, *d1); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; d1->neg().push_back(m.tbvm().allocate1()); - SASSERT(m.well_formed(*d1)); + ENSURE(m.well_formed(*d1)); d1_1 = m.project(m1, to_delete, *d1); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; @@ -146,11 +146,11 @@ class test_doc_cls { tbv_ref t(dm.tbvm()); t = mk_rand_tbv(); doc* result = dm.allocate(*t); - SASSERT(dm.tbvm().equals(*t, result->pos())); + ENSURE(dm.tbvm().equals(*t, result->pos())); for (unsigned i = 0; i < num_diff; ++i) { result->neg().push_back(mk_rand_tbv(result->pos())); } - SASSERT(dm.well_formed(*result)); + ENSURE(dm.well_formed(*result)); return result; } @@ -181,7 +181,7 @@ class test_doc_cls { expr_ref result(m); expr_ref_vector conjs(m); unsigned n = m2.num_tbits(); - SASSERT(n <= m_vars.size()); + ENSURE(n <= m_vars.size()); for (unsigned i = 0; i < n; ++i) { switch (t[i]) { case BIT_x: @@ -347,7 +347,7 @@ class test_doc_cls { tout << mk_pp(fml2, m) << "\n"; ); } - SASSERT(res == l_false); + ENSURE(res == l_false); } @@ -464,7 +464,7 @@ public: d2.display(dm, tout) << "\n";); d1.intersect(dm, d2); TRACE("doc", d1.display(dm, tout) << "\n";); - SASSERT(d1.well_formed(dm)); + ENSURE(d1.well_formed(dm)); fml3 = to_formula(d1, dm); fml1 = m.mk_and(fml1, fml2); check_equiv(fml1, fml3); diff --git a/src/test/ext_numeral.cpp b/src/test/ext_numeral.cpp index 6f92b1372..a35af1ba6 100644 --- a/src/test/ext_numeral.cpp +++ b/src/test/ext_numeral.cpp @@ -26,11 +26,11 @@ static void tst_ ## NAME(int a, ext_numeral_kind ak, int expected_c, ext_numeral scoped_mpq _a(m); \ m.set(_a, a); \ NAME(m, _a, ak); \ - SASSERT(ak == expected_ck); \ + ENSURE(ak == expected_ck); \ if (expected_ck == EN_NUMERAL) { \ scoped_mpq _expected_c(m); \ m.set(_expected_c, expected_c); \ - SASSERT(m.eq(_a, _expected_c)); \ + ENSURE(m.eq(_a, _expected_c)); \ } \ } @@ -45,11 +45,11 @@ static void FUN_NAME(int a, ext_numeral_kind ak, int b, ext_numeral_kind bk, int m.set(_b, b); \ ext_numeral_kind ck; \ OP_NAME(m, _a, ak, _b, bk, _c, ck); \ - SASSERT(ck == expected_ck); \ + ENSURE(ck == expected_ck); \ if (expected_ck == EN_NUMERAL) { \ scoped_mpq _expected_c(m); \ m.set(_expected_c, expected_c); \ - SASSERT(m.eq(_c, _expected_c)); \ + ENSURE(m.eq(_c, _expected_c)); \ } \ } @@ -340,52 +340,52 @@ static void tst2() { static void tst3() { unsynch_mpq_manager m; scoped_mpq a(m); - SASSERT(is_zero(m, a, EN_NUMERAL)); - SASSERT(!is_zero(m, a, EN_PLUS_INFINITY)); - SASSERT(!is_zero(m, a, EN_MINUS_INFINITY)); - SASSERT(!is_pos(m, a, EN_NUMERAL)); - SASSERT(is_pos(m, a, EN_PLUS_INFINITY)); - SASSERT(!is_pos(m, a, EN_MINUS_INFINITY)); - SASSERT(!is_infinite(EN_NUMERAL)); - SASSERT(is_infinite(EN_PLUS_INFINITY)); - SASSERT(is_infinite(EN_MINUS_INFINITY)); - SASSERT(!is_neg(m, a, EN_NUMERAL)); - SASSERT(!is_neg(m, a, EN_PLUS_INFINITY)); - SASSERT(is_neg(m, a, EN_MINUS_INFINITY)); + ENSURE(is_zero(m, a, EN_NUMERAL)); + ENSURE(!is_zero(m, a, EN_PLUS_INFINITY)); + ENSURE(!is_zero(m, a, EN_MINUS_INFINITY)); + ENSURE(!is_pos(m, a, EN_NUMERAL)); + ENSURE(is_pos(m, a, EN_PLUS_INFINITY)); + ENSURE(!is_pos(m, a, EN_MINUS_INFINITY)); + ENSURE(!is_infinite(EN_NUMERAL)); + ENSURE(is_infinite(EN_PLUS_INFINITY)); + ENSURE(is_infinite(EN_MINUS_INFINITY)); + ENSURE(!is_neg(m, a, EN_NUMERAL)); + ENSURE(!is_neg(m, a, EN_PLUS_INFINITY)); + ENSURE(is_neg(m, a, EN_MINUS_INFINITY)); m.set(a, 10); - SASSERT(!is_zero(m, a, EN_NUMERAL)); - SASSERT(is_pos(m, a, EN_NUMERAL)); - SASSERT(!is_neg(m, a, EN_NUMERAL)); - SASSERT(!is_infinite(EN_NUMERAL)); + ENSURE(!is_zero(m, a, EN_NUMERAL)); + ENSURE(is_pos(m, a, EN_NUMERAL)); + ENSURE(!is_neg(m, a, EN_NUMERAL)); + ENSURE(!is_infinite(EN_NUMERAL)); m.set(a, -5); - SASSERT(!is_zero(m, a, EN_NUMERAL)); - SASSERT(!is_pos(m, a, EN_NUMERAL)); - SASSERT(is_neg(m, a, EN_NUMERAL)); - SASSERT(!is_infinite(EN_NUMERAL)); + ENSURE(!is_zero(m, a, EN_NUMERAL)); + ENSURE(!is_pos(m, a, EN_NUMERAL)); + ENSURE(is_neg(m, a, EN_NUMERAL)); + ENSURE(!is_infinite(EN_NUMERAL)); ext_numeral_kind ak; ak = EN_MINUS_INFINITY; reset(m, a, ak); - SASSERT(is_zero(m, a, EN_NUMERAL)); + ENSURE(is_zero(m, a, EN_NUMERAL)); { std::ostringstream buffer; display(buffer, m, a, ak); - SASSERT(buffer.str() == "0"); + ENSURE(buffer.str() == "0"); } { std::ostringstream buffer; m.set(a, -10); display(buffer, m, a, ak); - SASSERT(buffer.str() == "-10"); + ENSURE(buffer.str() == "-10"); } { std::ostringstream buffer; display(buffer, m, a, EN_PLUS_INFINITY); - SASSERT(buffer.str() == "+oo"); + ENSURE(buffer.str() == "+oo"); } { std::ostringstream buffer; display(buffer, m, a, EN_MINUS_INFINITY); - SASSERT(buffer.str() == "-oo"); + ENSURE(buffer.str() == "-oo"); } } diff --git a/src/test/fixed_bit_vector.cpp b/src/test/fixed_bit_vector.cpp index 7bd9e62c3..0160fe574 100644 --- a/src/test/fixed_bit_vector.cpp +++ b/src/test/fixed_bit_vector.cpp @@ -31,11 +31,11 @@ static void tst1() { m.set(*b, 0, true); m.set(*b, 1, false); m.set(*b, 2, true); - SASSERT(b->get(0) == true); - SASSERT(b->get(1) == false); - SASSERT(b->get(2) == true); - SASSERT(b->get(3) == false); - SASSERT(b->get(29) == false); + ENSURE(b->get(0) == true); + ENSURE(b->get(1) == false); + ENSURE(b->get(2) == true); + ENSURE(b->get(3) == false); + ENSURE(b->get(29) == false); m.deallocate(b); } @@ -55,11 +55,11 @@ static void tst_or() { m.display(std::cout, *b2) << "\n"; m.set_or(*b1, *b2); m.display(std::cout, *b1) << "\n"; - SASSERT(!m.equals(*b1, *b2)); + ENSURE(!m.equals(*b1, *b2)); m.unset(*b1, 4); - SASSERT(m.equals(*b1, *b2)); + ENSURE(m.equals(*b1, *b2)); m.unset(*b1, 3); - SASSERT(!m.equals(*b1, *b2)); + ENSURE(!m.equals(*b1, *b2)); m.deallocate(b1); m.deallocate(b2); } @@ -78,25 +78,25 @@ static void tst_eq(unsigned num_bits) { fixed_bit_vector* b3 = m.allocate0(); m.set(*b1, 3, true); - SASSERT(!m.equals(*b1, *b2)); - SASSERT(m.equals(*b2, *b3)); + ENSURE(!m.equals(*b1, *b2)); + ENSURE(m.equals(*b2, *b3)); m.set(*b3, 3, true); - SASSERT(m.equals(*b1, *b3)); + ENSURE(m.equals(*b1, *b3)); m.set(*b2, num_bits-1, true); m.set(*b3, num_bits-1); m.unset(*b3, 3); - SASSERT(m.equals(*b2, *b3)); + ENSURE(m.equals(*b2, *b3)); m.fill0(*b1); m.set_neg(*b1); m.fill1(*b2); - SASSERT(m.equals(*b1, *b2)); + ENSURE(m.equals(*b1, *b2)); m.fill0(*b1); for (unsigned i = 0; i < num_bits; ++i) { m.set(*b1, i, true); } - SASSERT(m.equals(*b1, *b2)); + ENSURE(m.equals(*b1, *b2)); m.deallocate(b1); m.deallocate(b2); m.deallocate(b3); diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index f7da4edd7..029a13881 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -104,7 +104,7 @@ void test2() { VERIFY(l_true == fd_solver->check_sat(0,0)); fd_solver->get_model(mr); - SASSERT(mr.get()); + ENSURE(mr.get()); model_smt2_pp(std::cout, m, *mr.get(), 0); } diff --git a/src/test/get_implied_equalities.cpp b/src/test/get_implied_equalities.cpp index 37fbe2004..8ddcdb1e9 100644 --- a/src/test/get_implied_equalities.cpp +++ b/src/test/get_implied_equalities.cpp @@ -47,13 +47,13 @@ static void tst_get_implied_equalities1() { for (i = 0; i < num_terms; ++i) { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } - SASSERT(class_ids[1] == class_ids[0]); - SASSERT(class_ids[2] != class_ids[0]); - SASSERT(class_ids[3] == class_ids[0]); - SASSERT(class_ids[4] != class_ids[0]); - SASSERT(class_ids[5] != class_ids[0]); - SASSERT(class_ids[6] != class_ids[0]); - SASSERT(class_ids[4] == class_ids[5]); + ENSURE(class_ids[1] == class_ids[0]); + ENSURE(class_ids[2] != class_ids[0]); + ENSURE(class_ids[3] == class_ids[0]); + ENSURE(class_ids[4] != class_ids[0]); + ENSURE(class_ids[5] != class_ids[0]); + ENSURE(class_ids[6] != class_ids[0]); + ENSURE(class_ids[4] == class_ids[5]); printf("asserting b <= f(a)\n"); Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, b, fa)); @@ -61,12 +61,12 @@ static void tst_get_implied_equalities1() { for (i = 0; i < num_terms; ++i) { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } - SASSERT(class_ids[1] == class_ids[0]); - SASSERT(class_ids[2] != class_ids[0]); - SASSERT(class_ids[3] == class_ids[0]); - SASSERT(class_ids[4] == class_ids[0]); - SASSERT(class_ids[5] == class_ids[0]); - SASSERT(class_ids[6] == class_ids[0]); + ENSURE(class_ids[1] == class_ids[0]); + ENSURE(class_ids[2] != class_ids[0]); + ENSURE(class_ids[3] == class_ids[0]); + ENSURE(class_ids[4] == class_ids[0]); + ENSURE(class_ids[5] == class_ids[0]); + ENSURE(class_ids[6] == class_ids[0]); Z3_solver_dec_ref(ctx, solver); @@ -103,15 +103,15 @@ static void tst_get_implied_equalities2() { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } - SASSERT(class_ids[1] != class_ids[0]); - SASSERT(class_ids[2] != class_ids[0]); - SASSERT(class_ids[3] != class_ids[0]); - SASSERT(class_ids[4] != class_ids[0]); - SASSERT(class_ids[4] == class_ids[2]); - SASSERT(class_ids[2] != class_ids[1]); - SASSERT(class_ids[3] != class_ids[1]); - SASSERT(class_ids[4] != class_ids[1]); - SASSERT(class_ids[3] != class_ids[2]); + ENSURE(class_ids[1] != class_ids[0]); + ENSURE(class_ids[2] != class_ids[0]); + ENSURE(class_ids[3] != class_ids[0]); + ENSURE(class_ids[4] != class_ids[0]); + ENSURE(class_ids[4] == class_ids[2]); + ENSURE(class_ids[2] != class_ids[1]); + ENSURE(class_ids[3] != class_ids[1]); + ENSURE(class_ids[4] != class_ids[1]); + ENSURE(class_ids[3] != class_ids[2]); /* delete logical context */ Z3_solver_dec_ref(ctx, solver); diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index 47fae454a..0290ac161 100644 --- a/src/test/hashtable.cpp +++ b/src/test/hashtable.cpp @@ -23,10 +23,6 @@ Revision History: #include"hashtable.h" -#ifndef Z3DEBUG -#undef SASSERT -#define SASSERT(COND) { if (!(COND)) std::cerr << "ERROR: " << #COND << "\n"; } ((void) 0) -#endif struct int_hash_proc { unsigned operator()(int x) const { return x * 3; } }; typedef int_hashtable > int_set; @@ -48,16 +44,16 @@ static void tst1() { int v = rand() % (N / 2); h1.insert(v); vals[i] = v; - SASSERT(contains(h1, v)); + ENSURE(contains(h1, v)); } std::cout << "step1\n"; std::cout.flush(); for (int i = 1; i < N; i ++) { - SASSERT(contains(h1, vals[i])); + ENSURE(contains(h1, vals[i])); } std::cout << "step2\n"; std::cout.flush(); for (int i = 1; i < N; i += 2) { h1.erase(vals[i]); - SASSERT(!contains(h1, vals[i])); + ENSURE(!contains(h1, vals[i])); } std::cout << "step3\n"; std::cout.flush(); for (int i = 1; i < N; i += 2) { @@ -65,7 +61,7 @@ static void tst1() { } std::cout << "step4\n"; std::cout.flush(); for (int i = 1; i < N; i ++) { - SASSERT(contains(h1, vals[i])); + ENSURE(contains(h1, vals[i])); } } @@ -78,19 +74,19 @@ static void tst2() { if (rand() % 3 == 2) { h1.erase(v); h2.erase(v); - SASSERT(!contains(h1, v)); + ENSURE(!contains(h1, v)); } else { h1.insert(v); h2.insert(v); - SASSERT(contains(h1, v)); + ENSURE(contains(h1, v)); } } { safe_int_set::iterator it = h2.begin(); safe_int_set::iterator end = h2.end(); for(; it != end; ++it) { - SASSERT(contains(h1, *it)); + ENSURE(contains(h1, *it)); } } { @@ -98,12 +94,12 @@ static void tst2() { int_set::iterator end = h1.end(); int n = 0; for (; it != end; ++it) { - SASSERT(contains(h1, *it)); + ENSURE(contains(h1, *it)); n++; } - SASSERT(n == h1.size()); + ENSURE(n == h1.size()); } - SASSERT(h1.size() == h2.size()); + ENSURE(h1.size() == h2.size()); // std::cout << "size: " << h1.size() << ", capacity: " << h1.capacity() << "\n"; std::cout.flush(); } @@ -114,13 +110,13 @@ static void tst3() { h1.insert(30); h1.erase(20); int_set h2(h1); - SASSERT(h1.contains(10)); - SASSERT(!h1.contains(20)); - SASSERT(h1.contains(30)); - SASSERT(h2.contains(10)); - SASSERT(!h2.contains(20)); - SASSERT(h2.contains(30)); - SASSERT(h2.size() == 2); + ENSURE(h1.contains(10)); + ENSURE(!h1.contains(20)); + ENSURE(h1.contains(30)); + ENSURE(h2.contains(10)); + ENSURE(!h2.contains(20)); + ENSURE(h2.contains(30)); + ENSURE(h2.size() == 2); } void tst_hashtable() { diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 17f9cfaa0..6f827b5e8 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -33,33 +33,33 @@ static void tst1() { for (int i = 0; i < N * 3; i++) { int val = rand() % N; if (!h.contains(val)) { - SASSERT(!t.contains(val)); + ENSURE(!t.contains(val)); h.insert(val); t.insert(val); } else { - SASSERT(t.contains(val)); + ENSURE(t.contains(val)); } } - SASSERT(h.check_invariant()); + ENSURE(h.check_invariant()); int_set::iterator it = t.begin(); int_set::iterator end = t.end(); for (; it != end; ++it) { - SASSERT(h.contains(*it)); + ENSURE(h.contains(*it)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - SASSERT(m1 == m2); - SASSERT(-1 < m2); + ENSURE(m1 == m2); + ENSURE(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { SASSERT(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; +struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap int_heap2; static void init_values() { @@ -89,7 +89,7 @@ static void tst2() { TRACE("heap", tout << "inserting: " << val << "\n";); h.insert(val); TRACE("heap", dump_heap(h, tout);); - SASSERT(h.contains(val)); + ENSURE(h.contains(val)); } } else if (cmd <= 6) { @@ -98,7 +98,7 @@ static void tst2() { TRACE("heap", tout << "removing: " << val << "\n";); h.erase(val); TRACE("heap", dump_heap(h, tout);); - SASSERT(!h.contains(val)); + ENSURE(!h.contains(val)); } } else if (cmd <= 8) { @@ -119,10 +119,10 @@ static void tst2() { } } else { - SASSERT(h.check_invariant()); + ENSURE(h.check_invariant()); } } - SASSERT(h.check_invariant()); + ENSURE(h.check_invariant()); } void tst_heap() { diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index b46ede849..f2ca8a375 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -286,8 +286,8 @@ static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound, random_gen rand(seed); reslimit rl; hilbert_basis hb(rl); - SASSERT(0 < bound); - SASSERT(k <= n); + ENSURE(0 < bound); + ENSURE(k <= n); int ibound = static_cast(bound); for (unsigned i = 0; i < num_ineqs; ++i) { vector nv; diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp index 7a030a452..310d69be2 100644 --- a/src/test/hwf.cpp +++ b/src/test/hwf.cpp @@ -25,16 +25,16 @@ static void bug_set_double() { hwf a; m.set(a, 0.1); - SASSERT(m.is_regular(a)); + ENSURE(m.is_regular(a)); m.set(a, 1.1); - SASSERT(m.is_regular(a)); + ENSURE(m.is_regular(a)); m.set(a, 11.3); - SASSERT(m.is_regular(a)); + ENSURE(m.is_regular(a)); m.set(a, 0.0); - SASSERT(m.is_regular(a)); + ENSURE(m.is_regular(a)); } static void bug_to_rational() { @@ -62,31 +62,31 @@ static void bug_to_rational() { m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + ENSURE(ad == rd); m.set(a, 0.875); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + ENSURE(ad == rd); m.set(a, -1.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + ENSURE(ad == rd); m.set(a, -1.5); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + ENSURE(ad == rd); m.set(a, -0.875); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + ENSURE(ad == rd); m.set(a, 0.1); m.to_rational(a, r); @@ -96,7 +96,7 @@ static void bug_to_rational() { // CMW: This one depends on the rounding mode, // which is implicit in both hwf::set and in mpq::to_double. double diff = (ad-rd); - SASSERT(diff >= -DBL_EPSILON && diff <= DBL_EPSILON); + ENSURE(diff >= -DBL_EPSILON && diff <= DBL_EPSILON); #endif } @@ -107,7 +107,7 @@ static void bug_is_int() { hwf_manager m; hwf a; m.set(a, val); - SASSERT(!m.is_int(a)); + ENSURE(!m.is_int(a)); } void tst_hwf() { diff --git a/src/test/inf_rational.cpp b/src/test/inf_rational.cpp index 1b0a293ce..64d2ab921 100644 --- a/src/test/inf_rational.cpp +++ b/src/test/inf_rational.cpp @@ -23,8 +23,8 @@ Revision History: static void tst0() { inf_rational n(rational(0), false); TRACE("inf_rational", tout << n << "\n";); - SASSERT(n < inf_rational::zero()); - SASSERT(!(n >= inf_rational::zero())); + ENSURE(n < inf_rational::zero()); + ENSURE(!(n >= inf_rational::zero())); } void test_inc_dec( @@ -36,44 +36,44 @@ void test_inc_dec( ) { r += rational(1,5); - SASSERT (r == b_8_5); + ENSURE (r == b_8_5); r -= rational(1,5); - SASSERT (r == b_7_5); + ENSURE (r == b_7_5); r += inf_rational(1,5); - SASSERT (r == b_8_5); + ENSURE (r == b_8_5); r -= inf_rational(1,5); - SASSERT (r == b_7_5); + ENSURE (r == b_7_5); r /= rational(2,1); - SASSERT (r == b_7_10); + ENSURE (r == b_7_10); inf_rational r_pre = r++; - SASSERT (r_pre == b_7_10); - SASSERT (r == b_17_10); + ENSURE (r_pre == b_7_10); + ENSURE (r == b_17_10); inf_rational r_post = --r; - SASSERT (r_post == b_7_10); - SASSERT (r == b_7_10); + ENSURE (r_post == b_7_10); + ENSURE (r == b_7_10); r_post = ++r; - SASSERT (r_post == b_17_10); - SASSERT (r == b_17_10); + ENSURE (r_post == b_17_10); + ENSURE (r == b_17_10); r_pre = r--; - SASSERT (r_pre == b_17_10); - SASSERT (r == b_7_10); + ENSURE (r_pre == b_17_10); + ENSURE (r == b_7_10); r_pre = r; r_pre += inf_rational(1,2); r_post = r_pre; r_post -= inf_rational(1,2); - SASSERT(r == r_post); - SASSERT(r + inf_rational(1,2) == r_pre); + ENSURE(r == r_post); + ENSURE(r + inf_rational(1,2) == r_pre); r_pre = r; r_pre /= rational(2,1); r_post = r_pre; r_post /= rational(1,2); - SASSERT(r == r_post); - SASSERT(rational(1,2) * r == r_pre); - SASSERT(r == r_pre / rational(1,2)); + ENSURE(r == r_post); + ENSURE(rational(1,2) * r == r_pre); + ENSURE(r == r_pre / rational(1,2)); } @@ -84,27 +84,27 @@ tst_inf_rational() inf_rational r1; inf_rational r2(r1); - SASSERT (r1 == r2); + ENSURE (r1 == r2); inf_rational r3(1); inf_rational r4(0); - SASSERT (r4 == r1); - SASSERT (r3 != r4); + ENSURE (r4 == r1); + ENSURE (r3 != r4); inf_rational r5(0,1); inf_rational r6(1,1); inf_rational r7(2,2); inf_rational r8(7,5); - SASSERT (r1 == r5); - SASSERT (r6 == r3); - SASSERT (r7 == r3); + ENSURE (r1 == r5); + ENSURE (r6 == r3); + ENSURE (r7 == r3); inf_rational r9(rational(7,5)); - SASSERT (r8 == r9); + ENSURE (r8 == r9); r9.reset(); - SASSERT (r1 == r9); - SASSERT (r1.is_int()); - SASSERT (!r8.is_int()); - SASSERT (0 == r1.get_int64()); + ENSURE (r1 == r9); + ENSURE (r1.is_int()); + ENSURE (!r8.is_int()); + ENSURE (0 == r1.get_int64()); r9 = r8; - SASSERT (r8 == r9); + ENSURE (r8 == r9); inf_rational n = numerator(r7); inf_rational d = denominator(r7); @@ -130,50 +130,50 @@ tst_inf_rational() } - SASSERT(inf_rational(rational(1,2),true) > inf_rational(rational(1,2))); - SASSERT(inf_rational(rational(1,2),false) < inf_rational(rational(1,2))); - SASSERT(inf_rational(rational(1,2),true) >= inf_rational(rational(1,2))); - SASSERT(inf_rational(rational(1,2)) >= inf_rational(rational(1,2),false)); - SASSERT(inf_rational(rational(1,2),false) != inf_rational(rational(1,2))); - SASSERT(inf_rational(rational(1,2),true) != inf_rational(rational(1,2))); - SASSERT(inf_rational(rational(1,2),false) != inf_rational(rational(1,2),true)); + ENSURE(inf_rational(rational(1,2),true) > inf_rational(rational(1,2))); + ENSURE(inf_rational(rational(1,2),false) < inf_rational(rational(1,2))); + ENSURE(inf_rational(rational(1,2),true) >= inf_rational(rational(1,2))); + ENSURE(inf_rational(rational(1,2)) >= inf_rational(rational(1,2),false)); + ENSURE(inf_rational(rational(1,2),false) != inf_rational(rational(1,2))); + ENSURE(inf_rational(rational(1,2),true) != inf_rational(rational(1,2))); + ENSURE(inf_rational(rational(1,2),false) != inf_rational(rational(1,2),true)); inf_rational h_neg(rational(1,2),false); inf_rational h_pos(rational(1,2),true); h_neg.neg(); - SASSERT(h_neg == -inf_rational(rational(1,2),false)); + ENSURE(h_neg == -inf_rational(rational(1,2),false)); h_neg.neg(); - SASSERT(h_neg == inf_rational(rational(1,2),false)); + ENSURE(h_neg == inf_rational(rational(1,2),false)); - SASSERT(r1.is_zero() && !r1.is_one() && !r1.is_neg() && r1.is_nonneg() && r1.is_nonpos() && !r1.is_pos()); - SASSERT(!r3.is_zero() && r3.is_one() && !r3.is_neg() && r3.is_nonneg() && !r3.is_nonpos() && r3.is_pos()); + ENSURE(r1.is_zero() && !r1.is_one() && !r1.is_neg() && r1.is_nonneg() && r1.is_nonpos() && !r1.is_pos()); + ENSURE(!r3.is_zero() && r3.is_one() && !r3.is_neg() && r3.is_nonneg() && !r3.is_nonpos() && r3.is_pos()); - SASSERT(floor(inf_rational(rational(1,2),false)) == rational()); - SASSERT(floor(inf_rational(rational(1,2))) == rational()); - SASSERT(floor(inf_rational(rational(),false)) == rational(-1)); - SASSERT(floor(inf_rational(rational())) == rational()); - SASSERT(floor(inf_rational(rational(),true)) == rational()); - SASSERT(floor(inf_rational(rational(1),false)) == rational()); - SASSERT(floor(inf_rational(rational(1))) == rational(1)); - SASSERT(floor(inf_rational(rational(1),true)) == rational(1)); + ENSURE(floor(inf_rational(rational(1,2),false)) == rational()); + ENSURE(floor(inf_rational(rational(1,2))) == rational()); + ENSURE(floor(inf_rational(rational(),false)) == rational(-1)); + ENSURE(floor(inf_rational(rational())) == rational()); + ENSURE(floor(inf_rational(rational(),true)) == rational()); + ENSURE(floor(inf_rational(rational(1),false)) == rational()); + ENSURE(floor(inf_rational(rational(1))) == rational(1)); + ENSURE(floor(inf_rational(rational(1),true)) == rational(1)); - SASSERT(ceil(inf_rational(rational(1,2),false)) == rational(1)); - SASSERT(ceil(inf_rational(rational(1,2))) == rational(1)); - SASSERT(ceil(inf_rational(rational(),false)) == rational()); - SASSERT(ceil(inf_rational(rational())) == rational()); - SASSERT(ceil(inf_rational(rational(),true)) == rational(1)); - SASSERT(ceil(inf_rational(rational(1),false)) == rational(1)); - SASSERT(ceil(inf_rational(rational(1))) == rational(1)); - SASSERT(ceil(inf_rational(rational(1),true)) == rational(2)); + ENSURE(ceil(inf_rational(rational(1,2),false)) == rational(1)); + ENSURE(ceil(inf_rational(rational(1,2))) == rational(1)); + ENSURE(ceil(inf_rational(rational(),false)) == rational()); + ENSURE(ceil(inf_rational(rational())) == rational()); + ENSURE(ceil(inf_rational(rational(),true)) == rational(1)); + ENSURE(ceil(inf_rational(rational(1),false)) == rational(1)); + ENSURE(ceil(inf_rational(rational(1))) == rational(1)); + ENSURE(ceil(inf_rational(rational(1),true)) == rational(2)); inf_rational x(rational(1,2),true); inf_rational y(1,2); x.swap(y); - SASSERT (x == inf_rational(1,2)); - SASSERT (y == inf_rational(rational(1,2),true)); + ENSURE (x == inf_rational(1,2)); + ENSURE (y == inf_rational(rational(1,2),true)); - SASSERT(inf_rational(1,2) == abs(-inf_rational(1,2))); + ENSURE(inf_rational(1,2) == abs(-inf_rational(1,2))); } diff --git a/src/test/interval.cpp b/src/test/interval.cpp index ac242cc60..c22156988 100644 --- a/src/test/interval.cpp +++ b/src/test/interval.cpp @@ -438,7 +438,7 @@ void tst_pi() { im.pi(i, r); nm.display_decimal(std::cout, im.lower(r), 32); std::cout << " "; nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n"; - SASSERT(nm.lt(im.lower(r), im.upper(r))); + ENSURE(nm.lt(im.lower(r), im.upper(r))); } del_interval(imc, r); } diff --git a/src/test/karr.cpp b/src/test/karr.cpp index c69932e22..11e7ae17f 100644 --- a/src/test/karr.cpp +++ b/src/test/karr.cpp @@ -131,7 +131,7 @@ namespace karr { matrix T; // length of rows in Ab are twice as long as // length of rows in src. - SASSERT(2*src.A[0].size() == Ab.A[0].size()); + ENSURE(2*src.A[0].size() == Ab.A[0].size()); vector zeros; for (unsigned i = 0; i < src.A[0].size(); ++i) { zeros.push_back(rational(0)); diff --git a/src/test/list.cpp b/src/test/list.cpp index a7ad76972..e377e7bbf 100644 --- a/src/test/list.cpp +++ b/src/test/list.cpp @@ -27,10 +27,10 @@ static void tst1() { list * l2 = new (r) list(20, l1); list * l3 = new (r) list(30); list * l4 = new (r) list(40, l3); - SASSERT(append(r, l1, static_cast *>(0)) == l1); - SASSERT(append(r, l2, static_cast *>(0)) == l2); - SASSERT(append(r, static_cast *>(0), l2) == l2); - SASSERT(append(r, static_cast *>(0), static_cast *>(0)) == 0); + ENSURE(append(r, l1, static_cast *>(0)) == l1); + ENSURE(append(r, l2, static_cast *>(0)) == l2); + ENSURE(append(r, static_cast *>(0), l2) == l2); + ENSURE(append(r, static_cast *>(0), static_cast *>(0)) == 0); TRACE("list", display(tout, l2->begin(), l2->end()); tout << "\n";); list * l5 = append(r, l4, l2); TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";); diff --git a/src/test/map.cpp b/src/test/map.cpp index 7e2cc7e70..c0b084b73 100644 --- a/src/test/map.cpp +++ b/src/test/map.cpp @@ -22,22 +22,22 @@ Revision History: static void tst1() { map str2int; str2int.insert("foo", 35); - SASSERT(str2int.contains("foo")); - SASSERT(str2int.find_iterator("foo") != str2int.end()); - SASSERT((*(str2int.find_iterator("foo"))).m_value == 35); - SASSERT(str2int.size() == 1); + ENSURE(str2int.contains("foo")); + ENSURE(str2int.find_iterator("foo") != str2int.end()); + ENSURE((*(str2int.find_iterator("foo"))).m_value == 35); + ENSURE(str2int.size() == 1); str2int.insert("boo", 32); - SASSERT(str2int.contains("foo")); - SASSERT(str2int.find_iterator("foo") != str2int.end()); - SASSERT((*(str2int.find_iterator("foo"))).m_value == 35); - SASSERT(str2int.contains("boo")); - SASSERT(str2int.find_iterator("boo") != str2int.end()); - SASSERT((*(str2int.find_iterator("boo"))).m_value == 32); - SASSERT(str2int.size() == 2); + ENSURE(str2int.contains("foo")); + ENSURE(str2int.find_iterator("foo") != str2int.end()); + ENSURE((*(str2int.find_iterator("foo"))).m_value == 35); + ENSURE(str2int.contains("boo")); + ENSURE(str2int.find_iterator("boo") != str2int.end()); + ENSURE((*(str2int.find_iterator("boo"))).m_value == 32); + ENSURE(str2int.size() == 2); str2int.remove("boo"); - SASSERT(str2int.size() == 1); - SASSERT(!str2int.contains("boo")); - SASSERT(str2int.contains("foo")); + ENSURE(str2int.size() == 1); + ENSURE(!str2int.contains("boo")); + ENSURE(str2int.contains("foo")); } void tst_map() { diff --git a/src/test/mpf.cpp b/src/test/mpf.cpp index d12675b6d..f00152b09 100644 --- a/src/test/mpf.cpp +++ b/src/test/mpf.cpp @@ -24,38 +24,38 @@ static void bug_set_int() { scoped_mpf a(fm); fm.set(a, 11, 53, 3); - SASSERT(fm.to_double(a) == 3.0); + ENSURE(fm.to_double(a) == 3.0); fm.set(a, 11, 53, 0); - SASSERT(fm.to_double(a) == 0.0); + ENSURE(fm.to_double(a) == 0.0); fm.set(a, 11, 53, -1); - SASSERT(fm.to_double(a) == -1.0); + ENSURE(fm.to_double(a) == -1.0); fm.set(a, 11, 53, INT_MAX); - SASSERT(fm.to_double(a) == (double)INT_MAX); + ENSURE(fm.to_double(a) == (double)INT_MAX); fm.set(a, 11, 53, INT_MIN); - SASSERT(fm.to_double(a) == (double)INT_MIN); + ENSURE(fm.to_double(a) == (double)INT_MIN); fm.set(a, 8, 24, 3); - SASSERT(fm.to_float(a) == 3.0); - SASSERT(fm.to_double(a) == 3.0); + ENSURE(fm.to_float(a) == 3.0); + ENSURE(fm.to_double(a) == 3.0); fm.set(a, 8, 24, 0); - SASSERT(fm.to_float(a) == 0.0); - SASSERT(fm.to_double(a) == 0.0); + ENSURE(fm.to_float(a) == 0.0); + ENSURE(fm.to_double(a) == 0.0); fm.set(a, 8, 24, -1); - SASSERT(fm.to_float(a) == -1.0); - SASSERT(fm.to_double(a) == -1.0); + ENSURE(fm.to_float(a) == -1.0); + ENSURE(fm.to_double(a) == -1.0); fm.set(a, 8, 24, INT_MIN); - SASSERT(fm.to_float(a) == (float)INT_MIN); + ENSURE(fm.to_float(a) == (float)INT_MIN); // CMW: This one depends on the rounding mode, but fm.set(..., int) doesn't have one. // fm.set(a, 8, 24, INT_MAX); - // SASSERT(fm.to_float(a) == (float)INT_MAX); + // ENSURE(fm.to_float(a) == (float)INT_MAX); } static void bug_set_double() { @@ -63,22 +63,22 @@ static void bug_set_double() { scoped_mpf a(fm); fm.set(a, 11, 53, 2.5); - SASSERT(fm.to_double(a) == 2.5); + ENSURE(fm.to_double(a) == 2.5); fm.set(a, 11, 53, -42.25); - SASSERT(fm.to_double(a) == -42.25); + ENSURE(fm.to_double(a) == -42.25); fm.set(a, 8, 24, (double)2.5); - SASSERT(fm.to_double(a) == 2.5); + ENSURE(fm.to_double(a) == 2.5); fm.set(a, 8, 24, (double)-42.25); - SASSERT(fm.to_double(a) == -42.25); + ENSURE(fm.to_double(a) == -42.25); fm.set(a, 8, 24, (float)2.5); - SASSERT(fm.to_float(a) == 2.5); + ENSURE(fm.to_float(a) == 2.5); fm.set(a, 8, 24, (float)-42.25); - SASSERT(fm.to_float(a) == -42.25); + ENSURE(fm.to_float(a) == -42.25); } void tst_mpf() { diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index ca2354b8b..bb06846d5 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -77,10 +77,10 @@ static void tst5() { scoped_mpff a(m), b(m); m.set(a, static_cast(1) << 63); m.display_raw(std::cout, a); std::cout << "\n"; - SASSERT(m.is_zero(b)); - SASSERT(m.lt(b, a)); + ENSURE(m.is_zero(b)); + ENSURE(m.lt(b, a)); m.set(b, -1); - SASSERT(m.lt(b, a)); + ENSURE(m.lt(b, a)); } static void tst6() { @@ -90,10 +90,10 @@ static void tst6() { std::cout << "mpff(1/3) " << a << "\n"; b = a; m.next(b); - SASSERT(m.lt(a, b)); + ENSURE(m.lt(a, b)); std::cout << "b: " << b << "\n"; m.prev(b); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.ceil(b); std::cout << "b: " << b << "\n"; m.set(b, 4, 3); @@ -135,15 +135,15 @@ static void tst_ ## OP ## _core(int64 n1, uint64 d1, int64 n2, uint64 d2, unsign fm.round_to_plus_inf(); \ fm.OP(fa, fb, fc1); \ fm.to_mpq(fc1, qm, qt); \ - SASSERT(qm.le(qc, qt)); \ + ENSURE(qm.le(qc, qt)); \ } \ { \ fm.round_to_minus_inf(); \ fm.OP(fa, fb, fc2); \ fm.to_mpq(fc2, qm, qt); \ - SASSERT(qm.le(qt, qc)); \ + ENSURE(qm.le(qt, qc)); \ } \ - SASSERT(fm.le(fc2, fc1)); \ + ENSURE(fm.le(fc2, fc1)); \ } MK_BIN_OP(add); @@ -182,7 +182,7 @@ static void tst_bug() { scoped_mpq b(qm), c(qm); qm.set(b, 41, 36); fm.to_mpq(a, qm, c); - SASSERT(qm.le(b, c)); + ENSURE(qm.le(b, c)); } static void tst_bug2() { @@ -191,16 +191,16 @@ static void tst_bug2() { fm.set(b, 1); fm.sub(a, b, b); fm.set(a, -1); - SASSERT(fm.eq(a, b)); + ENSURE(fm.eq(a, b)); fm.set(a, 1); fm.set(b, 0); fm.sub(a, b, a); fm.set(b, 1); - SASSERT(fm.eq(a, b)); + ENSURE(fm.eq(a, b)); fm.set(a, 1); fm.set(b, 1); fm.sub(a, b, a); - SASSERT(fm.is_zero(a)); + ENSURE(fm.is_zero(a)); } static void tst_set64(unsigned N, unsigned prec) { @@ -208,69 +208,69 @@ static void tst_set64(unsigned N, unsigned prec) { scoped_mpff a(fm); fm.set(a, static_cast(INT64_MAX)); - SASSERT(fm.is_int64(a)); - SASSERT(fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); fm.inc(a); - SASSERT(!fm.is_int64(a)); - SASSERT(fm.is_uint64(a)); - SASSERT(fm.is_int(a)); + ENSURE(!fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); + ENSURE(fm.is_int(a)); fm.dec(a); - SASSERT(fm.is_int64(a)); - SASSERT(fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); fm.dec(a); - SASSERT(fm.is_int64(a)); - SASSERT(fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); fm.set(a, static_cast(INT64_MIN)); - SASSERT(fm.is_int64(a)); - SASSERT(!fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(!fm.is_uint64(a)); fm.dec(a); - SASSERT(!fm.is_int64(a)); - SASSERT(!fm.is_uint64(a)); - SASSERT(fm.is_int(a)); + ENSURE(!fm.is_int64(a)); + ENSURE(!fm.is_uint64(a)); + ENSURE(fm.is_int(a)); fm.inc(a); - SASSERT(fm.is_int64(a)); - SASSERT(!fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(!fm.is_uint64(a)); fm.inc(a); - SASSERT(fm.is_int64(a)); - SASSERT(!fm.is_uint64(a)); + ENSURE(fm.is_int64(a)); + ENSURE(!fm.is_uint64(a)); fm.set(a, static_cast(UINT64_MAX)); - SASSERT(fm.is_uint64(a)); - SASSERT(!fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); + ENSURE(!fm.is_int64(a)); fm.inc(a); - SASSERT(!fm.is_uint64(a)); - SASSERT(!fm.is_int64(a)); + ENSURE(!fm.is_uint64(a)); + ENSURE(!fm.is_int64(a)); fm.dec(a); - SASSERT(fm.is_uint64(a)); - SASSERT(!fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); + ENSURE(!fm.is_int64(a)); fm.dec(a); - SASSERT(fm.is_uint64(a)); - SASSERT(!fm.is_int64(a)); + ENSURE(fm.is_uint64(a)); + ENSURE(!fm.is_int64(a)); for (unsigned i = 0; i < N; i++) { { uint64 v = (static_cast(rand()) << 32) + static_cast(rand()); fm.set(a, v); - SASSERT(fm.is_uint64(a)); + ENSURE(fm.is_uint64(a)); v = (static_cast(rand() % 3) << 32) + static_cast(rand()); fm.set(a, v); - SASSERT(fm.is_uint64(a)); + ENSURE(fm.is_uint64(a)); } { int64 v = (static_cast(rand() % INT_MAX) << 32) + static_cast(rand()); if (rand()%2 == 0) v = -v; fm.set(a, v); - SASSERT(fm.is_int64(a)); + ENSURE(fm.is_int64(a)); v = (static_cast(rand() % 3) << 32) + static_cast(rand()); if (rand()%2 == 0) v = -v; fm.set(a, v); - SASSERT(fm.is_int64(a)); + ENSURE(fm.is_int64(a)); } } } @@ -282,12 +282,12 @@ static void tst_capacity(unsigned prec = 2) { for (unsigned i = 0; i < 50000; i++) { m.set(a, i); v.push_back(a); - SASSERT(m.is_int(v.back())); - SASSERT(m.is_int64(v.back())); - SASSERT(m.is_uint64(v.back())); + ENSURE(m.is_int(v.back())); + ENSURE(m.is_int64(v.back())); + ENSURE(m.is_uint64(v.back())); } for (unsigned i = 0; i < 50000; i++) { - SASSERT(m.get_int64(v[i]) == i); + ENSURE(m.get_int64(v[i]) == i); } } @@ -296,140 +296,140 @@ static void tst_power(unsigned prec = 2) { scoped_mpff a(m), b(m); // 0^k == 0 - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.power(a, 10, a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); // a != 0 ==> a^0 == 1 m.set(a, 33); m.power(a, 0, a); - SASSERT(m.is_one(a)); + ENSURE(m.is_one(a)); m.set(a, -33); m.power(a, 0, a); - SASSERT(m.is_one(a)); + ENSURE(m.is_one(a)); // a^1 == a m.set(a, 33); m.power(a, 1, b); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set(a, -33); m.power(a, 1, b); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); // checking special support for powers of 2 #ifdef Z3DEBUG unsigned k; #endif m.set(a, 1); - SASSERT(m.is_power_of_two(a, k) && k == 0); + ENSURE(m.is_power_of_two(a, k) && k == 0); m.set(a, 2); - SASSERT(m.is_power_of_two(a, k) && k == 1); + ENSURE(m.is_power_of_two(a, k) && k == 1); m.set(a, 3); - SASSERT(!m.is_power_of_two(a, k)); + ENSURE(!m.is_power_of_two(a, k)); m.set(a, 4); - SASSERT(m.is_power_of_two(a, k) && k == 2); + ENSURE(m.is_power_of_two(a, k) && k == 2); m.set(a, -4); - SASSERT(!m.is_power_of_two(a, k)); + ENSURE(!m.is_power_of_two(a, k)); m.set(a, 8); - SASSERT(m.is_power_of_two(a, k) && k == 3); + ENSURE(m.is_power_of_two(a, k) && k == 3); m.set(a, 0); - SASSERT(!m.is_power_of_two(a)); + ENSURE(!m.is_power_of_two(a)); m.set(a, UINT_MAX); m.inc(a); - SASSERT(m.is_power_of_two(a, k) && k == 32); - SASSERT(m.get_uint64(a) == static_cast(UINT_MAX) + 1); + ENSURE(m.is_power_of_two(a, k) && k == 32); + ENSURE(m.get_uint64(a) == static_cast(UINT_MAX) + 1); m.power(a, 2, a); - SASSERT(m.is_power_of_two(a, k) && k == 64); + ENSURE(m.is_power_of_two(a, k) && k == 64); m.power(a, 4, a); - SASSERT(m.is_power_of_two(a, k) && k == 256); + ENSURE(m.is_power_of_two(a, k) && k == 256); m.round_to_plus_inf(); m.inc(a); - SASSERT(!m.is_power_of_two(a, k)); + ENSURE(!m.is_power_of_two(a, k)); m.set(a, -4); m.power(a, 3, a); m.set(b, -64); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set(a, -4); m.power(a, 4, a); m.set(b, 256); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); // additional tests m.set(a, 5); m.power(a, 3, a); m.set(b, 5*5*5); - SASSERT(m.eq(a,b)); + ENSURE(m.eq(a,b)); m.set(a, -5); m.power(a, 3, a); m.set(b, -5*5*5); - SASSERT(m.eq(a,b)); + ENSURE(m.eq(a,b)); } static void tst_sgn(unsigned prec) { mpff_manager m(prec); scoped_mpff a(m), b(m); - SASSERT(m.is_zero(a) && !m.is_pos(a) && !m.is_neg(a) && m.is_nonpos(a) && m.is_nonneg(a)); + ENSURE(m.is_zero(a) && !m.is_pos(a) && !m.is_neg(a) && m.is_nonpos(a) && m.is_nonneg(a)); m.set(a, 3); - SASSERT(!m.is_zero(a) && m.is_pos(a) && !m.is_neg(a) && !m.is_nonpos(a) && m.is_nonneg(a)); + ENSURE(!m.is_zero(a) && m.is_pos(a) && !m.is_neg(a) && !m.is_nonpos(a) && m.is_nonneg(a)); m.set(a, -3); - SASSERT(!m.is_zero(a) && !m.is_pos(a) && m.is_neg(a) && m.is_nonpos(a) && !m.is_nonneg(a)); + ENSURE(!m.is_zero(a) && !m.is_pos(a) && m.is_neg(a) && m.is_nonpos(a) && !m.is_nonneg(a)); m.set(a, 8); m.power(a, 256, a); - SASSERT(!m.is_zero(a) && m.is_pos(a) && !m.is_neg(a) && !m.is_nonpos(a) && m.is_nonneg(a)); + ENSURE(!m.is_zero(a) && m.is_pos(a) && !m.is_neg(a) && !m.is_nonpos(a) && m.is_nonneg(a)); b = a; m.neg(a); - SASSERT(m.neq(a, b)); - SASSERT(!m.is_zero(a) && !m.is_pos(a) && m.is_neg(a) && m.is_nonpos(a) && !m.is_nonneg(a)); + ENSURE(m.neq(a, b)); + ENSURE(!m.is_zero(a) && !m.is_pos(a) && m.is_neg(a) && m.is_nonpos(a) && !m.is_nonneg(a)); m.neg(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set(a, 1); - SASSERT(m.is_one(a) && !m.is_zero(a) && !m.is_minus_one(a) && m.is_abs_one(a)); + ENSURE(m.is_one(a) && !m.is_zero(a) && !m.is_minus_one(a) && m.is_abs_one(a)); m.neg(a); - SASSERT(!m.is_one(a) && !m.is_zero(a) && m.is_minus_one(a) && m.is_abs_one(a)); + ENSURE(!m.is_one(a) && !m.is_zero(a) && m.is_minus_one(a) && m.is_abs_one(a)); m.set(a, 3); - SASSERT(!m.is_one(a) && !m.is_zero(a) && !m.is_minus_one(a)); + ENSURE(!m.is_one(a) && !m.is_zero(a) && !m.is_minus_one(a)); m.set(a, 3); b = a; m.abs(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set(a, -3); b = a; m.abs(a); - SASSERT(!m.eq(a,b) && m.is_pos(a)); + ENSURE(!m.eq(a,b) && m.is_pos(a)); m.set(a, 1); m.swap(a, a); - SASSERT(m.is_one(a)); + ENSURE(m.is_one(a)); m.set(b, -1); m.swap(a, b); - SASSERT(m.is_one(b) && m.is_minus_one(a)); + ENSURE(m.is_one(b) && m.is_minus_one(a)); m.neg(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); } static void tst_limits(unsigned prec) { mpff_manager m(prec); scoped_mpff a(m), b(m), two(m); m.set_max(a); - SASSERT(m.is_pos(a)); + ENSURE(m.is_pos(a)); m.set_min(b); - SASSERT(m.is_neg(b)); + ENSURE(m.is_neg(b)); m.neg(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set_max(a); m.set_max(b); m.round_to_minus_inf(); m.inc(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.dec(a); - SASSERT(m.lt(a, b)); + ENSURE(m.lt(a, b)); m.set_max(a); m.round_to_plus_inf(); bool overflow = false; @@ -438,99 +438,99 @@ static void tst_limits(unsigned prec) { VERIFY(overflow); m.set_max(a); m.dec(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.set_min(a); m.set_min(b); m.round_to_minus_inf(); m.inc(a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); overflow = true; try { m.dec(a); } catch (mpff_manager::overflow_exception) { overflow = true; } - SASSERT(overflow); + ENSURE(overflow); m.round_to_plus_inf(); m.set_min(a); m.inc(a); - SASSERT(m.gt(a,b)); + ENSURE(m.gt(a,b)); m.set_min(a); m.dec(a); - SASSERT(m.eq(a,b)); + ENSURE(m.eq(a,b)); m.set_plus_epsilon(a); m.set_plus_epsilon(b); - SASSERT(!m.is_zero(a) && m.is_pos(a)); + ENSURE(!m.is_zero(a) && m.is_pos(a)); m.set(two, 2); m.round_to_plus_inf(); m.div(a, two, a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.round_to_minus_inf(); m.div(a, two, a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.round_to_plus_inf(); m.set_plus_epsilon(a); m.add(a, a, a); - SASSERT(m.gt(a, b)); + ENSURE(m.gt(a, b)); m.round_to_minus_inf(); m.set_plus_epsilon(a); m.add(a, a, a); - SASSERT(m.gt(a, b)); + ENSURE(m.gt(a, b)); m.set_plus_epsilon(a); m.sub(a, a, a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.set_plus_epsilon(a); - SASSERT(m.is_plus_epsilon(a)); - SASSERT(!m.is_minus_epsilon(a)); + ENSURE(m.is_plus_epsilon(a)); + ENSURE(!m.is_minus_epsilon(a)); m.neg(a); - SASSERT(!m.is_plus_epsilon(a)); - SASSERT(m.is_minus_epsilon(a)); + ENSURE(!m.is_plus_epsilon(a)); + ENSURE(m.is_minus_epsilon(a)); for (unsigned i = 0; i < 2; i++) { m.set_rounding(i == 0); m.set_plus_epsilon(a); m.floor(a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.set_plus_epsilon(a); m.ceil(a); - SASSERT(m.is_one(a)); + ENSURE(m.is_one(a)); m.set_minus_epsilon(a); m.floor(a); - SASSERT(m.is_minus_one(a)); + ENSURE(m.is_minus_one(a)); m.set_minus_epsilon(a); m.ceil(a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); } m.set_minus_epsilon(a); m.set_minus_epsilon(b); - SASSERT(!m.is_zero(a) && m.is_neg(a)); + ENSURE(!m.is_zero(a) && m.is_neg(a)); m.set(two, 2); m.round_to_minus_inf(); m.div(a, two, a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); m.round_to_plus_inf(); m.div(a, two, a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.round_to_plus_inf(); m.set_minus_epsilon(a); m.add(a, a, a); - SASSERT(m.lt(a, b)); + ENSURE(m.lt(a, b)); m.round_to_minus_inf(); m.set_minus_epsilon(a); m.add(a, a, a); - SASSERT(m.lt(a, b)); + ENSURE(m.lt(a, b)); m.set_minus_epsilon(a); m.sub(a, a, a); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.set_minus_epsilon(a); - SASSERT(!m.is_plus_epsilon(a)); - SASSERT(m.is_minus_epsilon(a)); + ENSURE(!m.is_plus_epsilon(a)); + ENSURE(m.is_minus_epsilon(a)); m.neg(a); - SASSERT(m.is_plus_epsilon(a)); - SASSERT(!m.is_minus_epsilon(a)); + ENSURE(m.is_plus_epsilon(a)); + ENSURE(!m.is_minus_epsilon(a)); } #if 0 @@ -549,7 +549,7 @@ static void tst_decimal(int64 n, uint64 d, bool to_plus_inf, unsigned prec, char m.display_decimal(std::cout, a, decimal_places); std::cout << std::endl; std::ostringstream buffer; m.display_decimal(buffer, a, decimal_places); - SASSERT(strcmp(expected, buffer.str().c_str()) == 0); + ENSURE(strcmp(expected, buffer.str().c_str()) == 0); } static void tst_decimal() { @@ -573,7 +573,7 @@ static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { mpff_manager m; scoped_mpff a(m); m.set(a, n, d); - SASSERT(m.prev_power_of_two(a) == expected); + ENSURE(m.prev_power_of_two(a) == expected); } static void tst_prev_power_2() { diff --git a/src/test/mpfx.cpp b/src/test/mpfx.cpp index 9e8882a26..c83f73bad 100644 --- a/src/test/mpfx.cpp +++ b/src/test/mpfx.cpp @@ -39,7 +39,7 @@ static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { mpfx_manager m; scoped_mpfx a(m); m.set(a, n, d); - SASSERT(m.prev_power_of_two(a) == expected); + ENSURE(m.prev_power_of_two(a) == expected); } static void tst_prev_power_2() { diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp index 68c7d8bb3..0da7a584a 100644 --- a/src/test/mpq.cpp +++ b/src/test/mpq.cpp @@ -27,7 +27,7 @@ static void tst0() { m.set(a, 2, 3); m.set(b, 4, 3); m.div(a, b, b); - SASSERT(m.eq(b, m.mk_q(1, 2))); + ENSURE(m.eq(b, m.mk_q(1, 2))); } static void tst1() { @@ -41,15 +41,15 @@ static void tst1() { std::cout << "*-2 = \n" << m.to_string(v2) << "\n"; m.add(v, v2, v3); m.neg(v3); - SASSERT(m.eq(v, v3)); - SASSERT(m.le(v, v3)); - SASSERT(m.ge(v, v3)); - SASSERT(m.lt(v2, v)); - SASSERT(m.le(v2, v)); - SASSERT(m.gt(v, v2)); - SASSERT(m.ge(v, v2)); - SASSERT(m.neq(v, v2)); - SASSERT(!m.neq(v, v3)); + ENSURE(m.eq(v, v3)); + ENSURE(m.le(v, v3)); + ENSURE(m.ge(v, v3)); + ENSURE(m.lt(v2, v)); + ENSURE(m.le(v2, v)); + ENSURE(m.gt(v, v2)); + ENSURE(m.ge(v, v2)); + ENSURE(m.neq(v, v2)); + ENSURE(!m.neq(v, v3)); m.del(v); m.del(v2); m.del(v3); @@ -68,7 +68,7 @@ static void mk_random_num_str(unsigned buffer_sz, char * buffer) { if (div_pos == 0) div_pos++; } - SASSERT(sz < buffer_sz); + ENSURE(sz < buffer_sz); for (unsigned i = 0; i < sz-1; i++) { if (i == div_pos && i < sz-2) { buffer[i] = '/'; @@ -90,7 +90,7 @@ static void bug1() { m.set(a, 2); m.set(b, 1, 2); m.inv(a, a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); } static void bug2() { @@ -100,7 +100,7 @@ static void bug2() { m.set(a, -2); m.set(b, -1, 2); m.inv(a, a); - SASSERT(m.eq(a, b)); + ENSURE(m.eq(a, b)); } static void tst2() { @@ -122,22 +122,22 @@ static void set_str_bug() { m.set(a, "1.0"); std::cout << a << "\n"; m.set(b, 1); - SASSERT(a == b); + ENSURE(a == b); m.set(a, "1.1"); std::cout << a << "\n"; m.set(b, 11, 10); - SASSERT(a == b); + ENSURE(a == b); m.set(a, "1/3"); m.set(b, 1, 3); std::cout << a << "\n"; - SASSERT(a == b); + ENSURE(a == b); } static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { unsynch_mpq_manager m; scoped_mpq a(m); m.set(a, n, d); - SASSERT(m.prev_power_of_two(a) == expected); + ENSURE(m.prev_power_of_two(a) == expected); } static void tst_prev_power_2() { diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index 02627e842..1c587f8e9 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -33,15 +33,15 @@ static void tst1() { std::cout << "*-2 = \n" << m.to_string(v2) << "\n"; m.add(v, v2, v3); m.neg(v3); - SASSERT(m.eq(v, v3)); - SASSERT(m.le(v, v3)); - SASSERT(m.ge(v, v3)); - SASSERT(m.lt(v2, v)); - SASSERT(m.le(v2, v)); - SASSERT(m.gt(v, v2)); - SASSERT(m.ge(v, v2)); - SASSERT(m.neq(v, v2)); - SASSERT(!m.neq(v, v3)); + ENSURE(m.eq(v, v3)); + ENSURE(m.le(v, v3)); + ENSURE(m.ge(v, v3)); + ENSURE(m.lt(v2, v)); + ENSURE(m.le(v2, v)); + ENSURE(m.gt(v, v2)); + ENSURE(m.ge(v, v2)); + ENSURE(m.neq(v, v2)); + ENSURE(!m.neq(v, v3)); m.del(v); m.del(v2); m.del(v3); @@ -80,7 +80,7 @@ static void tst2b() { #if 0 static void mk_random_num_str(unsigned buffer_sz, char * buffer) { unsigned sz = (rand() % (buffer_sz-2)) + 1; - SASSERT(sz < buffer_sz); + ENSURE(sz < buffer_sz); for (unsigned i = 0; i < sz-1; i++) { buffer[i] = '0' + (rand() % 10); } @@ -96,7 +96,7 @@ static void bug1() { m.set(v1, "1002043949858757875676767675747473"); mpz v2; m.sub(v1, v1, v2); - SASSERT(m.is_zero(v2)); + ENSURE(m.is_zero(v2)); m.del(v1); m.del(v2); } @@ -119,7 +119,7 @@ static void bug3() { m.set(v2, INT_MAX); m.add(v2, m.mk_z(1), v2); m.neg(v1); - SASSERT(m.eq(v1, v2)); + ENSURE(m.eq(v1, v2)); m.del(v1); m.del(v2); } @@ -137,7 +137,7 @@ static void bug4() { m.bitwise_or(result2, y, result2); std::cout << m.to_string(result1) << " " << m.to_string(result2) << "\n"; - SASSERT(m.eq(result1, result2)); + ENSURE(m.eq(result1, result2)); m.del(x); m.del(y); m.del(result1); m.del(result2); } @@ -149,7 +149,7 @@ void tst_div2k(synch_mpz_manager & m, mpz const & v, unsigned k) { bool is_eq = m.eq(x, y); (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "div: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); - SASSERT(is_eq); + ENSURE(is_eq); m.del(x); m.del(y); m.del(pw); @@ -177,7 +177,7 @@ void tst_mul2k(synch_mpz_manager & m, mpz const & v, unsigned k) { bool is_eq = m.eq(x, y); (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "mul: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); - SASSERT(is_eq); + ENSURE(is_eq); m.del(x); m.del(y); m.del(pw); @@ -286,7 +286,7 @@ void tst_int_min_bug() { m.set(expected, "18446744075857035263"); m.sub(big, intmin, r); std::cout << "r: " << m.to_string(r) << "\nexpected: " << m.to_string(expected) << "\n"; - SASSERT(m.eq(r, expected)); + ENSURE(m.eq(r, expected)); m.del(intmin); m.del(big); m.del(expected); @@ -396,9 +396,9 @@ void tst_log2(unsynch_mpz_manager & m, mpz const & a) { scoped_mpz b(m); unsigned k = m.log2(a); m.power(mpz(2), k, b); - SASSERT(m.is_zero(a) || m.le(b, a)); + ENSURE(m.is_zero(a) || m.le(b, a)); m.power(mpz(2), k+1, b); - SASSERT(m.le(a, b)); + ENSURE(m.le(a, b)); scoped_mpz neg_a(m); m.set(neg_a, a); @@ -406,10 +406,10 @@ void tst_log2(unsynch_mpz_manager & m, mpz const & a) { k = m.mlog2(neg_a); m.power(mpz(2), k, b); m.neg(b); - SASSERT(m.is_zero(neg_a) || m.le(neg_a, b)); + ENSURE(m.is_zero(neg_a) || m.le(neg_a, b)); m.power(mpz(2), k+1, b); m.neg(b); - SASSERT(m.le(b, neg_a)); + ENSURE(m.le(b, neg_a)); } void tst_log2() { @@ -432,20 +432,20 @@ void tst_root() { m.set(a, 213); VERIFY(!m.root(a, 5)); std::cout << "213^{1/5}: " << a << "\n"; - SASSERT(m.eq(a, mpz(3))); + ENSURE(m.eq(a, mpz(3))); m.set(a, -213); VERIFY(!m.root(a, 5)); std::cout << "-213^{1/5}: " << a << "\n"; - SASSERT(m.eq(a, mpz(-2))); + ENSURE(m.eq(a, mpz(-2))); m.set(a, 0); VERIFY(m.root(a, 3)); - SASSERT(m.is_zero(a)); + ENSURE(m.is_zero(a)); m.set(a, 8); VERIFY(m.root(a, 3)); - SASSERT(m.eq(a, mpz(2))); + ENSURE(m.eq(a, mpz(2))); m.set(a, -8); VERIFY(m.root(a, 3)); - SASSERT(m.eq(a, mpz(-2))); + ENSURE(m.eq(a, mpz(-2))); } void tst_gcd_bug() { diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index df25db927..ccb534214 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -35,25 +35,25 @@ nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1, std::cout << "s2: " << s2 << "\n"; r = ism.mk_union(s1, s2); std::cout << "union(s1, s2): " << r << std::endl; - SASSERT(!check_num_intervals || ism.num_intervals(r) == expected_num_intervals); - SASSERT(ism.subset(s1, r)); - SASSERT(ism.subset(s2, r)); + ENSURE(!check_num_intervals || ism.num_intervals(r) == expected_num_intervals); + ENSURE(ism.subset(s1, r)); + ENSURE(ism.subset(s2, r)); if (ism.set_eq(s1, s2)) { - SASSERT(ism.set_eq(s1, r)); - SASSERT(ism.set_eq(s2, r)); + ENSURE(ism.set_eq(s1, r)); + ENSURE(ism.set_eq(s2, r)); } else { - SASSERT(ism.subset(s1, s2) || !ism.subset(r, s2)); - SASSERT(ism.subset(s2, s1) || !ism.subset(r, s1)); + ENSURE(ism.subset(s1, s2) || !ism.subset(r, s2)); + ENSURE(ism.subset(s2, s1) || !ism.subset(r, s1)); } nlsat::interval_set_ref r2(ism); r2 = ism.mk_union(s2, s1); - SASSERT(ism.set_eq(r, r2)); + ENSURE(ism.set_eq(r, r2)); anum zero; nlsat::interval_set_ref full(ism); nlsat::literal dummy(131, false); full = ism.mk(true, true, zero, true, true, zero, dummy); - SASSERT(ism.set_eq(r, full) == ism.is_full(r)); + ENSURE(ism.set_eq(r, full) == ism.is_full(r)); return r; } @@ -178,8 +178,8 @@ static void tst3() { static nlsat::interval_set_ref mk_random(nlsat::interval_set_manager & ism, anum_manager & am, int range, int space, int tries, bool minus_inf, bool plus_inf, nlsat::literal lit) { static random_gen gen; - SASSERT(range > 0); - SASSERT(space > 0); + ENSURE(range > 0); + ENSURE(space > 0); nlsat::interval_set_ref r(ism), curr(ism); scoped_anum lower(am); scoped_anum upper(am); @@ -227,17 +227,17 @@ static void check_subset_result(nlsat::interval_set_ref const & s1, unsigned num = ism.num_intervals(r); nlsat::literal_vector lits; ism.get_justifications(r, lits); - SASSERT(lits.size() <= 2); + ENSURE(lits.size() <= 2); for (unsigned i = 0; i < num; i++) { tmp = ism.get_interval(r, i); ism.get_justifications(tmp, lits); - SASSERT(lits.size() == 1); + ENSURE(lits.size() == 1); if (lits[0] == l1) { - SASSERT(ism.subset(tmp, s1)); + ENSURE(ism.subset(tmp, s1)); } else { - SASSERT(lits[0] == l2); - SASSERT(ism.subset(tmp, s2)); + ENSURE(lits[0] == l2); + ENSURE(ism.subset(tmp, s2)); } } } @@ -293,7 +293,7 @@ static void tst5() { bool is_even[1] = { false }; nlsat::bool_var b = s.mk_ineq_atom(nlsat::atom::GT, 1, _p, is_even); nlsat::atom * a = s.bool_var2atom(b); - SASSERT(a != 0); + ENSURE(a != 0); scoped_anum zero(am); am.set(zero, 0); as.set(0, zero); @@ -432,7 +432,7 @@ static void tst7() { litsv.reset(); litsv.append(2, lits.c_ptr()); res = s.check(litsv); - SASSERT(res == l_true); + ENSURE(res == l_true); s.display(std::cout); s.am().display(std::cout, s.value(x0)); std::cout << "\n"; s.am().display(std::cout, s.value(x1)); std::cout << "\n"; diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp index d795bc1fd..c528b0dbe 100644 --- a/src/test/no_overflow.cpp +++ b/src/test/no_overflow.cpp @@ -28,12 +28,12 @@ Revision History: { \ Z3_solver_push(ctx, s); \ Z3_solver_assert(ctx, s, TEST_NAME); \ - SASSERT(Z3_solver_check(ctx, s) == TEST_OUTCOME); \ + ENSURE(Z3_solver_check(ctx, s) == TEST_OUTCOME); \ Z3_solver_pop(ctx, s, 1); \ \ Z3_solver_push(ctx, s); \ Z3_solver_assert(ctx, s, Z3_mk_not(ctx, TEST_NAME)); \ - SASSERT(Z3_solver_check(ctx, s) == NEG_TEST_OUTCOME); \ + ENSURE(Z3_solver_check(ctx, s) == NEG_TEST_OUTCOME); \ Z3_solver_pop(ctx, s, 1); \ } \ } while (0) @@ -630,7 +630,7 @@ void test_equiv(Equivalence_params params, unsigned bvsize, bool is_signed) { equiv = Z3_mk_implies(ctx, cond, equiv); } Z3_solver_assert(ctx, s, Z3_mk_not(ctx, equiv)); - SASSERT(Z3_solver_check(ctx, s) == Z3_L_FALSE); + ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE); Z3_solver_pop(ctx, s, 1); Z3_solver_dec_ref(ctx, s); @@ -662,7 +662,7 @@ void test_equiv(Equivalence_params params, unsigned bvsize, bool is_signed) { // Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, t2, Z3_mk_numeral(ctx, "1", bv))); // //TEST_NO_UNDERFLOW; // Z3_solver_assert(ctx, s, test_udfl); -// SASSERT(Z3_check(ctx) == Z3_TRUE); +// ENSURE(Z3_check(ctx) == Z3_TRUE); // Z3_solver_pop(ctx, s, 1); // // Z3_del_config(cfg); diff --git a/src/test/object_allocator.cpp b/src/test/object_allocator.cpp index cca42cf6f..3ea646c0c 100644 --- a/src/test/object_allocator.cpp +++ b/src/test/object_allocator.cpp @@ -62,12 +62,12 @@ static void tst1() { cell * c3 = m.allocate(); (void)c3; - SASSERT(c3->m_coeff.is_zero()); + ENSURE(c3->m_coeff.is_zero()); } static void tst2() { cell_allocator m; - SASSERT(m.capacity() >= 2); + ENSURE(m.capacity() >= 2); cell_allocator::worker_object_allocator m1 = m.get_worker_allocator(0); cell_allocator::worker_object_allocator m2 = m.get_worker_allocator(1); m.enable_concurrent(true); @@ -83,7 +83,7 @@ static void tst2() { c = m1.allocate(); else c = m2.allocate(); - SASSERT(c->m_coeff.is_zero()); + ENSURE(c->m_coeff.is_zero()); int val = rand(); c->m_coeff = rational(val); object_coeff_pairs.push_back(std::make_pair(c, val)); @@ -93,7 +93,7 @@ static void tst2() { unsigned idx = rand() % object_coeff_pairs.size(); cell * c = object_coeff_pairs[idx].first; CTRACE("object_allocator", c->m_coeff != rational(object_coeff_pairs[idx].second), tout << c->m_coeff << " != " << rational(object_coeff_pairs[idx].second) << "\n";); - SASSERT(c->m_coeff == rational(object_coeff_pairs[idx].second)); + ENSURE(c->m_coeff == rational(object_coeff_pairs[idx].second)); if (idx < 5) m1.recycle(c); else @@ -118,5 +118,5 @@ void tst_object_allocator() { tst2(); TRACE("object_allocator", tout << "num. allocated cells: " << cell::g_num_allocated_cells << "\nnum. deallocated cells: " << cell::g_num_deallocated_cells << "\nnum. recycled cells: " << cell::g_num_recycled_cells << "\n";); - SASSERT(cell::g_num_allocated_cells == cell::g_num_deallocated_cells); + ENSURE(cell::g_num_allocated_cells == cell::g_num_deallocated_cells); } diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp index 12a45555d..da41d0d38 100644 --- a/src/test/old_interval.cpp +++ b/src/test/old_interval.cpp @@ -23,96 +23,96 @@ static void tst1() { ext_numeral minus_inf(false); ext_numeral zero(0); - SASSERT(ext_numeral(10) + ext_numeral(3) == ext_numeral(13)); - SASSERT(inf + zero == inf); - SASSERT(minus_inf + zero == minus_inf); - SASSERT(minus_inf + ext_numeral(3) == minus_inf); - SASSERT(inf + inf == inf); - SASSERT(minus_inf + minus_inf == minus_inf); - SASSERT(minus_inf + ext_numeral(10) == minus_inf); - SASSERT(minus_inf + ext_numeral(-10) == minus_inf); - SASSERT(inf + ext_numeral(10) == inf); - SASSERT(inf + ext_numeral(-10) == inf); + ENSURE(ext_numeral(10) + ext_numeral(3) == ext_numeral(13)); + ENSURE(inf + zero == inf); + ENSURE(minus_inf + zero == minus_inf); + ENSURE(minus_inf + ext_numeral(3) == minus_inf); + ENSURE(inf + inf == inf); + ENSURE(minus_inf + minus_inf == minus_inf); + ENSURE(minus_inf + ext_numeral(10) == minus_inf); + ENSURE(minus_inf + ext_numeral(-10) == minus_inf); + ENSURE(inf + ext_numeral(10) == inf); + ENSURE(inf + ext_numeral(-10) == inf); - SASSERT(ext_numeral(10) - ext_numeral(3) == ext_numeral(7)); - SASSERT(inf - zero == inf); - SASSERT(minus_inf - zero == minus_inf); - SASSERT(minus_inf - ext_numeral(3) == minus_inf); - SASSERT(inf - minus_inf == inf); - SASSERT(minus_inf - inf == minus_inf); - SASSERT(zero - minus_inf == inf); - SASSERT(zero - inf == minus_inf); - SASSERT(ext_numeral(-10) - minus_inf == inf); - SASSERT(ext_numeral(10) - minus_inf == inf); - SASSERT(ext_numeral(-10) - inf == minus_inf); - SASSERT(ext_numeral(10) - inf == minus_inf); + ENSURE(ext_numeral(10) - ext_numeral(3) == ext_numeral(7)); + ENSURE(inf - zero == inf); + ENSURE(minus_inf - zero == minus_inf); + ENSURE(minus_inf - ext_numeral(3) == minus_inf); + ENSURE(inf - minus_inf == inf); + ENSURE(minus_inf - inf == minus_inf); + ENSURE(zero - minus_inf == inf); + ENSURE(zero - inf == minus_inf); + ENSURE(ext_numeral(-10) - minus_inf == inf); + ENSURE(ext_numeral(10) - minus_inf == inf); + ENSURE(ext_numeral(-10) - inf == minus_inf); + ENSURE(ext_numeral(10) - inf == minus_inf); - SASSERT(ext_numeral(10) * inf == inf); - SASSERT(ext_numeral(-10) * inf == minus_inf); - SASSERT(zero * inf == zero); - SASSERT(zero * minus_inf == zero); - SASSERT(zero * ext_numeral(10) == zero); - SASSERT(ext_numeral(10) * ext_numeral(-20) == ext_numeral(-200)); - SASSERT(ext_numeral(3) * ext_numeral(2) == ext_numeral(6)); - SASSERT(inf * inf == inf); - SASSERT(inf * minus_inf == minus_inf); - SASSERT(minus_inf * minus_inf == inf); - SASSERT(minus_inf * inf == minus_inf); - SASSERT(minus_inf * ext_numeral(10) == minus_inf); - SASSERT(minus_inf * ext_numeral(-10) == inf); + ENSURE(ext_numeral(10) * inf == inf); + ENSURE(ext_numeral(-10) * inf == minus_inf); + ENSURE(zero * inf == zero); + ENSURE(zero * minus_inf == zero); + ENSURE(zero * ext_numeral(10) == zero); + ENSURE(ext_numeral(10) * ext_numeral(-20) == ext_numeral(-200)); + ENSURE(ext_numeral(3) * ext_numeral(2) == ext_numeral(6)); + ENSURE(inf * inf == inf); + ENSURE(inf * minus_inf == minus_inf); + ENSURE(minus_inf * minus_inf == inf); + ENSURE(minus_inf * inf == minus_inf); + ENSURE(minus_inf * ext_numeral(10) == minus_inf); + ENSURE(minus_inf * ext_numeral(-10) == inf); - SASSERT(minus_inf < inf); - SASSERT(!(inf < minus_inf)); - SASSERT(minus_inf < ext_numeral(10)); - SASSERT(ext_numeral(-3) < inf); - SASSERT(ext_numeral(-10) < ext_numeral(4)); - SASSERT(ext_numeral(2) < ext_numeral(10)); - SASSERT(!(inf < ext_numeral(30))); - SASSERT(!(ext_numeral(10) < minus_inf)); - SASSERT(!(inf < inf)); - SASSERT(!(minus_inf < minus_inf)); - SASSERT(!(zero < zero)); - SASSERT(!(ext_numeral(10) < ext_numeral(10))); - SASSERT(inf > minus_inf); - SASSERT(inf > zero); - SASSERT(inf > ext_numeral(10)); - SASSERT(ext_numeral(10) > minus_inf); - SASSERT(zero > minus_inf); - SASSERT(!(zero > inf)); - SASSERT(!(minus_inf > inf)); - SASSERT(inf >= minus_inf); - SASSERT(inf >= inf); - SASSERT(minus_inf >= minus_inf); - SASSERT(inf >= zero); - SASSERT(zero >= minus_inf); - SASSERT(inf <= inf); - SASSERT(minus_inf <= minus_inf); - SASSERT(zero <= inf); - SASSERT(minus_inf <= zero); + ENSURE(minus_inf < inf); + ENSURE(!(inf < minus_inf)); + ENSURE(minus_inf < ext_numeral(10)); + ENSURE(ext_numeral(-3) < inf); + ENSURE(ext_numeral(-10) < ext_numeral(4)); + ENSURE(ext_numeral(2) < ext_numeral(10)); + ENSURE(!(inf < ext_numeral(30))); + ENSURE(!(ext_numeral(10) < minus_inf)); + ENSURE(!(inf < inf)); + ENSURE(!(minus_inf < minus_inf)); + ENSURE(!(zero < zero)); + ENSURE(!(ext_numeral(10) < ext_numeral(10))); + ENSURE(inf > minus_inf); + ENSURE(inf > zero); + ENSURE(inf > ext_numeral(10)); + ENSURE(ext_numeral(10) > minus_inf); + ENSURE(zero > minus_inf); + ENSURE(!(zero > inf)); + ENSURE(!(minus_inf > inf)); + ENSURE(inf >= minus_inf); + ENSURE(inf >= inf); + ENSURE(minus_inf >= minus_inf); + ENSURE(inf >= zero); + ENSURE(zero >= minus_inf); + ENSURE(inf <= inf); + ENSURE(minus_inf <= minus_inf); + ENSURE(zero <= inf); + ENSURE(minus_inf <= zero); ext_numeral val(10); val.neg(); - SASSERT(val == ext_numeral(-10)); + ENSURE(val == ext_numeral(-10)); val = inf; val.neg(); - SASSERT(val == minus_inf); + ENSURE(val == minus_inf); val.neg(); - SASSERT(val == inf); + ENSURE(val == inf); - SASSERT(minus_inf.sign()); - SASSERT(!zero.sign()); - SASSERT(!inf.sign()); - SASSERT(ext_numeral(-10).sign()); - SASSERT(!ext_numeral(10).sign()); + ENSURE(minus_inf.sign()); + ENSURE(!zero.sign()); + ENSURE(!inf.sign()); + ENSURE(ext_numeral(-10).sign()); + ENSURE(!ext_numeral(10).sign()); - SASSERT(inf.is_infinite()); - SASSERT(minus_inf.is_infinite()); - SASSERT(!zero.is_infinite()); - SASSERT(!ext_numeral(10).is_infinite()); - SASSERT(!inf.is_zero()); - SASSERT(!minus_inf.is_zero()); - SASSERT(zero.is_zero()); - SASSERT(!ext_numeral(10).is_zero()); + ENSURE(inf.is_infinite()); + ENSURE(minus_inf.is_infinite()); + ENSURE(!zero.is_infinite()); + ENSURE(!ext_numeral(10).is_infinite()); + ENSURE(!inf.is_zero()); + ENSURE(!minus_inf.is_zero()); + ENSURE(zero.is_zero()); + ENSURE(!ext_numeral(10).is_zero()); } class interval_tester { @@ -182,12 +182,12 @@ static void tst2() { m.set(y, mpz(-2), mpz(3)); m.add(x, y, z); std::cout << "x: " << x << ", y: " << y << ", z: " << z << "\n"; - SASSERT(nm.eq(z.lower(), mpz(-1))); - SASSERT(nm.eq(z.upper(), mpz(5))); + ENSURE(nm.eq(z.lower(), mpz(-1))); + ENSURE(nm.eq(z.upper(), mpz(5))); m.mul(x, y, z); std::cout << "x: " << x << ", y: " << y << ", z: " << z << "\n"; - SASSERT(nm.eq(z.lower(), mpz(-4))); - SASSERT(nm.eq(z.upper(), mpz(6))); + ENSURE(nm.eq(z.lower(), mpz(-4))); + ENSURE(nm.eq(z.upper(), mpz(6))); } void tst_old_interval() { diff --git a/src/test/optional.cpp b/src/test/optional.cpp index 81b84cd59..40ca383a5 100644 --- a/src/test/optional.cpp +++ b/src/test/optional.cpp @@ -22,11 +22,11 @@ Revision History: static void tst1() { optional v; - SASSERT(!v); - SASSERT(v == false); + ENSURE(!v); + ENSURE(v == false); v = 10; - SASSERT(v); - SASSERT(*v == 10); + ENSURE(v); + ENSURE(*v == 10); TRACE("optional", tout << sizeof(v) << "\n";); } @@ -45,25 +45,25 @@ struct OptFoo { static void tst2() { optional v; - SASSERT(!v); + ENSURE(!v); v = OptFoo(10, 20); - SASSERT(v->m_x == 10); - SASSERT(v->m_y == 20); + ENSURE(v->m_x == 10); + ENSURE(v->m_y == 20); v = OptFoo(200, 300); - SASSERT(v->m_x == 200); - SASSERT(v->m_y == 300); + ENSURE(v->m_x == 200); + ENSURE(v->m_y == 300); TRACE("optional", tout << sizeof(v) << "\n";); } static void tst3() { optional v; - SASSERT(!v); + ENSURE(!v); int x = 10; v = &x; - SASSERT(v); - SASSERT(*v == &x); + ENSURE(v); + ENSURE(*v == &x); TRACE("optional", tout << sizeof(v) << "\n";); - SASSERT(*(*v) == 10); + ENSURE(*(*v) == 10); } void tst_optional() { diff --git a/src/test/parray.cpp b/src/test/parray.cpp index 7976971d8..df0fde516 100644 --- a/src/test/parray.cpp +++ b/src/test/parray.cpp @@ -46,36 +46,36 @@ static void tst1() { int_array a3; m.mk(a1); - SASSERT(m.size(a1) == 0); + ENSURE(m.size(a1) == 0); m.push_back(a1, 10, a2); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n";); - SASSERT(m.size(a1) == 0); - SASSERT(m.size(a2) == 1); + ENSURE(m.size(a1) == 0); + ENSURE(m.size(a2) == 1); m.push_back(a1, 20, a1); m.push_back(a1, 30, a1); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n";); - SASSERT(m.get(a1, 0) == 20); - SASSERT(m.get(a1, 1) == 30); - SASSERT(m.get(a2, 0) == 10); - SASSERT(m.size(a1) == 2); - SASSERT(m.size(a2) == 1); - SASSERT(m.size(a3) == 0); + ENSURE(m.get(a1, 0) == 20); + ENSURE(m.get(a1, 1) == 30); + ENSURE(m.get(a2, 0) == 10); + ENSURE(m.size(a1) == 2); + ENSURE(m.size(a2) == 1); + ENSURE(m.size(a3) == 0); m.push_back(a2, 100, a3); - SASSERT(m.size(a3) == 2); - SASSERT(m.get(a3, 0) == 10); - SASSERT(m.get(a3, 1) == 100); + ENSURE(m.size(a3) == 2); + ENSURE(m.get(a3, 0) == 10); + ENSURE(m.get(a3, 1) == 100); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n"; m.display_info(tout, a3); tout << "\n";); m.push_back(a2, 50); - SASSERT(m.get(a2, 0) == 10); - SASSERT(m.get(a2, 1) == 50); - SASSERT(m.size(a2) == 2); + ENSURE(m.get(a2, 0) == 10); + ENSURE(m.get(a2, 1) == 50); + ENSURE(m.size(a2) == 2); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n"; @@ -100,22 +100,22 @@ static void tst2() { for (unsigned i = 0; i < 100; i++) m.push_back(a1, i); - SASSERT(m.size(a1) == 100); + ENSURE(m.size(a1) == 100); m.push_back(a1, 100, a2); for (unsigned i = 0; i < 10; i++) m.push_back(a2, i+101); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n";); - SASSERT(m.get(a1, 0) == 0); + ENSURE(m.get(a1, 0) == 0); TRACE("parray", m.display_info(tout, a1); tout << "\n"; m.display_info(tout, a2); tout << "\n";); for (unsigned i = 0; i < m.size(a1); i++) { - SASSERT(static_cast(m.get(a1, i)) == i); + ENSURE(static_cast(m.get(a1, i)) == i); } for (unsigned i = 0; i < m.size(a2); i++) { - SASSERT(static_cast(m.get(a2, i)) == i); + ENSURE(static_cast(m.get(a2, i)) == i); } TRACE("parray", m.display_info(tout, a1); tout << "\n"; @@ -145,7 +145,7 @@ static void tst3() { for (unsigned i = 0; i < 20; i++) m.push_back(a1, i); - SASSERT(m.size(a1) == 20); + ENSURE(m.size(a1) == 20); m.set(a1, 0, 1, a2); for (unsigned i = 1; i < 20; i++) { if (i == 6) { @@ -161,7 +161,7 @@ static void tst3() { m.push_back(a4, 30); for (unsigned i = 0; i < 20; i++) { - SASSERT(static_cast(m.get(a2, i)) == i+1); + ENSURE(static_cast(m.get(a2, i)) == i+1); } TRACE("parray", m.display_info(tout, a1); tout << "\n"; @@ -169,7 +169,7 @@ static void tst3() { m.display_info(tout, a3); tout << "\n"; m.display_info(tout, a4); tout << "\n"; ); - SASSERT(m.get(a1, 10) == 10); + ENSURE(m.get(a1, 10) == 10); TRACE("parray", tout << "after rerooting...\n"; m.display_info(tout, a1); tout << "\n"; @@ -177,19 +177,19 @@ static void tst3() { m.display_info(tout, a3); tout << "\n"; m.display_info(tout, a4); tout << "\n"; ); - SASSERT(m.size(a1) == 20); - SASSERT(m.size(a2) == 20); - SASSERT(m.size(a3) == 19); - SASSERT(m.size(a4) == 19); + ENSURE(m.size(a1) == 20); + ENSURE(m.size(a2) == 20); + ENSURE(m.size(a3) == 19); + ENSURE(m.size(a4) == 19); for (unsigned i = 0; i < 20; i++) { - SASSERT(static_cast(m.get(a1, i)) == i); - SASSERT(static_cast(m.get(a2, i)) == i+1); - SASSERT(i >= 18 || static_cast(m.get(a4, i)) == i+1); - SASSERT(i >= 6 || static_cast(m.get(a3, i)) == i+1); - SASSERT(!(6 <= i && i <= 17) || static_cast(m.get(a3, i)) == i); + ENSURE(static_cast(m.get(a1, i)) == i); + ENSURE(static_cast(m.get(a2, i)) == i+1); + ENSURE(i >= 18 || static_cast(m.get(a4, i)) == i+1); + ENSURE(i >= 6 || static_cast(m.get(a3, i)) == i+1); + ENSURE(!(6 <= i && i <= 17) || static_cast(m.get(a3, i)) == i); } - SASSERT(m.get(a4, 18) == 30); - SASSERT(m.get(a3, 18) == 40); + ENSURE(m.get(a4, 18) == 30); + ENSURE(m.get(a3, 18) == 40); TRACE("parray", tout << "after many gets...\n"; m.display_info(tout, a1); tout << "\n"; diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index fcc309883..07cb047b3 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -81,7 +81,7 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vectorcheck_sat(0,0); VERIFY(res == l_true); slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); diff --git a/src/test/permutation.cpp b/src/test/permutation.cpp index d5929b6c0..e0d208520 100644 --- a/src/test/permutation.cpp +++ b/src/test/permutation.cpp @@ -48,7 +48,7 @@ static void tst1(unsigned sz, unsigned num_tries, unsigned max = UINT_MAX) { apply_permutation(sz, data.c_ptr(), p.c_ptr()); // std::cout << "data: "; display(std::cout, data.begin(), data.end()); std::cout << "\n"; for (unsigned i = 0; i < 0; i++) - SASSERT(data[i] == new_data[i]); + ENSURE(data[i] == new_data[i]); } #endif } diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp index 03eb321cd..0a6418a6c 100644 --- a/src/test/polynomial.cpp +++ b/src/test/polynomial.cpp @@ -39,7 +39,7 @@ static void tst1() { p = (x0^3) + x1*x0 + 2; std::cout << p << "\n"; std::cout << "max_var(p): " << max_var(p) << "\n"; - SASSERT(max_var(p) == 1); + ENSURE(max_var(p) == 1); std::cout << (2*x2 - x1*x0) << "\n"; std::cout << (p + (2*x2 - x1*x0)) << "\n"; std::cout << (p*p + 2*x2) << "\n"; @@ -79,7 +79,7 @@ static void tst_pseudo_div(polynomial_ref const & A, polynomial_ref const & B, p std::cout << "l_B^d: " << l_B_d << "\n"; std::cout << "Q * B + R: " << Q * B + R << "\n"; std::cout << "l_B_d * A: " << l_B_d * A << "\n"; - SASSERT(eq((Q * B + R), (l_B_d * A))); + ENSURE(eq((Q * B + R), (l_B_d * A))); } static void tst2() { @@ -329,13 +329,13 @@ static void tst11() { polynomial_ref d(m); d = exact_div(p, q); std::cout << "p: " << p << "\nq: " << q << "\nd: " << d << "\n"; - SASSERT(eq(q * d, p)); + ENSURE(eq(q * d, p)); q = ((x1^3) + x1 + 1)*((x2^2) + x2 + x2 + 1)*((x3^2) + 2); p = (x1 + (x3^2) + x3 + x2 + (x2^2) + 1)*((x1^3) + x1 + 1)*((x2^2) + x2 + x2 + 1)*((x3^2) + 2); d = exact_div(p, q); std::cout << "p: " << p << "\nq: " << q << "\nd: " << d << "\n"; - SASSERT(eq(q * d, p)); + ENSURE(eq(q * d, p)); } static void tst_discriminant(polynomial_ref const & p, polynomial::var x, polynomial_ref const & expected) { @@ -344,7 +344,7 @@ static void tst_discriminant(polynomial_ref const & p, polynomial::var x, polyno r = discriminant(p, x); std::cout << "r: " << r << "\n"; std::cout << "expected: " << expected << "\n"; - SASSERT(eq(r, expected)); + ENSURE(eq(r, expected)); m.lex_sort(r); std::cout << "r (sorted): " << r << "\n"; } @@ -463,7 +463,7 @@ static void tst_resultant(polynomial_ref const & p, polynomial_ref const & q, po std::cout << "expected: " << expected << "\n"; if (degree(p, x) > 0 && degree(q, x) > 0) std::cout << "quasi-resultant: " << quasi_resultant(p, q, x) << "\n"; - SASSERT(eq(r, expected)); + ENSURE(eq(r, expected)); m.lex_sort(r); std::cout << "r (sorted): " << r << "\n"; } @@ -570,8 +570,8 @@ static void tst_compose() { p = (x0^3) - x0 + 3; std::cout << "p: " << p << "\np(x - y): " << compose_x_minus_y(p, 1) << "\np(x + y): " << compose_x_plus_y(p, 1) << "\np(x - x): " << compose_x_minus_y(p, 0) << "\np(x + x): " << compose_x_plus_y(p, 0) << "\n"; - SASSERT(eq(compose_x_minus_y(p, 1), (x0^3) - 3*(x0^2)*x1 + 3*x0*(x1^2) - (x1^3) - x0 + x1 + 3)); - SASSERT(eq(compose_x_plus_y(p, 1), (x0^3) + 3*(x0^2)*x1 + 3*x0*(x1^2) + (x1^3) - x0 - x1 + 3)); + ENSURE(eq(compose_x_minus_y(p, 1), (x0^3) - 3*(x0^2)*x1 + 3*x0*(x1^2) - (x1^3) - x0 + x1 + 3)); + ENSURE(eq(compose_x_plus_y(p, 1), (x0^3) + 3*(x0^2)*x1 + 3*x0*(x1^2) + (x1^3) - x0 - x1 + 3)); } void tst_prem() { @@ -604,11 +604,11 @@ void tst_sqrt() { p = (4*x*y + 3*(x^2)*y + (y^2) + 3)^4; polynomial_ref q(m); VERIFY(sqrt(p, q)); - SASSERT(eq(p, q*q)); + ENSURE(eq(p, q*q)); std::cout << "p: " << p << "\n"; std::cout << "q: " << q << "\n"; p = p - 1; - SASSERT(!sqrt(p, q)); + ENSURE(!sqrt(p, q)); } static void tst_content(polynomial_ref const & p, polynomial::var x, polynomial_ref const & expected) { @@ -616,7 +616,7 @@ static void tst_content(polynomial_ref const & p, polynomial::var x, polynomial_ std::cout << "p: " << p << std::endl; std::cout << "content(p): " << content(p, x) << std::endl; std::cout << "expected: " << expected << std::endl; - SASSERT(eq(content(p, x), expected)); + ENSURE(eq(content(p, x), expected)); } static void tst_primitive(polynomial_ref const & p, polynomial::var x, polynomial_ref const & expected) { @@ -624,7 +624,7 @@ static void tst_primitive(polynomial_ref const & p, polynomial::var x, polynomia std::cout << "p: " << p << std::endl; std::cout << "primitive(p): " << primitive(p, x) << std::endl; std::cout << "expected: " << expected << std::endl; - SASSERT(eq(primitive(p, x), expected)); + ENSURE(eq(primitive(p, x), expected)); } static void tst_gcd(polynomial_ref const & p, polynomial_ref const & q, polynomial_ref const & expected) { @@ -635,7 +635,7 @@ static void tst_gcd(polynomial_ref const & p, polynomial_ref const & q, polynomi r = gcd(p, q); std::cout << "gcd(p, q): " << r << std::endl; std::cout << "expected: " << expected << std::endl; - SASSERT(eq(r, expected)); + ENSURE(eq(r, expected)); } static void tst_gcd() { @@ -711,15 +711,15 @@ static void tst_psc(polynomial_ref const & p, polynomial_ref const & q, polynomi std::cout << "S_" << i << ": " << polynomial_ref(S.get(i), m) << std::endl; } if (sz > 0) { - SASSERT(m.eq(S.get(0), first) || m.eq(S.get(0), neg(first))); + ENSURE(m.eq(S.get(0), first) || m.eq(S.get(0), neg(first))); } if (sz > 1) { - SASSERT(m.eq(S.get(1), second) || m.eq(S.get(1), neg(second))); + ENSURE(m.eq(S.get(1), second) || m.eq(S.get(1), neg(second))); } if (sz > 0) { polynomial_ref Res(m); Res = resultant(p, q, x); - SASSERT(m.eq(Res, S.get(0)) || m.eq(S.get(0), neg(Res))); + ENSURE(m.eq(Res, S.get(0)) || m.eq(S.get(0), neg(Res))); } } @@ -843,11 +843,11 @@ static void tst_vars(polynomial_ref const & p, unsigned sz, polynomial::var * xs std::cout << r[i] << " "; } std::cout << std::endl; - SASSERT(r.size() == sz); + ENSURE(r.size() == sz); std::sort(r.begin(), r.end()); std::sort(xs, xs + sz); for (unsigned i = 0; i < r.size(); i++) { - SASSERT(r[i] == xs[i]); + ENSURE(r[i] == xs[i]); } } @@ -886,9 +886,9 @@ static void tst_sqf(polynomial_ref const & p, polynomial_ref const & expected) { r = square_free(p); std::cout << "sqf(p): " << r << std::endl; std::cout << "expected: " << expected << std::endl; - SASSERT(is_square_free(r)); - SASSERT(!eq(r, p) || is_square_free(p)); - SASSERT(eq(expected, r)); + ENSURE(is_square_free(r)); + ENSURE(!eq(r, p) || is_square_free(p)); + ENSURE(eq(expected, r)); } static void tst_sqf() { @@ -931,7 +931,7 @@ static void tst_substitute(polynomial_ref const & p, r = p.m().substitute(p, 2, xs, vs.c_ptr()); std::cout << "r: " << r << std::endl; std::cout << "expected: " << expected << std::endl; - SASSERT(eq(r, expected)); + ENSURE(eq(r, expected)); p.m().lex_sort(r); std::cout << "r (sorted): " << r << std::endl; } @@ -972,7 +972,7 @@ static void tst_qsubstitute(polynomial_ref const & p, r = p.m().substitute(p, 2, xs, vs.c_ptr()); std::cout << "r: " << r << std::endl; std::cout << "expected (modulo a constant): " << expected << std::endl; - SASSERT(eq(r, normalize(expected))); + ENSURE(eq(r, normalize(expected))); p.m().lex_sort(r); std::cout << "r (sorted): " << r << std::endl; } @@ -1024,10 +1024,10 @@ void tst_mfact(polynomial_ref const & p, unsigned num_distinct_factors) { for (unsigned i = 0; i < fs.distinct_factors(); i++) { std::cout << "*(" << fs[i] << ")^" << fs.get_degree(i) << std::endl; } - SASSERT(fs.distinct_factors() == num_distinct_factors); + ENSURE(fs.distinct_factors() == num_distinct_factors); polynomial_ref p2(p.m()); fs.multiply(p2); - SASSERT(eq(p, p2)); + ENSURE(eq(p, p2)); } static void tst_mfact() { @@ -1247,7 +1247,7 @@ static void tst_translate(polynomial_ref const & p, polynomial::var x0, int v0, polynomial_ref r(p.m()); p.m().translate(p, 3, xs, vs, r); std::cout << "r: " << r << std::endl; - SASSERT(eq(expected, r)); + ENSURE(eq(expected, r)); } static void tst_translate() { @@ -1326,11 +1326,11 @@ static void tst_mm() { std::cout << "p1: " << p1 << "\n"; p2 = convert(pm1, p1, pm2); std::cout << "p2: " << p2 << "\n"; - SASSERT(pm1.get_monomial(p1, 0) == pm2.get_monomial(p2, 0)); + ENSURE(pm1.get_monomial(p1, 0) == pm2.get_monomial(p2, 0)); polynomial_ref p3(pm3); p3 = convert(pm1, p1, pm3); - SASSERT(pm1.get_monomial(p1, 0) != pm3.get_monomial(p3, 0)); + ENSURE(pm1.get_monomial(p1, 0) != pm3.get_monomial(p3, 0)); } dealloc(pm1_ptr); // p2 is still ok @@ -1351,7 +1351,7 @@ static void tst_eval(polynomial_ref const & p, polynomial::var x0, rational v0, std::cout << "r: " << r << "\nexpected: " << expected << "\n"; scoped_mpq ex(qm); qm.set(ex, expected.to_mpq()); - SASSERT(qm.eq(r, ex)); + ENSURE(qm.eq(r, ex)); } static void tst_eval() { @@ -1407,18 +1407,18 @@ static void tst_mk_unique() { std::cout << "p: " << p << "\n"; std::cout << "q: " << q << "\n"; std::cout << "r: " << r << "\n"; - SASSERT(m.eq(p, q)); - SASSERT(!m.eq(p, r)); - SASSERT(p.get() != q.get()); + ENSURE(m.eq(p, q)); + ENSURE(!m.eq(p, r)); + ENSURE(p.get() != q.get()); q = uniq.mk_unique(q); p = uniq.mk_unique(p); r = uniq.mk_unique(r); std::cout << "after mk_unique\np: " << p << "\n"; std::cout << "q: " << q << "\n"; std::cout << "r: " << r << "\n"; - SASSERT(m.eq(p, q)); - SASSERT(!m.eq(r, q)); - SASSERT(p.get() == q.get()); + ENSURE(m.eq(p, q)); + ENSURE(!m.eq(r, q)); + ENSURE(p.get() == q.get()); } struct dummy_del_eh : public polynomial::manager::del_eh { @@ -1442,24 +1442,24 @@ static void tst_del_eh() { m.add_del_eh(&eh1); x1 = 0; - SASSERT(eh1.m_counter == 1); + ENSURE(eh1.m_counter == 1); m.add_del_eh(&eh2); x1 = m.mk_polynomial(m.mk_var()); x1 = 0; - SASSERT(eh1.m_counter == 2); - SASSERT(eh2.m_counter == 1); + ENSURE(eh1.m_counter == 2); + ENSURE(eh2.m_counter == 1); m.remove_del_eh(&eh1); x0 = 0; x1 = m.mk_polynomial(m.mk_var()); x1 = 0; - SASSERT(eh1.m_counter == 2); - SASSERT(eh2.m_counter == 3); + ENSURE(eh1.m_counter == 2); + ENSURE(eh2.m_counter == 3); m.remove_del_eh(&eh2); x1 = m.mk_polynomial(m.mk_var()); x1 = 0; - SASSERT(eh1.m_counter == 2); - SASSERT(eh2.m_counter == 3); + ENSURE(eh1.m_counter == 2); + ENSURE(eh2.m_counter == 3); } static void tst_const_coeff() { @@ -1475,36 +1475,36 @@ static void tst_const_coeff() { polynomial_ref p(m); p = (x0^2)*x1 + 3*x0 + x1; - SASSERT(!m.const_coeff(p, 0, 2, c)); - SASSERT(m.const_coeff(p, 0, 1, c) && c == 3); - SASSERT(!m.const_coeff(p, 0, 0, c)); + ENSURE(!m.const_coeff(p, 0, 2, c)); + ENSURE(m.const_coeff(p, 0, 1, c) && c == 3); + ENSURE(!m.const_coeff(p, 0, 0, c)); p = (x0^2)*x1 + 3*x0 + x1 + 1; - SASSERT(!m.const_coeff(p, 0, 2, c)); - SASSERT(m.const_coeff(p, 0, 1, c) && c == 3); - SASSERT(!m.const_coeff(p, 0, 0, c)); + ENSURE(!m.const_coeff(p, 0, 2, c)); + ENSURE(m.const_coeff(p, 0, 1, c) && c == 3); + ENSURE(!m.const_coeff(p, 0, 0, c)); p = (x0^2)*x1 + 3*x0 + 1; - SASSERT(!m.const_coeff(p, 0, 2, c)); - SASSERT(m.const_coeff(p, 0, 1, c) && c == 3); - SASSERT(m.const_coeff(p, 0, 0, c) && c == 1); + ENSURE(!m.const_coeff(p, 0, 2, c)); + ENSURE(m.const_coeff(p, 0, 1, c) && c == 3); + ENSURE(m.const_coeff(p, 0, 0, c) && c == 1); p = x1 + 3*x0 + 1; - SASSERT(m.const_coeff(p, 0, 2, c) && c == 0); - SASSERT(m.const_coeff(p, 0, 1, c) && c == 3); - SASSERT(!m.const_coeff(p, 0, 0, c)); + ENSURE(m.const_coeff(p, 0, 2, c) && c == 0); + ENSURE(m.const_coeff(p, 0, 1, c) && c == 3); + ENSURE(!m.const_coeff(p, 0, 0, c)); p = 5*(x0^2) + 3*x0 + 7; - SASSERT(m.const_coeff(p, 0, 5, c) && c == 0); - SASSERT(m.const_coeff(p, 0, 2, c) && c == 5); - SASSERT(m.const_coeff(p, 0, 1, c) && c == 3); - SASSERT(m.const_coeff(p, 0, 0, c) && c == 7); + ENSURE(m.const_coeff(p, 0, 5, c) && c == 0); + ENSURE(m.const_coeff(p, 0, 2, c) && c == 5); + ENSURE(m.const_coeff(p, 0, 1, c) && c == 3); + ENSURE(m.const_coeff(p, 0, 0, c) && c == 7); p = 5*(x0^2) + 3*x0; - SASSERT(m.const_coeff(p, 0, 0, c) && c == 0); + ENSURE(m.const_coeff(p, 0, 0, c) && c == 0); p = - x0*x1 - x1 + 1; - SASSERT(!m.const_coeff(p, 0, 1, c)); + ENSURE(!m.const_coeff(p, 0, 1, c)); } static void tst_gcd2() { @@ -1669,7 +1669,7 @@ static void tst_newton_interpolation() { m.newton_interpolation(0, 2, ins.c_ptr(), outs, r); } std::cout << "interpolation result: " << r << "\n"; - SASSERT(m.eq((x^2)*y + 5*x*y + 41*x - 9*y - 21, r)); + ENSURE(m.eq((x^2)*y + 5*x*y + 41*x - 9*y - 21, r)); } static void tst_slow_mod_gcd() { @@ -1732,9 +1732,9 @@ void tst_linear_solver() { solver.add(2, as.c_ptr(), b); VERIFY(solver.solve(xs.c_ptr())); - SASSERT(qm.eq(xs[0], mpq(2))); - SASSERT(qm.eq(xs[1], mpq(3))); - SASSERT(qm.eq(xs[2], mpq(-1))); + ENSURE(qm.eq(xs[0], mpq(2))); + ENSURE(qm.eq(xs[1], mpq(3))); + ENSURE(qm.eq(xs[2], mpq(-1))); } static void tst_lex(polynomial_ref const & p1, polynomial_ref const & p2, int lex_expected, polynomial::var min, int lex2_expected) { @@ -1746,11 +1746,11 @@ static void tst_lex(polynomial_ref const & p1, polynomial_ref const & p2, int le std::cout << " "; std::cout.flush(); int r1 = lex_compare(m.get_monomial(p1, 0), m.get_monomial(p2, 0)); int r2 = lex_compare2(m.get_monomial(p1, 0), m.get_monomial(p2, 0), min); - SASSERT(r1 == lex_expected); - SASSERT(r2 == lex2_expected); + ENSURE(r1 == lex_expected); + ENSURE(r2 == lex2_expected); std::cout << r1 << " " << r2 << "\n"; - SASSERT(lex_compare(m.get_monomial(p2, 0), m.get_monomial(p1, 0)) == -r1); - SASSERT(lex_compare2(m.get_monomial(p2, 0), m.get_monomial(p1, 0), min) == -r2); + ENSURE(lex_compare(m.get_monomial(p2, 0), m.get_monomial(p1, 0)) == -r1); + ENSURE(lex_compare2(m.get_monomial(p2, 0), m.get_monomial(p1, 0), min) == -r2); } static void tst_lex() { diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 987d8e13b..03735fef9 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -25,7 +25,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(assert " << str << ")\n"; std::istringstream is(buffer.str()); VERIFY(parse_smt2_commands(ctx, is)); - SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + ENSURE(ctx.begin_assertions() != ctx.end_assertions()); result = *ctx.begin_assertions(); return result; } @@ -125,8 +125,8 @@ private: else if (m_arith.is_numeral(f, r)) { factors[i] = factors.back(); factors.pop_back(); - SASSERT(coefficient.is_zero()); - SASSERT(!r.is_zero()); + ENSURE(coefficient.is_zero()); + ENSURE(!r.is_zero()); coefficient = r; --i; // repeat examining 'i' } @@ -205,8 +205,8 @@ static void nf(expr_ref& term) { else if (arith.is_numeral(f, r)) { factors[i] = factors.back(); factors.pop_back(); - SASSERT(coefficient.is_zero()); - SASSERT(!r.is_zero()); + ENSURE(coefficient.is_zero()); + ENSURE(!r.is_zero()); coefficient = r; --i; // repeat examining 'i' } diff --git a/src/test/prime_generator.cpp b/src/test/prime_generator.cpp index a2610b35e..5af014e0a 100644 --- a/src/test/prime_generator.cpp +++ b/src/test/prime_generator.cpp @@ -35,7 +35,7 @@ void tst_prime_generator() { m.root(sqrt_p, 2); uint64 k = m.get_uint64(sqrt_p); for (uint64 i = 2; i <= k; i++) { - SASSERT(p % i != 0); + ENSURE(p % i != 0); } } std::cout << std::endl; diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index a52c02ecb..83b6e2620 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -37,7 +37,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(assert " << str << ")\n"; std::istringstream is(buffer.str()); VERIFY(parse_smt2_commands(ctx, is)); - SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + ENSURE(ctx.begin_assertions() != ctx.end_assertions()); result = *ctx.begin_assertions(); return result; } diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index ed332ce26..2dc987d77 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -39,7 +39,7 @@ static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe:: smt::kernel solver(m, fp); solver.assert_expr(tmp); lbool res = solver.check(); - //SASSERT(res == l_false); + //ENSURE(res == l_false); if (res != l_false) { std::cout << "Validation failed: " << res << "\n"; std::cout << mk_pp(tmp, m) << "\n"; @@ -75,7 +75,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) solver.assert_expr(tmp); lbool res = solver.check(); std::cout << "checked\n"; - SASSERT(res == l_false); + ENSURE(res == l_false); if (res != l_false) { std::cout << res << "\n"; fatal_error(0); @@ -131,7 +131,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(assert " << str << ")\n"; std::istringstream is(buffer.str()); VERIFY(parse_smt2_commands(ctx, is)); - SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + ENSURE(ctx.begin_assertions() != ctx.end_assertions()); result = *ctx.begin_assertions(); return result; } diff --git a/src/test/rational.cpp b/src/test/rational.cpp index ac478af98..6fa1005b0 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -27,85 +27,85 @@ static void tst1() { rational r1(1); rational r2(1,2); rational r3(2,4); - SASSERT(r2 == r3); - SASSERT(r1 != r2); - SASSERT(r2 + r3 == r1); - SASSERT(r1.is_pos()); - SASSERT((r2 - r1).is_neg()); - SASSERT((r2 - r3).is_zero()); - SASSERT(floor(r2).is_zero()); - SASSERT(ceil(r2).is_one()); + ENSURE(r2 == r3); + ENSURE(r1 != r2); + ENSURE(r2 + r3 == r1); + ENSURE(r1.is_pos()); + ENSURE((r2 - r1).is_neg()); + ENSURE((r2 - r3).is_zero()); + ENSURE(floor(r2).is_zero()); + ENSURE(ceil(r2).is_one()); // std::cout << "-r2: " << (-r2) << ", floor(-r2):" << floor(-r2) << "\n"; - SASSERT(floor(-r2).is_minus_one()); - SASSERT(ceil(-r2).is_zero()); - SASSERT(floor(r1) == r1); - SASSERT(ceil(r1) == r1); + ENSURE(floor(-r2).is_minus_one()); + ENSURE(ceil(-r2).is_zero()); + ENSURE(floor(r1) == r1); + ENSURE(ceil(r1) == r1); rational r4(3,5); - SASSERT(r3 * r4 == rational(3, 10)); - SASSERT(r3 / r4 == rational(5, 6)); + ENSURE(r3 * r4 == rational(3, 10)); + ENSURE(r3 / r4 == rational(5, 6)); rational r5(2,3); - SASSERT(r4 * r5 == rational(2, 5)); + ENSURE(r4 * r5 == rational(2, 5)); --r2; - SASSERT(r2 == -r3); + ENSURE(r2 == -r3); r2.neg(); - SASSERT(r2 == r3); + ENSURE(r2 == r3); --r2; r2 = abs(r2); - SASSERT(r2 == r3); + ENSURE(r2 == r3); --r2; ++r2; - SASSERT(r2 == r3); - SASSERT(r2 == abs(r2)); - SASSERT(r4 * rational(1) == r4); - SASSERT((r4 * rational(0)).is_zero()); - SASSERT(r4 * rational(-1) == -r4); - SASSERT(rational(1) * r4 == r4); - SASSERT((rational(0) * r4).is_zero()); - SASSERT(rational(-1) * r4 == -r4); - SASSERT(r4 + rational(0) == r4); - SASSERT(ceil(r4).is_one()); + ENSURE(r2 == r3); + ENSURE(r2 == abs(r2)); + ENSURE(r4 * rational(1) == r4); + ENSURE((r4 * rational(0)).is_zero()); + ENSURE(r4 * rational(-1) == -r4); + ENSURE(rational(1) * r4 == r4); + ENSURE((rational(0) * r4).is_zero()); + ENSURE(rational(-1) * r4 == -r4); + ENSURE(r4 + rational(0) == r4); + ENSURE(ceil(r4).is_one()); // std::cout << "r3: " << r3 << ", r4: " << r4 << ", -r4: " << -r4 << ", r3 / (-r4): " << (r3 / (-r4)) << "\n"; - SASSERT(r3 / (-r4) == rational(5,-6)); - SASSERT(div(rational(7), rational(2)) == rational(3)); - SASSERT(rational(7) % rational(4) == rational(3)); - SASSERT(div(rational(7), rational(-2)) == rational(-3)); - SASSERT(rational(3) + rational(5) == rational(8)); - SASSERT(rational("13/10") + rational("7/10") == rational(2)); - SASSERT(rational("100/20") == rational(5)); - SASSERT(gcd(rational(12), rational(8)) == rational(4)); - SASSERT(ceil(rational(-3,2)) == rational(-1)); - SASSERT(floor(rational(-3,2)) == rational(-2)); - SASSERT(ceil(rational(3,2)) == rational(2)); - SASSERT(floor(rational(3,2)) == rational(1)); - SASSERT(rational(3).is_pos()); - SASSERT(rational(0).is_nonneg()); - SASSERT(rational(3).is_pos()); - SASSERT(rational(3).is_nonneg()); - SASSERT(rational(0).is_nonneg()); - SASSERT(!rational(3).is_zero()); - SASSERT(!rational(-3).is_zero()); - SASSERT(rational(0).is_zero()); - SASSERT(rational(1).is_one()); - SASSERT(!rational(2).is_one()); - SASSERT(rational(3,4) >= rational(2,8)); - SASSERT(rational(3,4) <= rational(7,8)); - SASSERT(rational(3,4) <= rational(3,4)); - SASSERT(rational(3,4) >= rational(3,4)); - SASSERT(rational(3,4) > rational(2,8)); - SASSERT(rational(3,4) < rational(7,8)); + ENSURE(r3 / (-r4) == rational(5,-6)); + ENSURE(div(rational(7), rational(2)) == rational(3)); + ENSURE(rational(7) % rational(4) == rational(3)); + ENSURE(div(rational(7), rational(-2)) == rational(-3)); + ENSURE(rational(3) + rational(5) == rational(8)); + ENSURE(rational("13/10") + rational("7/10") == rational(2)); + ENSURE(rational("100/20") == rational(5)); + ENSURE(gcd(rational(12), rational(8)) == rational(4)); + ENSURE(ceil(rational(-3,2)) == rational(-1)); + ENSURE(floor(rational(-3,2)) == rational(-2)); + ENSURE(ceil(rational(3,2)) == rational(2)); + ENSURE(floor(rational(3,2)) == rational(1)); + ENSURE(rational(3).is_pos()); + ENSURE(rational(0).is_nonneg()); + ENSURE(rational(3).is_pos()); + ENSURE(rational(3).is_nonneg()); + ENSURE(rational(0).is_nonneg()); + ENSURE(!rational(3).is_zero()); + ENSURE(!rational(-3).is_zero()); + ENSURE(rational(0).is_zero()); + ENSURE(rational(1).is_one()); + ENSURE(!rational(2).is_one()); + ENSURE(rational(3,4) >= rational(2,8)); + ENSURE(rational(3,4) <= rational(7,8)); + ENSURE(rational(3,4) <= rational(3,4)); + ENSURE(rational(3,4) >= rational(3,4)); + ENSURE(rational(3,4) > rational(2,8)); + ENSURE(rational(3,4) < rational(7,8)); TRACE("rational", tout << rational(3,4) << "\n";); TRACE("rational", tout << rational(7,9) << "\n";); TRACE("rational", tout << rational(-3,7) << "\n";); TRACE("rational", tout << rational(5,8) << "\n";); TRACE("rational", tout << rational(4,2) << "\n";); - SASSERT(rational(3) + rational(2) == rational(5)); - SASSERT(rational(3) - rational(2) == rational(1)); - SASSERT(rational(3) * rational(2) == rational(6)); - SASSERT(rational(6) / rational(2) == rational(3)); - SASSERT(rational(6) % rational(4) == rational(2)); - SASSERT(power(rational(2),0) == rational(1)); - SASSERT(power(rational(2),1) == rational(2)); - SASSERT(power(rational(2),3) == rational(8)); + ENSURE(rational(3) + rational(2) == rational(5)); + ENSURE(rational(3) - rational(2) == rational(1)); + ENSURE(rational(3) * rational(2) == rational(6)); + ENSURE(rational(6) / rational(2) == rational(3)); + ENSURE(rational(6) % rational(4) == rational(2)); + ENSURE(power(rational(2),0) == rational(1)); + ENSURE(power(rational(2),1) == rational(2)); + ENSURE(power(rational(2),3) == rational(8)); } static void tst2() { @@ -116,90 +116,90 @@ static void tst2() { TRACE("rational", tout << r2 << std::endl;); TRACE("rational", tout << r3 << std::endl;); - SASSERT(r2 == r3); - SASSERT(r1 != r2); - SASSERT(rational(2)*r2 + r3 == r1); - SASSERT(r1.is_pos()); - SASSERT((r2 - r1).is_neg()); - SASSERT((r2 - r3).is_zero()); + ENSURE(r2 == r3); + ENSURE(r1 != r2); + ENSURE(rational(2)*r2 + r3 == r1); + ENSURE(r1.is_pos()); + ENSURE((r2 - r1).is_neg()); + ENSURE((r2 - r3).is_zero()); // std::cout << "===> " << floor(r2) << "\n"; { rational r0("1/3000000000000000000000000"); - SASSERT(ceil(r0).is_one()); - SASSERT(floor(-r0).is_minus_one()); - SASSERT(ceil(-r0).is_zero()); + ENSURE(ceil(r0).is_one()); + ENSURE(floor(-r0).is_minus_one()); + ENSURE(ceil(-r0).is_zero()); } - SASSERT(floor(r1) == r1); - SASSERT(ceil(r1) == r1); + ENSURE(floor(r1) == r1); + ENSURE(ceil(r1) == r1); rational r4("300000000/5"); - SASSERT(rational(1,2) * r4 == rational("300000000/10")); - SASSERT(rational(1,2) / r4 == rational("5/600000000")); + ENSURE(rational(1,2) * r4 == rational("300000000/10")); + ENSURE(rational(1,2) / r4 == rational("5/600000000")); rational r5(2,3); - SASSERT(r4 * r5 == rational("200000000/5")); + ENSURE(r4 * r5 == rational("200000000/5")); rational r6("10000000000000000000000000000000003/3"); --r6; - SASSERT(r6 == r2); + ENSURE(r6 == r2); r6.neg(); - SASSERT(r6 != r2); - SASSERT(abs(r6) == r2); + ENSURE(r6 != r2); + ENSURE(abs(r6) == r2); --r2; ++r2; r2.neg(); - SASSERT(r2 == r6); - SASSERT(r6 * rational(1) == r6); - SASSERT((r6 * rational(0)).is_zero()); - SASSERT(r6 * rational(-1) == -r6); - SASSERT(rational(1) * r6 == r6); - SASSERT((rational(0) * r6).is_zero()); - SASSERT(rational(-1) * r6 == -r6); - SASSERT(r6 + rational(0) == r6); + ENSURE(r2 == r6); + ENSURE(r6 * rational(1) == r6); + ENSURE((r6 * rational(0)).is_zero()); + ENSURE(r6 * rational(-1) == -r6); + ENSURE(rational(1) * r6 == r6); + ENSURE((rational(0) * r6).is_zero()); + ENSURE(rational(-1) * r6 == -r6); + ENSURE(r6 + rational(0) == r6); - SASSERT(rational("300000000000000").is_pos()); - SASSERT(rational("0000000000000000000").is_nonneg()); - SASSERT(rational("0000000000000000000").is_nonpos()); - SASSERT(rational("3000000000000000000/2").is_pos()); - SASSERT(rational("3000000000000000000/2").is_nonneg()); - SASSERT((-rational("3000000000000000000/2")).is_neg()); - SASSERT(!rational("3000000000000000000/2").is_neg()); - SASSERT(!rational("3000000000000000000/2").is_zero()); - SASSERT(!rational("3000000000000000000/2").is_one()); - SASSERT(rational("99999999999/2") >= rational("23/2")); - SASSERT(rational("99999999999/2") > rational("23/2")); - SASSERT(rational("23/2") <= rational("99999999999/2")); - SASSERT(rational("23/2") < rational("99999999999/2")); - SASSERT(!(rational("99999999999/2") < rational("23/2"))); + ENSURE(rational("300000000000000").is_pos()); + ENSURE(rational("0000000000000000000").is_nonneg()); + ENSURE(rational("0000000000000000000").is_nonpos()); + ENSURE(rational("3000000000000000000/2").is_pos()); + ENSURE(rational("3000000000000000000/2").is_nonneg()); + ENSURE((-rational("3000000000000000000/2")).is_neg()); + ENSURE(!rational("3000000000000000000/2").is_neg()); + ENSURE(!rational("3000000000000000000/2").is_zero()); + ENSURE(!rational("3000000000000000000/2").is_one()); + ENSURE(rational("99999999999/2") >= rational("23/2")); + ENSURE(rational("99999999999/2") > rational("23/2")); + ENSURE(rational("23/2") <= rational("99999999999/2")); + ENSURE(rational("23/2") < rational("99999999999/2")); + ENSURE(!(rational("99999999999/2") < rational("23/2"))); rational int64_max("9223372036854775807"); rational int64_min((-int64_max) - rational(1)); // is_int64 - SASSERT(int64_max.is_int64()); - SASSERT(int64_min.is_int64()); - SASSERT(rational(0).is_int64()); - SASSERT(rational(1).is_int64()); - SASSERT(rational(-1).is_int64()); - SASSERT(!(int64_max + rational(1)).is_int64()); - SASSERT(!(int64_min - rational(1)).is_int64()); + ENSURE(int64_max.is_int64()); + ENSURE(int64_min.is_int64()); + ENSURE(rational(0).is_int64()); + ENSURE(rational(1).is_int64()); + ENSURE(rational(-1).is_int64()); + ENSURE(!(int64_max + rational(1)).is_int64()); + ENSURE(!(int64_min - rational(1)).is_int64()); // is_uint64 - SASSERT(int64_max.is_uint64()); - SASSERT(!int64_min.is_uint64()); - SASSERT(rational(0).is_uint64()); - SASSERT(rational(1).is_uint64()); - SASSERT(!rational(-1).is_uint64()); - SASSERT((int64_max + rational(1)).is_uint64()); - SASSERT(!(int64_min - rational(1)).is_uint64()); + ENSURE(int64_max.is_uint64()); + ENSURE(!int64_min.is_uint64()); + ENSURE(rational(0).is_uint64()); + ENSURE(rational(1).is_uint64()); + ENSURE(!rational(-1).is_uint64()); + ENSURE((int64_max + rational(1)).is_uint64()); + ENSURE(!(int64_min - rational(1)).is_uint64()); rational uint64_max(rational(1) + (rational(2) * int64_max)); - SASSERT(uint64_max.is_uint64()); + ENSURE(uint64_max.is_uint64()); // get_int64, get_uint64 uint64 u1 = uint64_max.get_uint64(); uint64 u2 = UINT64_MAX; VERIFY(u1 == u2); std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n"; - SASSERT(int64_max.get_int64() == INT64_MAX); - SASSERT(int64_min.get_int64() == INT64_MIN); + ENSURE(int64_max.get_int64() == INT64_MAX); + ENSURE(int64_min.get_int64() == INT64_MIN); // extended Euclid: @@ -219,7 +219,7 @@ void tst3() { TRACE("rational", tout << "n4: " << n4 << "\n"; tout << "n5: " << n5 << "\n";); - SASSERT(n5 == rational("2147483646")); + ENSURE(n5 == rational("2147483646")); } void tst4() { @@ -236,7 +236,7 @@ void tst5() { TRACE("rational", tout << n1 << " " << n2 << " " << n1.is_big() << " " << n2.is_big() << "\n";); n1 *= n2; TRACE("rational", tout << "after: " << n1 << " " << n2 << "\n";); - SASSERT(n1.is_minus_one()); + ENSURE(n1.is_minus_one()); } void tst6() { @@ -274,8 +274,8 @@ public: static void tst1() { rational n1(-1); rational n2(8); - SASSERT((n1 % n2).is_minus_one()); - SASSERT(mod(n1, n2) == rational(7)); + ENSURE((n1 % n2).is_minus_one()); + ENSURE(mod(n1, n2) == rational(7)); } static void tst_hash(int val) { @@ -283,7 +283,7 @@ public: rational n2("10203939394995449949494394932929"); rational n3(val); n2 = n3; - SASSERT(n1.hash() == n2.hash()); + ENSURE(n1.hash() == n2.hash()); } static void tst2() { @@ -306,47 +306,47 @@ static void tst7() { rational gcd; extended_gcd(n, p, gcd, x, y); TRACE("gcd", tout << n << " " << p << ": " << gcd << " " << x << " " << y << "\n";); - SASSERT(!mod(n, rational(2)).is_one() || mod(n * x, p).is_one()); + ENSURE(!mod(n, rational(2)).is_one() || mod(n * x, p).is_one()); } } static void tst8() { rational r; - SASSERT(!rational(-4).is_int_perfect_square(r) && r.is_zero()); - SASSERT(!rational(-3).is_int_perfect_square(r) && r.is_zero()); - SASSERT(!rational(-2).is_int_perfect_square(r) && r.is_zero()); - SASSERT(!rational(-1).is_int_perfect_square(r) && r.is_zero()); - SASSERT(rational(0).is_int_perfect_square(r) && r.is_zero()); - SASSERT(rational(1).is_int_perfect_square(r) && r.is_one()); - SASSERT(!rational(2).is_int_perfect_square(r) && r == rational(2)); - SASSERT(!rational(3).is_int_perfect_square(r) && r == rational(2)); - SASSERT(rational(4).is_int_perfect_square(r) && r == rational(2)); - SASSERT(!rational(5).is_int_perfect_square(r) && r == rational(3)); - SASSERT(!rational(6).is_int_perfect_square(r) && r == rational(3)); - SASSERT(!rational(7).is_int_perfect_square(r) && r == rational(3)); - SASSERT(!rational(8).is_int_perfect_square(r) && r == rational(3)); - SASSERT(rational(9).is_int_perfect_square(r) && r == rational(3)); - SASSERT(!rational(10).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(11).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(12).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(13).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(14).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(15).is_int_perfect_square(r) && r == rational(4)); - SASSERT(rational(16).is_int_perfect_square(r) && r == rational(4)); - SASSERT(!rational(17).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(18).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(19).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(20).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(21).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(22).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(23).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(24).is_int_perfect_square(r) && r == rational(5)); - SASSERT(rational(25).is_int_perfect_square(r) && r == rational(5)); - SASSERT(!rational(26).is_int_perfect_square(r) && r == rational(6)); - SASSERT(rational(36).is_int_perfect_square(r) && r == rational(6)); + ENSURE(!rational(-4).is_int_perfect_square(r) && r.is_zero()); + ENSURE(!rational(-3).is_int_perfect_square(r) && r.is_zero()); + ENSURE(!rational(-2).is_int_perfect_square(r) && r.is_zero()); + ENSURE(!rational(-1).is_int_perfect_square(r) && r.is_zero()); + ENSURE(rational(0).is_int_perfect_square(r) && r.is_zero()); + ENSURE(rational(1).is_int_perfect_square(r) && r.is_one()); + ENSURE(!rational(2).is_int_perfect_square(r) && r == rational(2)); + ENSURE(!rational(3).is_int_perfect_square(r) && r == rational(2)); + ENSURE(rational(4).is_int_perfect_square(r) && r == rational(2)); + ENSURE(!rational(5).is_int_perfect_square(r) && r == rational(3)); + ENSURE(!rational(6).is_int_perfect_square(r) && r == rational(3)); + ENSURE(!rational(7).is_int_perfect_square(r) && r == rational(3)); + ENSURE(!rational(8).is_int_perfect_square(r) && r == rational(3)); + ENSURE(rational(9).is_int_perfect_square(r) && r == rational(3)); + ENSURE(!rational(10).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(11).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(12).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(13).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(14).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(15).is_int_perfect_square(r) && r == rational(4)); + ENSURE(rational(16).is_int_perfect_square(r) && r == rational(4)); + ENSURE(!rational(17).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(18).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(19).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(20).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(21).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(22).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(23).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(24).is_int_perfect_square(r) && r == rational(5)); + ENSURE(rational(25).is_int_perfect_square(r) && r == rational(5)); + ENSURE(!rational(26).is_int_perfect_square(r) && r == rational(6)); + ENSURE(rational(36).is_int_perfect_square(r) && r == rational(6)); - SASSERT(rational(1,9).is_perfect_square(r) && r == rational(1,3)); - SASSERT(rational(4,9).is_perfect_square(r) && r == rational(2,3)); + ENSURE(rational(1,9).is_perfect_square(r) && r == rational(1,3)); + ENSURE(rational(4,9).is_perfect_square(r) && r == rational(2,3)); } @@ -363,9 +363,9 @@ static void tstmod(rational const& m, rational const& n) { std::cout << m << " " << n << " " << q << " " << r << "\n"; std::cout << m << " == " << n*q+r << "\n"; - SASSERT(m == (n * q) + r); - SASSERT(rational::zero() <= r); - SASSERT(r < abs(n)); + ENSURE(m == (n * q) + r); + ENSURE(rational::zero() <= r); + ENSURE(r < abs(n)); } diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp index 170c053f1..082147190 100644 --- a/src/test/rcf.cpp +++ b/src/test/rcf.cpp @@ -116,13 +116,13 @@ static void tst_solve(unsigned n, int _A[], int _b[], int _c[], bool solved) { svector b; b.resize(n, 0); if (mm.solve(A, b.c_ptr(), _c)) { - SASSERT(solved); + ENSURE(solved); for (unsigned i = 0; i < n; i++) { - SASSERT(b[i] == _b[i]); + ENSURE(b[i] == _b[i]); } } else { - SASSERT(!solved); + ENSURE(!solved); } } @@ -140,7 +140,7 @@ static void tst_lin_indep(unsigned m, unsigned n, int _A[], unsigned ex_sz, unsi scoped_mpz_matrix B(mm); mm.linear_independent_rows(A, r.c_ptr(), B); for (unsigned i = 0; i < ex_sz; i++) { - SASSERT(r[i] == ex_r[i]); + ENSURE(r[i] == ex_r[i]); } } diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index a271ce6bb..7e3d50e8d 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -73,7 +73,7 @@ static void check_coherence(sat::solver& s1, trail_t& t) { s2.display(std::cout); } std::cout << is_sat1 << "\n"; - SASSERT(is_sat1 == is_sat2); + ENSURE(is_sat1 == is_sat2); } void tst_sat_user_scope() { diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp index 6f08bd04d..8e57f6110 100644 --- a/src/test/simplex.cpp +++ b/src/test/simplex.cpp @@ -84,7 +84,7 @@ void add_row(Simplex& S, vector const& _v, R const& _b, bool is_eq = false) { coeffs.push_back(b.to_mpq().numerator()); mpq_inf one(mpq(1),mpq(0)); mpq_inf zero(mpq(0),mpq(0)); - SASSERT(vars.size() == coeffs.size()); + ENSURE(vars.size() == coeffs.size()); S.set_lower(nv, zero); if (is_eq) S.set_upper(nv, zero); S.set_lower(nv+1, one); diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index 2e8f434e1..5a05ab30f 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -18,7 +18,7 @@ static void ev_const(Z3_context ctx, Z3_ast e) { tout << Z3_ast_to_string(ctx, e) << " -> "; tout << Z3_ast_to_string(ctx, r) << "\n";); Z3_ast_kind k = Z3_get_ast_kind(ctx, r); - SASSERT(k == Z3_NUMERAL_AST || + ENSURE(k == Z3_NUMERAL_AST || (k == Z3_APP_AST && (Z3_OP_TRUE == Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx, Z3_to_app(ctx, r))) || Z3_OP_FALSE == Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx, Z3_to_app(ctx, r)))))); @@ -34,7 +34,7 @@ static void test_bv() { Z3_ast bit3_2 = Z3_mk_numeral(ctx, "3", bv2); Z3_ast e = Z3_mk_eq(ctx, bit3_2, Z3_mk_sign_ext(ctx, 1, bit1_1)); - SASSERT(Z3_simplify(ctx, e) == Z3_mk_true(ctx)); + ENSURE(Z3_simplify(ctx, e) == Z3_mk_true(ctx)); TRACE("simplifier", tout << Z3_ast_to_string(ctx, e) << "\n";); Z3_ast b12 = Z3_mk_numeral(ctx, "12", bv72); @@ -97,18 +97,18 @@ static void test_datatypes() { nil = Z3_mk_app(ctx, nil_decl, 0, 0); Z3_ast a = Z3_simplify(ctx, Z3_mk_app(ctx, is_nil_decl, 1, &nil)); - SASSERT(a == Z3_mk_true(ctx)); + ENSURE(a == Z3_mk_true(ctx)); a = Z3_simplify(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &nil)); - SASSERT(a == Z3_mk_false(ctx)); + ENSURE(a == Z3_mk_false(ctx)); Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty); Z3_ast args[2] = { one, nil }; l1 = Z3_mk_app(ctx, cons_decl, 2, args); - SASSERT(nil == Z3_simplify(ctx, Z3_mk_app(ctx, tail_decl, 1, &l1))); - SASSERT(one == Z3_simplify(ctx, Z3_mk_app(ctx, head_decl, 1, &l1))); + ENSURE(nil == Z3_simplify(ctx, Z3_mk_app(ctx, tail_decl, 1, &l1))); + ENSURE(one == Z3_simplify(ctx, Z3_mk_app(ctx, head_decl, 1, &l1))); - SASSERT(Z3_mk_false(ctx) == Z3_simplify(ctx, Z3_mk_eq(ctx, nil, l1))); + ENSURE(Z3_mk_false(ctx) == Z3_simplify(ctx, Z3_mk_eq(ctx, nil, l1))); Z3_del_config(cfg); Z3_del_context(ctx); @@ -147,8 +147,8 @@ static void test_bool() { Z3_ast a = Z3_simplify(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)))); Z3_ast b = Z3_simplify(ctx, Z3_mk_not(ctx, Z3_mk_iff(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)))); - SASSERT(Z3_mk_true(ctx) == a); - SASSERT(Z3_mk_true(ctx) == b); + ENSURE(Z3_mk_true(ctx) == a); + ENSURE(Z3_mk_true(ctx) == b); TRACE("simplifier", tout << Z3_ast_to_string(ctx, a) << "\n";); TRACE("simplifier", tout << Z3_ast_to_string(ctx, b) << "\n";); @@ -179,8 +179,8 @@ static void test_array() { TRACE("simplifier", tout << Z3_ast_to_string(ctx, rxy) << "\n";); TRACE("simplifier", tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3))) << "\n";); - // SASSERT(rxy == Z3_mk_true(ctx)); - // SASSERT(Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3)) == Z3_mk_false(ctx)); + // ENSURE(rxy == Z3_mk_true(ctx)); + // ENSURE(Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3)) == Z3_mk_false(ctx)); for (unsigned i = 0; i < 4; ++i) { for (unsigned j = 0; j < 4; ++j) { diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 87cc05375..9836bc04d 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -57,7 +57,7 @@ struct unsigned_ext { static void is_sorted(svector const& v) { for (unsigned i = 0; i + 1 < v.size(); ++i) { - SASSERT(v[i] <= v[i+1]); + ENSURE(v[i] <= v[i+1]); } } @@ -184,7 +184,7 @@ struct ast_ext2 { static void test_sorting_eq(unsigned n, unsigned k) { - SASSERT(k < n); + ENSURE(k < n); ast_manager m; reg_decl_plugins(m); ast_ext2 ext(m); @@ -206,14 +206,14 @@ static void test_sorting_eq(unsigned n, unsigned k) { solver.assert_expr(ext.m_clauses[i].get()); } lbool res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); solver.push(); for (unsigned i = 0; i < k; ++i) { solver.assert_expr(in[i].get()); } res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); solver.assert_expr(in[k].get()); res = solver.check(); if (res == l_true) { @@ -227,7 +227,7 @@ static void test_sorting_eq(unsigned n, unsigned k) { model_smt2_pp(std::cout, m, *model, 0); TRACE("pb", model_smt2_pp(tout, m, *model, 0);); } - SASSERT(res == l_false); + ENSURE(res == l_false); solver.pop(1); ext.m_clauses.reset(); } @@ -253,13 +253,13 @@ static void test_sorting_le(unsigned n, unsigned k) { solver.assert_expr(ext.m_clauses[i].get()); } lbool res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); for (unsigned i = 0; i < k; ++i) { solver.assert_expr(in[i].get()); } res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); solver.assert_expr(in[k].get()); res = solver.check(); if (res == l_true) { @@ -273,7 +273,7 @@ static void test_sorting_le(unsigned n, unsigned k) { model_smt2_pp(std::cout, m, *model, 0); TRACE("pb", model_smt2_pp(tout, m, *model, 0);); } - SASSERT(res == l_false); + ENSURE(res == l_false); solver.pop(1); ext.m_clauses.reset(); } @@ -300,14 +300,14 @@ void test_sorting_ge(unsigned n, unsigned k) { solver.assert_expr(ext.m_clauses[i].get()); } lbool res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); solver.push(); for (unsigned i = 0; i < n - k; ++i) { solver.assert_expr(m.mk_not(in[i].get())); } res = solver.check(); - SASSERT(res == l_true); + ENSURE(res == l_true); solver.assert_expr(m.mk_not(in[n - k].get())); res = solver.check(); if (res == l_true) { @@ -321,7 +321,7 @@ void test_sorting_ge(unsigned n, unsigned k) { model_smt2_pp(std::cout, m, *model, 0); TRACE("pb", model_smt2_pp(tout, m, *model, 0);); } - SASSERT(res == l_false); + ENSURE(res == l_false); solver.pop(1); } diff --git a/src/test/stack.cpp b/src/test/stack.cpp index 6a4dd3cd8..c8f3d88a6 100644 --- a/src/test/stack.cpp +++ b/src/test/stack.cpp @@ -27,8 +27,8 @@ static void tst1() { point * p1 = new (s) point(10, 20); point * p2 = new (s) point(30, 40); void * ptr = s.allocate(16000); - SASSERT(p2->first == 30 && p2->second == 40); - SASSERT(p1->first == 10 && p1->second == 20); + ENSURE(p2->first == 30 && p2->second == 40); + ENSURE(p1->first == 10 && p1->second == 20); s.deallocate(static_cast(ptr)); s.deallocate(p2); s.deallocate(p1); @@ -38,8 +38,8 @@ static void tst2(unsigned num, unsigned del_rate) { ptr_vector ptrs; stack s; for (unsigned i = 0; i < num; i++) { - SASSERT(ptrs.empty() == s.empty()); - SASSERT(s.empty() || ptrs.back() == s.top()); + ENSURE(ptrs.empty() == s.empty()); + ENSURE(s.empty() || ptrs.back() == s.top()); if (!ptrs.empty() && rand() % del_rate == 0) { s.deallocate(); ptrs.pop_back(); @@ -57,8 +57,8 @@ static void tst2(unsigned num, unsigned del_rate) { } } while (s.empty()) { - SASSERT(ptrs.empty() == s.empty()); - SASSERT(s.empty() || ptrs.back() == s.top()); + ENSURE(ptrs.empty() == s.empty()); + ENSURE(s.empty() || ptrs.back() == s.top()); s.deallocate(); ptrs.pop_back(); } diff --git a/src/test/string_buffer.cpp b/src/test/string_buffer.cpp index 67d60528c..7d7854a9c 100644 --- a/src/test/string_buffer.cpp +++ b/src/test/string_buffer.cpp @@ -24,7 +24,7 @@ Revision History: static void tst1() { string_buffer<> b; b << "Testing" << 10 << true; - SASSERT(strcmp(b.c_str(), "Testing10true") == 0); + ENSURE(strcmp(b.c_str(), "Testing10true") == 0); } static void tst2() { @@ -34,7 +34,7 @@ static void tst2() { b << r; } TRACE("string_buffer", tout << b.c_str() << "\n";); - SASSERT(strlen(b.c_str()) == 10000); + ENSURE(strlen(b.c_str()) == 10000); } static void tst3() { @@ -42,7 +42,7 @@ static void tst3() { string_buffer<128> b2; b2 << "World"; b << "Hello" << " " << b2; - SASSERT(strcmp(b.c_str(), "Hello World") == 0); + ENSURE(strcmp(b.c_str(), "Hello World") == 0); } void tst_string_buffer() { diff --git a/src/test/symbol.cpp b/src/test/symbol.cpp index c87955116..e91332285 100644 --- a/src/test/symbol.cpp +++ b/src/test/symbol.cpp @@ -24,31 +24,31 @@ static void tst1() { symbol s1("foo"); symbol s2("boo"); symbol s3("foo"); - SASSERT(s1 != s2); - SASSERT(s1 == s3); + ENSURE(s1 != s2); + ENSURE(s1 == s3); std::cout << s1 << " " << s2 << " " << s3 << "\n"; - SASSERT(s1 == "foo"); - SASSERT(s1 != "boo"); - SASSERT(s2 != "foo"); - SASSERT(s3 == "foo"); - SASSERT(s2 == "boo"); + ENSURE(s1 == "foo"); + ENSURE(s1 != "boo"); + ENSURE(s2 != "foo"); + ENSURE(s3 == "foo"); + ENSURE(s2 == "boo"); - SASSERT(lt(s2, s1)); - SASSERT(!lt(s1, s2)); - SASSERT(!lt(s1, s3)); - SASSERT(lt(symbol("abcc"), symbol("abcd"))); - SASSERT(!lt(symbol("abcd"), symbol("abcc"))); - SASSERT(lt(symbol("abc"), symbol("abcc"))); - SASSERT(!lt(symbol("abcd"), symbol("abc"))); - SASSERT(lt(symbol(10), s1)); - SASSERT(!lt(s1, symbol(10))); - SASSERT(lt(symbol(10), symbol(20))); - SASSERT(!lt(symbol(20), symbol(10))); - SASSERT(!lt(symbol(10), symbol(10))); - SASSERT(lt(symbol("a"), symbol("b"))); - SASSERT(!lt(symbol("z"), symbol("b"))); - SASSERT(!lt(symbol("zzz"), symbol("b"))); - SASSERT(lt(symbol("zzz"), symbol("zzzb"))); + ENSURE(lt(s2, s1)); + ENSURE(!lt(s1, s2)); + ENSURE(!lt(s1, s3)); + ENSURE(lt(symbol("abcc"), symbol("abcd"))); + ENSURE(!lt(symbol("abcd"), symbol("abcc"))); + ENSURE(lt(symbol("abc"), symbol("abcc"))); + ENSURE(!lt(symbol("abcd"), symbol("abc"))); + ENSURE(lt(symbol(10), s1)); + ENSURE(!lt(s1, symbol(10))); + ENSURE(lt(symbol(10), symbol(20))); + ENSURE(!lt(symbol(20), symbol(10))); + ENSURE(!lt(symbol(10), symbol(10))); + ENSURE(lt(symbol("a"), symbol("b"))); + ENSURE(!lt(symbol("z"), symbol("b"))); + ENSURE(!lt(symbol("zzz"), symbol("b"))); + ENSURE(lt(symbol("zzz"), symbol("zzzb"))); } void tst_symbol() { diff --git a/src/test/symbol_table.cpp b/src/test/symbol_table.cpp index f67ef6f66..8c3c55c9d 100644 --- a/src/test/symbol_table.cpp +++ b/src/test/symbol_table.cpp @@ -21,24 +21,24 @@ Revision History: static void tst1() { symbol_table t; t.insert(symbol("foo"), 35); - SASSERT(t.contains(symbol("foo"))); - SASSERT(!t.contains(symbol("boo"))); + ENSURE(t.contains(symbol("foo"))); + ENSURE(!t.contains(symbol("boo"))); t.begin_scope(); t.insert(symbol("boo"), 20); - SASSERT(t.contains(symbol("boo"))); + ENSURE(t.contains(symbol("boo"))); #ifdef Z3DEBUG int tmp; #endif - SASSERT(t.find(symbol("boo"), tmp) && tmp == 20); - SASSERT(t.find(symbol("foo"), tmp) && tmp == 35); + ENSURE(t.find(symbol("boo"), tmp) && tmp == 20); + ENSURE(t.find(symbol("foo"), tmp) && tmp == 35); t.insert(symbol("foo"), 100); - SASSERT(t.find(symbol("foo"), tmp) && tmp == 100); + ENSURE(t.find(symbol("foo"), tmp) && tmp == 100); t.end_scope(); - SASSERT(t.find(symbol("foo"), tmp) && tmp == 35); - SASSERT(!t.contains(symbol("boo"))); + ENSURE(t.find(symbol("foo"), tmp) && tmp == 35); + ENSURE(!t.contains(symbol("boo"))); t.reset(); - SASSERT(!t.contains(symbol("boo"))); - SASSERT(!t.contains(symbol("foo"))); + ENSURE(!t.contains(symbol("boo"))); + ENSURE(!t.contains(symbol("foo"))); } void tst_symbol_table() { diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index 7637c7e83..00f7e0960 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -17,18 +17,18 @@ static void tst1(unsigned num_bits) { m.display(std::cout, *b1) << "\n"; m.display(std::cout, *bX) << "\n"; m.display(std::cout, *bN) << "\n"; - SASSERT(!m.equals(*b1,*b0)); - SASSERT(!m.equals(*b1,*bX)); - SASSERT(!m.equals(*b0,*bX)); + ENSURE(!m.equals(*b1,*b0)); + ENSURE(!m.equals(*b1,*bX)); + ENSURE(!m.equals(*b0,*bX)); m.set_and(*bX,*b0); - SASSERT(m.equals(*b0,*bX)); - SASSERT(!m.equals(*b1,*bX)); + ENSURE(m.equals(*b0,*bX)); + ENSURE(!m.equals(*b1,*bX)); m.copy(*bX,*b1); - SASSERT(m.equals(*b1,*bX)); - SASSERT(!m.equals(*b0,*bX)); + ENSURE(m.equals(*b1,*bX)); + ENSURE(!m.equals(*b0,*bX)); m.fillX(*bX); VERIFY(m.intersect(*bX,*b0,*bN)); - SASSERT(m.equals(*b0, *bN)); + ENSURE(m.equals(*b0, *bN)); VERIFY(!m.intersect(*b0,*b1,*bN)); m.fill1(*b1); bit_vector to_delete; @@ -58,8 +58,8 @@ static void tst0() { m.display(std::cout, *t1) << "\n"; m.display(std::cout, *t2) << "\n"; m.display(std::cout, *t3) << "\n"; - SASSERT(m.equals(*t1, *t2)); - SASSERT(m.equals(*t1, *t3)); + ENSURE(m.equals(*t1, *t2)); + ENSURE(m.equals(*t1, *t3)); } static void tst2(unsigned num_bits) { @@ -67,10 +67,10 @@ static void tst2(unsigned num_bits) { tbv_ref t(m), t2(m); for (unsigned i = 0; i < 55; ++i) { t = m.allocate(i); - SASSERT(m.is_well_formed(*t)); + ENSURE(m.is_well_formed(*t)); t2 = m.allocate(i+1); VERIFY(!m.set_and(*t2, *t)); - SASSERT(!m.is_well_formed(*t2)); + ENSURE(!m.is_well_formed(*t2)); } } diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp index 3a229d951..42a03f619 100644 --- a/src/test/theory_pb.cpp +++ b/src/test/theory_pb.cpp @@ -12,7 +12,7 @@ Copyright (c) 2015 Microsoft Corporation #include "th_rewriter.h" unsigned populate_literals(unsigned k, smt::literal_vector& lits) { - SASSERT(k < (1u << lits.size())); + ENSURE(k < (1u << lits.size())); unsigned t = 0; for (unsigned i = 0; i < lits.size(); ++i) { if (k & (1 << i)) { @@ -159,7 +159,7 @@ void tst_theory_pb() { smt::context ctx(m, params); ctx.push(); smt::literal l = smt::theory_pb::assert_ge(ctx, k, lits.size(), lits.c_ptr()); - SASSERT(l != smt::false_literal); + ENSURE(l != smt::false_literal); ctx.assign(l, 0, false); TRACE("pb", ctx.display(tout);); VERIFY(l_true == ctx.check()); diff --git a/src/test/total_order.cpp b/src/test/total_order.cpp index 2fa22065f..12bb4d977 100644 --- a/src/test/total_order.cpp +++ b/src/test/total_order.cpp @@ -25,12 +25,12 @@ static void tst1() { to.insert(1); to.insert_after(1, 2); to.insert_after(1, 3); - SASSERT(to.lt(1, 2)); - SASSERT(to.lt(3, 2)); - SASSERT(to.lt(1, 3)); - SASSERT(!to.lt(2, 3)); - SASSERT(!to.lt(3, 1)); - SASSERT(!to.lt(2, 2)); + ENSURE(to.lt(1, 2)); + ENSURE(to.lt(3, 2)); + ENSURE(to.lt(1, 3)); + ENSURE(!to.lt(2, 3)); + ENSURE(!to.lt(3, 1)); + ENSURE(!to.lt(2, 2)); std::cout << to << "\n"; } @@ -43,8 +43,8 @@ static void tst2() { to.move_after(3, 1); to.move_after(1, 2); to.move_after(2, 3); - SASSERT(to.lt(1,2)); - SASSERT(to.lt(2,3)); + ENSURE(to.lt(1,2)); + ENSURE(to.lt(2,3)); } } @@ -75,7 +75,7 @@ void move_after(unsigned_vector & v, unsigned_vector & inv_v, unsigned a, unsign // std::cout << "move_after(" << a << ", " << b << ")\n"; unsigned pos_a = inv_v[a]; unsigned pos_b = inv_v[b]; - SASSERT(pos_a != pos_b); + ENSURE(pos_a != pos_b); if (pos_b < pos_a) { for (unsigned i = pos_b; i < pos_a; i++) { v[i] = v[i+1]; @@ -83,17 +83,17 @@ void move_after(unsigned_vector & v, unsigned_vector & inv_v, unsigned a, unsign } v[pos_a] = b; inv_v[b] = pos_a; - SASSERT(inv_v[b] == inv_v[a] + 1); + ENSURE(inv_v[b] == inv_v[a] + 1); } else { - SASSERT(pos_b > pos_a); + ENSURE(pos_b > pos_a); for (unsigned i = pos_b; i > pos_a + 1; i--) { v[i] = v[i-1]; inv_v[v[i-1]] = i; } v[pos_a+1] = b; inv_v[b] = pos_a+1; - SASSERT(inv_v[b] == inv_v[a] + 1); + ENSURE(inv_v[b] == inv_v[a] + 1); } // display(std::cout, v.begin(), v.end()); std::cout << std::endl; } @@ -118,8 +118,8 @@ static void tst4(unsigned sz, unsigned num_rounds) { move_after(v, inv_v, v1, v2); } for (unsigned k = 0; k < sz - 1; k++) { - SASSERT(inv_v[v[k]] == k); - SASSERT(to.lt(v[k], v[k+1])); + ENSURE(inv_v[v[k]] == k); + ENSURE(to.lt(v[k], v[k+1])); } if (i % 1000 == 0) { std::cout << "*"; diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index dc88e20af..57866c3ac 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -85,7 +85,7 @@ class udoc_tester { doc_ref result(dm); t = mk_rand_tbv(dm); result = dm.allocate(*t); - SASSERT(dm.tbvm().equals(*t, result->pos())); + ENSURE(dm.tbvm().equals(*t, result->pos())); for (unsigned i = 0; i < num_diff; ++i) { t = mk_rand_tbv(dm, result->pos()); if (dm.tbvm().equals(*t, result->pos())) { @@ -97,7 +97,7 @@ class udoc_tester { } result->neg().push_back(t.detach()); } - SASSERT(dm.well_formed(*result)); + ENSURE(dm.well_formed(*result)); return result.detach(); } @@ -121,7 +121,7 @@ public: } udoc_relation* mk_empty(relation_signature const& sig) { - SASSERT(p.can_handle_signature(sig)); + ENSURE(p.can_handle_signature(sig)); relation_base* empty = p.mk_empty(sig); return dynamic_cast(empty); } @@ -210,7 +210,7 @@ public: jc1.push_back(1); jc2.push_back(1); datalog::relation_join_fn* join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr()); - SASSERT(join_fn); + ENSURE(join_fn); t = (*join_fn)(*t1, *t2); cr.verify_join(*t1, *t2, *t, jc1, jc2); t->display(std::cout); std::cout << "\n"; @@ -218,13 +218,13 @@ public: t = (*join_fn)(*t1, *t3); cr.verify_join(*t1, *t3, *t, jc1, jc2); - SASSERT(t->empty()); + ENSURE(t->empty()); t->display(std::cout); std::cout << "\n"; t->deallocate(); t = (*join_fn)(*t3, *t3); cr.verify_join(*t3, *t3, *t, jc1, jc2); - SASSERT(t->empty()); + ENSURE(t->empty()); t->display(std::cout); std::cout << "\n"; t->deallocate(); @@ -843,9 +843,9 @@ public: rel_union union_fn = p.mk_union_fn(r, r, 0); (*union_fn)(r, *full); doc_manager& dm = r.get_dm(); - SASSERT(r.get_udoc().size() == 1); + ENSURE(r.get_udoc().size() == 1); doc& d0 = r.get_udoc()[0]; - SASSERT(dm.is_full(d0)); + ENSURE(dm.is_full(d0)); for (unsigned i = 0; i < num_vals; ++i) { unsigned idx = m_rand(num_bits); unsigned val = m_rand(2); diff --git a/src/test/uint_set.cpp b/src/test/uint_set.cpp index fcbbd5c48..3134ada7b 100644 --- a/src/test/uint_set.cpp +++ b/src/test/uint_set.cpp @@ -44,91 +44,91 @@ static void tst1(unsigned n) { s2[idx] = false; s1.remove(idx); } - SASSERT(s1.num_elems() == size); - SASSERT((size == 0) == s1.empty()); + ENSURE(s1.num_elems() == size); + ENSURE((size == 0) == s1.empty()); for (unsigned idx = 0; idx < n; idx++) { - SASSERT(s2[idx] == s1.contains(idx)); + ENSURE(s2[idx] == s1.contains(idx)); } } } static void tst2(unsigned n) { uint_set s; - SASSERT(s.empty()); + ENSURE(s.empty()); unsigned val = rand()%n; s.insert(val); - SASSERT(!s.empty()); - SASSERT(s.num_elems() == 1); + ENSURE(!s.empty()); + ENSURE(s.num_elems() == 1); for (unsigned i = 0; i < 100; i++) { unsigned val2 = rand()%n; if (val != val2) { - SASSERT(!s.contains(val2)); + ENSURE(!s.contains(val2)); } } s.remove(val); - SASSERT(s.num_elems() == 0); - SASSERT(s.empty()); + ENSURE(s.num_elems() == 0); + ENSURE(s.empty()); } static void tst3(unsigned n) { - SASSERT(n > 10); + ENSURE(n > 10); uint_set s1; uint_set s2; - SASSERT(s1 == s2); + ENSURE(s1 == s2); s1.insert(3); - SASSERT(s1.num_elems() == 1); - SASSERT(s2.num_elems() == 0); - SASSERT(s1 != s2); + ENSURE(s1.num_elems() == 1); + ENSURE(s2.num_elems() == 0); + ENSURE(s1 != s2); s2.insert(5); - SASSERT(s2.num_elems() == 1); - SASSERT(s1 != s2); - SASSERT(!s1.subset_of(s2)); + ENSURE(s2.num_elems() == 1); + ENSURE(s1 != s2); + ENSURE(!s1.subset_of(s2)); s2 |= s1; - SASSERT(s1.subset_of(s2)); - SASSERT(s2.num_elems() == 2); - SASSERT(s1 != s2); + ENSURE(s1.subset_of(s2)); + ENSURE(s2.num_elems() == 2); + ENSURE(s1 != s2); s1 |= s2; - SASSERT(s1.subset_of(s2)); - SASSERT(s2.subset_of(s1)); - SASSERT(s1.num_elems() == 2); - SASSERT(s2.num_elems() == 2); - SASSERT(s1 == s2); + ENSURE(s1.subset_of(s2)); + ENSURE(s2.subset_of(s1)); + ENSURE(s1.num_elems() == 2); + ENSURE(s2.num_elems() == 2); + ENSURE(s1 == s2); s1.insert(9); - SASSERT(s1.num_elems() == 3); - SASSERT(s2.num_elems() == 2); + ENSURE(s1.num_elems() == 3); + ENSURE(s2.num_elems() == 2); s1.insert(9); - SASSERT(s1.num_elems() == 3); - SASSERT(s2.num_elems() == 2); - SASSERT(s2.subset_of(s1)); - SASSERT(!s1.subset_of(s2)); - SASSERT(s1 != s2); + ENSURE(s1.num_elems() == 3); + ENSURE(s2.num_elems() == 2); + ENSURE(s2.subset_of(s1)); + ENSURE(!s1.subset_of(s2)); + ENSURE(s1 != s2); uint_set s3(s1); - SASSERT(s1 == s3); - SASSERT(s1.subset_of(s3)); - SASSERT(s3.subset_of(s1)); - SASSERT(s2 != s3); + ENSURE(s1 == s3); + ENSURE(s1.subset_of(s3)); + ENSURE(s3.subset_of(s1)); + ENSURE(s2 != s3); uint_set s4(s2); - SASSERT(s2 == s4); - SASSERT(s2.subset_of(s4)); - SASSERT(s4.subset_of(s2)); - SASSERT(s2 != s3); + ENSURE(s2 == s4); + ENSURE(s2.subset_of(s4)); + ENSURE(s4.subset_of(s2)); + ENSURE(s2 != s3); for (unsigned i = 0; i < n; i++) { uint_set s5; s5.insert(i); - SASSERT(s1.contains(i) == s5.subset_of(s1)); + ENSURE(s1.contains(i) == s5.subset_of(s1)); } } static void tst4() { uint_set s; s.insert(32); - SASSERT(s.contains(32)); - SASSERT(!s.contains(31)); - SASSERT(!s.contains(0)); + ENSURE(s.contains(32)); + ENSURE(!s.contains(31)); + ENSURE(!s.contains(0)); s.remove(32); - SASSERT(!s.contains(32)); - SASSERT(!s.contains(31)); - SASSERT(!s.contains(0)); + ENSURE(!s.contains(32)); + ENSURE(!s.contains(31)); + ENSURE(!s.contains(0)); } #include "map.h" diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index 43aefed99..4c8358b3a 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -101,10 +101,10 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana std::cout << "num. roots: " << roots.size() + lowers.size() << "\n"; std::cout << "sign var(-oo): " << um.sign_variations_at_minus_inf(sseq) << "\n"; std::cout << "sign var(+oo): " << um.sign_variations_at_plus_inf(sseq) << "\n"; - SASSERT(roots.size() + lowers.size() == um.sign_variations_at_minus_inf(sseq) - um.sign_variations_at_plus_inf(sseq)); + ENSURE(roots.size() + lowers.size() == um.sign_variations_at_minus_inf(sseq) - um.sign_variations_at_plus_inf(sseq)); std::cout << "roots:"; for (unsigned i = 0; i < roots.size(); i++) { - SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), roots[i]) == 0); + ENSURE(um.eval_sign_at(q.size(), q.c_ptr(), roots[i]) == 0); std::cout << " "; bqm.display_decimal(std::cout, roots[i], prec); } { @@ -118,7 +118,7 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana bqm.display_decimal(std::cout, uppers[i], prec); std::cout << ")"; // Check interval with Sturm sequence. Small detail: Sturm sequence is for close intervals. - SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || + ENSURE(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || um.sign_variations_at(sseq, lowers[i]) - um.sign_variations_at(sseq, uppers[i]) == 1); // Fourier sequence may also be used to check if the interval is isolating @@ -155,7 +155,7 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec = 5) { } static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, mpbq_vector const & uppers, unsigned expected_sz, rational const * expected_roots) { - SASSERT(expected_sz == roots.size() + lowers.size()); + ENSURE(expected_sz == roots.size() + lowers.size()); svector visited; visited.resize(expected_sz, false); for (unsigned i = 0; i < expected_sz; i++) { @@ -163,7 +163,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m bool found = false; for (unsigned j = 0; j < roots.size(); j++) { if (to_rational(roots[j]) == r) { - SASSERT(!visited[j]); + ENSURE(!visited[j]); VERIFY(!found); found = true; visited[j] = true; @@ -173,12 +173,12 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m unsigned j_prime = j + roots.size(); if (to_rational(lowers[j]) < r && r < to_rational(uppers[j])) { VERIFY(!found); - SASSERT(!visited[j_prime]); + ENSURE(!visited[j_prime]); found = true; visited[j_prime] = true; } } - SASSERT(found); + ENSURE(found); } } @@ -292,21 +292,21 @@ static void tst_remove_one_half() { upolynomial::scoped_numeral_vector _p(um), _q(um), _r(um); um.to_numeral_vector(p, _p); um.to_numeral_vector(r, _r); - SASSERT(um.has_one_half_root(_p.size(), _p.c_ptr())); + ENSURE(um.has_one_half_root(_p.size(), _p.c_ptr())); um.remove_one_half_root(_p.size(), _p.c_ptr(), _q); - SASSERT(!um.has_one_half_root(_q.size(), _q.c_ptr())); + ENSURE(!um.has_one_half_root(_q.size(), _q.c_ptr())); std::cout << "_p: "; um.display(std::cout, _p); std::cout << "\n"; std::cout << "_r: "; um.display(std::cout, _r); std::cout << "\n"; std::cout << "_q: "; um.display(std::cout, _q); std::cout << "\n"; - SASSERT(um.eq(_q, _r)); + ENSURE(um.eq(_q, _r)); p = (((x^5) - 1000000000)^3)*((3*x - 10000000)^2)*((10*x - 632)^2); um.to_numeral_vector(p, _p); - SASSERT(!um.has_one_half_root(_p.size(), _p.c_ptr())); + ENSURE(!um.has_one_half_root(_p.size(), _p.c_ptr())); p = (x - 2)*(x - 4)*(x - 8)*(x - 16)*(x - 32)*(x - 64)*(2*x - 1)*(4*x - 1)*(8*x - 1)*(16*x - 1)*(32*x - 1); um.to_numeral_vector(p, _p); - SASSERT(um.has_one_half_root(_p.size(), _p.c_ptr())); + ENSURE(um.has_one_half_root(_p.size(), _p.c_ptr())); } template @@ -503,7 +503,7 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a } else { std::cout << "new root: " << bqm.to_string(a) << "\n"; - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), a) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), a) == 0); } } @@ -608,13 +608,13 @@ static void tst_translate_q() { upolynomial::manager um(rl, nm); upolynomial::scoped_numeral_vector _p(um), _q(um); um.to_numeral_vector(p, _p); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(1)) == 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(2)) == 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(3)) == 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(4)) == 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(-1)) != 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(5)) != 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(-2)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(1)) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(2)) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(3)) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(4)) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(-1)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(5)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(-2)) != 0); scoped_mpq c(nm); nm.set(c, 1, 3); scoped_mpq r1(nm); @@ -623,32 +623,32 @@ static void tst_translate_q() { scoped_mpq r2(nm); r2 = 3; r2 -= c; - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), r1) != 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), r2) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), r1) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), r2) != 0); std::cout << "p: "; um.display(std::cout, _p); std::cout << "\n"; um.translate_q(_p.size(), _p.c_ptr(), c, _q); std::cout << "q: "; um.display(std::cout, _q); std::cout << "\n"; - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(1)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(2)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(3)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(4)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(-1)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(5)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(-2)) != 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), r1) == 0); - SASSERT(um.eval_sign_at(_q.size(), _q.c_ptr(), r2) == 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(1)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(2)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(3)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(4)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(-1)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(5)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), mpq(-2)) != 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), r1) == 0); + ENSURE(um.eval_sign_at(_q.size(), _q.c_ptr(), r2) == 0); um.p_1_div_x(_p.size(), _p.c_ptr()); std::cout << "p: "; um.display(std::cout, _p); std::cout << "\n"; - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(1)) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(1)) == 0); nm.set(c, 1, 2); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); nm.set(c, 1, 3); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); nm.set(c, 1, 4); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(2)) != 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(3)) != 0); - SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(4)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), c) == 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(2)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(3)) != 0); + ENSURE(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(4)) != 0); } static void tst_convert_q2bq(unsynch_mpq_manager & m, polynomial_ref const & p, mpq const & a, mpq const & b) { @@ -848,9 +848,9 @@ static void tst_exact_div(polynomial_ref const & p1, polynomial_ref const & p2, std::cout << "expected: "; um.display(std::cout, _q); std::cout << "\n"; } std::cout.flush(); - SASSERT(res == expected); - SASSERT(expected == um.divides(_p1.size(), _p1.c_ptr(), _p2.size(), _p2.c_ptr())); - SASSERT(!expected || um.eq(_r, _q)); + ENSURE(res == expected); + ENSURE(expected == um.divides(_p1.size(), _p1.c_ptr(), _p2.size(), _p2.c_ptr())); + ENSURE(!expected || um.eq(_r, _q)); } static void tst_exact_div() { @@ -878,7 +878,7 @@ static void tst_exact_div() { } static void tst_fact(polynomial_ref const & p, unsigned num_distinct_factors, upolynomial::factor_params const & params = upolynomial::factor_params()) { - SASSERT(is_univariate(p)); + ENSURE(is_univariate(p)); std::cout << "---------------\n"; std::cout << "p: " << p << std::endl; reslimit rl; upolynomial::manager um(rl, p.m().m()); @@ -891,11 +891,11 @@ static void tst_fact(polynomial_ref const & p, unsigned num_distinct_factors, up for (unsigned i = 0; i < fs.distinct_factors(); i++) { std::cout << "*("; um.display(std::cout, fs[i]); std::cout << ")^" << fs.get_degree(i) << std::endl; } - SASSERT(fs.distinct_factors() == num_distinct_factors); + ENSURE(fs.distinct_factors() == num_distinct_factors); upolynomial::scoped_numeral_vector _r(um); fs.multiply(_r); TRACE("upolynomial", tout << "_r: "; um.display(tout, _r); tout << "\n_p: "; um.display(tout, _p); tout << "\n";); - SASSERT(um.eq(_p, _r)); + ENSURE(um.eq(_p, _r)); } static void tst_fact() { @@ -992,8 +992,8 @@ static void tst_fact() { } static void tst_rem(polynomial_ref const & p, polynomial_ref const & q, polynomial_ref const & expected) { - SASSERT(is_univariate(p)); - SASSERT(is_univariate(q)); + ENSURE(is_univariate(p)); + ENSURE(is_univariate(q)); std::cout << "---------------\n"; std::cout << "p: " << p << std::endl; std::cout << "q: " << q << std::endl; @@ -1005,7 +1005,7 @@ static void tst_rem(polynomial_ref const & p, polynomial_ref const & q, polynomi polynomial_ref r(p.m()); r = p.m().to_polynomial(_r.size(), _r.c_ptr(), 0); std::cout << "r: " << r << std::endl; - SASSERT(eq(expected, r)); + ENSURE(eq(expected, r)); } static void tst_rem() { @@ -1022,7 +1022,7 @@ static void tst_rem() { } static void tst_lower_bound(polynomial_ref const & p) { - SASSERT(is_univariate(p)); + ENSURE(is_univariate(p)); std::cout << "---------------\n"; std::cout << "p: " << p << std::endl; reslimit rl; upolynomial::manager um(rl, p.m().m()); diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp index e82c09218..f90292d11 100644 --- a/src/test/var_subst.cpp +++ b/src/test/var_subst.cpp @@ -87,7 +87,7 @@ void tst_subst(ast_manager& m) { std::cout << mk_pp(e2, m) << "\n"; std::cout << mk_pp(e3, m) << "\n"; std::cout << mk_pp(t1, m) << "\n"; - SASSERT(e3.get() == t1.get()); + ENSURE(e3.get() == t1.get()); // replace #2 -> #3, #3 -> #2 e2 = m.mk_forall(2, ss, names, e1); @@ -95,7 +95,7 @@ void tst_subst(ast_manager& m) { std::cout << mk_pp(e2, m) << "\n"; std::cout << mk_pp(e3, m) << "\n"; std::cout << mk_pp(t2, m) << "\n"; - SASSERT(e3.get() == t2.get()); + ENSURE(e3.get() == t2.get()); } diff --git a/src/test/vector.cpp b/src/test/vector.cpp index 86ae997ca..f7d70a87b 100644 --- a/src/test/vector.cpp +++ b/src/test/vector.cpp @@ -20,28 +20,28 @@ Revision History: static void tst1() { svector v1; - SASSERT(v1.empty()); + ENSURE(v1.empty()); for (unsigned i = 0; i < 1000; i++) { v1.push_back(i + 3); - SASSERT(static_cast(v1[i]) == i + 3); - SASSERT(v1.capacity() >= v1.size()); - SASSERT(!v1.empty()); + ENSURE(static_cast(v1[i]) == i + 3); + ENSURE(v1.capacity() >= v1.size()); + ENSURE(!v1.empty()); } for (unsigned i = 0; i < 1000; i++) { - SASSERT(static_cast(v1[i]) == i + 3); + ENSURE(static_cast(v1[i]) == i + 3); } svector::iterator it = v1.begin(); svector::iterator end = v1.end(); for (int i = 0; it != end; ++it, ++i) { - SASSERT(*it == i + 3); + ENSURE(*it == i + 3); } for (unsigned i = 0; i < 1000; i++) { - SASSERT(static_cast(v1.back()) == 1000 - i - 1 + 3); - SASSERT(v1.size() == 1000 - i); + ENSURE(static_cast(v1.back()) == 1000 - i - 1 + 3); + ENSURE(v1.size() == 1000 - i); v1.pop_back(); } - SASSERT(v1.empty()); - SASSERT(v1.size() == 0); + ENSURE(v1.empty()); + ENSURE(v1.size() == 0); unsigned i = 1000000000; while (true) { std::cout << "resize " << i << "\n"; diff --git a/src/util/debug.h b/src/util/debug.h index 6e295dcaa..ec0f600b5 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -79,14 +79,10 @@ bool is_debug_enabled(const char * tag); #define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) -#ifdef Z3DEBUG #define VERIFY(_x_) if (!(_x_)) { \ std::cerr << "Failed to verify: " << #_x_ << "\n"; \ UNREACHABLE(); \ } -#else -#define VERIFY(_x_) (void)(_x_) -#endif #define ENSURE(_x_) \ if (!(_x_)) { \