mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

simplify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-02 20:17:29 -07:00
parent 85869b575b
commit f8942dfdee
1 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/nra_solver.cpp
View file

@ -194,7 +194,7 @@ struct solver::imp {
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon; map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
// Create polynomial definition for variable v used in setup_assignment_solver. // Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable. // Side-effects: updates m_vars2mon when v is a monic variable.
polynomial::polynomial_ref mk_definition(unsigned v, polynomial_ref_vector const& definitions) { void mk_definition(unsigned v, polynomial_ref_vector& definitions) {
auto &pm = m_nlsat->pm(); auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm); polynomial::polynomial_ref p(pm);
if (m_nla_core.emons().is_monic_var(v)) { if (m_nla_core.emons().is_monic_var(v)) {
@ -209,19 +209,22 @@ struct solver::imp {
else else
p = pm.mul(p, pv); p = pm.mul(p, pv);
} }
} else if (lra.column_has_term(v)) { }
for (auto const& [w, coeff] : lra.get_term(v)) { else if (lra.column_has_term(v)) {
for (auto const &[w, coeff] : lra.get_term(v)) {
auto pw = definitions.get(w); auto pw = definitions.get(w);
if (!p) if (!p)
p = pm.mul(coeff, pw); p = pm.mul(coeff, pw);
else else
p = pm.add(p, pm.mul(coeff, pw)); p = pm.add(p, pm.mul(coeff, pw));
} }
} else {
p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created)
} }
return p; else {
p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created)
}
definitions.push_back(p);
} }
void setup_assignment_solver() { void setup_assignment_solver() {
SASSERT(need_check()); SASSERT(need_check());
reset(); reset();
@ -238,7 +241,7 @@ struct solver::imp {
scoped_anum a(am()); scoped_anum a(am());
am().set(a, m_nla_core.val(v).to_mpq()); am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a); m_values->push_back(a);
definitions.push_back(mk_definition(v, definitions)); mk_definition(v, definitions);
} }
// we rely on that all information encoded into the tableau is present as a constraint. // we rely on that all information encoded into the tableau is present as a constraint.