mirror of
https://github.com/Z3Prover/z3
synced 2025-08-26 13:06:05 +00:00
work on well-orientedness
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
b2f01706be
commit
945eef7ab6
9 changed files with 559 additions and 326 deletions
|
|
@ -94,7 +94,7 @@ namespace nlsat {
|
|||
\brief Remove the maximal polynomials from the set and store
|
||||
them in max_polys. Return the maximal variable
|
||||
*/
|
||||
var remove_max_polys(polynomial_ref_vector & max_polys) {
|
||||
var extract_max_polys(polynomial_ref_vector & max_polys) {
|
||||
max_polys.reset();
|
||||
var x = max_var();
|
||||
pmanager & pm = m_set.m();
|
||||
|
|
@ -333,7 +333,6 @@ namespace nlsat {
|
|||
polynomial_ref lc(m_pm);
|
||||
polynomial_ref reduct(m_pm);
|
||||
while (true) {
|
||||
TRACE(nlsat_explain, tout << "elim vanishing x" << x << " k:" << k << " " << p << "\n";);
|
||||
if (is_const(p))
|
||||
return;
|
||||
if (k == 0) {
|
||||
|
|
@ -342,16 +341,6 @@ namespace nlsat {
|
|||
SASSERT(x != null_var);
|
||||
k = degree(p, x);
|
||||
}
|
||||
#if 0
|
||||
anum const & x_val = m_assignment.value(x);
|
||||
if (m_am.is_zero(x_val)) {
|
||||
// add_zero_assumption(lc);
|
||||
lc = m_pm.coeff(p, x, k, reduct);
|
||||
k--;
|
||||
p = reduct;
|
||||
continue;
|
||||
}
|
||||
#endif
|
||||
if (m_pm.nonzero_const_coeff(p, x, k)) {
|
||||
TRACE(nlsat_explain, tout << "nonzero const x" << x << "\n";);
|
||||
return; // lc is a nonzero constant
|
||||
|
|
@ -359,16 +348,24 @@ namespace nlsat {
|
|||
lc = m_pm.coeff(p, x, k, reduct);
|
||||
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
|
||||
if (!is_zero(lc)) {
|
||||
if (!::is_zero(sign(lc)))
|
||||
if (!::is_zero(sign(lc))) {
|
||||
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
|
||||
return;
|
||||
}
|
||||
TRACE(nlsat_explain, tout << "got a zero sign on lc\n";);
|
||||
|
||||
|
||||
// lc is not the zero polynomial, but it vanished in the current interpretation.
|
||||
// so we keep searching...
|
||||
TRACE(nlsat_explain, tout << "adding zero assumption for var:"; m_solver.display_var(tout, x); tout << ", degree k:" << k << ", p:" ; display(tout, p) << "\n";);
|
||||
|
||||
add_zero_assumption(lc);
|
||||
}
|
||||
if (k == 0) {
|
||||
// all coefficients of p vanished in the current interpretation,
|
||||
// and were added as assumptions.
|
||||
p = m_pm.mk_zero();
|
||||
TRACE(nlsat_explain, tout << "all coefficients of p vanished\n";);
|
||||
return;
|
||||
}
|
||||
k--;
|
||||
|
|
@ -621,25 +618,57 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
|
||||
void add_sample_coeff(polynomial_ref_vector &ps, var x){
|
||||
polynomial_ref p(m_pm);
|
||||
polynomial_ref lc(m_pm);
|
||||
unsigned sz = ps.size();
|
||||
for (unsigned i = 0; i < sz; i++){
|
||||
p = ps.get(i);
|
||||
unsigned k = degree(p, x);
|
||||
SASSERT(k > 0);
|
||||
TRACE(nlsat_explain, tout << "add_lc, x: "; display_var(tout, x); tout << "\nk: " << k << "\n"; display(tout, p); tout << "\n";);
|
||||
for(; k > 0; k--){
|
||||
lc = m_pm.coeff(p, x, k);
|
||||
add_factors(lc);
|
||||
if (m_pm.nonzero_const_coeff(p, x, k)){
|
||||
TRACE(nlsat_explain, tout << "constant coefficient, skipping...\n";);
|
||||
break;
|
||||
}
|
||||
bool is_well_oriented(polynomial_ref_vector &ps, var x) {
|
||||
polynomial_ref p_poly(m_pm);
|
||||
polynomial_ref lc_poly(m_pm);
|
||||
polynomial_ref disc_poly(m_pm);
|
||||
polynomial_ref current_coeff_poly(m_pm);
|
||||
|
||||
for (unsigned i = 0; i < ps.size(); i++) {
|
||||
p_poly = ps.get(i);
|
||||
unsigned k_deg = m_pm.degree(p_poly, x);
|
||||
if (k_deg == 0)
|
||||
continue;
|
||||
// p_poly depends on x
|
||||
lc_poly = m_pm.coeff(p_poly, x, k_deg);
|
||||
if (sign(lc_poly) == 0) { // LC is zero
|
||||
TRACE(nlsat_explain, tout << "Global !WO: LC of poly is zero. Poly: "; display(tout, p_poly); tout << " LC: "; display(tout, lc_poly) << "\\n";);
|
||||
return false;
|
||||
}
|
||||
SASSERT(sign(lc) != 0);
|
||||
SASSERT(!is_const(lc));
|
||||
|
||||
disc_poly = discriminant(p_poly, x); // Use global helper
|
||||
if (sign(disc_poly) == 0) { // Discriminant is zero
|
||||
TRACE(nlsat_explain, tout << "Global !WO: Discriminant of poly is zero. Poly: "; display(tout, p_poly); tout << " Disc: "; display(tout, disc_poly) << "\\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// For each p in ps add the leading or all the coefficients of p to the projection,
|
||||
// depending on the well-orientedness of ps.
|
||||
void add_lcs(polynomial_ref_vector &ps, var x) {
|
||||
polynomial_ref p_poly(m_pm);
|
||||
polynomial_ref coeff(m_pm);
|
||||
polynomial_ref disc_poly(m_pm);
|
||||
|
||||
bool wo = is_well_oriented(ps, x);
|
||||
// Add coefficients based on well-orientedness
|
||||
for (unsigned i = 0; i < ps.size(); i++) {
|
||||
p_poly = ps.get(i);
|
||||
unsigned k_deg = m_pm.degree(p_poly, x);
|
||||
if (k_deg == 0) continue;
|
||||
// p_poly depends on x
|
||||
TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p_poly); tout << (wo ? " (wo)" : " (!wo)") << "\\n";);
|
||||
for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) {
|
||||
coeff = m_pm.coeff(p_poly, x, j_coeff_deg);
|
||||
TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\\n";);
|
||||
add_factors(coeff);
|
||||
if (wo)
|
||||
break;
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -659,35 +688,6 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Add leading coefficients of the polynomials in ps.
|
||||
|
||||
\pre all polynomials in ps contain x
|
||||
|
||||
Remark: the leading coefficients do not vanish in the current model,
|
||||
since all polynomials in ps were pre-processed using elim_vanishing.
|
||||
*/
|
||||
void add_lc(polynomial_ref_vector & ps, var x) {
|
||||
polynomial_ref p(m_pm);
|
||||
polynomial_ref lc(m_pm);
|
||||
unsigned sz = ps.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
p = ps.get(i);
|
||||
unsigned k = degree(p, x);
|
||||
SASSERT(k > 0);
|
||||
TRACE(nlsat_explain, tout << "add_lc, x: "; display_var(tout, x); tout << "\nk: " << k << "\n"; display(tout, p); tout << "\n";);
|
||||
if (m_pm.nonzero_const_coeff(p, x, k)) {
|
||||
TRACE(nlsat_explain, tout << "constant coefficient, skipping...\n";);
|
||||
continue;
|
||||
}
|
||||
lc = m_pm.coeff(p, x, k);
|
||||
SASSERT(sign(lc) != 0);
|
||||
SASSERT(!is_const(lc));
|
||||
add_factors(lc);
|
||||
}
|
||||
}
|
||||
|
||||
void add_zero_assumption_on_factor(polynomial_ref& f) {
|
||||
display(std::cout << "zero factors \n", f);
|
||||
}
|
||||
|
|
@ -1198,7 +1198,7 @@ namespace nlsat {
|
|||
for (poly* p : ps) {
|
||||
m_todo.insert(p);
|
||||
}
|
||||
var x = m_todo.remove_max_polys(ps);
|
||||
var x = m_todo.extract_max_polys(ps);
|
||||
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
|
||||
if (x < max_x)
|
||||
add_cell_lits(ps, x);
|
||||
|
|
@ -1207,14 +1207,15 @@ namespace nlsat {
|
|||
m_todo.reset();
|
||||
break;
|
||||
}
|
||||
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
|
||||
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x);
|
||||
tout << "\npolynomials\n";
|
||||
display(tout, ps); tout << "\n";);
|
||||
add_lc(ps, x);
|
||||
add_lcs(ps, x);
|
||||
psc_discriminant(ps, x);
|
||||
psc_resultant(ps, x);
|
||||
if (m_todo.empty())
|
||||
break;
|
||||
x = m_todo.remove_max_polys(ps);
|
||||
x = m_todo.extract_max_polys(ps);
|
||||
add_cell_lits(ps, x);
|
||||
}
|
||||
}
|
||||
|
|
@ -1229,12 +1230,12 @@ namespace nlsat {
|
|||
void project_cdcac(polynomial_ref_vector & ps, var max_x) {
|
||||
if (ps.empty())
|
||||
return;
|
||||
bool first = true;
|
||||
|
||||
m_todo.reset();
|
||||
for (poly* p : ps) {
|
||||
m_todo.insert(p);
|
||||
}
|
||||
var x = m_todo.remove_max_polys(ps);
|
||||
var x = m_todo.extract_max_polys(ps);
|
||||
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
|
||||
|
||||
polynomial_ref_vector samples(m_pm);
|
||||
|
|
@ -1251,23 +1252,13 @@ namespace nlsat {
|
|||
}
|
||||
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
|
||||
display(tout, ps); tout << "\n";);
|
||||
|
||||
if (first) {
|
||||
add_lc(ps, x);
|
||||
psc_discriminant(ps, x);
|
||||
psc_resultant(ps, x);
|
||||
first = false;
|
||||
}
|
||||
else {
|
||||
add_lc(ps, x);
|
||||
// add_sample_coeff(ps, x);
|
||||
psc_discriminant(ps, x);
|
||||
psc_resultant_sample(ps, x, samples);
|
||||
}
|
||||
add_lcs(ps, x);
|
||||
psc_discriminant(ps, x);
|
||||
psc_resultant(ps, x);
|
||||
|
||||
if (m_todo.empty())
|
||||
break;
|
||||
x = m_todo.remove_max_polys(ps);
|
||||
x = m_todo.extract_max_polys(ps);
|
||||
cac_add_cell_lits(ps, x, samples);
|
||||
}
|
||||
}
|
||||
|
|
@ -1426,12 +1417,10 @@ namespace nlsat {
|
|||
// If the leading coefficient is not a constant, we must store this information as an extra assumption.
|
||||
if (d % 2 == 0 || // d is even
|
||||
is_even || // rewriting a factor of even degree, sign flip doesn't matter
|
||||
_a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
|
||||
_a->get_kind() == atom::EQ) // rewriting an equation, sign flip doesn't matter
|
||||
info.add_lc_diseq();
|
||||
}
|
||||
else {
|
||||
else
|
||||
info.add_lc_ineq();
|
||||
}
|
||||
}
|
||||
if (s < 0 && !is_even) {
|
||||
atom_sign = -atom_sign;
|
||||
|
|
@ -1444,12 +1433,10 @@ namespace nlsat {
|
|||
if (!info.m_lc_const) {
|
||||
if (d % 2 == 0 || // d is even
|
||||
is_even || // rewriting a factor of even degree, sign flip doesn't matter
|
||||
_a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
|
||||
_a->get_kind() == atom::EQ) // rewriting an equation, sign flip doesn't matter
|
||||
info.add_lc_diseq();
|
||||
}
|
||||
else {
|
||||
else
|
||||
info.add_lc_ineq();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1755,7 +1742,7 @@ namespace nlsat {
|
|||
TRACE(nlsat_explain,
|
||||
tout << "[explain] set of literals is infeasible in the current interpretation\n";
|
||||
display(tout, num, ls) << "\n";
|
||||
m_assignment.display(tout);
|
||||
m_solver.display_assignment(tout);
|
||||
);
|
||||
m_result = &result;
|
||||
process(num, ls);
|
||||
|
|
@ -2140,7 +2127,7 @@ namespace nlsat {
|
|||
m_imp->m_signed_project = f;
|
||||
}
|
||||
|
||||
void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) {
|
||||
void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
|
||||
(*m_imp)(n, ls, result);
|
||||
}
|
||||
|
||||
|
|
@ -2157,7 +2144,6 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
};
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
#include <iostream>
|
||||
void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue