mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#6429

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-29 13:42:57 -07:00
parent 0e651eee04
commit 0da0fa2b27
2 changed files with 23 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1299,7 +1299,7 @@ namespace opt {
def result; def result;
unsigned_vector div_rows(_div_rows), mod_rows(_mod_rows); unsigned_vector div_rows(_div_rows), mod_rows(_mod_rows);
SASSERT(!div_rows.empty() || !mod_rows.empty()); SASSERT(!div_rows.empty() || !mod_rows.empty());
TRACE("opt", display(tout << "solve_div " << x << "\n")); TRACE("opt", display(tout << "solve_div v" << x << "\n"));
rational K(1); rational K(1);
for (unsigned ri : div_rows) for (unsigned ri : div_rows)

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

@ -421,15 +421,23 @@ namespace mbp {
mbo.display(tout);); mbo.display(tout););
vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def); vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
vector<row> rows; vector<row> rows;
u_map<row> def_vars;
mbo.get_live_rows(rows); mbo.get_live_rows(rows);
rows2fmls(rows, index2expr, fmls); for (row const& r : rows) {
if (r.m_type == opt::t_mod)
def_vars.insert(r.m_id, r);
else if (r.m_type == opt::t_div)
def_vars.insert(r.m_id, r);
}
rows2fmls(def_vars, rows, index2expr, fmls);
TRACE("qe", mbo.display(tout << "mbo result\n"); TRACE("qe", mbo.display(tout << "mbo result\n");
for (auto const& d : defs) tout << "def: " << d << "\n"; for (auto const& d : defs) tout << "def: " << d << "\n";
tout << fmls << "\n";); tout << fmls << "\n";);
if (compute_def) if (compute_def)
optdefs2mbpdef(defs, index2expr, real_vars, result); optdefs2mbpdef(def_vars, defs, index2expr, real_vars, result);
if (m_apply_projection && !apply_projection(eval, result, fmls)) if (m_apply_projection && !apply_projection(eval, result, fmls))
return false; return false;
@ -442,7 +450,7 @@ namespace mbp {
return true; return true;
} }
void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) { void optdefs2mbpdef(u_map<row> const& def_vars, vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
SASSERT(defs.size() == real_vars.size()); SASSERT(defs.size() == real_vars.size());
for (unsigned i = 0; i < defs.size(); ++i) { for (unsigned i = 0; i < defs.size(); ++i) {
auto const& d = defs[i]; auto const& d = defs[i];
@ -450,8 +458,12 @@ namespace mbp {
bool is_int = a.is_int(x); bool is_int = a.is_int(x);
expr_ref_vector ts(m); expr_ref_vector ts(m);
expr_ref t(m); expr_ref t(m);
for (var const& v : d.m_vars) for (var const& v : d.m_vars) {
ts.push_back(var2expr(index2expr, v)); t = id2expr(def_vars, index2expr, v.m_id);
if (v.m_coeff != 1)
t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
ts.push_back(t);
}
if (!d.m_coeff.is_zero()) if (!d.m_coeff.is_zero())
ts.push_back(a.mk_numeral(d.m_coeff, is_int)); ts.push_back(a.mk_numeral(d.m_coeff, is_int));
if (ts.empty()) if (ts.empty())
@ -492,6 +504,7 @@ namespace mbp {
t = a.mk_int(mod(r.m_coeff, r.m_mod)); t = a.mk_int(mod(r.m_coeff, r.m_mod));
return t; return t;
} }
if (r.m_coeff != 0)
ts.push_back(a.mk_int(r.m_coeff)); ts.push_back(a.mk_int(r.m_coeff));
t = mk_add(ts); t = mk_add(ts);
t = a.mk_mod(t, a.mk_int(r.m_mod)); t = a.mk_mod(t, a.mk_int(r.m_mod));
@ -501,6 +514,7 @@ namespace mbp {
t = a.mk_int(div(r.m_coeff, r.m_mod)); t = a.mk_int(div(r.m_coeff, r.m_mod));
return t; return t;
} }
if (r.m_coeff != 0)
ts.push_back(a.mk_int(r.m_coeff)); ts.push_back(a.mk_int(r.m_coeff));
t = mk_add(ts); t = mk_add(ts);
t = a.mk_idiv(t, a.mk_int(r.m_mod)); t = a.mk_idiv(t, a.mk_int(r.m_mod));
@ -513,15 +527,7 @@ namespace mbp {
} }
} }
void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) { void rows2fmls(u_map<row>& def_vars, vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
u_map<row> def_vars;
for (row const& r : rows) {
if (r.m_type == opt::t_mod)
def_vars.insert(r.m_id, r);
else if (r.m_type == opt::t_div)
def_vars.insert(r.m_id, r);
}
for (row const& r : rows) { for (row const& r : rows) {
expr_ref t(m), s(m), val(m); expr_ref t(m), s(m), val(m);