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

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-11 21:00:58 +02:00
parent 18a76ab82c
commit cab1076514
4 changed files with 35 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -134,20 +134,29 @@ namespace opt {
}
void model_based_opt::def::normalize() {
if (m_div.is_one()) return;
SASSERT(m_div.is_int());
if (m_div.is_neg()) {
for (var& v : m_vars)
v.m_coeff.neg();
m_coeff.neg();
m_div.neg();
}
if (m_div.is_one())
return;
rational g(m_div);
if (!m_coeff.is_int())
return;
g = gcd(g, m_coeff);
for (var const& v : m_vars) {
if (!v.m_coeff.is_int())
return;
g = gcd(g, abs(v.m_coeff));
if (g.is_one()) break;
}
if (m_div.is_neg()) {
g.neg();
if (g.is_one())
break;
}
if (!g.is_one()) {
for (var& v : m_vars) {
v.m_coeff /= g;
}
for (var& v : m_vars)
v.m_coeff /= g;
m_coeff /= g;
m_div /= g;
}
@ -1130,9 +1139,12 @@ namespace opt {
}
TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
def result = project(y, compute_def);
if (compute_def)
result = (result * D) + u;
SASSERT(!compute_def || eval(result) == eval(x));
if (compute_def) {
result = (result * D) + u;
m_var2value[x] = eval(result);
}
TRACE("opt1", display(tout << "tableau after project y" << y << "\n"););
return result;
}
@ -1181,7 +1193,7 @@ namespace opt {
// 3 | -t & 21 | (-ct + 3s) & a-t <= 3u
model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) {
TRACE("opt", tout << "v" << x << "\n" << m_rows[row_id1] << "\n";);
TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";);
rational a = get_coefficient(row_id1, x), b;
ineq_type ty = m_rows[row_id1].m_type;
SASSERT(!a.is_zero());
@ -1231,6 +1243,7 @@ namespace opt {
if (compute_def) {
result = def(m_rows[row_id1], x);
m_var2value[x] = eval(result);
TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
}
retire_row(row_id1);
return result;

4
src/qe/mbp/mbp_arith.cpp
View file

@ -294,7 +294,9 @@ namespace mbp {
}
}
fmls.shrink(j);
TRACE("qe", tout << "formulas\n" << fmls << "\n";);
TRACE("qe", tout << "formulas\n" << fmls << "\n";
for (auto [e, id] : tids)
tout << mk_pp(e, m) << " -> " << id << "\n";);
// fmls holds residue,
// mbo holds linear inequalities that are in scope

2
src/qe/mbp/mbp_plugin.cpp
View file

@ -102,7 +102,7 @@ namespace mbp {
model_evaluator eval(model);
eval.set_expand_array_equalities(true);
TRACE("qe", tout << fmls << "\n";);
DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); });
DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;

8
src/sat/smt/euf_solver.cpp
View file

@ -302,13 +302,17 @@ namespace euf {
size_t* c = to_ptr(l);
SASSERT(is_literal(c));
SASSERT(l == get_literal(c));
if (!sign && n->is_equality()) {
if (n->value_conflict()) {
euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, c);
}
else if (!sign && n->is_equality()) {
SASSERT(!m.is_iff(e));
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
m_egraph.merge(na, nb, c);
}
else if (n->merge_tf() || n->value_conflict()) {
else if (n->merge_tf()) {
euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, c);
}