mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-07-28 20:24:35 +01:00
parent 0610392a05 27114ce9dd
commit a30c343d7a
87 changed files with 1422 additions and 1356 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
CMakeLists.txt
View file

@ -411,6 +411,38 @@ endif()
################################################################################
include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake)
################################################################################
# Control flow integrity
################################################################################
option(ENABLE_CFI "Enable control flow integrity checking" OFF)
if (ENABLE_CFI)
set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO")
if (NOT LINK_TIME_OPTIMIZATION)
message(FATAL_ERROR "Cannot enable control flow integrity checking without link-time optimization."
"You should set LINK_TIME_OPTIMIZATION to ON or ENABLE_CFI to OFF.")
endif()
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi configuration generator
message(STATUS "Note CFI is only enabled for the following configurations: ${build_types_with_cfi}")
# No need for else because this is the same as the set that LTO requires.
endif()
if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
z3_add_cxx_flag("/guard:cf" REQUIRED)
message(STATUS "Enabling CFI for MSVC")
foreach (_build_type ${build_types_with_cfi})
message(STATUS "Enabling CFI for MSVC")
string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /GUARD:CF")
string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /GUARD:CF")
endforeach()
else()
message(FATAL_ERROR "Can't enable control flow integrity for compiler \"${CMAKE_CXX_COMPILER_ID}\"."
"You should set ENABLE_CFI to OFF or use Clang or MSVC to compile.")
endif()
endif()
################################################################################
# MSVC specific flags inherited from old build system
################################################################################

2
README-CMake.md
View file

@ -265,6 +265,8 @@ The following useful options can be passed to CMake whilst configuring.
* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
* ``ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will
fail on other compilers. This requires LINK_TIME_OPTIMIZATION to also be enabled.
* ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.

7
cmake/msvc_legacy_quirks.cmake
View file

@ -184,7 +184,12 @@ foreach (_build_type ${_build_types_as_upper})
# Address space layout randomization
# See https://msdn.microsoft.com/en-us/library/bb384887.aspx
string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /DYNAMICBASE")
string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO")
if(ENABLE_CFI)
# CFI requires /DYNAMICBASE to be enabled.
string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE")
else()
string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO")
endif()
# FIXME: This is not necessary. This is MSVC's default.
# Indicate that the executable is compatible with DEP

4
contrib/ci/scripts/test_z3_unit_tests_cmake.sh
View file

@ -1,6 +1,7 @@
#!/bin/bash
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
. ${SCRIPT_DIR}/run_quiet.sh
set -x
set -e
@ -21,4 +22,5 @@ cd "${Z3_BUILD_DIR}"
# Build and run internal tests
cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
./test-z3
# Run all tests that don't require arguments
run_quiet ./test-z3 /a

40
scripts/update_api.py
View file

@ -321,16 +321,19 @@ def mk_py_wrappers():
core_py.write("def %s(" % name)
display_args(num)
core_py.write("):\n")
core_py.write(" _lib = lib()\n")
core_py.write(" if _lib.%s is None:\n" % name)
core_py.write(" return\n")
if result != VOID:
core_py.write(" r = lib().%s(" % name)
core_py.write(" r = _lib.%s(" % name)
else:
core_py.write(" lib().%s(" % name)
core_py.write(" _lib.%s(" % name)
display_args_to_z3(params)
core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT:
core_py.write(" err = lib().Z3_get_error_code(a0)\n")
core_py.write(" err = _lib.Z3_get_error_code(a0)\n")
core_py.write(" if err != Z3_OK:\n")
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg(a0, err))\n")
core_py.write(" raise Z3Exception(_lib.Z3_get_error_msg(a0, err))\n")
if result == STRING:
core_py.write(" return _to_pystr(r)\n")
elif result != VOID:
@ -765,11 +768,11 @@ def mk_log_macro(file, name, params):
cap = param_array_capacity_pos(p)
if cap not in auxs:
auxs.add(cap)
file.write("unsigned _Z3_UNUSED Z3ARG%s; " % cap)
file.write("unsigned _Z3_UNUSED Z3ARG%s = 0; " % cap)
sz = param_array_size_pos(p)
if sz not in auxs:
auxs.add(sz)
file.write("unsigned * _Z3_UNUSED Z3ARG%s; " % sz)
file.write("unsigned * _Z3_UNUSED Z3ARG%s = 0; " % sz)
file.write("%s _Z3_UNUSED Z3ARG%s; " % (param2str(p), i))
i = i + 1
file.write("if (_LOG_CTX.enabled()) { log_%s(" % name)
@ -1600,6 +1603,11 @@ def write_exe_c_preamble(exe_c):
#
exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
def write_core_py_post(core_py):
core_py.write("""
""")
def write_core_py_preamble(core_py):
core_py.write('# Automatically generated file\n')
core_py.write('import sys, os\n')
@ -1612,18 +1620,19 @@ def write_core_py_preamble(core_py):
_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
_lib = None
def lib():
global _lib
if _lib is None:
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
break
except:
pass
if _lib is None:
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
break
except:
pass
if _lib is None:
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
return _lib
def _to_ascii(s):
@ -1728,6 +1737,7 @@ def generate_files(api_files,
def_APIs(api_files)
mk_bindings(exe_c)
mk_py_wrappers()
write_core_py_post(core_py)
if mk_util.is_verbose():
print("Generated '{}'".format(log_h.name))

6
src/ast/arith_decl_plugin.cpp
View file

@ -403,6 +403,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
}
}
void arith_decl_plugin::check_arity(unsigned arity, unsigned expected_arity) {
if (arity != expected_arity) {
m_manager->raise_exception("invalid number of arguments passed to function");
}
}
inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
if (k == OP_SUB && arity == 1) {
return OP_UMINUS;

1
src/ast/arith_decl_plugin.h
View file

@ -157,6 +157,7 @@ protected:
func_decl * mk_func_decl(decl_kind k, bool is_real);
virtual void set_manager(ast_manager * m, family_id id);
decl_kind fix_kind(decl_kind k, unsigned arity);
void check_arity(unsigned arity, unsigned expected_arity);
func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
public:

5
src/ast/ast.cpp
View file

@ -2178,7 +2178,10 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
throw ast_exception(buffer.str().c_str());
}
app * r = 0;
if (num_args > 2 && !decl->is_flat_associative()) {
if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {
r = mk_true();
}
else if (num_args > 2 && !decl->is_flat_associative()) {
if (decl->is_right_associative()) {
unsigned j = num_args - 1;
r = mk_app_core(decl, args[j-1], args[j]);

6
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -106,7 +106,7 @@ class subst_cmd : public cmd {
public:
subst_cmd():cmd("dbg-subst") {}
virtual char const * get_usage() const { return "<symbol> (<symbol>*) <symbol>"; }
virtual char const * get_descr() const { return "substitute the free variables in the AST referenced by <symbol> using the ASTs referenced by <symbol>*"; }
virtual char const * get_descr(cmd_context & ctx) const { return "substitute the free variables in the AST referenced by <symbol> using the ASTs referenced by <symbol>*"; }
virtual unsigned get_arity() const { return 3; }
virtual void prepare(cmd_context & ctx) { m_idx = 0; m_source = 0; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
@ -285,7 +285,7 @@ protected:
public:
instantiate_cmd_core(char const * name):cmd(name) {}
virtual char const * get_usage() const { return "<quantifier> (<symbol>*)"; }
virtual char const * get_descr() const { return "instantiate the quantifier using the given expressions."; }
virtual char const * get_descr(cmd_context & ctx) const { return "instantiate the quantifier using the given expressions."; }
virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_q = 0; m_args.reset(); }
@ -333,7 +333,7 @@ class instantiate_nested_cmd : public instantiate_cmd_core {
public:
instantiate_nested_cmd():instantiate_cmd_core("dbg-instantiate-nested") {}
virtual char const * get_descr() const { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; }
virtual char const * get_descr(cmd_context & ctx) const { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; }
virtual void set_next_arg(cmd_context & ctx, expr * s) {
instantiate_cmd_core::set_next_arg(ctx, s);

12
src/cmd_context/interpolant_cmds.cpp
View file

@ -46,20 +46,14 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
ctx.regular_stream() << "(interpolants";
for(unsigned i = 0; i < interps.size(); i++){
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
s(to_expr(interps[i]),r,pr);
ctx.regular_stream() << mk_pp(r.get(), ctx.m()) << std::endl;
#if 0
ast_smt_pp pp(ctx.m());
pp.set_logic(ctx.get_logic().str().c_str());
pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
ctx.regular_stream() << std::endl;
#endif
ctx.regular_stream() << "\n " << r;
}
ctx.regular_stream() << ")\n";
s.cleanup();

3
src/cmd_context/tactic_cmds.cpp
View file

@ -308,6 +308,9 @@ public:
}
virtual void execute(cmd_context & ctx) {
if (!m_tactic) {
throw cmd_exception("apply needs a tactic argument");
}
params_ref p = ctx.params().merge_default_params(ps());
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{

11
src/math/simplex/model_based_opt.cpp
View file

@ -18,8 +18,9 @@ Revision History:
--*/
#include "model_based_opt.h"
#include "uint_set.h"
#include "math/simplex/model_based_opt.h"
#include "util/uint_set.h"
#include "util/z3_exception.h"
std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
switch (ie) {
@ -868,6 +869,9 @@ namespace opt {
for (unsigned i = 0; i < mod_rows.size(); ++i) {
D = lcm(D, m_rows[mod_rows[i]].m_mod);
}
if (D.is_zero()) {
throw default_exception("modulo 0 is not defined");
}
TRACE("opt", display(tout << "lcm: " << D << " tableau\n"););
rational val_x = m_var2value[x];
rational u = mod(val_x, D);
@ -954,7 +958,8 @@ namespace opt {
row& r1 = m_rows[row_id1];
vector<var> coeffs;
mk_coeffs_without(coeffs, r1.m_vars, x);
add_divides(coeffs, r1.m_coeff, abs(a));
rational c = r1.m_coeff;
add_divides(coeffs, c, abs(a));
}
unsigned_vector const& row_ids = m_var2row_ids[x];
uint_set visited;

15
src/muz/fp/dl_cmds.cpp
View file

@ -374,12 +374,9 @@ class dl_declare_rel_cmd : public cmd {
unsigned m_arg_idx;
mutable unsigned m_query_arg_idx;
symbol m_rel_name;
scoped_ptr<sort_ref_vector> m_domain;
ptr_vector<sort> m_domain;
svector<symbol> m_kinds;
void ensure_domain(cmd_context& ctx) {
if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
}
public:
dl_declare_rel_cmd(dl_context * dl_ctx):
@ -395,7 +392,7 @@ public:
ctx.m(); // ensure manager is initialized.
m_arg_idx = 0;
m_query_arg_idx = 0;
m_domain = 0;
m_domain.reset();
m_kinds.reset();
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
@ -406,8 +403,8 @@ public:
}
}
virtual void set_next_arg(cmd_context & ctx, unsigned num, sort * const * slist) {
ensure_domain(ctx);
m_domain->append(num, slist);
m_domain.reset();
m_domain.append(num, slist);
m_arg_idx++;
}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
@ -424,14 +421,12 @@ public:
if(m_arg_idx<2) {
throw cmd_exception("at least 2 arguments expected");
}
ensure_domain(ctx);
ast_manager& m = ctx.m();
func_decl_ref pred(
m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
m.mk_func_decl(m_rel_name, m_domain.size(), m_domain.c_ptr(), m.mk_bool_sort()), m);
ctx.insert(pred);
m_dl_ctx->register_predicate(pred, m_kinds.size(), m_kinds.c_ptr());
m_domain = 0;
}
};

7
src/parsers/smt2/smt2parser.cpp
View file

@ -1656,7 +1656,9 @@ namespace smt2 {
fr->m_in_decls = false;
SASSERT(symbol_stack().size() >= fr->m_sym_spos);
SASSERT(expr_stack().size() >= fr->m_expr_spos);
SASSERT(symbol_stack().size() - fr->m_sym_spos == expr_stack().size() - fr->m_expr_spos);
if (symbol_stack().size() - fr->m_sym_spos != expr_stack().size() - fr->m_expr_spos) {
throw parser_exception("malformed let expression");
}
unsigned num_decls = expr_stack().size() - fr->m_expr_spos;
symbol * sym_it = symbol_stack().c_ptr() + fr->m_sym_spos;
expr ** expr_it = expr_stack().c_ptr() + fr->m_expr_spos;
@ -2238,6 +2240,9 @@ namespace smt2 {
m_assert_expr = m_scanner.cached_str(0, m_cache_end);
m_scanner.stop_caching();
}
if (expr_stack().empty()) {
throw cmd_exception("invalid assert command, expression required as argument");
}
expr * f = expr_stack().back();
if (!m().is_bool(f))
throw cmd_exception("invalid assert command, term is not Boolean");

10
src/qe/qe_arith.cpp
View file

@ -90,8 +90,8 @@ namespace qe {
rational r1, r2;
expr_ref val1 = eval(e1);
expr_ref val2 = eval(e2);
VERIFY(a.is_numeral(val1, r1));
VERIFY(a.is_numeral(val2, r2));
if (!a.is_numeral(val1, r1)) return false;
if (!a.is_numeral(val2, r2)) return false;
SASSERT(r1 != r2);
if (r1 < r2) {
std::swap(e1, e2);
@ -107,7 +107,7 @@ namespace qe {
vector<std::pair<expr*,rational> > nums;
for (unsigned i = 0; i < alit->get_num_args(); ++i) {
val = eval(alit->get_arg(i));
VERIFY(a.is_numeral(val, r));
if (!a.is_numeral(val, r)) return false;
nums.push_back(std::make_pair(alit->get_arg(i), r));
}
std::sort(nums.begin(), nums.end(), compare_second());
@ -129,7 +129,7 @@ namespace qe {
expr* arg1 = to_app(lit)->get_arg(i), *arg2 = 0;
rational r;
expr_ref val = eval(arg1);
VERIFY(a.is_numeral(val, r));
if (!a.is_numeral(val, r)) return false;
if (values.find(r, arg2)) {
ty = opt::t_eq;
linearize(mbo, eval, mul, arg1, c, fmls, ts, tids);
@ -196,7 +196,7 @@ namespace qe {
linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
}
}
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1)) {
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
rational r;
val = eval(t);
VERIFY(a.is_numeral(val, r));

21
src/smt/smt_case_split_queue.cpp
View file

@ -51,9 +51,9 @@ namespace smt {
if (!m_theory_var_priority.find(v2, p_v2)) {
p_v2 = 0.0;
}
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
return p_v1 > p_v2;
}
};
@ -82,6 +82,7 @@ namespace smt {
virtual void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
SASSERT(!m_queue.contains(v));
m_queue.insert(v);
}
@ -130,10 +131,7 @@ namespace smt {
virtual void display(std::ostream & out) {
bool first = true;
bool_var_act_queue::const_iterator it = m_queue.begin();
bool_var_act_queue::const_iterator end = m_queue.end();
for (; it != end ; ++it) {
unsigned v = *it;
for (unsigned v : m_queue) {
if (m_context.get_assignment(v) == l_undef) {
if (first) {
out << "remaining case-splits:\n";
@ -143,8 +141,7 @@ namespace smt {
}
}
if (!first)
out << "\n";
out << "\n";
}
virtual ~act_case_split_queue() {};
@ -166,11 +163,15 @@ namespace smt {
act_case_split_queue::activity_increased_eh(v);
if (m_queue.contains(v))
m_queue.decreased(v);
if (m_delayed_queue.contains(v))
m_delayed_queue.decreased(v);
}
virtual void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
m_delayed_queue.reserve(v+1);
SASSERT(!m_delayed_queue.contains(v));
SASSERT(!m_queue.contains(v));
if (m_context.is_searching())
m_delayed_queue.insert(v);
else
@ -1099,8 +1100,6 @@ namespace smt {
#endif
GOAL_STOP();
//std::cout << "goal set, time " << m_goal_time.get_seconds() << "\n";
}
void set_global_generation()

1
src/smt/smt_context.cpp
View file

@ -1826,6 +1826,7 @@ namespace smt {
}
void context::rescale_bool_var_activity() {
TRACE("case_split", tout << "rescale\n";);
svector<double>::iterator it = m_activity.begin();
svector<double>::iterator end = m_activity.end();
for (; it != end; ++it)

1
src/smt/smt_context.h
View file

@ -1040,6 +1040,7 @@ namespace smt {
if (act > ACTIVITY_LIMIT)
rescale_bool_var_activity();
m_case_split_queue->activity_increased_eh(v);
TRACE("case_split", tout << "v" << v << " " << m_bvar_inc << " -> " << act << "\n";);
}
protected:

8
src/smt/theory_str.cpp
View file

@ -1549,14 +1549,12 @@ namespace smt {
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
assert_axiom(breakdownAssert);
SASSERT(breakdownAssert);
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
SASSERT(reduceToResult);
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
assert_axiom(reduceToResult);
}
void theory_str::instantiate_axiom_str_to_int(enode * e) {

24
src/test/algebraic.cpp
View file

@ -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<int> 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";

2
src/test/api.cpp
View file

@ -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);

2
src/test/arith_rewriter.cpp
View file

@ -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;
}

52
src/test/ast.cpp
View file

@ -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<numeral_ast> n1(m.mk_numeral(rational(2,3)), m);
// ast_ref<numeral_ast> n2(m.mk_numeral(rational(2,3)), m);
// SASSERT(n1 == n2);
// ENSURE(n1 == n2);
// ast_ref<numeral_ast> n3(m.mk_numeral(rational(1,2)), m);
// SASSERT(n1 != n3);
// ENSURE(n1 != n3);
// ast_ref<var_ast> v1 (m.mk_var(1), m);
// ast_ref<var_ast> v2 (m.mk_var(2), m);
// ast_ref<var_ast> 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<const_ast> foo_x(m.mk_const(foo_decl.get(), x.get()), m);
// ast_ref<const_ast> foo_foo_x(m.mk_const(foo_decl.get(), foo_x.get()), m);
// ast_ref<const_ast> 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);

96
src/test/bit_vector.cpp
View file

@ -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() {

14
src/test/bits.cpp
View file

@ -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<unsigned>(m.get_uint64(tmp)));
m.div(_dst, max, _dst);
}

18
src/test/buffer.cpp
View file

@ -24,22 +24,22 @@ template class ptr_scoped_buffer<point>;
static void tst1() {
ptr_scoped_buffer<point> 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));
}

22
src/test/bv_simplifier_plugin.cpp
View file

@ -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);

86
src/test/chashtable.cpp
View file

@ -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_hash, default_eq<int> > 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);
});
}

46
src/test/diff_logic.cpp
View file

@ -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<bool> 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;

10
src/test/dl_context.cpp
View file

@ -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
}

112
src/test/dl_product_relation.cpp
View file

@ -37,12 +37,12 @@ namespace datalog {
sparse_table_plugin & plugin =
static_cast<sparse_table_plugin &>(*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<table_transformer_fn> 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<table_transformer_fn> 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<table_transformer_fn> 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<table_join_fn> 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<relation_base> r2 = r1->clone();
scoped_rel<relation_base> 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<relation_union_fn> 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<relation_base> sr_2r = (*proj_2r)(*r31);
scoped_rel<relation_base> 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<relation_mutator_fn> 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));
}

12
src/test/dl_query.cpp
View file

@ -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: "<<found<<"\n";
@ -192,7 +192,7 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
query_lit = m.mk_app(v_pred, q_args.c_ptr());
is_sat = ctx.query(query_lit.get());
SASSERT(is_sat != l_false);
ENSURE(is_sat != l_false);
std::cerr<<"non-ground query finished\n";
if(ctx.result_contains_fact(ans_fact)!=found) {
std::cerr<<"wrong wpa answer!\n";

22
src/test/dl_relation.cpp
View file

@ -24,7 +24,7 @@ namespace datalog {
relation_manager & m = ctx.get_rel_context()->get_rmanager();
m.register_plugin(alloc(interval_relation_plugin, m));
interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*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<bound_relation_plugin&>(*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);

10
src/test/dl_table.cpp
View file

@ -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);

12
src/test/dl_util.cpp
View file

@ -22,7 +22,7 @@ void dl_util_two_array_sort() {
datalog::sort_two_arrays(num, a1, a2);
for(unsigned i=0; i<num; i++) {
SASSERT(a2[i]==i+3);
ENSURE(a2[i]==i+3);
}
}
@ -32,10 +32,10 @@ void dl_util_cycle_from_permutation() {
unsigned_vector cycle;
datalog::cycle_from_permutation(perm, cycle);
SASSERT(cycle.size()==2);
SASSERT(cycle[0]==2 || cycle[0]==4);
SASSERT(cycle[1]==2 || cycle[1]==4);
SASSERT((cycle[0]==2) == (cycle[1]==4));
ENSURE(cycle.size()==2);
ENSURE(cycle[0]==2 || cycle[0]==4);
ENSURE(cycle[1]==2 || cycle[1]==4);
ENSURE((cycle[0]==2) == (cycle[1]==4));
unsigned permutation_arr2[] = { 1, 2, 3, 4, 5, 6, 7, 0 };
unsigned len2 = sizeof(permutation_arr2)/sizeof(unsigned);
@ -44,7 +44,7 @@ void dl_util_cycle_from_permutation() {
datalog::cycle_from_permutation(perm2, cycle);
for(unsigned i=0; i<len2; i++) {
SASSERT( (cycle[i]+1)%len2==cycle[(i+1)%len2] );
ENSURE( (cycle[i]+1)%len2==cycle[(i+1)%len2] );
}
}

48
src/test/doc.cpp
View file

@ -36,41 +36,41 @@ static void tst_doc1(unsigned n) {
m.display(std::cout, *d20) << "\n";
if (n < 64) {
unsigned hi = 3, lo = 1;
SASSERT(hi <= n);
ENSURE(hi <= n);
doc_ref d111X(m, m.allocate(0xFF, hi, lo));
}
m.copy(*d, *d10);
SASSERT(m.equals(*d, *d10));
ENSURE(m.equals(*d, *d10));
m.reset(*d);
SASSERT(!m.equals(*d, *d10));
ENSURE(!m.equals(*d, *d10));
m.fill0(*d10);
SASSERT(m.equals(*d, *d10));
ENSURE(m.equals(*d, *d10));
m.fill1(*d);
d10 = m.allocate(10);
SASSERT(!m.equals(*d, *d10));
SASSERT(m.equals(*d, *d1));
ENSURE(!m.equals(*d, *d10));
ENSURE(m.equals(*d, *d1));
m.fillX(*d);
SASSERT(m.equals(*d, *dX));
SASSERT(m.is_full(*dX));
SASSERT(!m.is_full(*d1));
ENSURE(m.equals(*d, *dX));
ENSURE(m.is_full(*dX));
ENSURE(!m.is_full(*d1));
VERIFY(m.set_and(*dX,*dX));
SASSERT(m.equals(*dXc,*dX));
ENSURE(m.equals(*dXc,*dX));
VERIFY(m.set_and(*dX,*d1));
SASSERT(!m.equals(*dXc,*dX));
SASSERT(m.equals(*dX,*d1));
ENSURE(!m.equals(*dXc,*dX));
ENSURE(m.equals(*dX,*d1));
VERIFY(m.fold_neg(*dX));
ptr_vector<doc> 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);

58
src/test/ext_numeral.cpp
View file

@ -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");
}
}

28
src/test/fixed_bit_vector.cpp
View file

@ -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);

2
src/test/get_consequences.cpp
View file

@ -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);
}

44
src/test/get_implied_equalities.cpp
View file

@ -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);

38
src/test/hashtable.cpp
View file

@ -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_hash_proc, default_eq<int> > 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() {

22
src/test/heap.cpp
View file

@ -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<lt_proc2> 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() {

4
src/test/hilbert_basis.cpp
View file

@ -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<int>(bound);
for (unsigned i = 0; i < num_ineqs; ++i) {
vector<rational> nv;

22
src/test/hwf.cpp
View file

@ -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() {

124
src/test/inf_rational.cpp
View file

@ -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)));
}

2
src/test/interval.cpp
View file

@ -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);
}

2
src/test/karr.cpp
View file

@ -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<rational> zeros;
for (unsigned i = 0; i < src.A[0].size(); ++i) {
zeros.push_back(rational(0));

8
src/test/list.cpp
View file

@ -27,10 +27,10 @@ static void tst1() {
list<int> * l2 = new (r) list<int>(20, l1);
list<int> * l3 = new (r) list<int>(30);
list<int> * l4 = new (r) list<int>(40, l3);
SASSERT(append(r, l1, static_cast<list<int> *>(0)) == l1);
SASSERT(append(r, l2, static_cast<list<int> *>(0)) == l2);
SASSERT(append(r, static_cast<list<int> *>(0), l2) == l2);
SASSERT(append(r, static_cast<list<int> *>(0), static_cast<list<int> *>(0)) == 0);
ENSURE(append(r, l1, static_cast<list<int> *>(0)) == l1);
ENSURE(append(r, l2, static_cast<list<int> *>(0)) == l2);
ENSURE(append(r, static_cast<list<int> *>(0), l2) == l2);
ENSURE(append(r, static_cast<list<int> *>(0), static_cast<list<int> *>(0)) == 0);
TRACE("list", display(tout, l2->begin(), l2->end()); tout << "\n";);
list<int> * l5 = append(r, l4, l2);
TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";);

28
src/test/map.cpp
View file

@ -22,22 +22,22 @@ Revision History:
static void tst1() {
map<char const *, int, str_hash_proc, str_eq_proc> 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() {

38
src/test/mpf.cpp
View file

@ -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() {

240
src/test/mpff.cpp
View file

@ -77,10 +77,10 @@ static void tst5() {
scoped_mpff a(m), b(m);
m.set(a, static_cast<uint64>(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>(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>(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>(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<uint64>(rand()) << 32) + static_cast<uint64>(rand());
fm.set(a, v);
SASSERT(fm.is_uint64(a));
ENSURE(fm.is_uint64(a));
v = (static_cast<uint64>(rand() % 3) << 32) + static_cast<uint64>(rand());
fm.set(a, v);
SASSERT(fm.is_uint64(a));
ENSURE(fm.is_uint64(a));
}
{
int64 v = (static_cast<uint64>(rand() % INT_MAX) << 32) + static_cast<uint64>(rand());
if (rand()%2 == 0)
v = -v;
fm.set(a, v);
SASSERT(fm.is_int64(a));
ENSURE(fm.is_int64(a));
v = (static_cast<uint64>(rand() % 3) << 32) + static_cast<uint64>(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,138 @@ 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<uint64>(UINT_MAX) + 1);
ENSURE(m.is_power_of_two(a, k) && k == 32);
ENSURE(m.get_uint64(a) == static_cast<uint64>(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 +436,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 +547,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 +571,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() {

2
src/test/mpfx.cpp
View file

@ -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() {

34
src/test/mpq.cpp
View file

@ -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() {

50
src/test/mpz.cpp
View file

@ -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() {

36
src/test/nlsat.cpp
View file

@ -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";

8
src/test/no_overflow.cpp
View file

@ -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);

10
src/test/object_allocator.cpp
View file

@ -62,12 +62,12 @@ static void tst1() {
cell * c3 = m.allocate<true>();
(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<true>();
else
c = m2.allocate<true>();
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);
}

166
src/test/old_interval.cpp
View file

@ -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() {

26
src/test/optional.cpp
View file

@ -22,11 +22,11 @@ Revision History:
static void tst1() {
optional<int> 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<OptFoo> 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<int *> 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() {

66
src/test/parray.cpp
View file

@ -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<unsigned>(m.get(a1, i)) == i);
ENSURE(static_cast<unsigned>(m.get(a1, i)) == i);
}
for (unsigned i = 0; i < m.size(a2); i++) {
SASSERT(static_cast<unsigned>(m.get(a2, i)) == i);
ENSURE(static_cast<unsigned>(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<unsigned>(m.get(a2, i)) == i+1);
ENSURE(static_cast<unsigned>(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<unsigned>(m.get(a1, i)) == i);
SASSERT(static_cast<unsigned>(m.get(a2, i)) == i+1);
SASSERT(i >= 18 || static_cast<unsigned>(m.get(a4, i)) == i+1);
SASSERT(i >= 6 || static_cast<unsigned>(m.get(a3, i)) == i+1);
SASSERT(!(6 <= i && i <= 17) || static_cast<unsigned>(m.get(a3, i)) == i);
ENSURE(static_cast<unsigned>(m.get(a1, i)) == i);
ENSURE(static_cast<unsigned>(m.get(a2, i)) == i+1);
ENSURE(i >= 18 || static_cast<unsigned>(m.get(a4, i)) == i+1);
ENSURE(i >= 6 || static_cast<unsigned>(m.get(a3, i)) == i+1);
ENSURE(!(6 <= i && i <= 17) || static_cast<unsigned>(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";

4
src/test/pb2bv.cpp
View file

@ -81,7 +81,7 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<r
}
std::cout << fml1 << " " << fml2 << "\n";
th_rw(fml2, result2, proof);
SASSERT(m.is_true(result2) || m.is_false(result2));
ENSURE(m.is_true(result2) || m.is_false(result2));
lbool res = solver.check();
VERIFY(res == l_true);
solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
@ -150,7 +150,7 @@ static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, v
}
std::cout << fml1 << " " << fml2 << "\n";
th_rw(fml2, result2, proof);
SASSERT(m.is_true(result2) || m.is_false(result2));
ENSURE(m.is_true(result2) || m.is_false(result2));
lbool res = slv->check_sat(0,0);
VERIFY(res == l_true);
slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());

2
src/test/permutation.cpp
View file

@ -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
}

136
src/test/polynomial.cpp
View file

@ -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() {

10
src/test/polynorm.cpp
View file

@ -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'
}

2
src/test/prime_generator.cpp
View file

@ -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;

2
src/test/qe_arith.cpp
View file

@ -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;
}

6
src/test/quant_solve.cpp
View file

@ -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;
}

326
src/test/rational.cpp
View file

@ -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));
}

8
src/test/rcf.cpp
View file

@ -116,13 +116,13 @@ static void tst_solve(unsigned n, int _A[], int _b[], int _c[], bool solved) {
svector<int> 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]);
}
}

2
src/test/sat_user_scope.cpp
View file

@ -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() {

2
src/test/simplex.cpp
View file

@ -84,7 +84,7 @@ void add_row(Simplex& S, vector<R> 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);

22
src/test/simplifier.cpp
View file

@ -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) {

22
src/test/sorting_network.cpp
View file

@ -57,7 +57,7 @@ struct unsigned_ext {
static void is_sorted(svector<unsigned> 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);
}

12
src/test/stack.cpp
View file

@ -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<int*>(ptr));
s.deallocate(p2);
s.deallocate(p1);
@ -38,8 +38,8 @@ static void tst2(unsigned num, unsigned del_rate) {
ptr_vector<char> 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();
}

6
src/test/string_buffer.cpp
View file

@ -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() {

46
src/test/symbol.cpp
View file

@ -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() {

22
src/test/symbol_table.cpp
View file

@ -21,24 +21,22 @@ Revision History:
static void tst1() {
symbol_table<int> 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")));
#ifdef Z3DEBUG
ENSURE(t.contains(symbol("boo")));
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() {

24
src/test/tbv.cpp
View file

@ -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));
}
}

4
src/test/theory_pb.cpp
View file

@ -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());

28
src/test/total_order.cpp
View file

@ -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 << "*";

16
src/test/udoc_relation.cpp
View file

@ -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<udoc_relation*>(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);

94
src/test/uint_set.cpp
View file

@ -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"

96
src/test/upolynomial.cpp
View file

@ -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<bool> 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<typename pmanager>
@ -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());

4
src/test/var_subst.cpp
View file

@ -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());
}

20
src/test/vector.cpp
View file

@ -20,28 +20,28 @@ Revision History:
static void tst1() {
svector<int> v1;
SASSERT(v1.empty());
ENSURE(v1.empty());
for (unsigned i = 0; i < 1000; i++) {
v1.push_back(i + 3);
SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
SASSERT(v1.capacity() >= v1.size());
SASSERT(!v1.empty());
ENSURE(static_cast<unsigned>(v1[i]) == i + 3);
ENSURE(v1.capacity() >= v1.size());
ENSURE(!v1.empty());
}
for (unsigned i = 0; i < 1000; i++) {
SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
ENSURE(static_cast<unsigned>(v1[i]) == i + 3);
}
svector<int>::iterator it = v1.begin();
svector<int>::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<unsigned>(v1.back()) == 1000 - i - 1 + 3);
SASSERT(v1.size() == 1000 - i);
ENSURE(static_cast<unsigned>(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";

4
src/util/debug.h
View file

@ -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_)) { \

20
src/util/heap.h
View file

@ -43,7 +43,15 @@ class heap : private LT {
return i >> 1;
}
#ifdef Z3DEBUG
void display(std::ostream& out, unsigned indent, int idx) const {
if (idx < static_cast<int>(m_values.size())) {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << m_values[idx] << "\n";
display(out, indent + 1, left(idx));
display(out, indent + 1, right(idx));
}
}
// Return true if the value can be inserted in the heap. That is, the vector m_value2indices is big enough to store this value.
bool is_valid_value(int v) const {
SASSERT(v >= 0 && v < static_cast<int>(m_value2indices.size()));
@ -59,11 +67,13 @@ class heap : private LT {
}
return true;
}
public:
bool check_invariant() const {
return check_invariant_core(1);
}
#endif
private:
void move_up(int idx) {
@ -219,6 +229,7 @@ public:
void insert(int val) {
CASSERT("heap", check_invariant());
CASSERT("heap", !contains(val));
SASSERT(is_valid_value(val));
int idx = static_cast<int>(m_values.size());
m_value2indices[val] = idx;
@ -272,6 +283,11 @@ public:
}
}
}
void display(std::ostream& out) const {
display(out, 0, 1);
}
};