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

adjust solve_for to handle rationals

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-17 13:59:23 -08:00
parent 528efbb535
commit f977b48161
2 changed files with 22 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -684,6 +684,7 @@ namespace lp {
return; return;
tabu.insert(j); tabu.insert(j);
IF_VERBOSE(10, verbose_stream() << "solve for " << j << " base " << is_base(j) << " " << column_is_fixed(j) << "\n"); IF_VERBOSE(10, verbose_stream() << "solve for " << j << " base " << is_base(j) << " " << column_is_fixed(j) << "\n");
TRACE("arith", tout << "solve for " << j << " base " << is_base(j) << " " << column_is_fixed(j) << "\n");
if (column_is_fixed(j)) if (column_is_fixed(j))
return; return;
@ -711,7 +712,6 @@ namespace lp {
lp::impq lo, hi; lp::impq lo, hi;
bool lo_valid = true, hi_valid = true; bool lo_valid = true, hi_valid = true;
for (auto const& v : t) { for (auto const& v : t) {
if (v.coeff().is_pos()) { if (v.coeff().is_pos()) {
if (lo_valid && column_has_lower_bound(v.j())) if (lo_valid && column_has_lower_bound(v.j()))
lo += column_lower_bound(v.j()) * v.coeff(); lo += column_lower_bound(v.j()) * v.coeff();
@ -756,7 +756,8 @@ namespace lp {
update_column_type_and_bound(j, hi.y == 0 ? lconstraint_kind::LE : lconstraint_kind::LT, hi.x, dep); update_column_type_and_bound(j, hi.y == 0 ? lconstraint_kind::LE : lconstraint_kind::LT, hi.x, dep);
} }
if (!column_is_fixed(j)) TRACE("arith", print_term(t, tout << "j" << j << " := ") << "\n");
if (!column_is_fixed(j))
sols.push_back({j, t}); sols.push_back({j, t});
} }

33
src/smt/theory_lra.cpp
View file

@ -3642,7 +3642,7 @@ public:
term = a.mk_numeral(lp().get_value(j), a.is_int(n->get_expr())); term = a.mk_numeral(lp().get_value(j), a.is_int(n->get_expr()));
reset_evidence(); reset_evidence();
add_explain(j); add_explain(j);
guard = extract_explain(); guard = mk_and(extract_explain());
} }
void add_explain(unsigned j) { void add_explain(unsigned j) {
@ -3650,7 +3650,7 @@ public:
set_evidence(d, m_core, m_eqs); set_evidence(d, m_core, m_eqs);
} }
expr_ref extract_explain() { expr_ref_vector extract_explain() {
expr_ref_vector es(m); expr_ref_vector es(m);
for (auto [l, r] : m_eqs) for (auto [l, r] : m_eqs)
es.push_back(a.mk_eq(l->get_expr(), r->get_expr())); es.push_back(a.mk_eq(l->get_expr(), r->get_expr()));
@ -3665,32 +3665,34 @@ public:
es[j++] = es.get(i); es[j++] = es.get(i);
} }
es.shrink(j); es.shrink(j);
return mk_and(es); return es;
} }
void solve_term(enode* n, lp::lar_term & lt, expr_ref& term, expr_ref& guard) { void solve_term(enode* n, lp::lar_term & lt, expr_ref& term, expr_ref& guard) {
bool is_int = a.is_int(n->get_expr()); bool is_int = a.is_int(n->get_expr());
bool all_int = is_int; bool all_int = is_int;
lp::lar_term t; lp::lar_term t;
rational coeff(0); rational coeff(0), lc(1);
expr_ref_vector guards(m); expr_ref_vector guards(m);
reset_evidence(); reset_evidence();
// extract coeff
for (auto const& cv : lt) { for (auto const& cv : lt) {
all_int &= lp().column_is_int(cv.j());
if (lp().column_is_fixed(cv.j())) { if (lp().column_is_fixed(cv.j())) {
coeff += lp().get_value(cv.j()) * cv.coeff(); coeff += lp().get_value(cv.j()) * cv.coeff();
add_explain(cv.j()); add_explain(cv.j());
} }
else else {
t.add_monomial(cv.coeff(), cv.j()); t.add_monomial(cv.coeff(), cv.j());
lc = lcm(denominator(cv.coeff()), lc);
}
} }
guards.push_back(extract_explain()); // extract lc
rational lc = denominator(coeff); lc = lcm(lc, denominator(coeff));
for (auto const& cv : t) {
lc = lcm(denominator(cv.coeff()), lc); guards.append(extract_explain());
all_int &= lp().column_is_int(cv.j());
}
if (lc != 1) if (lc != 1)
t *= lc, coeff *= lc; t *= lc, coeff *= lc;
term = mk_term(t, is_int); term = mk_term(t, is_int);
if (coeff != 0) if (coeff != 0)
term = a.mk_add(term, a.mk_numeral(coeff, is_int)); term = a.mk_add(term, a.mk_numeral(coeff, is_int));
@ -3699,12 +3701,15 @@ public:
guard = mk_and(guards); guard = mk_and(guards);
return; return;
} }
expr_ref lce(a.mk_numeral(lc, true), m); expr_ref lce(a.mk_numeral(lc, is_int), m);
if (all_int) if (all_int)
guards.push_back(m.mk_eq(a.mk_mod(term, lce), a.mk_int(0))); guards.push_back(m.mk_eq(a.mk_mod(term, lce), a.mk_int(0)));
else if (is_int) else if (is_int)
guards.push_back(a.mk_is_int(a.mk_div(term, lce))); guards.push_back(a.mk_is_int(a.mk_div(term, lce)));
term = a.mk_idiv(term, lce); if (is_int)
term = a.mk_idiv(term, lce);
else
term = a.mk_div(term, lce);
guard = mk_and(guards); guard = mk_and(guards);
} }