mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

refactor

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-15 11:44:57 -07:00
parent 56adbe3c12
commit 4acdd952c2
6 changed files with 119 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/nlsat/levelwise.cpp
View file

@ -6,7 +6,7 @@
#include <map> #include <map>
#include <algorithm> #include <algorithm>
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
#include "nlsat_pp.h" #include "nlsat_common.h"
namespace nlsat { namespace nlsat {
// Local enums reused from previous scaffolding // Local enums reused from previous scaffolding
@ -41,7 +41,6 @@ namespace nlsat {
solver& m_solver; solver& m_solver;
polynomial_ref_vector const& m_P; polynomial_ref_vector const& m_P;
var m_n; var m_n;
assignment const& sample() { return m_solver.get_assignment();}
pmanager& m_pm; pmanager& m_pm;
anum_manager& m_am; anum_manager& m_am;
std::vector<property> m_Q; // the set of properties to prove as in single_cell std::vector<property> m_Q; // the set of properties to prove as in single_cell
@ -52,6 +51,10 @@ namespace nlsat {
// Transitive closure matrix: dom[a][b] == true iff a ▹ b (a strictly dominates b). // Transitive closure matrix: dom[a][b] == true iff a ▹ b (a strictly dominates b).
// Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser. // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser.
std::vector<std::vector<bool>> m_prop_dom; std::vector<std::vector<bool>> m_prop_dom;
assignment const& sample() const { return m_solver.get_assignment();}
assignment & sample() { return m_solver.get_assignment(); }
// max_x plays the role of n in algorith 1 of the levelwise paper. // max_x plays the role of n in algorith 1 of the levelwise paper.
impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am) impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)
: m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am) { : m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am) {
@ -181,12 +184,6 @@ namespace nlsat {
return ret; return ret;
} }
::sign sign(poly * p) {
polynomial_ref pr(p, m_P.m());
auto s = m_am.eval_sign_at(pr, sample());
TRACE(levelwise, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";);
return s;
}
result_struct construct_interval() { result_struct construct_interval() {
result_struct ret; result_struct ret;
@ -212,7 +209,7 @@ namespace nlsat {
std::vector<const poly*> p_non_null; std::vector<const poly*> p_non_null;
for (const auto & pr: m_Q) { for (const auto & pr: m_Q) {
if (pr.prop == prop_enum::sgn_inv_irreducible && m_pm.max_var(pr.p) < m_i && sign(pr.p) != 0) if (pr.prop == prop_enum::sgn_inv_irreducible && m_pm.max_var(pr.p) < m_i && sign(polynomial_ref(pr.p, m_pm), sample(), m_am) != 0)
p_non_null.push_back(pr.p); p_non_null.push_back(pr.p);
} }

71
src/nlsat/nlsat_common.h Normal file
View file

@ -0,0 +1,71 @@
/*++
Copyright (c) 2025
Module Name:
nlsat_common.h
Abstract:
Pretty-print helpers for NLSAT components as free functions.
These forward to existing solver/pmanager display facilities.
--*/
#pragma once
#include "nlsat/nlsat_solver.h"
#include "nlsat/nlsat_scoped_literal_vector.h"
namespace nlsat {
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;
}
inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref_vector const& ps, display_var_proc const& proc, char const* delim = "\n") {
for (unsigned i = 0; i < ps.size(); ++i) {
if (i > 0) out << delim;
pm.display(out, ps.get(i), proc);
}
return out;
}
inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref const& p) {
return display(out, s.pm(), p, s.display_proc());
}
inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref_vector const& ps, char const* delim = "\n") {
return display(out, s.pm(), ps, s.display_proc(), delim);
}
inline std::ostream& display(std::ostream& out, solver& s, literal l) {
return s.display(out, l);
}
inline std::ostream& display(std::ostream& out, solver& s, unsigned n, literal const* ls) {
return s.display(out, n, ls);
}
inline std::ostream& display(std::ostream& out, solver& s, literal_vector const& ls) {
return s.display(out, ls);
}
inline std::ostream& display(std::ostream& out, solver& s, scoped_literal_vector const& ls) {
return s.display(out, ls.size(), ls.data());
}
inline std::ostream& display_var(std::ostream& out, solver& s, var x) {
return s.display(out, x);
}
/**
\brief evaluate the given polynomial in the current interpretation.
max_var(p) must be assigned in the current interpretation.
*/
inline ::sign sign(polynomial_ref const & p, assignment & x2v, anum_manager& am) {
SASSERT(max_var(p) == null_var || x2v.is_assigned(max_var(p)));
auto s = am.eval_sign_at(p, x2v);
TRACE(nlsat_explain, tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
return s;
}
} // namespace nlsat

77
src/nlsat/nlsat_explain.cpp
View file

@ -21,7 +21,7 @@ Revision History:
#include "nlsat/nlsat_assignment.h" #include "nlsat/nlsat_assignment.h"
#include "nlsat/nlsat_evaluator.h" #include "nlsat/nlsat_evaluator.h"
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
#include "nlsat/nlsat_pp.h" #include "nlsat/nlsat_common.h"
#include "util/ref_buffer.h" #include "util/ref_buffer.h"
namespace nlsat { namespace nlsat {
@ -31,7 +31,6 @@ namespace nlsat {
struct explain::imp { struct explain::imp {
solver & m_solver; solver & m_solver;
assignment const & m_assignment;
atom_vector const & m_atoms; atom_vector const & m_atoms;
atom_vector const & m_x2eq; atom_vector const & m_x2eq;
anum_manager & m_am; anum_manager & m_am;
@ -49,6 +48,8 @@ namespace nlsat {
bool m_signed_project; bool m_signed_project;
bool m_cell_sample; bool m_cell_sample;
assignment const & sample() const { return m_solver.get_assignment(); }
assignment & sample() { return m_solver.get_assignment(); }
struct todo_set { struct todo_set {
polynomial::cache & m_cache; polynomial::cache & m_cache;
@ -136,7 +137,6 @@ namespace nlsat {
imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev, bool is_sample): evaluator & ev, bool is_sample):
m_solver(s), m_solver(s),
m_assignment(x2v),
m_atoms(atoms), m_atoms(atoms),
m_x2eq(x2eq), m_x2eq(x2eq),
m_am(x2v.am()), m_am(x2v.am()),
@ -159,7 +159,7 @@ namespace nlsat {
m_signed_project = false; m_signed_project = false;
} }
// display helpers moved to free functions in nlsat_pp.h // display helpers moved to free functions in nlsat_common.h
/** /**
\brief Add literal to the result vector. \brief Add literal to the result vector.
@ -188,17 +188,6 @@ namespace nlsat {
} }
/**
\brief evaluate the given polynomial in the current interpretation.
max_var(p) must be assigned in the current interpretation.
*/
::sign sign(polynomial_ref const & p) {
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
auto s = m_am.eval_sign_at(p, m_assignment);
TRACE(nlsat_explain, tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
return s;
}
/** /**
\brief Wrapper for factorization \brief Wrapper for factorization
*/ */
@ -275,7 +264,7 @@ namespace nlsat {
polynomial_ref f(m_pm); polynomial_ref f(m_pm);
for (unsigned i = 0; i < num_factors; i++) { for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i); f = m_factors.get(i);
if (is_zero(sign(f))) { if (is_zero(sign(f, m_solver.get_assignment(), m_am))) {
m_zero_fs.push_back(m_factors.get(i)); m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false); m_is_even.push_back(false);
} }
@ -332,7 +321,7 @@ namespace nlsat {
lc = m_pm.coeff(p, x, k, reduct); lc = m_pm.coeff(p, x, k, reduct);
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";); TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
if (!is_zero(lc)) { if (!is_zero(lc)) {
if (!::is_zero(sign(lc))) { if (!::is_zero(sign(lc, m_solver.get_assignment(), m_am))) {
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";); TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return; return;
} }
@ -420,7 +409,7 @@ namespace nlsat {
if (max_var(p) == max) if (max_var(p) == max)
elim_vanishing(p); // eliminate vanishing coefficients of max elim_vanishing(p); // eliminate vanishing coefficients of max
if (is_const(p) || max_var(p) < max) { if (is_const(p) || max_var(p) < max) {
int s = sign(p); int s = sign(p, m_solver.get_assignment(), m_am);
if (!is_const(p)) { if (!is_const(p)) {
SASSERT(max_var(p) != null_var); SASSERT(max_var(p) != null_var);
SASSERT(max_var(p) < max); SASSERT(max_var(p) < max);
@ -617,7 +606,7 @@ namespace nlsat {
continue; continue;
// p depends on x // p depends on x
disc_poly = discriminant(p, x); // Use global helper disc_poly = discriminant(p, x); // Use global helper
if (sign(disc_poly) == 0) { // Discriminant is zero if (sign(disc_poly, sample(), m_am) == 0) { // Discriminant is zero
TRACE(nlsat_explain, tout << "p is not square free:\n "; TRACE(nlsat_explain, tout << "p is not square free:\n ";
display(tout, m_solver, p); tout << "\ndiscriminant: "; display(tout, m_solver, disc_poly) << "\n"; display(tout, m_solver, p); tout << "\ndiscriminant: "; display(tout, m_solver, disc_poly) << "\n";
m_solver.display_assignment(tout) << '\n'; m_solver.display_assignment(tout) << '\n';
@ -696,7 +685,7 @@ namespace nlsat {
auto c = polynomial_ref(this->m_pm); auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; j++) { for (unsigned j = 0; j <= n; j++) {
c = m_pm.coeff(s, x, j); c = m_pm.coeff(s, x, j);
SASSERT(sign(c) == 0); SASSERT(sign(c, sample(), m_am) == 0);
ensure_sign(c); ensure_sign(c);
} }
return true; return true;
@ -709,7 +698,7 @@ namespace nlsat {
auto c = polynomial_ref(this->m_pm); auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; j++) { for (unsigned j = 0; j <= n; j++) {
c = m_pm.coeff(s, x, j); c = m_pm.coeff(s, x, j);
if (sign(c) != 0) if (sign(c, sample(), m_am) != 0)
return false; return false;
} }
return true; return true;
@ -741,7 +730,7 @@ namespace nlsat {
TRACE(nlsat_explain, tout << "done, psc is a constant\n";); TRACE(nlsat_explain, tout << "done, psc is a constant\n";);
return; return;
} }
if (is_zero(sign(s))) { if (is_zero(sign(s, sample(), m_am))) {
TRACE(nlsat_explain, tout << "psc vanished, adding zero assumption\n";); TRACE(nlsat_explain, tout << "psc vanished, adding zero assumption\n";);
add_zero_assumption(s); add_zero_assumption(s);
continue; continue;
@ -847,7 +836,7 @@ namespace nlsat {
} }
polynomial_ref c(m_pm); polynomial_ref c(m_pm);
c = m_pm.coeff(p, y, 1); c = m_pm.coeff(p, y, 1);
int s = sign(c); int s = sign(c, sample(), m_am);
if (s == 0) { if (s == 0) {
return false; return false;
} }
@ -880,7 +869,7 @@ namespace nlsat {
return false; return false;
} }
SASSERT(m_assignment.is_assigned(y)); SASSERT(sample().is_assigned(y));
polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm); polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm);
A = m_pm.coeff(p, y, 2); A = m_pm.coeff(p, y, 2);
B = m_pm.coeff(p, y, 1); B = m_pm.coeff(p, y, 1);
@ -929,7 +918,7 @@ namespace nlsat {
} }
return s; return s;
#else #else
int s = sign(p); int s = sign(p, sample(), m_am);
if (!is_const(p)) { if (!is_const(p)) {
TRACE(nlsat_explain, tout << p << "\n";); TRACE(nlsat_explain, tout << p << "\n";);
add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
@ -969,13 +958,13 @@ namespace nlsat {
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) { void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {
res.reset(); res.reset();
SASSERT(m_assignment.is_assigned(y)); SASSERT(sample().is_assigned(y));
bool lower_inf = true; bool lower_inf = true;
bool upper_inf = true; bool upper_inf = true;
scoped_anum_vector & roots = m_roots_tmp; scoped_anum_vector & roots = m_roots_tmp;
scoped_anum lower(m_am); scoped_anum lower(m_am);
scoped_anum upper(m_am); scoped_anum upper(m_am);
anum const & y_val = m_assignment.value(y); anum const & y_val = sample().value(y);
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, m_solver, y); tout << " -> "; TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, m_solver, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";); m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm); polynomial_ref p_lower(m_pm);
@ -989,9 +978,9 @@ namespace nlsat {
if (max_var(p) != y) if (max_var(p) != y)
continue; continue;
roots.reset(); roots.reset();
// Variable y is assigned in m_assignment. We must temporarily unassign it. // Variable y is assigned in asgnm. We must temporarily unassign it.
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial. // Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); m_am.isolate_roots(p, undef_var_assignment(sample(), y), roots);
unsigned num_roots = roots.size(); unsigned num_roots = roots.size();
bool all_lt = true; bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) { for (unsigned i = 0; i < num_roots; i++) {
@ -1072,13 +1061,13 @@ namespace nlsat {
! (y > root_i(p1)) or !(y < root_j(p2)) ! (y > root_i(p1)) or !(y < root_j(p2))
*/ */
void add_cell_lits(polynomial_ref_vector & ps, var y) { void add_cell_lits(polynomial_ref_vector & ps, var y) {
SASSERT(m_assignment.is_assigned(y)); SASSERT(sample().is_assigned(y));
bool lower_inf = true; bool lower_inf = true;
bool upper_inf = true; bool upper_inf = true;
scoped_anum_vector & roots = m_roots_tmp; scoped_anum_vector & roots = m_roots_tmp;
scoped_anum lower(m_am); scoped_anum lower(m_am);
scoped_anum upper(m_am); scoped_anum upper(m_am);
anum const & y_val = m_assignment.value(y); anum const & y_val = sample().value(y);
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, m_solver, y); tout << " -> "; TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, m_solver, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";); m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm); polynomial_ref p_lower(m_pm);
@ -1092,9 +1081,9 @@ namespace nlsat {
if (max_var(p) != y) if (max_var(p) != y)
continue; continue;
roots.reset(); roots.reset();
// Variable y is assigned in m_assignment. We must temporarily unassign it. // Variable y is assigned in asgnm. We must temporarily unassign it.
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial. // Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); m_am.isolate_roots(p, undef_var_assignment(sample(), y), roots);
unsigned num_roots = roots.size(); unsigned num_roots = roots.size();
bool all_lt = true; bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) { for (unsigned i = 0; i < num_roots; i++) {
@ -1228,7 +1217,7 @@ namespace nlsat {
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
levelwise lws(m_solver, ps, max_x, m_assignment, m_pm, m_am); levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am);
auto cell = lws.single_cell(); auto cell = lws.single_cell();
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);
@ -1382,7 +1371,7 @@ namespace nlsat {
} }
if (is_const(new_factor)) { if (is_const(new_factor)) {
TRACE(nlsat_simplify_core, tout << "new factor is const\n";); TRACE(nlsat_simplify_core, tout << "new factor is const\n";);
auto s = sign(new_factor); auto s = sign(new_factor, sample(), m_am);
if (is_zero(s)) { if (is_zero(s)) {
bool atom_val = a->get_kind() == atom::EQ; bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val; bool lit_val = l.sign() ? !atom_val : atom_val;
@ -1465,7 +1454,7 @@ namespace nlsat {
polynomial_ref lc_eq(m_pm); polynomial_ref lc_eq(m_pm);
lc_eq = m_pm.coeff(eq, info.m_x, info.m_k); lc_eq = m_pm.coeff(eq, info.m_x, info.m_k);
info.m_lc = lc_eq.get(); info.m_lc = lc_eq.get();
info.m_lc_sign = sign(lc_eq); info.m_lc_sign = sign(lc_eq, sample(), m_am);
info.m_lc_add = false; info.m_lc_add = false;
info.m_lc_add_ineq = false; info.m_lc_add_ineq = false;
info.m_lc_const = m_pm.is_const(lc_eq); info.m_lc_const = m_pm.is_const(lc_eq);
@ -1852,7 +1841,7 @@ namespace nlsat {
unsigned eq_degree = 0; unsigned eq_degree = 0;
for (unsigned i = 0; i < ps.size(); ++i) { for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i); p = ps.get(i);
int s = sign(p); int s = sign(p, sample(), m_am);
if (max_var(p) != x) { if (max_var(p) != x) {
atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT)); atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
add_simple_assumption(k, p, false); add_simple_assumption(k, p, false);
@ -1896,7 +1885,7 @@ namespace nlsat {
if (j == eq_index) if (j == eq_index)
continue; continue;
p = ps.get(j); p = ps.get(j);
int s = sign(p); int s = sign(p, sample(), m_am);
atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT)); atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
add_simple_assumption(k, p, false); add_simple_assumption(k, p, false);
} }
@ -1907,13 +1896,13 @@ namespace nlsat {
unsigned num_lub = 0, num_glb = 0; unsigned num_lub = 0, num_glb = 0;
unsigned glb_index = 0, lub_index = 0; unsigned glb_index = 0, lub_index = 0;
scoped_anum lub(m_am), glb(m_am), x_val(m_am); scoped_anum lub(m_am), glb(m_am), x_val(m_am);
x_val = m_assignment.value(x); x_val = sample().value(x);
bool glb_valid = false, lub_valid = false; bool glb_valid = false, lub_valid = false;
for (unsigned i = 0; i < ps.size(); ++i) { for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i); p = ps.get(i);
scoped_anum_vector & roots = m_roots_tmp; scoped_anum_vector & roots = m_roots_tmp;
roots.reset(); roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots);
for (auto const& r : roots) { for (auto const& r : roots) {
int s = m_am.compare(x_val, r); int s = m_am.compare(x_val, r);
SASSERT(s != 0); SASSERT(s != 0);
@ -1959,7 +1948,7 @@ namespace nlsat {
unsigned d = degree(p, x); unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d); lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) { if (!is_const(lc)) {
int s = sign(p); int s = sign(p, sample(), m_am);
SASSERT(s != 0); SASSERT(s != 0);
atom::kind k = (s > 0)?(atom::GT):(atom::LT); atom::kind k = (s > 0)?(atom::GT):(atom::LT);
add_simple_assumption(k, lc); add_simple_assumption(k, lc);
@ -1974,7 +1963,7 @@ namespace nlsat {
unsigned d = degree(p, x); unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d); lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) { if (!is_const(lc)) {
int s = sign(p); int s = sign(p, sample(), m_am);
TRACE(nlsat_explain, tout << "degree: " << d << " " << lc << " sign: " << s << "\n";); TRACE(nlsat_explain, tout << "degree: " << d << " " << lc << " sign: " << s << "\n";);
SASSERT(s != 0); SASSERT(s != 0);
atom::kind k; atom::kind k;
@ -2063,12 +2052,12 @@ namespace nlsat {
collect_polys(lits.size(), lits.data(), m_ps); collect_polys(lits.size(), lits.data(), m_ps);
unbounded = true; unbounded = true;
scoped_anum x_val(m_am); scoped_anum x_val(m_am);
x_val = m_assignment.value(x); x_val = sample().value(x);
for (unsigned i = 0; i < m_ps.size(); ++i) { for (unsigned i = 0; i < m_ps.size(); ++i) {
p = m_ps.get(i); p = m_ps.get(i);
scoped_anum_vector & roots = m_roots_tmp; scoped_anum_vector & roots = m_roots_tmp;
roots.reset(); roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots);
for (unsigned j = 0; j < roots.size(); ++j) { for (unsigned j = 0; j < roots.size(); ++j) {
int s = m_am.compare(x_val, roots[j]); int s = m_am.compare(x_val, roots[j]);
if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) { if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) {

61
src/nlsat/nlsat_pp.h
View file

@ -1,61 +0,0 @@
/*++
Copyright (c) 2025
Module Name:
nlsat_pp.h
Abstract:
Pretty-print helpers for NLSAT components as free functions.
These forward to existing solver/pmanager display facilities.
--*/
#pragma once
#include "nlsat/nlsat_solver.h"
#include "nlsat/nlsat_scoped_literal_vector.h"
namespace nlsat {
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;
}
inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref_vector const& ps, display_var_proc const& proc, char const* delim = "\n") {
for (unsigned i = 0; i < ps.size(); ++i) {
if (i > 0) out << delim;
pm.display(out, ps.get(i), proc);
}
return out;
}
inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref const& p) {
return display(out, s.pm(), p, s.display_proc());
}
inline std::ostream& display(std::ostream& out, solver& s, polynomial_ref_vector const& ps, char const* delim = "\n") {
return display(out, s.pm(), ps, s.display_proc(), delim);
}
inline std::ostream& display(std::ostream& out, solver& s, literal l) {
return s.display(out, l);
}
inline std::ostream& display(std::ostream& out, solver& s, unsigned n, literal const* ls) {
return s.display(out, n, ls);
}
inline std::ostream& display(std::ostream& out, solver& s, literal_vector const& ls) {
return s.display(out, ls);
}
inline std::ostream& display(std::ostream& out, solver& s, scoped_literal_vector const& ls) {
return s.display(out, ls.size(), ls.data());
}
inline std::ostream& display_var(std::ostream& out, solver& s, var x) {
return s.display(out, x);
}
} // namespace nlsat

5
src/nlsat/nlsat_solver.cpp
View file

@ -4127,6 +4127,11 @@ namespace nlsat {
const assignment &solver::get_assignment() const { const assignment &solver::get_assignment() const {
return m_imp->m_assignment; return m_imp->m_assignment;
} }
assignment &solver::get_assignment() {
return m_imp->m_assignment;
}
unsynch_mpq_manager &solver::qm() unsynch_mpq_manager &solver::qm()
{ {
return m_imp->m_qm; return m_imp->m_qm;

2
src/nlsat/nlsat_solver.h
View file

@ -245,6 +245,8 @@ namespace nlsat {
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
const assignment& get_assignment() const; const assignment& get_assignment() const;
assignment& get_assignment();
void reset(); void reset();
void collect_statistics(statistics & st); void collect_statistics(statistics & st);
void reset_statistics(); void reset_statistics();