mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

bug fixes to mod/div quantifier elimination features

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-13 06:18:13 -07:00
parent 88b6c4a30d
commit 5669cf65bc
2 changed files with 16 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -91,4 +91,5 @@ examples/**/obj
CMakeSettings.json CMakeSettings.json
# Editor temp files # Editor temp files
*.swp *.swp
.DS_Store .DS_Store
dbg/**

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

@ -871,6 +871,7 @@ namespace opt {
unsigned model_based_opt::add_var(rational const& value, bool is_int) { unsigned model_based_opt::add_var(rational const& value, bool is_int) {
unsigned v = m_var2value.size(); unsigned v = m_var2value.size();
verbose_stream() << "add var " << v << "\n";
m_var2value.push_back(value); m_var2value.push_back(value);
m_var2is_int.push_back(is_int); m_var2is_int.push_back(is_int);
SASSERT(value.is_int() || !is_int); SASSERT(value.is_int() || !is_int);
@ -1208,7 +1209,7 @@ namespace opt {
// compute a_inv // compute a_inv
rational a_inv, m_inv; rational a_inv, m_inv;
rational g = gcd(a, m, a_inv, m_inv); rational g = mod(gcd(a, m, a_inv, m_inv), m);
if (a_inv.is_neg()) if (a_inv.is_neg())
a_inv = mod(a_inv, m); a_inv = mod(a_inv, m);
SASSERT(mod(a_inv * a, m) == g); SASSERT(mod(a_inv * a, m) == g);
@ -1252,7 +1253,7 @@ namespace opt {
// add g*z + w - v - k*m = 0, for k = (g*z_value + w_value) div m // add g*z + w - v - k*m = 0, for k = (g*z_value + w_value) div m
rational km = div(g*z_value + w_value, m)*m; rational km = div(g*z_value + w_value, m)*m;
vector<var> mod_coeffs; vector<var> mod_coeffs;
mod_coeffs.push_back(var(z, g)); if (g != 0) mod_coeffs.push_back(var(z, g));
mod_coeffs.push_back(var(w, rational::one())); mod_coeffs.push_back(var(w, rational::one()));
mod_coeffs.push_back(var(v, rational::minus_one())); mod_coeffs.push_back(var(v, rational::minus_one()));
add_constraint(mod_coeffs, km, t_eq); add_constraint(mod_coeffs, km, t_eq);
@ -1270,7 +1271,7 @@ namespace opt {
result = (y_def * m) + z_def * a_inv; result = (y_def * m) + z_def * a_inv;
m_var2value[x] = eval(result); m_var2value[x] = eval(result);
} }
TRACE("opt", display(tout << "solve_mod\n"));
return result; return result;
} }
@ -1308,11 +1309,14 @@ namespace opt {
replace_var(row_index, x, rational::zero()); replace_var(row_index, x, rational::zero());
rational b_value = m_rows[row_index].m_value; rational b_value = m_rows[row_index].m_value;
TRACE("opt", display(tout << "solve_div\n"));
// compute a_inv // compute a_inv
rational a_inv, m_inv; rational a_inv, m_inv;
rational g = gcd(a, m, a_inv, m_inv); rational g = mod(gcd(a, m, a_inv, m_inv), m);
if (a_inv.is_neg()) if (a_inv.is_neg())
a_inv = mod(a_inv, m); a_inv = mod(a_inv, m);
SASSERT(mod(a_inv * a, m) == g); SASSERT(mod(a_inv * a, m) == g);
// solve for x_value = m*y_value + a_inv*z_value, 0 <= z_value < m. // solve for x_value = m*y_value + a_inv*z_value, 0 <= z_value < m.
@ -1366,7 +1370,7 @@ namespace opt {
// add g*z + (b mod m) < (k + 1)*m // add g*z + (b mod m) < (k + 1)*m
vector<var> bound_coeffs; vector<var> bound_coeffs;
bound_coeffs.push_back(var(z, g)); if (g != 0) bound_coeffs.push_back(var(z, g));
bound_coeffs.push_back(var(u, rational::one())); bound_coeffs.push_back(var(u, rational::one()));
add_constraint(bound_coeffs, 1 - m * (k + 1), t_le); add_constraint(bound_coeffs, 1 - m * (k + 1), t_le);
@ -1387,6 +1391,7 @@ namespace opt {
result = (y_def * m) + (z_def * a_inv); result = (y_def * m) + (z_def * a_inv);
m_var2value[x] = eval(result); m_var2value[x] = eval(result);
} }
TRACE("opt", display(tout << "solve_div\n"));
return result; return result;
} }
@ -1505,13 +1510,13 @@ namespace opt {
if (coeff.is_zero() || !r.m_alive) if (coeff.is_zero() || !r.m_alive)
return; return;
replace_var(row_id, x, rational::zero()); replace_var(row_id, x, rational::zero());
r.m_vars.push_back(var(y, coeff*A)); if (A != 0) r.m_vars.push_back(var(y, coeff*A));
r.m_vars.push_back(var(z, coeff*B)); if (B != 0) r.m_vars.push_back(var(z, coeff*B));
r.m_value += coeff*A*m_var2value[y]; r.m_value += coeff*A*m_var2value[y];
r.m_value += coeff*B*m_var2value[z]; r.m_value += coeff*B*m_var2value[z];
std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare()); std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare());
m_var2row_ids[y].push_back(row_id); if (A != 0) m_var2row_ids[y].push_back(row_id);
m_var2row_ids[z].push_back(row_id); if (B != 0) m_var2row_ids[z].push_back(row_id);
SASSERT(invariant(row_id, r)); SASSERT(invariant(row_id, r));
} }