mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 03:25:43 +00:00
test: replace SASSERT with ENSURE, remove Windows-only guards (#10086)
Unit tests relied on `SASSERT()` which is a no-op in release builds (`DEBUG_CODE` wrapper), silently skipping all assertions outside debug mode. Several test files were also gated behind `#ifdef _WINDOWS`, making them dead code on Linux/macOS CI. ## Changes - **`SASSERT` → `ENSURE` in 20 test files (200 occurrences)**: `ENSURE` maps to `VERIFY` and always executes regardless of build type, ensuring test assertions are active in both debug and release builds. - **`src/test/diff_logic.cpp`**: Removed `#ifdef _WINDOWS` wrapping the entire file. No Windows-specific APIs were used; the guard only prevented compilation on non-Windows platforms. - **`src/test/dl_product_relation.cpp`**: Removed `#ifdef _WINDOWS` guard around `tst_dl_product_relation()`. The function body has no platform dependencies. - **`src/test/sat_local_search.cpp`**: Replaced `sscanf_s` (MSVC-specific) with portable `sscanf`; added return-value check to detect malformed input. Previously, `build_instance()` unconditionally returned `false` on non-Windows, making the SAT local search test a no-op on Linux/macOS. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot
GitHub
parent
b0a77d2a58
commit
c4b0fe33bc
23 changed files with 205 additions and 219 deletions
|
|
@ -45,7 +45,7 @@ void display(std::ostream & out, expr_ref_vector & r, bool ll=true) {
|
|||
}
|
||||
|
||||
static unsigned to_int(model_core & mdl, expr_ref_vector & out) {
|
||||
SASSERT(out.size() <= sizeof(unsigned) * 8);
|
||||
ENSURE(out.size() <= sizeof(unsigned) * 8);
|
||||
ast_manager & m = mdl.get_manager();
|
||||
model_evaluator eval(mdl);
|
||||
expr_ref bit(m);
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifdef _WINDOWS
|
||||
#include "util/rational.h"
|
||||
#include "smt/diff_logic.h"
|
||||
#include "smt/smt_literal.h"
|
||||
|
|
@ -169,7 +168,3 @@ void tst_diff_logic() {
|
|||
//tst2();
|
||||
//tst3();
|
||||
}
|
||||
#else
|
||||
void tst_diff_logic() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -351,7 +351,6 @@ namespace datalog {
|
|||
|
||||
using namespace datalog;
|
||||
|
||||
#ifdef _WINDOWS
|
||||
void tst_dl_product_relation() {
|
||||
smt_params fparams;
|
||||
params_ref params;
|
||||
|
|
@ -362,7 +361,3 @@ void tst_dl_product_relation() {
|
|||
test_finite_product_relation(fparams, params);
|
||||
|
||||
}
|
||||
#else
|
||||
void tst_dl_product_relation() {}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -30,28 +30,28 @@ public:
|
|||
// Test the prev() method
|
||||
void test_prev() {
|
||||
TestNode node(1);
|
||||
SASSERT(node.prev() == &node);
|
||||
ENSURE(node.prev() == &node);
|
||||
std::cout << "test_prev passed." << std::endl;
|
||||
}
|
||||
|
||||
// Test the next() method
|
||||
static void test_next() {
|
||||
TestNode node(1);
|
||||
SASSERT(node.next() == &node);
|
||||
ENSURE(node.next() == &node);
|
||||
std::cout << "test_next passed." << std::endl;
|
||||
}
|
||||
|
||||
// Test the const prev() method
|
||||
static void test_const_prev() {
|
||||
const TestNode node(1);
|
||||
SASSERT(node.prev() == &node);
|
||||
ENSURE(node.prev() == &node);
|
||||
std::cout << "test_const_prev passed." << std::endl;
|
||||
}
|
||||
|
||||
// Test the const next() method
|
||||
static void test_const_next() {
|
||||
const TestNode node(1);
|
||||
SASSERT(node.next() == &node);
|
||||
ENSURE(node.next() == &node);
|
||||
std::cout << "test_const_next passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -59,9 +59,9 @@ static void test_const_next() {
|
|||
static void test_init() {
|
||||
TestNode node(1);
|
||||
node.init(&node);
|
||||
SASSERT(node.next() == &node);
|
||||
SASSERT(node.prev() == &node);
|
||||
SASSERT(node.invariant());
|
||||
ENSURE(node.next() == &node);
|
||||
ENSURE(node.prev() == &node);
|
||||
ENSURE(node.invariant());
|
||||
std::cout << "test_init passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -71,10 +71,10 @@ static void test_pop() {
|
|||
TestNode node1(1);
|
||||
TestNode::push_to_front(list, &node1);
|
||||
[[maybe_unused]] TestNode* popped = TestNode::pop(list);
|
||||
SASSERT(popped == &node1);
|
||||
SASSERT(list == nullptr);
|
||||
SASSERT(popped->next() == popped);
|
||||
SASSERT(popped->prev() == popped);
|
||||
ENSURE(popped == &node1);
|
||||
ENSURE(list == nullptr);
|
||||
ENSURE(popped->next() == popped);
|
||||
ENSURE(popped->prev() == popped);
|
||||
std::cout << "test_pop passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -83,12 +83,12 @@ static void test_insert_after() {
|
|||
TestNode node1(1);
|
||||
TestNode node2(2);
|
||||
node1.insert_after(&node2);
|
||||
SASSERT(node1.next() == &node2);
|
||||
SASSERT(node2.prev() == &node1);
|
||||
SASSERT(node1.prev() == &node2);
|
||||
SASSERT(node2.next() == &node1);
|
||||
SASSERT(node1.invariant());
|
||||
SASSERT(node2.invariant());
|
||||
ENSURE(node1.next() == &node2);
|
||||
ENSURE(node2.prev() == &node1);
|
||||
ENSURE(node1.prev() == &node2);
|
||||
ENSURE(node2.next() == &node1);
|
||||
ENSURE(node1.invariant());
|
||||
ENSURE(node2.invariant());
|
||||
std::cout << "test_insert_after passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -97,12 +97,12 @@ static void test_insert_before() {
|
|||
TestNode node1(1);
|
||||
TestNode node2(2);
|
||||
node1.insert_before(&node2);
|
||||
SASSERT(node1.prev() == &node2);
|
||||
SASSERT(node2.next() == &node1);
|
||||
SASSERT(node1.next() == &node2);
|
||||
SASSERT(node2.prev() == &node1);
|
||||
SASSERT(node1.invariant());
|
||||
SASSERT(node2.invariant());
|
||||
ENSURE(node1.prev() == &node2);
|
||||
ENSURE(node2.next() == &node1);
|
||||
ENSURE(node1.next() == &node2);
|
||||
ENSURE(node2.prev() == &node1);
|
||||
ENSURE(node1.invariant());
|
||||
ENSURE(node2.invariant());
|
||||
std::cout << "test_insert_before passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -115,9 +115,9 @@ static void test_remove_from() {
|
|||
TestNode::push_to_front(list, &node1);
|
||||
TestNode::push_to_front(list, &node2);
|
||||
TestNode::remove_from(list, &node1);
|
||||
SASSERT(list == &node2);
|
||||
SASSERT(node2.next() == &node2);
|
||||
SASSERT(node2.prev() == &node2);
|
||||
ENSURE(list == &node2);
|
||||
ENSURE(node2.next() == &node2);
|
||||
ENSURE(node2.prev() == &node2);
|
||||
std::cout << "test_remove_from passed." << std::endl;
|
||||
}
|
||||
#endif
|
||||
|
|
@ -127,9 +127,9 @@ static void test_push_to_front() {
|
|||
TestNode* list = nullptr;
|
||||
TestNode node1(1);
|
||||
TestNode::push_to_front(list, &node1);
|
||||
SASSERT(list == &node1);
|
||||
SASSERT(node1.next() == &node1);
|
||||
SASSERT(node1.prev() == &node1);
|
||||
ENSURE(list == &node1);
|
||||
ENSURE(node1.next() == &node1);
|
||||
ENSURE(node1.prev() == &node1);
|
||||
std::cout << "test_push_to_front passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -137,20 +137,20 @@ static void test_push_to_front() {
|
|||
static void test_detach() {
|
||||
TestNode node(1);
|
||||
TestNode::detach(&node);
|
||||
SASSERT(node.next() == &node);
|
||||
SASSERT(node.prev() == &node);
|
||||
SASSERT(node.invariant());
|
||||
ENSURE(node.next() == &node);
|
||||
ENSURE(node.prev() == &node);
|
||||
ENSURE(node.invariant());
|
||||
std::cout << "test_detach passed." << std::endl;
|
||||
}
|
||||
|
||||
// Test the invariant() method
|
||||
static void test_invariant() {
|
||||
TestNode node1(1);
|
||||
SASSERT(node1.invariant());
|
||||
ENSURE(node1.invariant());
|
||||
TestNode node2(2);
|
||||
node1.insert_after(&node2);
|
||||
SASSERT(node1.invariant());
|
||||
SASSERT(node2.invariant());
|
||||
ENSURE(node1.invariant());
|
||||
ENSURE(node2.invariant());
|
||||
std::cout << "test_invariant passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -161,10 +161,10 @@ static void test_contains() {
|
|||
TestNode node2(2);
|
||||
TestNode::push_to_front(list, &node1);
|
||||
TestNode::push_to_front(list, &node2);
|
||||
SASSERT(TestNode::contains(list, &node1));
|
||||
SASSERT(TestNode::contains(list, &node2));
|
||||
ENSURE(TestNode::contains(list, &node1));
|
||||
ENSURE(TestNode::contains(list, &node2));
|
||||
TestNode node3(3);
|
||||
SASSERT(!TestNode::contains(list, &node3));
|
||||
ENSURE(!TestNode::contains(list, &node3));
|
||||
std::cout << "test_contains passed." << std::endl;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -116,12 +116,12 @@ static void test3() {
|
|||
g.merge(nx, nz, justifications + 2);
|
||||
g.merge(nx, nu, justifications + 3);
|
||||
g.propagate();
|
||||
SASSERT(!g.inconsistent());
|
||||
ENSURE(!g.inconsistent());
|
||||
g.merge(nx, ny, justifications + 4);
|
||||
std::cout << g << "\n";
|
||||
g.propagate();
|
||||
std::cout << g << "\n";
|
||||
SASSERT(g.inconsistent());
|
||||
ENSURE(g.inconsistent());
|
||||
ptr_vector<int> js;
|
||||
g.begin_explain();
|
||||
g.explain<int>(js, nullptr);
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ static void test2() {
|
|||
TRACE(plugin, tout << "before propagate\n" << g << "\n");
|
||||
g.propagate();
|
||||
TRACE(plugin, tout << "after propagate\n" << g << "\n");
|
||||
SASSERT(nx->get_root() == ny->get_root());
|
||||
ENSURE(nx->get_root() == ny->get_root());
|
||||
g.merge(get_node(g, a, a.mk_add(x, a.mk_add(y, y))), get_node(g, a, a.mk_add(y, x)), nullptr);
|
||||
g.propagate();
|
||||
std::cout << g << "\n";
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ static void test1() {
|
|||
g.propagate();
|
||||
TRACE(bv, tout << "after propagate\n" << g << "\n");
|
||||
std::cout << g << "\n";
|
||||
SASSERT(nx->get_root() == ny->get_root());
|
||||
ENSURE(nx->get_root() == ny->get_root());
|
||||
}
|
||||
|
||||
// propagate values down
|
||||
|
|
@ -70,10 +70,10 @@ static void test2() {
|
|||
expr_ref xx(bv.mk_concat(x1, bv.mk_concat(x2, x3)), m);
|
||||
g.merge(get_node(g, bv, xx), get_node(g, bv, bv.mk_numeral((1 << 27) + (1 << 17) + (1 << 3), 32)), nullptr);
|
||||
g.propagate();
|
||||
SASSERT(get_node(g, bv, x1)->get_root()->interpreted());
|
||||
SASSERT(get_node(g, bv, x2)->get_root()->interpreted());
|
||||
SASSERT(get_node(g, bv, x3)->get_root()->interpreted());
|
||||
SASSERT(get_node(g, bv, x)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x1)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x2)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x3)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x)->get_root()->interpreted());
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -96,9 +96,9 @@ static void test3() {
|
|||
g.merge(get_node(g, bv, x1), get_node(g, bv, bv.mk_numeral(2, 8)), nullptr);
|
||||
g.merge(get_node(g, bv, x2), get_node(g, bv, bv.mk_numeral(8, 8)), nullptr);
|
||||
g.propagate();
|
||||
SASSERT(get_node(g, bv, bv.mk_concat(x1, x2))->get_root()->interpreted());
|
||||
SASSERT(get_node(g, bv, x1)->get_root()->interpreted());
|
||||
SASSERT(get_node(g, bv, x2)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, bv.mk_concat(x1, x2))->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x1)->get_root()->interpreted());
|
||||
ENSURE(get_node(g, bv, x2)->get_root()->interpreted());
|
||||
}
|
||||
|
||||
// propagate extract up
|
||||
|
|
@ -121,7 +121,7 @@ static void test4() {
|
|||
g.merge(get_node(g, bv, x1), get_node(g, bv, a), nullptr);
|
||||
g.propagate();
|
||||
TRACE(bv, tout << g << "\n");
|
||||
SASSERT(get_node(g, bv, bv.mk_extract(23, 8, x))->get_root() == get_node(g, bv, y)->get_root());
|
||||
ENSURE(get_node(g, bv, bv.mk_extract(23, 8, x))->get_root() == get_node(g, bv, y)->get_root());
|
||||
}
|
||||
|
||||
// iterative slicing
|
||||
|
|
|
|||
|
|
@ -61,13 +61,13 @@ bool expr_delta::delta_dfs(unsigned& n, expr* e, expr_ref& result) {
|
|||
}
|
||||
else if (is_app(e)) {
|
||||
if (m.is_bool(e)) {
|
||||
SASSERT(n >= 2);
|
||||
ENSURE(n >= 2);
|
||||
n -= 2;
|
||||
}
|
||||
return delta_dfs(n, to_app(e), result);
|
||||
}
|
||||
else if (is_quantifier(e)) {
|
||||
SASSERT(n >= 2);
|
||||
ENSURE(n >= 2);
|
||||
n -= 2;
|
||||
quantifier* q = to_quantifier(e);
|
||||
if (delta_dfs(n, q->get_expr(), result)) {
|
||||
|
|
|
|||
|
|
@ -77,7 +77,7 @@ expr* expr_rand::choose_expr(sort* s) {
|
|||
if (!m_nodes.find(s, vals)) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
SASSERT(vals);
|
||||
ENSURE(vals);
|
||||
}
|
||||
unsigned idx = m_random(vals->size());
|
||||
return (*vals)[idx].get();
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ struct gomory_test {
|
|||
expl.add_pair(column_lower_bound_constraint(x_j), new_a);
|
||||
}
|
||||
else {
|
||||
SASSERT(at_upper(x_j));
|
||||
ENSURE(at_upper(x_j));
|
||||
if (a.is_pos()) {
|
||||
new_a = a / f_0;
|
||||
new_a.neg(); // the upper terms are inverted.
|
||||
|
|
@ -88,9 +88,9 @@ struct gomory_test {
|
|||
}
|
||||
|
||||
void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & t, explanation& expl, mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) {
|
||||
SASSERT(is_integer(x_j));
|
||||
SASSERT(!a.is_int());
|
||||
SASSERT(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
|
||||
ENSURE(is_integer(x_j));
|
||||
ENSURE(!a.is_int());
|
||||
ENSURE(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
|
||||
mpq f_j = fractional_part(a);
|
||||
TRACE(gomory_cut_detail,
|
||||
tout << a << " x_j = " << x_j << ", k = " << k << "\n";
|
||||
|
|
@ -99,7 +99,7 @@ struct gomory_test {
|
|||
tout << "1 - f_0: " << one_minus_f_0 << "\n";
|
||||
tout << "at_low(" << x_j << ") = " << at_low(x_j) << std::endl;
|
||||
);
|
||||
SASSERT (!f_j.is_zero());
|
||||
ENSURE (!f_j.is_zero());
|
||||
mpq new_a;
|
||||
if (at_low(x_j)) {
|
||||
if (f_j <= one_minus_f_0) {
|
||||
|
|
@ -112,7 +112,7 @@ struct gomory_test {
|
|||
expl.add_pair(column_lower_bound_constraint(x_j), new_a);
|
||||
}
|
||||
else {
|
||||
SASSERT(at_upper(x_j));
|
||||
ENSURE(at_upper(x_j));
|
||||
if (f_j <= f_0) {
|
||||
new_a = f_j / f_0;
|
||||
}
|
||||
|
|
@ -134,13 +134,13 @@ struct gomory_test {
|
|||
}
|
||||
|
||||
void adjust_term_and_k_for_some_ints_case_gomory(lar_term& t, mpq& k, mpq &lcm_den) {
|
||||
SASSERT(!t.is_empty());
|
||||
ENSURE(!t.is_empty());
|
||||
auto pol = t.coeffs_as_vector();
|
||||
t.clear();
|
||||
if (pol.size() == 1) {
|
||||
TRACE(gomory_cut_detail, tout << "pol.size() is 1" << std::endl;);
|
||||
unsigned v = pol[0].second;
|
||||
SASSERT(is_integer(v));
|
||||
ENSURE(is_integer(v));
|
||||
const mpq& a = pol[0].first;
|
||||
k /= a;
|
||||
if (a.is_pos()) { // we have av >= k
|
||||
|
|
@ -162,12 +162,12 @@ struct gomory_test {
|
|||
tout << pol[i].first << " " << pol[i].second << "\n";
|
||||
}
|
||||
tout << "k: " << k << "\n";);
|
||||
SASSERT(lcm_den.is_pos());
|
||||
ENSURE(lcm_den.is_pos());
|
||||
if (!lcm_den.is_one()) {
|
||||
// normalize coefficients of integer parameters to be integers.
|
||||
for (auto & pi: pol) {
|
||||
pi.first *= lcm_den;
|
||||
SASSERT(!is_integer(pi.second) || pi.first.is_int());
|
||||
ENSURE(!is_integer(pi.second) || pi.first.is_int());
|
||||
}
|
||||
k *= lcm_den;
|
||||
}
|
||||
|
|
@ -183,7 +183,7 @@ struct gomory_test {
|
|||
k.neg();
|
||||
}
|
||||
TRACE(gomory_cut_detail, tout << "k = " << k << std::endl;);
|
||||
SASSERT(k.is_int());
|
||||
ENSURE(k.is_int());
|
||||
}
|
||||
|
||||
void print_term(lar_term & t, std::ostream & out) {
|
||||
|
|
|
|||
|
|
@ -387,7 +387,7 @@ vector<int> allocate_basis_heading(
|
|||
|
||||
void init_basic_part_of_basis_heading(vector<unsigned> &basis,
|
||||
vector<int> &basis_heading) {
|
||||
SASSERT(basis_heading.size() >= basis.size());
|
||||
ENSURE(basis_heading.size() >= basis.size());
|
||||
unsigned m = basis.size();
|
||||
for (unsigned i = 0; i < m; ++i) {
|
||||
unsigned column = basis[i];
|
||||
|
|
@ -581,7 +581,7 @@ void test_stacked_unsigned() {
|
|||
v = 3;
|
||||
v = 4;
|
||||
v.pop();
|
||||
SASSERT(v == 2);
|
||||
ENSURE(v == 2);
|
||||
v++;
|
||||
v++;
|
||||
std::cout << "before push v=" << v << std::endl;
|
||||
|
|
@ -591,7 +591,7 @@ void test_stacked_unsigned() {
|
|||
v += 1;
|
||||
std::cout << "v = " << v << std::endl;
|
||||
v.pop(2);
|
||||
SASSERT(v == 4);
|
||||
ENSURE(v == 4);
|
||||
const unsigned &rr = v;
|
||||
std::cout << rr << std::endl;
|
||||
}
|
||||
|
|
@ -755,22 +755,22 @@ void test_numeric_pair() {
|
|||
numeric_pair<lp::mpq> c(0.1, 0.5);
|
||||
a += 2 * c;
|
||||
a -= c;
|
||||
SASSERT(a == b + c);
|
||||
ENSURE(a == b + c);
|
||||
numeric_pair<lp::mpq> d = a * 2;
|
||||
std::cout << a << std::endl;
|
||||
SASSERT(b == b);
|
||||
SASSERT(b < a);
|
||||
SASSERT(b <= a);
|
||||
SASSERT(a > b);
|
||||
SASSERT(a != b);
|
||||
SASSERT(a >= b);
|
||||
SASSERT(-a < b);
|
||||
SASSERT(a < 2 * b);
|
||||
SASSERT(b + b > a);
|
||||
SASSERT(lp::mpq(2.1) * b + b > a);
|
||||
SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a);
|
||||
ENSURE(b == b);
|
||||
ENSURE(b < a);
|
||||
ENSURE(b <= a);
|
||||
ENSURE(a > b);
|
||||
ENSURE(a != b);
|
||||
ENSURE(a >= b);
|
||||
ENSURE(-a < b);
|
||||
ENSURE(a < 2 * b);
|
||||
ENSURE(b + b > a);
|
||||
ENSURE(lp::mpq(2.1) * b + b > a);
|
||||
ENSURE(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a);
|
||||
std::cout << -b * lp::mpq(2.1) - b << std::endl;
|
||||
SASSERT(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b);
|
||||
ENSURE(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b);
|
||||
std::cout << -b * (lp::mpq(2.1) + 1) << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -859,7 +859,7 @@ void test_evidence_for_total_inf_simple(argument_parser &args_parser) {
|
|||
auto status = solver.solve();
|
||||
std::cout << lp_status_to_string(status) << std::endl;
|
||||
std::unordered_map<lpvar, mpq> model;
|
||||
SASSERT(solver.get_status() == lp_status::INFEASIBLE);
|
||||
ENSURE(solver.get_status() == lp_status::INFEASIBLE);
|
||||
}
|
||||
void test_bound_propagation_one_small_sample1() {
|
||||
/*
|
||||
|
|
@ -1065,8 +1065,8 @@ void test_total_case_l() {
|
|||
// ls.solve();
|
||||
// my_bound_propagator bp(ls);
|
||||
// ls.propagate_bounds_for_touched_rows(bp);
|
||||
// SASSERT(ev.size() == 4);
|
||||
// SASSERT(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
|
||||
// ENSURE(ev.size() == 4);
|
||||
// ENSURE(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
|
||||
}
|
||||
void test_bound_propagation() {
|
||||
test_total_case_u();
|
||||
|
|
@ -1082,14 +1082,14 @@ void test_int_set() {
|
|||
indexed_uint_set s;
|
||||
s.insert(1);
|
||||
s.insert(2);
|
||||
SASSERT(s.contains(2));
|
||||
SASSERT(s.size() == 2);
|
||||
ENSURE(s.contains(2));
|
||||
ENSURE(s.size() == 2);
|
||||
s.remove(2);
|
||||
SASSERT(s.size() == 1);
|
||||
ENSURE(s.size() == 1);
|
||||
s.insert(3);
|
||||
s.insert(2);
|
||||
s.reset();
|
||||
SASSERT(s.size() == 0);
|
||||
ENSURE(s.size() == 0);
|
||||
std::cout << "done test_int_set\n";
|
||||
}
|
||||
|
||||
|
|
@ -1197,12 +1197,12 @@ void get_random_interval(bool &neg_inf, bool &pos_inf, int &x, int &y) {
|
|||
pos_inf = false;
|
||||
if (!neg_inf) {
|
||||
y = x + my_random() % (101 - x);
|
||||
SASSERT(y >= x);
|
||||
ENSURE(y >= x);
|
||||
} else {
|
||||
y = my_random() % 100;
|
||||
}
|
||||
}
|
||||
SASSERT((neg_inf || (0 <= x && x <= 100)) &&
|
||||
ENSURE((neg_inf || (0 <= x && x <= 100)) &&
|
||||
(pos_inf || (0 <= y && y <= 100)));
|
||||
}
|
||||
|
||||
|
|
@ -1633,7 +1633,7 @@ void test_maximize_term() {
|
|||
solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>());
|
||||
solver.add_var_bound(term_2x_pl_2y, LE, mpq(5));
|
||||
solver.find_feasible_solution();
|
||||
SASSERT(solver.get_status() == lp_status::OPTIMAL);
|
||||
ENSURE(solver.get_status() == lp_status::OPTIMAL);
|
||||
std::cout << solver.constraints();
|
||||
std::unordered_map<lpvar, mpq> model;
|
||||
solver.get_model(model);
|
||||
|
|
@ -1707,7 +1707,7 @@ void test_dio() {
|
|||
solver.add_var_bound(t1, LE, mpq(0));
|
||||
solver.add_var_bound(t1, GE, mpq(0));
|
||||
// solver.find_feasible_solution();
|
||||
//SASSERT(solver.get_status() == lp_status::OPTIMAL);
|
||||
//ENSURE(solver.get_status() == lp_status::OPTIMAL);
|
||||
enable_trace("dioph_eq");
|
||||
enable_trace("dioph_eq_fresh");
|
||||
#ifdef Z3DEBUG
|
||||
|
|
@ -1754,14 +1754,14 @@ void test_gomory_cut() {
|
|||
matrix.add_rows(mpq(2), 0, 1); // row 1 = row 1 + 2 * row 0
|
||||
|
||||
// Verify the results
|
||||
SASSERT(matrix.get_elem(1, 0) == 5); // 3 + 2*1
|
||||
SASSERT(matrix.get_elem(1, 1) == 4); // 0 + 2*2
|
||||
SASSERT(matrix.get_elem(1, 2) == 4); // unchanged
|
||||
ENSURE(matrix.get_elem(1, 0) == 5); // 3 + 2*1
|
||||
ENSURE(matrix.get_elem(1, 1) == 4); // 0 + 2*2
|
||||
ENSURE(matrix.get_elem(1, 2) == 4); // unchanged
|
||||
|
||||
matrix.add_rows(mpq(-2), 0, 1);
|
||||
SASSERT(matrix.get_elem(1, 0) == 3); // 5 - 2*1
|
||||
SASSERT(matrix.get_elem(1, 1) == 0); // 4 - 2*2
|
||||
SASSERT(matrix.get_elem(1, 2) == 4); // unchanged
|
||||
ENSURE(matrix.get_elem(1, 0) == 3); // 5 - 2*1
|
||||
ENSURE(matrix.get_elem(1, 1) == 0); // 4 - 2*2
|
||||
ENSURE(matrix.get_elem(1, 2) == 4); // unchanged
|
||||
}
|
||||
|
||||
void test_nla_order_lemma() { nla::test_order_lemma(); }
|
||||
|
|
@ -1787,7 +1787,7 @@ void test_restore_x() {
|
|||
solver.add_var_bound(t, LE, mpq(15));
|
||||
|
||||
auto status = solver.solve();
|
||||
SASSERT(status == lp_status::OPTIMAL);
|
||||
ENSURE(status == lp_status::OPTIMAL);
|
||||
|
||||
// Backup the current solution
|
||||
solver.backup_x();
|
||||
|
|
@ -1802,7 +1802,7 @@ void test_restore_x() {
|
|||
|
||||
// The solver should find a feasible solution
|
||||
status = solver.get_status();
|
||||
SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
|
||||
ENSURE(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
|
||||
std::cout << " test 1 (backup shorter): " << lp_status_to_string(status) << " - PASSED" << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -1829,7 +1829,7 @@ void test_restore_x() {
|
|||
|
||||
auto status = solver.solve();
|
||||
(void)status;
|
||||
SASSERT(status == lp_status::OPTIMAL);
|
||||
ENSURE(status == lp_status::OPTIMAL);
|
||||
|
||||
// Backup with the full system
|
||||
solver.backup_x();
|
||||
|
|
@ -1850,7 +1850,7 @@ void test_restore_x() {
|
|||
solver.add_var_bound(y, LE, mpq(10));
|
||||
|
||||
auto status = solver.solve();
|
||||
SASSERT(status == lp_status::OPTIMAL);
|
||||
ENSURE(status == lp_status::OPTIMAL);
|
||||
|
||||
// Add new constraint: x + y >= 5
|
||||
vector<std::pair<mpq, lpvar>> coeffs;
|
||||
|
|
@ -1867,17 +1867,17 @@ void test_restore_x() {
|
|||
|
||||
// Solve expanded system, then move non-basic columns to bounds
|
||||
status = solver.solve();
|
||||
SASSERT(status == lp_status::OPTIMAL);
|
||||
ENSURE(status == lp_status::OPTIMAL);
|
||||
solver.move_non_basic_columns_to_bounds();
|
||||
status = solver.get_status();
|
||||
SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
|
||||
ENSURE(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
|
||||
|
||||
// Verify the model satisfies the constraints
|
||||
std::unordered_map<lpvar, mpq> model;
|
||||
solver.get_model(model);
|
||||
SASSERT(model[x] >= mpq(1) && model[x] <= mpq(10));
|
||||
SASSERT(model[y] >= mpq(1) && model[y] <= mpq(10));
|
||||
SASSERT(model[w] >= mpq(2) && model[w] <= mpq(8));
|
||||
ENSURE(model[x] >= mpq(1) && model[x] <= mpq(10));
|
||||
ENSURE(model[y] >= mpq(1) && model[y] <= mpq(10));
|
||||
ENSURE(model[w] >= mpq(2) && model[w] <= mpq(8));
|
||||
std::cout << " test 3 (move_non_basic_columns_to_bounds): " << lp_status_to_string(status) << " - PASSED" << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -2036,13 +2036,13 @@ void asserts_on_patching(const rational &x, const rational &alpha) {
|
|||
auto a2 = denominator(alpha);
|
||||
auto x1 = numerator(x);
|
||||
auto x2 = denominator(x);
|
||||
SASSERT(a1.is_pos());
|
||||
SASSERT(abs(a1) < abs(a2));
|
||||
SASSERT(coprime(a1, a2));
|
||||
SASSERT(x1.is_pos());
|
||||
SASSERT(x1 < x2);
|
||||
SASSERT(coprime(x1, x2));
|
||||
SASSERT((a2 / x2).is_int());
|
||||
ENSURE(a1.is_pos());
|
||||
ENSURE(abs(a1) < abs(a2));
|
||||
ENSURE(coprime(a1, a2));
|
||||
ENSURE(x1.is_pos());
|
||||
ENSURE(x1 < x2);
|
||||
ENSURE(coprime(x1, x2));
|
||||
ENSURE((a2 / x2).is_int());
|
||||
}
|
||||
void get_patching_deltas(const rational &x, const rational &alpha, rational &delta_0, rational &delta_1) {
|
||||
std::cout << "get_patching_deltas(" << x << ", " << alpha << ")" << std::endl;
|
||||
|
|
@ -2050,7 +2050,7 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del
|
|||
auto a2 = denominator(alpha);
|
||||
auto x1 = numerator(x);
|
||||
auto x2 = denominator(x);
|
||||
SASSERT(divides(x2, a2));
|
||||
ENSURE(divides(x2, a2));
|
||||
// delta has to be integral.
|
||||
// We need to find delta such that x1/x2 + (a1/a2)*delta is integral.
|
||||
// Then a2*x1/x2 + a1*delta is integral, that means that t = a2/x2 is integral.
|
||||
|
|
@ -2064,17 +2064,17 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del
|
|||
// We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are coprime.
|
||||
rational u, v;
|
||||
auto g = gcd(a1, x2, u, v);
|
||||
SASSERT(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2);
|
||||
ENSURE(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2);
|
||||
std::cout << "u = " << u << ", v = " << v << std::endl;
|
||||
std::cout << "x= " << (x1 / x2) << std::endl;
|
||||
std::cout << "x + (a1 / a2) * (-u * t) * x1 = " << x + (a1 / a2) * (-u * t) * x1 << std::endl;
|
||||
SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int());
|
||||
ENSURE((x + (a1 / a2) * (-u * t) * x1).is_int());
|
||||
// 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l.
|
||||
rational d = u * t * x1;
|
||||
delta_0 = mod(d, a2);
|
||||
SASSERT(delta_0 > 0);
|
||||
ENSURE(delta_0 > 0);
|
||||
delta_1 = delta_0 - a2;
|
||||
SASSERT(delta_1 < 0);
|
||||
ENSURE(delta_1 < 0);
|
||||
std::cout << "delta_0 = " << delta_0 << std::endl;
|
||||
std::cout << "delta_1 = " << delta_1 << std::endl;
|
||||
}
|
||||
|
|
@ -2102,10 +2102,10 @@ void test_patching_alpha(const rational &x, const rational &alpha) {
|
|||
rational delta_0, delta_1;
|
||||
get_patching_deltas(x, alpha, delta_0, delta_1);
|
||||
|
||||
SASSERT(delta_0 * delta_1 < 0);
|
||||
ENSURE(delta_0 * delta_1 < 0);
|
||||
|
||||
SASSERT((x - alpha * delta_0).is_int());
|
||||
SASSERT((x - alpha * delta_1).is_int());
|
||||
ENSURE((x - alpha * delta_0).is_int());
|
||||
ENSURE((x - alpha * delta_1).is_int());
|
||||
try_find_smaller_delta(x, alpha, delta_0, delta_1);
|
||||
// std::cout << "delta_minus = " << delta_minus << ", delta_1 = " << delta_1 << "\n";
|
||||
// std::cout << "x + alpha*delta_minus = " << x + alpha * delta_minus << "\n";
|
||||
|
|
@ -2116,7 +2116,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) {
|
|||
x2 = (rand() % a2) + (int)(a2 / 3);
|
||||
auto g = gcd(rational(a2), rational(x2));
|
||||
a2 *= (x2 / numerator(g).get_int32());
|
||||
SASSERT(rational(a2, x2).is_int());
|
||||
ENSURE(rational(a2, x2).is_int());
|
||||
do {
|
||||
x1 = rand() % (unsigned)x2 + 1;
|
||||
} while (!coprime(x1, x2));
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ void add_equality(int n_of_vars, var_eqs<emonics> & var_eqs, random_gen& rand, b
|
|||
while (a == b) {
|
||||
b = rand() % n_of_vars;
|
||||
}
|
||||
SASSERT(a != b);
|
||||
ENSURE(a != b);
|
||||
var_eqs.merge_plus(a, b, eq_justification({0}));
|
||||
}
|
||||
|
||||
|
|
@ -262,7 +262,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
|
|||
|
||||
VERIFY(nla.get_core().test_check() == l_false);
|
||||
auto const& lemma = nla.get_core().lemmas();
|
||||
SASSERT(lemma[0].size() == 4);
|
||||
ENSURE(lemma[0].size() == 4);
|
||||
nla.get_core().print_lemma(lemma.back(), std::cout);
|
||||
|
||||
lp::lar_term t0, t1, t2, t3;
|
||||
|
|
@ -348,7 +348,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
|
|||
VERIFY(nla.get_core().test_check() == l_false);
|
||||
auto const& lemma = nla.get_core().lemmas();
|
||||
nla.get_core().print_lemma(lemma.back(), std::cout);
|
||||
SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
|
||||
ENSURE(lemma.size() == 1 && lemma[0].size() == 2);
|
||||
lp::lar_term t0, t1;
|
||||
t0.add_var(lp_b);
|
||||
t1.add_var(lp_be);
|
||||
|
|
@ -697,7 +697,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
|
|||
|
||||
// set abef = cdij, while it has to be abef < cdij
|
||||
if (sign > 0) {
|
||||
SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
ENSURE(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we have ab < cd
|
||||
|
||||
// we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij
|
||||
|
|
@ -707,7 +707,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
|
|||
|
||||
}
|
||||
else {
|
||||
SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
ENSURE(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we need to have abef < cdij, so let us make abef < cdij
|
||||
s_set_column_value_test(s, lp_cdij, nla.get_core().mon_value_by_vars(mon_cdij));
|
||||
s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
|
||||
|
|
@ -722,7 +722,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
|
|||
// ineq q(llc::EQ, t, rational(0));
|
||||
|
||||
nla.get_core().print_lemma(lemma.back(), std::cout);
|
||||
// SASSERT(q == lemma.back());
|
||||
// ENSURE(q == lemma.back());
|
||||
// ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
// i0.m_term.add_monomial(lp_bde);
|
||||
// i0.m_term.add_monomial(rational(1), lp_acd);
|
||||
|
|
@ -733,7 +733,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
|
|||
// }
|
||||
// }
|
||||
|
||||
// SASSERT(found);
|
||||
// ENSURE(found);
|
||||
*/
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -117,13 +117,13 @@ namespace lp {
|
|||
|
||||
void fill_simple_elem(lisp_elem & lm) {
|
||||
int separator = first_separator();
|
||||
SASSERT(-1 != separator && separator != 0);
|
||||
ENSURE(-1 != separator && separator != 0);
|
||||
lm.m_head = m_line.substr(0, separator);
|
||||
m_line = m_line.substr(separator);
|
||||
}
|
||||
|
||||
void fill_nested_elem(lisp_elem & lm) {
|
||||
SASSERT(m_line[0] == '(');
|
||||
ENSURE(m_line[0] == '(');
|
||||
m_line = m_line.substr(1);
|
||||
int separator = first_separator();
|
||||
lm.m_head = m_line.substr(0, separator);
|
||||
|
|
@ -190,11 +190,11 @@ namespace lp {
|
|||
}
|
||||
|
||||
void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
|
||||
// SASSERT(el.m_head == "0"); // do nothing for the time being
|
||||
// ENSURE(el.m_head == "0"); // do nothing for the time being
|
||||
}
|
||||
|
||||
void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
|
||||
SASSERT(el.m_elems.size() == 2);
|
||||
ENSURE(el.m_elems.size() == 2);
|
||||
set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
|
||||
adjust_right_side(c, el.m_elems[1]);
|
||||
}
|
||||
|
|
@ -210,7 +210,7 @@ namespace lp {
|
|||
add_mult_elem(c, el.m_elems);
|
||||
} else if (el.m_head == "~") {
|
||||
lisp_elem & minel = el.m_elems[0];
|
||||
SASSERT(minel.is_simple());
|
||||
ENSURE(minel.is_simple());
|
||||
c.m_right_side += mpq(str_to_int(minel.m_head));
|
||||
} else {
|
||||
std::cout << "unexpected input " << el.m_head << std::endl;
|
||||
|
|
@ -220,14 +220,14 @@ namespace lp {
|
|||
}
|
||||
|
||||
std::string get_name(lisp_elem & name) {
|
||||
SASSERT(name.is_simple());
|
||||
SASSERT(!is_integer(name.m_head));
|
||||
ENSURE(name.is_simple());
|
||||
ENSURE(!is_integer(name.m_head));
|
||||
return name.m_head;
|
||||
}
|
||||
|
||||
|
||||
void add_mult_elem(formula_constraint & c, std::vector<lisp_elem> & els) {
|
||||
SASSERT(els.size() == 2);
|
||||
ENSURE(els.size() == 2);
|
||||
mpq coeff = get_coeff(els[0]);
|
||||
std::string col_name = get_name(els[1]);
|
||||
c.add_pair(coeff, col_name);
|
||||
|
|
@ -237,16 +237,16 @@ namespace lp {
|
|||
if (le.is_simple()) {
|
||||
return mpq(str_to_int(le.m_head));
|
||||
} else {
|
||||
SASSERT(le.m_head == "~");
|
||||
SASSERT(le.size() == 1);
|
||||
ENSURE(le.m_head == "~");
|
||||
ENSURE(le.size() == 1);
|
||||
lisp_elem & el = le.m_elems[0];
|
||||
SASSERT(el.is_simple());
|
||||
ENSURE(el.is_simple());
|
||||
return -mpq(str_to_int(el.m_head));
|
||||
}
|
||||
}
|
||||
|
||||
int str_to_int(std::string & s) {
|
||||
SASSERT(is_integer(s));
|
||||
ENSURE(is_integer(s));
|
||||
return atoi(s.c_str());
|
||||
}
|
||||
|
||||
|
|
@ -254,7 +254,7 @@ namespace lp {
|
|||
if (el.size()) {
|
||||
add_complex_sum_elem(c, el);
|
||||
} else {
|
||||
SASSERT(is_integer(el.m_head));
|
||||
ENSURE(is_integer(el.m_head));
|
||||
int v = atoi(el.m_head.c_str());
|
||||
mpq vr(v);
|
||||
c.m_right_side -= vr;
|
||||
|
|
|
|||
|
|
@ -78,17 +78,17 @@ void tst_model_evaluator() {
|
|||
fi2.insert_entry(args, i == 599 ? one.get() : zero.get());
|
||||
}
|
||||
fi2.compress();
|
||||
SASSERT(fi2.num_entries() == 1);
|
||||
ENSURE(fi2.num_entries() == 1);
|
||||
|
||||
expr_ref removed_arg(a.mk_int(0), m);
|
||||
[[maybe_unused]] expr* removed_args[1] = { removed_arg.get() };
|
||||
SASSERT(fi2.get_entry(removed_args) == nullptr);
|
||||
ENSURE(fi2.get_entry(removed_args) == nullptr);
|
||||
|
||||
expr_ref kept_arg(a.mk_int(599), m);
|
||||
expr* kept_args[1] = { kept_arg.get() };
|
||||
[[maybe_unused]] func_entry* kept = fi2.get_entry(kept_args);
|
||||
SASSERT(kept != nullptr);
|
||||
SASSERT(kept->get_result() == one.get());
|
||||
ENSURE(kept != nullptr);
|
||||
ENSURE(kept->get_result() == one.get());
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@
|
|||
static void test_constructor() {
|
||||
permutation p(5);
|
||||
for (unsigned i = 0; i < 5; ++i) {
|
||||
SASSERT(p(i) == i);
|
||||
SASSERT(p.inv(i) == i);
|
||||
ENSURE(p(i) == i);
|
||||
ENSURE(p.inv(i) == i);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -19,28 +19,28 @@ static void test_reset() {
|
|||
p.swap(0, 2);
|
||||
p.reset(3);
|
||||
for (unsigned i = 0; i < 3; ++i) {
|
||||
SASSERT(p(i) == i);
|
||||
SASSERT(p.inv(i) == i);
|
||||
ENSURE(p(i) == i);
|
||||
ENSURE(p.inv(i) == i);
|
||||
}
|
||||
}
|
||||
|
||||
static void test_swap() {
|
||||
permutation p(4);
|
||||
p.swap(1, 3);
|
||||
SASSERT(p(1) == 3);
|
||||
SASSERT(p(3) == 1);
|
||||
SASSERT(p.inv(1) == 3);
|
||||
SASSERT(p.inv(3) == 1);
|
||||
ENSURE(p(1) == 3);
|
||||
ENSURE(p(3) == 1);
|
||||
ENSURE(p.inv(1) == 3);
|
||||
ENSURE(p.inv(3) == 1);
|
||||
}
|
||||
|
||||
static void test_move_after() {
|
||||
permutation p(5);
|
||||
p.move_after(1, 3);
|
||||
SASSERT(p(0) == 0);
|
||||
SASSERT(p(1) == 2);
|
||||
SASSERT(p(2) == 3);
|
||||
SASSERT(p(3) == 1);
|
||||
SASSERT(p(4) == 4);
|
||||
ENSURE(p(0) == 0);
|
||||
ENSURE(p(1) == 2);
|
||||
ENSURE(p(2) == 3);
|
||||
ENSURE(p(3) == 1);
|
||||
ENSURE(p(4) == 4);
|
||||
}
|
||||
|
||||
void apply_permutation_copy(unsigned sz, unsigned const * src, unsigned const * p, unsigned * target) {
|
||||
|
|
@ -74,18 +74,18 @@ static void test_apply_permutation(unsigned sz, unsigned num_tries, unsigned max
|
|||
|
||||
static void test_check_invariant() {
|
||||
permutation p(4);
|
||||
SASSERT(p.check_invariant());
|
||||
ENSURE(p.check_invariant());
|
||||
p.swap(0, 2);
|
||||
SASSERT(p.check_invariant());
|
||||
ENSURE(p.check_invariant());
|
||||
p.move_after(1, 3);
|
||||
SASSERT(p.check_invariant());
|
||||
ENSURE(p.check_invariant());
|
||||
}
|
||||
|
||||
static void test_display() {
|
||||
permutation p(4);
|
||||
std::ostringstream out;
|
||||
p.display(out);
|
||||
SASSERT(out.str() == "0:0 1:1 2:2 3:3");
|
||||
ENSURE(out.str() == "0:0 1:1 2:2 3:3");
|
||||
}
|
||||
|
||||
void tst_permutation() {
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ static void tst_psmt_worker() {
|
|||
expr_dependency_ref core(m);
|
||||
std::string reason_unknown;
|
||||
lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
|
||||
SASSERT(r == l_true);
|
||||
ENSURE(r == l_true);
|
||||
(void)r;
|
||||
std::cout << "psmt SAT: " << r << "\n";
|
||||
}
|
||||
|
|
@ -82,7 +82,7 @@ static void tst_psmt_worker() {
|
|||
expr_dependency_ref core(m);
|
||||
std::string reason_unknown;
|
||||
lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
|
||||
SASSERT(r == l_false);
|
||||
ENSURE(r == l_false);
|
||||
(void)r;
|
||||
std::cout << "psmt UNSAT: " << r << "\n";
|
||||
}
|
||||
|
|
@ -131,7 +131,7 @@ static void tst_psmt_worker() {
|
|||
lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
|
||||
// The result must be l_undef (theory-incomplete).
|
||||
// If the fix is absent, this call deadlocks instead of returning.
|
||||
SASSERT(r == l_undef);
|
||||
ENSURE(r == l_undef);
|
||||
(void)r;
|
||||
std::cout << "psmt UNKNOWN (no deadlock): " << r << "\n";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -457,10 +457,10 @@ static void tst12() {
|
|||
std::cout << "test12\n";
|
||||
rational r;
|
||||
r = 5;
|
||||
SASSERT(r.get_bit(0));
|
||||
SASSERT(!r.get_bit(1));
|
||||
SASSERT(r.get_bit(2));
|
||||
SASSERT(!r.get_bit(3));
|
||||
ENSURE(r.get_bit(0));
|
||||
ENSURE(!r.get_bit(1));
|
||||
ENSURE(r.get_bit(2));
|
||||
ENSURE(!r.get_bit(3));
|
||||
r = rational("10000000000000000000000000000000001");
|
||||
for (unsigned i = 0; i < r.get_num_bits(); ++i)
|
||||
std::cout << i << ": " << r.get_bit(i) << "\n";
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
#include "util/cancel_eh.h"
|
||||
#include "util/scoped_ctrl_c.h"
|
||||
#include "util/scoped_timer.h"
|
||||
#include <cstdio>
|
||||
#include <iostream>
|
||||
|
||||
static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
|
||||
|
|
@ -16,13 +17,12 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
|
|||
return false;
|
||||
}
|
||||
infile.getline(line, 16383);
|
||||
#ifdef _WINDOWS
|
||||
int cur_term;
|
||||
int num_vars = 0, num_constraints = 0;
|
||||
sscanf_s(line, "%d %d", &num_vars, &num_constraints);
|
||||
//std::cout << "number of variables: " << num_vars << '\n';
|
||||
//std::cout << "number of constraints: " << num_constraints << '\n';
|
||||
|
||||
if (sscanf(line, "%d %d", &num_vars, &num_constraints) != 2) {
|
||||
std::cout << "Failed to parse header (expected: num_vars num_constraints)\n";
|
||||
return false;
|
||||
}
|
||||
|
||||
unsigned_vector coefficients;
|
||||
sat::literal_vector lits;
|
||||
|
|
@ -57,15 +57,11 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
|
|||
infile >> cur_term;
|
||||
}
|
||||
infile >> k;
|
||||
//local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
|
||||
local_search.add_cardinality(lits.size(), lits.data(), static_cast<unsigned>(k));
|
||||
}
|
||||
|
||||
infile.close();
|
||||
return true;
|
||||
#else
|
||||
return false;
|
||||
#endif
|
||||
}
|
||||
|
||||
void tst_sat_local_search(char ** argv, int argc, int& i) {
|
||||
|
|
|
|||
|
|
@ -7,9 +7,9 @@ void test_push_back_and_access() {
|
|||
|
||||
sv.push_back(20);
|
||||
|
||||
SASSERT(sv.size() == 2);
|
||||
SASSERT(sv[0] == 10);
|
||||
SASSERT(sv[1] == 20);
|
||||
ENSURE(sv.size() == 2);
|
||||
ENSURE(sv[0] == 10);
|
||||
ENSURE(sv[1] == 20);
|
||||
|
||||
std::cout << "test_push_back_and_access passed." << std::endl;
|
||||
}
|
||||
|
|
@ -23,16 +23,16 @@ void test_scopes() {
|
|||
sv.push_back(30);
|
||||
sv.push_back(40);
|
||||
|
||||
SASSERT(sv.size() == 4);
|
||||
SASSERT(sv[2] == 30);
|
||||
SASSERT(sv[3] == 40);
|
||||
ENSURE(sv.size() == 4);
|
||||
ENSURE(sv[2] == 30);
|
||||
ENSURE(sv[3] == 40);
|
||||
|
||||
sv.pop_scope(1);
|
||||
|
||||
std::cout << "test_scopes passed." << std::endl;
|
||||
SASSERT(sv.size() == 2);
|
||||
SASSERT(sv[0] == 10);
|
||||
SASSERT(sv[1] == 20);
|
||||
ENSURE(sv.size() == 2);
|
||||
ENSURE(sv[0] == 10);
|
||||
ENSURE(sv[1] == 20);
|
||||
|
||||
std::cout << "test_scopes passed." << std::endl;
|
||||
}
|
||||
|
|
@ -45,15 +45,15 @@ void test_set() {
|
|||
sv.set(0, 30);
|
||||
sv.set(1, 40);
|
||||
|
||||
SASSERT(sv.size() == 2);
|
||||
SASSERT(sv[0] == 30);
|
||||
SASSERT(sv[1] == 40);
|
||||
ENSURE(sv.size() == 2);
|
||||
ENSURE(sv[0] == 30);
|
||||
ENSURE(sv[1] == 40);
|
||||
|
||||
sv.push_scope();
|
||||
sv.set(0, 50);
|
||||
SASSERT(sv[0] == 50);
|
||||
ENSURE(sv[0] == 50);
|
||||
sv.pop_scope(1);
|
||||
SASSERT(sv[0] == 30);
|
||||
ENSURE(sv[0] == 30);
|
||||
|
||||
std::cout << "test_set passed." << std::endl;
|
||||
}
|
||||
|
|
@ -63,12 +63,12 @@ void test_pop_back() {
|
|||
sv.push_back(10);
|
||||
sv.push_back(20);
|
||||
|
||||
SASSERT(sv.size() == 2);
|
||||
ENSURE(sv.size() == 2);
|
||||
sv.pop_back();
|
||||
SASSERT(sv.size() == 1);
|
||||
SASSERT(sv[0] == 10);
|
||||
ENSURE(sv.size() == 1);
|
||||
ENSURE(sv[0] == 10);
|
||||
sv.pop_back();
|
||||
SASSERT(sv.size() == 0);
|
||||
ENSURE(sv.size() == 0);
|
||||
|
||||
std::cout << "test_pop_back passed." << std::endl;
|
||||
}
|
||||
|
|
@ -81,9 +81,9 @@ void test_erase_and_swap() {
|
|||
|
||||
sv.erase_and_swap(1);
|
||||
|
||||
SASSERT(sv.size() == 2);
|
||||
SASSERT(sv[0] == 10);
|
||||
SASSERT(sv[1] == 30);
|
||||
ENSURE(sv.size() == 2);
|
||||
ENSURE(sv[0] == 10);
|
||||
ENSURE(sv[1] == 30);
|
||||
|
||||
std::cout << "test_erase_and_swap passed." << std::endl;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -221,7 +221,7 @@ struct test_seq {
|
|||
}
|
||||
|
||||
zstring& strval0(expr* e) {
|
||||
SASSERT(seq.is_string(e->get_sort()));
|
||||
ENSURE(seq.is_string(e->get_sort()));
|
||||
return get_eval(e).val0.svalue;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -86,7 +86,7 @@ namespace bv {
|
|||
verbose_stream() << mk_pp(e, m) << " computed value " << val << "\n";
|
||||
verbose_stream() << "should be " << n2 << "\n";
|
||||
}
|
||||
SASSERT(n1 == n2);
|
||||
ENSURE(n1 == n2);
|
||||
VERIFY(n1 == n2);
|
||||
}
|
||||
else if (m.is_bool(e)) {
|
||||
|
|
@ -96,7 +96,7 @@ namespace bv {
|
|||
verbose_stream() << mk_pp(e, m) << " computed value " << val1
|
||||
<< " at odds with definition " << val2 << "\n";
|
||||
}
|
||||
SASSERT(val1 == val2);
|
||||
ENSURE(val1 == val2);
|
||||
VERIFY(val1 == val2);
|
||||
}
|
||||
}
|
||||
|
|
@ -193,7 +193,7 @@ namespace bv {
|
|||
ev.init();
|
||||
|
||||
if (m.is_bool(e1)) {
|
||||
SASSERT(m.is_true(r) || m.is_false(r));
|
||||
ENSURE(m.is_true(r) || m.is_false(r));
|
||||
auto val = m.is_true(r);
|
||||
auto val2 = ev.bval1(to_app(e2));
|
||||
if (val != val2) {
|
||||
|
|
@ -208,7 +208,7 @@ namespace bv {
|
|||
ev.display(std::cout);
|
||||
exit(0);
|
||||
}
|
||||
//SASSERT(rep1);
|
||||
//ENSURE(rep1);
|
||||
}
|
||||
}
|
||||
if (bv.is_bv(e1)) {
|
||||
|
|
@ -226,7 +226,7 @@ namespace bv {
|
|||
if (!val3.eq(val1)) {
|
||||
verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
|
||||
}
|
||||
//SASSERT(rep2);
|
||||
//ENSURE(rep2);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -539,7 +539,7 @@ static void test_pb(unsigned max_w, unsigned sz, unsigned_vector& ws) {
|
|||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(ws.size() == sz);
|
||||
ENSURE(ws.size() == sz);
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
expr_ref_vector xs(m), nxs(m);
|
||||
|
|
|
|||
|
|
@ -103,7 +103,7 @@ static void test_dc() {
|
|||
todo.pop_back();
|
||||
bool found = false;
|
||||
tbit tvalue = eval[t];
|
||||
SASSERT(tvalue != BIT_z);
|
||||
ENSURE(tvalue != BIT_z);
|
||||
for (unsigned j = 0; j < 2*num_bits; ++j) {
|
||||
tbit tb = (*t)[j];
|
||||
if (tb == BIT_x)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue