mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

partial fix to make computed term integer well-formed for solve_for functionality

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-05 17:10:52 -08:00
parent bcb61ee12c
commit 1ab0962d43
2 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_solver.cpp
View file

@ -619,6 +619,7 @@ namespace lp {
bool lar_solver::solve_for(unsigned j, lar_term& t, mpq& coeff) {
t.clear();
IF_VERBOSE(10, verbose_stream() << column_is_fixed(j) << " " << is_base(j) << "\n");
if (column_is_fixed(j)) {
coeff = get_value(j);
return true;
@ -626,6 +627,7 @@ namespace lp {
if (!is_base(j)) {
for (const auto & c : A_r().m_columns[j]) {
lpvar basic_in_row = r_basis()[c.var()];
IF_VERBOSE(10, verbose_stream() << "c.var() = " << c.var() << " basic_in_row = " << basic_in_row << "\n");
pivot(j, basic_in_row);
break;
}

12
src/smt/theory_lra.cpp
View file

@ -3638,9 +3638,21 @@ public:
rational coeff;
if (!lp().solve_for(vi, t, coeff))
return false;
rational lc(1);
if (is_int(v)) {
lc = denominator(coeff);
for (auto const& cv : t)
lc = lcm(denominator(cv.coeff()), lc);
if (lc != 1) {
coeff *= lc;
t *= lc;
}
}
term = mk_term(t, is_int(v));
if (coeff != 0)
term = a.mk_add(a.mk_numeral(coeff, is_int(v)), term);
if (lc != 1)
term = a.mk_idiv(term, a.mk_numeral(lc, true));
return true;
}