mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 20:46:01 +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:47:34 -07:00
parent 4acdd952c2
commit f74d1fc8ec
4 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -52,8 +52,8 @@ namespace nlsat {
// 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 const& sample() const { return m_solver.sample();}
assignment & sample() { return m_solver.get_assignment(); } assignment & sample() { return m_solver.sample(); }
// 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)

10
src/nlsat/nlsat_explain.cpp
View file

@ -48,8 +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 const & sample() const { return m_solver.sample(); }
assignment & sample() { return m_solver.get_assignment(); } assignment & sample() { return m_solver.sample(); }
struct todo_set { struct todo_set {
polynomial::cache & m_cache; polynomial::cache & m_cache;
@ -264,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, m_solver.get_assignment(), m_am))) { if (is_zero(sign(f, m_solver.sample(), 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);
} }
@ -321,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, m_solver.get_assignment(), m_am))) { if (!::is_zero(sign(lc, m_solver.sample(), m_am))) {
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";); TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return; return;
} }
@ -409,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, m_solver.get_assignment(), m_am); int s = sign(p, m_solver.sample(), 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);

4
src/nlsat/nlsat_solver.cpp
View file

@ -4124,11 +4124,11 @@ namespace nlsat {
nlsat_params::collect_param_descrs(d); nlsat_params::collect_param_descrs(d);
} }
const assignment &solver::get_assignment() const { const assignment &solver::sample() const {
return m_imp->m_assignment; return m_imp->m_assignment;
} }
assignment &solver::get_assignment() { assignment &solver::sample() {
return m_imp->m_assignment; return m_imp->m_assignment;
} }

4
src/nlsat/nlsat_solver.h
View file

@ -244,8 +244,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& sample() const;
assignment& get_assignment(); assignment& sample();
void reset(); void reset();
void collect_statistics(statistics & st); void collect_statistics(statistics & st);