mirror of
https://github.com/Z3Prover/z3
synced 2026-07-03 22:06:11 +00:00
remove dead code in nlsat_explain
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
cf6c8810ee
commit
e351266ecb
3 changed files with 0 additions and 178 deletions
|
|
@ -106,8 +106,6 @@ namespace nlsat {
|
||||||
/**
|
/**
|
||||||
* Check whether all coefficients of the polynomial `s` (viewed as a polynomial
|
* Check whether all coefficients of the polynomial `s` (viewed as a polynomial
|
||||||
* in its main variable) evaluate to zero under the given assignment `x2v`.
|
* 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) {
|
inline bool coeffs_are_zeroes_on_sample(polynomial_ref const & s, pmanager & pm, assignment & x2v, anum_manager & am) {
|
||||||
polynomial_ref c(pm);
|
polynomial_ref c(pm);
|
||||||
|
|
|
||||||
|
|
@ -40,7 +40,6 @@ namespace nlsat {
|
||||||
polynomial::cache & m_cache;
|
polynomial::cache & m_cache;
|
||||||
pmanager & m_pm;
|
pmanager & m_pm;
|
||||||
polynomial_ref_vector m_ps;
|
polynomial_ref_vector m_ps;
|
||||||
polynomial_ref_vector m_ps2;
|
|
||||||
polynomial_ref_vector m_psc_tmp;
|
polynomial_ref_vector m_psc_tmp;
|
||||||
polynomial_ref_vector m_factors, m_factors_save;
|
polynomial_ref_vector m_factors, m_factors_save;
|
||||||
scoped_anum_vector m_roots_tmp;
|
scoped_anum_vector m_roots_tmp;
|
||||||
|
|
@ -85,7 +84,6 @@ namespace nlsat {
|
||||||
m_cache(u),
|
m_cache(u),
|
||||||
m_pm(u.pm()),
|
m_pm(u.pm()),
|
||||||
m_ps(m_pm),
|
m_ps(m_pm),
|
||||||
m_ps2(m_pm),
|
|
||||||
m_psc_tmp(m_pm),
|
m_psc_tmp(m_pm),
|
||||||
m_factors(m_pm),
|
m_factors(m_pm),
|
||||||
m_factors_save(m_pm),
|
m_factors_save(m_pm),
|
||||||
|
|
@ -166,8 +164,6 @@ namespace nlsat {
|
||||||
/**
|
/**
|
||||||
\brief Add literal p != 0 into m_result.
|
\brief Add literal p != 0 into m_result.
|
||||||
*/
|
*/
|
||||||
ptr_vector<poly> m_zero_fs;
|
|
||||||
bool_vector m_is_even;
|
|
||||||
struct restore_factors {
|
struct restore_factors {
|
||||||
polynomial_ref_vector& m_factors, &m_factors_save;
|
polynomial_ref_vector& m_factors, &m_factors_save;
|
||||||
unsigned num_saved = 0;
|
unsigned num_saved = 0;
|
||||||
|
|
@ -589,25 +585,6 @@ namespace nlsat {
|
||||||
return max;
|
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
|
\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
|
\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.
|
\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 {
|
bool check_already_added() const {
|
||||||
for (bool b : m_already_added_literal) {
|
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<literal> 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);
|
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) {
|
void explain::display_last_lws_input(std::ostream& out) {
|
||||||
out << "=== POLYNOMIALS PASSED TO LEVELWISE ===\n";
|
out << "=== POLYNOMIALS PASSED TO LEVELWISE ===\n";
|
||||||
for (unsigned i = 0; i < m_imp->m_last_lws_input_polys.size(); i++) {
|
for (unsigned i = 0; i < m_imp->m_last_lws_input_polys.size(); i++) {
|
||||||
|
|
|
||||||
|
|
@ -97,18 +97,6 @@ namespace nlsat {
|
||||||
*/
|
*/
|
||||||
void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result);
|
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).
|
Print the polynomials that were passed to levelwise in the last call (for debugging).
|
||||||
*/
|
*/
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue