mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

debug nl2lin

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-20 15:59:11 -07:00
parent 5d08ebdffd
commit 6ef8a0b7bb
3 changed files with 24 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/nla_core.cpp
View file

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -88,6 +88,13 @@ lpvar core::map_to_root(lpvar j) const {
return m_evars.find(j).var();
}
// Reduce a single variable to its root and provide the reduction sign.
lpvar core::reduce_var_to_rooted(lpvar j, rational & sign) const {
auto root = m_evars.find(j);
sign = rational(root.sign() ? -1 : 1);
return root.var();
}
svector<lpvar> core::sorted_rvars(const factor& f) const {
if (f.is_var()) {
svector<lpvar> r; r.push_back(map_to_root(f.var()));

10
src/math/lp/nla_core.h
View file

@ -281,8 +281,12 @@ public:
svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
monic_coeff canonize_monic(monic const& m) const;
// Reduce a single variable to its canonical root under current equalities
// and return the convertion sign as either 1 or -1
lpvar reduce_var_to_rooted(lpvar v, rational & sign) const;
monic_coeff canonize_monic(monic const& m) const;
int vars_sign(const svector<lpvar>& v);
bool has_upper_bound(lpvar j) const;
bool has_lower_bound(lpvar j) const;
@ -357,10 +361,6 @@ public:
template <typename T>
bool vars_are_roots(const T& v) const;
void register_monic_in_tables(unsigned i_mon);
void register_monics_in_tables();
void clear();
void init_search();

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

@ -280,6 +280,7 @@ struct solver::imp {
TRACE(nra,
m_nlsat->display(tout << r << "\n");
display(tout);
tout << "m_lp2nl:\n";
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
switch (r) {
case l_true:
@ -317,14 +318,19 @@ struct solver::imp {
case 0:
bound -= coeff;
break;
case 1:
v = nl2lp[pm.get_var(m, 0)];
t.add_monomial(coeff, v);
case 1: {
v = nl2lp[pm.get_var(m, 0)];
rational s;
v = m_nla_core.reduce_var_to_rooted(v, s);
t.add_monomial(s * coeff, v);
}
break;
default: {
svector<lp::lpvar> vars;
for (unsigned j = 0; j < num_vars; ++j)
vars.push_back(nl2lp[pm.get_var(m, j)]);
rational s(1);
vars = m_nla_core.reduce_monic_to_rooted(vars, s);
auto mon = m_nla_core.emons().find_canonical(vars);
if (mon)
v = mon->var();
@ -339,12 +345,12 @@ struct solver::imp {
// polynomials so punt for now.
m_nla_core.add_monic(v, vars.size(), vars.data());
}
t.add_monomial(coeff, v);
t.add_monomial(s * coeff, v);
break;
}
}
}
TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;);
switch (a->get_kind()) {
case nlsat::atom::EQ:
lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound);