diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h index 9a3949533..360180c4a 100644 --- a/src/nlsat/nlsat_common.h +++ b/src/nlsat/nlsat_common.h @@ -106,8 +106,6 @@ namespace nlsat { /** * Check whether all coefficients of the polynomial `s` (viewed as a polynomial * in its main variable) evaluate to zero under the given assignment `x2v`. - * This is exactly the logic used in several places in the nlsat codebase - * (e.g. coeffs_are_zeroes_in_factor in nlsat_explain.cpp). */ inline bool coeffs_are_zeroes_on_sample(polynomial_ref const & s, pmanager & pm, assignment & x2v, anum_manager & am) { polynomial_ref c(pm); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 1555e2989..d9a0bf131 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -40,7 +40,6 @@ namespace nlsat { polynomial::cache & m_cache; pmanager & m_pm; polynomial_ref_vector m_ps; - polynomial_ref_vector m_ps2; polynomial_ref_vector m_psc_tmp; polynomial_ref_vector m_factors, m_factors_save; scoped_anum_vector m_roots_tmp; @@ -85,7 +84,6 @@ namespace nlsat { m_cache(u), m_pm(u.pm()), m_ps(m_pm), - m_ps2(m_pm), m_psc_tmp(m_pm), m_factors(m_pm), m_factors_save(m_pm), @@ -166,8 +164,6 @@ namespace nlsat { /** \brief Add literal p != 0 into m_result. */ - ptr_vector m_zero_fs; - bool_vector m_is_even; struct restore_factors { polynomial_ref_vector& m_factors, &m_factors_save; unsigned num_saved = 0; @@ -589,25 +585,6 @@ namespace nlsat { return max; } - /** - \brief Move the polynomials in q in ps that do not contain x to qs. - */ - void keep_p_x(polynomial_ref_vector & ps, var x, polynomial_ref_vector & qs) { - unsigned sz = ps.size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; ++i) { - poly * q = ps.get(i); - if (max_var(q) != x) { - qs.push_back(q); - } - else { - ps.set(j, q); - j++; - } - } - ps.shrink(j); - } - /** \brief Add factors of p to todo */ @@ -680,48 +657,6 @@ namespace nlsat { } } - // this function also explains the value 0, if met - bool coeffs_are_zeroes(polynomial_ref &s) { - restore_factors _restore(m_factors, m_factors_save); - factor(s, m_cache, m_factors); - unsigned num_factors = m_factors.size(); - m_zero_fs.reset(); - m_is_even.reset(); - polynomial_ref f(m_pm); - bool have_zero = false; - for (unsigned i = 0; i < num_factors; ++i) { - f = m_factors.get(i); - if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) { - have_zero = true; - break; - } - } - if (!have_zero) - return false; - var x = max_var(f); - unsigned n = degree(f, x); - auto c = polynomial_ref(this->m_pm); - for (unsigned j = 0; j <= n; ++j) { - c = m_pm.coeff(s, x, j); - SASSERT(sign(c) == 0); - ensure_sign(c); - } - return true; - } - - - bool coeffs_are_zeroes_in_factor(polynomial_ref & s) { - var x = max_var(s); - unsigned n = degree(s, x); - auto c = polynomial_ref(this->m_pm); - for (unsigned j = 0; j <= n; ++j) { - c = m_pm.coeff(s, x, j); - if (nlsat::sign(c, sample(), m_am) != 0) - return false; - } - return true; - } - /** \brief Add v-psc(p, q, x) into m_todo */ @@ -987,40 +922,6 @@ namespace nlsat { } } - - /** - Add one or two literals that specify in which cell of variable y the current interpretation is. - One literal is added for the cases: - - y in (-oo, min) where min is the minimal root of the polynomials p2 in ps - We add literal - ! (y < root_1(p2)) - - y in (max, oo) where max is the maximal root of the polynomials p1 in ps - We add literal - ! (y > root_k(p1)) where k is the number of real roots of p - - y = r where r is the k-th root of a polynomial p in ps - We add literal - ! (y = root_k(p)) - Two literals are added when - - y in (l, u) where (l, u) does not contain any root of polynomials p in ps, and - l is the i-th root of a polynomial p1 in ps, and u is the j-th root of a polynomial p2 in ps. - We add literals - ! (y > root_i(p1)) or !(y < root_j(p2)) - */ - void add_cell_lits(polynomial_ref_vector & ps, var y) { - cell_root_info info(m_pm); - find_cell_roots(ps, y, info); - if (info.m_has_eq) { - add_root_literal(atom::ROOT_EQ, y, info.m_eq_idx, info.m_eq); - return; - } - if (info.m_has_lower) { - add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, info.m_lower_idx, info.m_lower); - } - if (info.m_has_upper) { - add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, info.m_upper_idx, info.m_upper); - } - } - /** \brief Return true if all polynomials in ps are univariate in x. */ @@ -1142,19 +1043,6 @@ namespace nlsat { } - /** - * \brief compute the resultants of p with each polynomial in ps w.r.t. x - */ - void psc_resultants_with(polynomial_ref_vector const& ps, polynomial_ref p, var const x) { - polynomial_ref q(m_pm); - unsigned sz = ps.size(); - for (unsigned i = 0; i < sz; i++) { - q = ps.get(i); - if (q == p) continue; - psc(p, q, x); - } - } - bool check_already_added() const { for (bool b : m_already_added_literal) { @@ -1828,55 +1716,7 @@ namespace nlsat { } } } - - - void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) { - TRACE(nlsat_explain, tout << "project pairs\n";); - polynomial_ref p(m_pm); - p = ps.get(idx); - for (unsigned i = 0; i < ps.size(); ++i) { - if (i != idx) { - project_pair(x, ps.get(i), p); - } - } - } - void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) { - m_ps2.reset(); - m_ps2.push_back(p1); - m_ps2.push_back(p2); - project(m_ps2, x); - } - - void project_single(var x, polynomial::polynomial* p) { - m_ps2.reset(); - m_ps2.push_back(p); - project(m_ps2, x); - } - - - void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) { - svector lits; - polynomial_ref p(m_pm); - split_literals(x, num, ls, lits); - collect_polys(lits.size(), lits.data(), m_ps); - unbounded = true; - scoped_anum x_val(m_am); - x_val = sample().value(x); - for (unsigned i = 0; i < m_ps.size(); ++i) { - p = m_ps.get(i); - scoped_anum_vector & roots = m_roots_tmp; - roots.reset(); - m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots); - for (unsigned j = 0; j < roots.size(); ++j) { - int s = m_am.compare(x_val, roots[j]); - if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) { - unbounded = false; - val = roots[j]; - } - } - } - } }; @@ -1930,10 +1770,6 @@ namespace nlsat { m_imp->project(x, n, ls, result); } - void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) { - m_imp->maximize(x, n, ls, val, unbounded); - } - void explain::display_last_lws_input(std::ostream& out) { out << "=== POLYNOMIALS PASSED TO LEVELWISE ===\n"; for (unsigned i = 0; i < m_imp->m_last_lws_input_polys.size(); i++) { diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index e33477a80..60a7c53e1 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -97,18 +97,6 @@ namespace nlsat { */ void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result); - /** - Maximize the value of x (locally) under the current assignment to other variables and - while maintaining the assignment to the literals ls. - Set unbounded to 'true' if the value of x is unbounded. - - Precondition: the set of literals are true in the current model. - - By local optimization we understand that x is increased to the largest value within - the signs delineated by the roots of the polynomials in ls. - */ - void maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded); - /** Print the polynomials that were passed to levelwise in the last call (for debugging). */