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

build errors/warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-07 10:09:10 -08:00
parent bd444f8ec7
commit 88374a15d0
8 changed files with 31 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/dd/pdd_eval.h
View file

@ -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<rational (unsigned)> m_var2val;
public:
pdd_eval(pdd_manager& m): m(m) {}
pdd_eval() {}
std::function<rational (unsigned)>& var2val() { return m_var2val; } // setter
const std::function<rational (unsigned)>& var2val() const { return m_var2val; } // getter

3
src/math/dd/pdd_interval.h
View file

@ -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<interval (unsigned, bool)> 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<interval (unsigned, bool)>& var2interval() { return m_var2interval; } // setter
const std::function<interval (unsigned, bool)>& var2interval() const { return m_var2interval; } // getter

4
src/math/lp/nla_core.cpp
View file

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

1
src/smt/smt_case_split_queue.cpp
View file

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

3
src/smt/smt_internalizer.cpp
View file

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

11
src/smt/theory_str.cpp
View file

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

2
src/smt/theory_str_mc.cpp
View file

@ -576,6 +576,8 @@ namespace smt {
return true;
}
}
UNREACHABLE(); // ???
return false;
}
/*

42
src/test/lp/lp.cpp
View file

@ -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<var_index, mpq> model;
solver.get_model(model);
for (auto p : model) {