mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-03 15:47:55 +00:00
Code Activity

use polynomial_ref instead of poly*

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-05 18:51:45 -10:00
parent 412ed2aa7f
commit e8ac85293c
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/nlsat/levelwise.cpp
View file

@ -134,7 +134,7 @@ namespace nlsat {
struct root_function { struct root_function {
scoped_anum val; scoped_anum val;
indexed_root_expr ire; indexed_root_expr ire;
root_function(anum_manager& am, poly* p, unsigned idx, anum const& v) root_function(anum_manager& am, polynomial_ref p, unsigned idx, anum const& v)
: val(am), ire{ p, idx } { am.set(val, v); } : val(am), ire{ p, idx } { am.set(val, v); }
root_function(root_function&& other) noexcept : val(other.val.m()), ire(other.ire) { val = other.val; } root_function(root_function&& other) noexcept : val(other.val.m()), ire(other.ire) { val = other.val; }
root_function(root_function const&) = delete; root_function(root_function const&) = delete;
@ -223,7 +223,7 @@ namespace nlsat {
prepare the initial properties prepare the initial properties
*/ */
// Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
void collect_top_level_properties(std::vector<poly*> & ps_of_n_level) { void collect_top_level_properties(polynomial_ref_vector & ps_of_n_level) {
for (unsigned i = 0; i < m_P.size(); ++i) { for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_P[i]; poly* p = m_P[i];
polynomial_ref pref(p, m_pm); polynomial_ref pref(p, m_pm);
@ -245,7 +245,7 @@ namespace nlsat {
} }
// isolate and collect algebraic roots for the given polynomials // isolate and collect algebraic roots for the given polynomials
void collect_roots_for_ps(std::vector<poly*> const & ps_of_n_level, std::vector<std::pair<scoped_anum, poly*>> & root_vals) { 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) { for (poly * p : ps_of_n_level) {
scoped_anum_vector roots(m_am); scoped_anum_vector roots(m_am);
m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(sample(), m_n), roots); m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(sample(), m_n), roots);
@ -317,7 +317,7 @@ namespace nlsat {
∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent root functions }. ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent root functions }.
*/ */
void init_properties() { void init_properties() {
std::vector<poly*> ps_of_n_level; polynomial_ref_vector ps_of_n_level(m_pm);
collect_top_level_properties(ps_of_n_level); collect_top_level_properties(ps_of_n_level);
std::vector<std::pair<scoped_anum, poly*>> root_vals; std::vector<std::pair<scoped_anum, poly*>> root_vals;
collect_roots_for_ps(ps_of_n_level, root_vals); collect_roots_for_ps(ps_of_n_level, root_vals);
@ -415,7 +415,7 @@ namespace nlsat {
// Part B of construct_interval: build (I, E, ≼) representation for level i // Part B of construct_interval: build (I, E, ≼) representation for level i
void build_representation() { void build_representation() {
// collect non-null polynomials (up to polynomial_manager equality) // collect non-null polynomials (up to polynomial_manager equality)
std::vector<const poly*> p_non_null; polynomial::polynomial_ref_vector p_non_null(m_pm);
for (auto & pr: m_Q[m_level]) { for (auto & pr: m_Q[m_level]) {
if (!pr.m_poly) continue; if (!pr.m_poly) continue;
SASSERT(max_var(pr.m_poly) == m_level); SASSERT(max_var(pr.m_poly) == m_level);
@ -482,12 +482,14 @@ namespace nlsat {
} }
// Step 1a: collect E the set of root functions on m_level // Step 1a: collect E the set of root functions on m_level
void collect_E(std::vector<const poly*> const& p_non_null) { void collect_E(polynomial_ref_vector & p_non_null) {
TRACE(lws, tout << "enter\n";); TRACE(lws, tout << "enter\n";);
m_rel.clear(); m_rel.clear();
for (auto const* p0 : p_non_null) { for (unsigned i = 0; i < p_non_null.size(); i++) {
auto* p = const_cast<poly*>(p0);
polynomial_ref p(m_pm);
p = p_non_null.get(i);
if (m_pm.max_var(p) != m_level) { if (m_pm.max_var(p) != m_level) {
TRACE(lws, ::nlsat::display(tout << "strange, skipping p:", m_solver, p) << "\n";); TRACE(lws, ::nlsat::display(tout << "strange, skipping p:", m_solver, p) << "\n";);
continue; continue;

2
src/nlsat/levelwise.h
View file

@ -9,7 +9,7 @@ namespace nlsat {
class levelwise { class levelwise {
public: public:
struct indexed_root_expr { struct indexed_root_expr {
poly* p; polynomial_ref p;
unsigned i; unsigned i;
}; };
struct root_function_interval { struct root_function_interval {