diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 435c0f6b7..6d5351c25 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -52,8 +52,8 @@ namespace nlsat { // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser. std::vector> m_prop_dom; - assignment const& sample() const { return m_solver.get_assignment();} - assignment & sample() { return m_solver.get_assignment(); } + assignment const& sample() const { return m_solver.sample();} + assignment & sample() { return m_solver.sample(); } // 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) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index d78b88c98..aa56f78a9 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -52,8 +52,8 @@ namespace nlsat { bool m_add_zero_disc; bool m_cell_sample; - assignment const & sample() const { return m_solver.get_assignment(); } - assignment & sample() { return m_solver.get_assignment(); } + assignment const & sample() const { return m_solver.sample(); } + assignment & sample() { return m_solver.sample(); } struct todo_set { polynomial::cache & m_cache; @@ -514,7 +514,7 @@ namespace nlsat { if (max_var(p) == max) elim_vanishing(p); // eliminate vanishing coefficients of 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)) { SASSERT(max_var(p) != null_var); SASSERT(max_var(p) < max); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index abe222362..c0ecd97d3 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -4348,11 +4348,11 @@ namespace nlsat { nlsat_params::collect_param_descrs(d); } - const assignment &solver::get_assignment() const { + const assignment &solver::sample() const { return m_imp->m_assignment; } - assignment &solver::get_assignment() { + assignment &solver::sample() { return m_imp->m_assignment; } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index a3656590d..67335a2c8 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -244,8 +244,8 @@ namespace nlsat { // ----------------------- void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - const assignment& get_assignment() const; - assignment& get_assignment(); + const assignment& sample() const; + assignment& sample(); void reset(); void collect_statistics(statistics & st);