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

create polynomials with integer coefficients, use the hook to create new monomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-06 11:53:06 -07:00
parent f8942dfdee
commit 6cbc6f4f84
2 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

31
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.
void mk_definition(unsigned v, polynomial_ref_vector& 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,22 +209,25 @@ struct solver::imp {
else else
p = pm.mul(p, pv); p = pm.mul(p, pv);
} }
} }
else if (lra.column_has_term(v)) { else if (lra.column_has_term(v)) {
for (auto const &[w, coeff] : lra.get_term(v)) { // Scale coefficients by a common denominator so that they become integers.
rational den(1);
for (auto const& [w, coeff] : lra.get_term(v))
den = lcm(den, denominator(coeff));
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(den*coeff, pw);
else else
p = pm.add(p, pm.mul(coeff, pw)); p = pm.add(p, pm.mul(den*coeff, pw));
} }
} }
else { else {
p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created)
} }
definitions.push_back(p); definitions.push_back(p);
} }
void setup_assignment_solver() { void setup_assignment_solver() {
SASSERT(need_check()); SASSERT(need_check());
reset(); reset();
@ -366,13 +369,15 @@ struct solver::imp {
break; break;
} }
default: { default: {
IF_VERBOSE(0, verbose_stream() << "Valentin! we don't really expect non-linear literals here\n");
svector<lp::lpvar> vars; svector<lp::lpvar> vars;
for (unsigned j = 0; j < num_vars; ++j) for (unsigned j = 0; j < num_vars; ++j)
vars.push_back(nl2lp[pm.get_var(m, j)]); vars.push_back(nl2lp[pm.get_var(m, j)]);
std::sort(vars.begin(), vars.end()); std::sort(vars.begin(), vars.end());
SASSERT(m_vars2mon.contains(vars)); lp::lpvar v;
auto v = m_vars2mon[vars]; if (m_vars2mon.contains(vars))
v = m_vars2mon[vars];
else
v = m_nla_core.add_mul_def(vars.size(), vars.data());
TRACE(nra, tout << " vars=" << vars << "\n"); TRACE(nra, tout << " vars=" << vars << "\n");
t.add_monomial(coeff, v); t.add_monomial(coeff, v);
break; break;

2
src/smt/theory_lra.cpp
View file

@ -276,7 +276,7 @@ class theory_lra::imp {
} }
} }
lpvar add_mul_def(unsigned sz, lpvar const* vs) { // under 10 lines lpvar add_mul_def(unsigned sz, lpvar const* vs) {
bool is_int = true; bool is_int = true;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
theory_var tv = lp().local_to_external(vs[i]); theory_var tv = lp().local_to_external(vs[i]);