diff --git a/src/math/dd/pdd_eval.h b/src/math/dd/pdd_eval.h index ac590686b..3a5e85cf4 100644 --- a/src/math/dd/pdd_eval.h +++ b/src/math/dd/pdd_eval.h @@ -22,13 +22,12 @@ Revision History: namespace dd { // calculates the value of a pdd expression based on the given values of the variables class pdd_eval { - pdd_manager& m; std::function m_var2val; public: - pdd_eval(pdd_manager& m): m(m) {} + pdd_eval() {} std::function& var2val() { return m_var2val; } // setter const std::function& var2val() const { return m_var2val; } // getter diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index fae3a9598..fd796b6a1 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -25,13 +25,12 @@ typedef dep_intervals::interval interval; typedef dep_intervals::with_deps_t w_dep; // calculates the interval of a pdd expression based on the given intervals of the variables class pdd_interval { - pdd_manager& m; dep_intervals m_dep_intervals; std::function m_var2interval; public: - pdd_interval(pdd_manager& m, reslimit& lim): m(m), m_dep_intervals(lim) {} + pdd_interval(reslimit& lim): m_dep_intervals(lim) {} std::function& var2interval() { return m_var2interval; } // setter const std::function& var2interval() const { return m_var2interval; } // getter diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 24369dda5..2a99fe10c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1463,7 +1463,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) { // m_pdd_grobner.display(out); - dd::pdd_eval eval(m_pdd_manager); + dd::pdd_eval eval; eval.var2val() = [&](unsigned j){ return val(j); }; for (auto* e : m_pdd_grobner.equations()) { dd::pdd p = e->poly(); @@ -1486,7 +1486,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) { } bool core::check_pdd_eq(const dd::solver::equation* e) { - dd::pdd_interval eval(m_pdd_manager, m_reslim); + dd::pdd_interval eval(m_reslim); eval.var2interval() = [this](lpvar j, bool deps) { intervals::interval a; diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 87bc2b7c5..2ce274b51 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -757,7 +757,6 @@ namespace { static const unsigned start_gen = 0; static const unsigned goal_gen_decrement = 100; - static const unsigned stop_gen = goal_gen_decrement + 1; public: diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 7917f9976..f30994c38 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -227,9 +227,6 @@ namespace smt { } case OP_OR: { literal_buffer lits; - expr* a = nullptr; - expr_ref b(m), c(m); - // perform light-weight rewriting on clauses. for (expr * arg : *to_app(n)) { internalize(arg, true); lits.push_back(get_literal(arg)); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 05f9b38eb..5bd52e61b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9686,8 +9686,7 @@ namespace smt { arith_value v(m); v.init(&ctx); rational val; - bool val_exists = v.get_value(fromInt, val); - SASSERT(val_exists); + VERIFY(v.get_value(fromInt, val)); std::string s = std::to_string(val.get_int32()); extra_deps.push_back(ctx.mk_eq_atom(fromInt, mk_int(val))); @@ -9700,9 +9699,8 @@ namespace smt { arith_value v(m); v.init(&ctx); rational pos; - bool pos_exists = v.get_value(substrPos, pos); + VERIFY(v.get_value(substrPos, pos)); - SASSERT(pos_exists); extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos))); return 1; @@ -9714,10 +9712,9 @@ namespace smt { arith_value v(m); v.init(&ctx); rational len, pos; - bool len_exists = v.get_value(substrLen, len); - bool pos_exists = v.get_value(substrPos, pos); + VERIFY(v.get_value(substrLen, len)); + VERIFY(v.get_value(substrPos, pos)); - SASSERT(len_exists && pos_exists); extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos))); return len.get_unsigned(); diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 2a5f4ab7f..33bd1d664 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -576,6 +576,8 @@ namespace smt { return true; } } + UNREACHABLE(); // ??? + return false; } /* diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 003d64d85..7dc04a8f8 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -86,29 +86,29 @@ void test_nex_order() { nex_var* a = r.mk_var(0); nex_var* b = r.mk_var(1); nex_var* c = r.mk_var(2); - SASSERT(r.gt(a, b)); - SASSERT(r.gt(b, c)); - SASSERT(r.gt(a, c)); + ENSURE(r.gt(a, b)); + ENSURE(r.gt(b, c)); + ENSURE(r.gt(a, c)); nex* ab = r.mk_mul(a, b); nex* ba = r.mk_mul(b, a); nex* ac = r.mk_mul(a, c); - SASSERT(r.gt(ab, ac)); - SASSERT(!r.gt(ac, ab)); + ENSURE(r.gt(ab, ac)); + ENSURE(!r.gt(ac, ab)); nex* _3ac = r.mk_mul(rational(3), a, c); nex* _2ab = r.mk_mul(rational(2), a, b); - SASSERT(r.gt(ab, _3ac)); - SASSERT(!r.gt(_3ac, ab)); - SASSERT(!r.gt(a, ab)); - SASSERT(r.gt(ab, a)); - SASSERT(r.gt(_2ab, _3ac)); - SASSERT(!r.gt(_3ac, _2ab)); + ENSURE(r.gt(ab, _3ac)); + ENSURE(!r.gt(_3ac, ab)); + ENSURE(!r.gt(a, ab)); + ENSURE(r.gt(ab, a)); + ENSURE(r.gt(_2ab, _3ac)); + ENSURE(!r.gt(_3ac, _2ab)); nex* _2a = r.mk_mul(rational(2), a); - SASSERT(!r.gt(_2a, _2ab)); - SASSERT(r.gt(_2ab, _2a)); - SASSERT(nex_creator::equal(ab, ba)); + ENSURE(!r.gt(_2a, _2ab)); + ENSURE(r.gt(_2ab, _2a)); + ENSURE(nex_creator::equal(ab, ba)); nex_sum * five_a_pl_one = r.mk_sum(r.mk_mul(rational(5), a), r.mk_scalar(rational(1))); nex_mul * poly = r.mk_mul(five_a_pl_one, b); nex * p = r.simplify(poly); @@ -142,9 +142,9 @@ void test_simplify() { auto two_a_plus_bc = r.mk_mul(r.mk_scalar(rational(2)), a_plus_bc); auto simp_two_a_plus_bc = r.simplify(two_a_plus_bc); TRACE("nla_test", tout << * simp_two_a_plus_bc << "\n";); - SASSERT(nex_creator::equal(simp_two_a_plus_bc, two_a_plus_bc)); + ENSURE(nex_creator::equal(simp_two_a_plus_bc, two_a_plus_bc)); auto simp_a_plus_bc = r.simplify(a_plus_bc); - SASSERT(to_sum(simp_a_plus_bc)->size() > 1); + ENSURE(to_sum(simp_a_plus_bc)->size() > 1); auto three_ab = r.mk_mul(r.mk_scalar(rational(3)), a, b); auto three_ab_square = r.mk_mul(three_ab, three_ab, three_ab); @@ -153,7 +153,7 @@ void test_simplify() { three_ab_square = to_mul(r.simplify(three_ab_square)); TRACE("nla_test", tout << *three_ab_square << "\n";); const rational& s = three_ab_square->coeff(); - SASSERT(s == rational(27)); + ENSURE(s == rational(27)); auto m = r.mk_mul(a, a); TRACE("nla_test_", tout << "m = " << *m << "\n";); /* @@ -171,7 +171,7 @@ void test_simplify() { TRACE("nla_test", tout << "before simplify e = " << *e << "\n";); e = to_sum(r.simplify(e)); TRACE("nla_test", tout << "simplified e = " << *e << "\n";); - SASSERT(e->children().size() > 2); + ENSURE(e->children().size() > 2); nex_sum * e_m = r.mk_sum(); for (const nex* ex: to_sum(e)->children()) { nex* ce = r.mk_mul(r.clone(ex), r.mk_scalar(rational(3))); @@ -290,7 +290,7 @@ void test_cn() { // nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d); // nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); // clone = cr.simplify(clone); -// SASSERT(cr.is_simplified(clone)); +// ENSURE(cr.is_simplified(clone)); // TRACE("nla_test", tout << "clone = " << *clone << "\n";); // // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); // test_cn_on_expr(to_sum(clone), cn); @@ -2956,7 +2956,7 @@ void test_term() { std::cout << "non optimal" << std::endl; return; } - solver.print_constraints(std::cout); + std::cout << solver.constraints(); std::cout << "\ntableau before cube\n"; solver.m_mpq_lar_core_solver.m_r_solver.pretty_print(std::cout); std::cout << "\n"; @@ -3781,7 +3781,7 @@ void test_maximize_term() { solver.add_var_bound(term_2x_pl_2y, LE, mpq(5)); solver.find_feasible_solution(); lp_assert(solver.get_status() == lp_status::OPTIMAL); - solver.print_constraints(std::cout); + std::cout << solver.constraints(); std::unordered_map model; solver.get_model(model); for (auto p : model) {