mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-31 08:19:54 +00:00
Code Activity

canonicalize polinomals in todo_set

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-08 11:33:31 -10:00
parent aa6dae8f5f
commit bf32a437c1
4 changed files with 111 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/nlsat/levelwise.cpp
View file

@ -220,10 +220,10 @@ namespace nlsat {
}
/*
prepare the initial properties
*/
// Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
void collect_top_level_properties(polynomial_ref_vector & ps_of_n_level) {
prepare the initial properties:
scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
*/
void collect_top_level_properties(todo_set& ps_of_n_level) {
for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_P[i];
polynomial_ref pref(p, m_pm);
@ -235,7 +235,7 @@ namespace nlsat {
m_Q[level].push(property(prop_enum::sgn_inv, prim));
else if (level == m_n){
m_Q[level].push(property(prop_enum::an_del, prim));
ps_of_n_level.push_back(prim.get());
ps_of_n_level.insert(f.get());
}
else {
UNREACHABLE();
@ -245,8 +245,8 @@ namespace nlsat {
}
// isolate and collect algebraic roots for the given polynomials
void collect_roots_for_ps(polynomial_ref_vector & ps_of_n_level, std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
for (poly * p : ps_of_n_level) {
void collect_roots_for_ps(todo_set const& ps_of_n_level, std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
for (poly * p : ps_of_n_level.m_set) {
scoped_anum_vector roots(m_am);
m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(sample(), m_n), roots);
TRACE(lws,
@ -262,7 +262,7 @@ namespace nlsat {
}
}
// Helper 3: given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...))
// Given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...))
// for adjacent roots coming from different polynomials. Avoid adding the same unordered pair twice.
// Returns false on failure (e.g. when encountering an ambiguous zero resultant).
bool add_adjacent_resultants(std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
@ -317,7 +317,7 @@ namespace nlsat {
∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent root functions }.
*/
void init_properties() {
polynomial_ref_vector ps_of_n_level(m_pm);
todo_set ps_of_n_level(m_cache, true);
collect_top_level_properties(ps_of_n_level);
std::vector<std::pair<scoped_anum, poly*>> root_vals;
collect_roots_for_ps(ps_of_n_level, root_vals);
@ -414,25 +414,19 @@ namespace nlsat {
// Part B of construct_interval: build (I, E, ≼) representation for level i
void build_representation() {
// collect non-null polynomials (up to polynomial_manager equality)
polynomial::polynomial_ref_vector p_non_null(m_pm);
// collect non-null polynomials (up to polynomial_manager equality and canonicalization)
todo_set p_non_null(m_cache, true);
for (auto & pr: m_Q[m_level]) {
if (!pr.m_poly) continue;
SASSERT(max_var(pr.m_poly) == m_level);
if (pr.m_prop_tag == prop_enum::sgn_inv
&& !coeffs_are_zeroes_on_sample(pr.m_poly, m_pm, sample(), m_am )) {
TRACE(lws, tout << "adding:" << pr.m_poly.get() << "\n";);
poly* new_p = pr.m_poly.get();
auto it = std::find_if(p_non_null.begin(), p_non_null.end(),
[this, new_p](const poly* q){
return m_pm.eq(q, new_p);
});
if (it == p_non_null.end())
p_non_null.push_back(new_p);
p_non_null.insert(pr.m_poly.get());
}
}
collect_E(p_non_null);
collect_E(p_non_null.m_set);
// todo: this order needs to be abstracted: it does not have to be linear.
// We need a boolean function E_rel(a, b)
@ -995,12 +989,10 @@ or
SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ;
polynomial_ref r(m_pm);
enable_trace("lws");
r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):";
::nlsat::display(tout, m_solver, a) << "\n";
::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");
disable_trace("lws");
if (m_pm.is_zero(r)) {
TRACE(lws, tout << "fail\n";);
fail();

75
src/nlsat/nlsat_common.cpp
View file

@ -18,6 +18,81 @@ Revision History:
--*/
#include "nlsat/nlsat_common.h"
namespace nlsat {
todo_set::todo_set(polynomial::cache& u, bool canonicalize): m_cache(u), m_set(u.pm()), m_canonicalize(canonicalize) {}
void todo_set::reset() {
pmanager& pm = m_set.m();
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
m_in_set[pm.id(m_set.get(i))] = false;
}
m_set.reset();
}
void todo_set::insert(poly* p) {
pmanager& pm = m_set.m();
if (m_canonicalize) {
// Canonicalize content+sign so scalar multiples share the same representative.
if (!pm.is_zero(p) && !pm.is_const(p)) {
polynomial_ref prim(pm);
var x = pm.max_var(p);
pm.primitive(p, x, prim);
p = prim.get();
}
p = pm.flip_sign_if_lm_neg(p);
}
p = m_cache.mk_unique(p);
unsigned pid = pm.id(p);
if (m_in_set.get(pid, false))
return;
m_in_set.setx(pid, true, false);
m_set.push_back(p);
}
bool todo_set::empty() const { return m_set.empty(); }
// Return max variable in todo_set
var todo_set::max_var() const {
pmanager& pm = m_set.m();
var max = null_var;
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
var x = pm.max_var(m_set.get(i));
SASSERT(x != null_var);
if (max == null_var || x > max)
max = x;
}
return max;
}
/**
\brief Remove the maximal polynomials from the set and store
them in max_polys. Return the maximal variable
*/
var todo_set::extract_max_polys(polynomial_ref_vector& max_polys) {
max_polys.reset();
var x = max_var();
pmanager& pm = m_set.m();
unsigned sz = m_set.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
poly* p = m_set.get(i);
var y = pm.max_var(p);
SASSERT(y <= x);
if (y == x) {
max_polys.push_back(p);
m_in_set[pm.id(p)] = false;
}
else {
m_set.set(j, p);
j++;
}
}
m_set.shrink(j);
return x;
}
/**
\brief Wrapper for factorization
*/

23
src/nlsat/nlsat_common.h
View file

@ -20,6 +20,29 @@
namespace nlsat {
// Lightweight set of polynomials that keeps elements unique (by cache id) and
// supports extracting all polynomials whose maximal variable is maximal.
// Optional canonicalization (primitive + sign) can be enabled per instance.
struct todo_set {
polynomial::cache& m_cache;
polynomial_ref_vector m_set;
svector<char> m_in_set;
bool m_canonicalize;
todo_set(polynomial::cache& u, bool canonicalize = false);
void reset();
void insert(poly* p);
bool empty() const;
// Return max variable in todo_set
var max_var() const;
/**
\brief Remove the maximal polynomials from the set and store
them in max_polys. Return the maximal variable
*/
var extract_max_polys(polynomial_ref_vector& max_polys);
};
inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) {
pm.display(out, p, proc);
return out;

70
src/nlsat/nlsat_explain.cpp
View file

@ -55,76 +55,6 @@ namespace nlsat {
assignment const & sample() const { return m_solver.sample(); }
assignment & sample() { return m_solver.sample(); }
struct todo_set {
polynomial::cache & m_cache;
polynomial_ref_vector m_set;
svector<char> m_in_set;
todo_set(polynomial::cache & u):m_cache(u), m_set(u.pm()) {}
void reset() {
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
m_in_set[pm.id(m_set.get(i))] = false;
}
m_set.reset();
}
void insert(poly * p) {
pmanager & pm = m_set.m();
p = m_cache.mk_unique(p);
unsigned pid = pm.id(p);
if (m_in_set.get(pid, false))
return;
m_in_set.setx(pid, true, false);
m_set.push_back(p);
}
bool empty() const { return m_set.empty(); }
// Return max variable in todo_set
var max_var() const {
pmanager & pm = m_set.m();
var max = null_var;
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
var x = pm.max_var(m_set.get(i));
SASSERT(x != null_var);
if (max == null_var || x > max)
max = x;
}
return max;
}
/**
\brief Remove the maximal polynomials from the set and store
them in max_polys. Return the maximal variable
*/
var extract_max_polys(polynomial_ref_vector & max_polys) {
max_polys.reset();
var x = max_var();
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
poly * p = m_set.get(i);
var y = pm.max_var(p);
SASSERT(y <= x);
if (y == x) {
max_polys.push_back(p);
m_in_set[pm.id(p)] = false;
}
else {
m_set.set(j, p);
j++;
}
}
m_set.shrink(j);
return x;
}
};
// temporary field for store todo set of polynomials
todo_set m_todo;