mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

work on well-orientedness

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-16 14:07:19 -07:00
parent b2f01706be
commit ef965574e2
9 changed files with 559 additions and 326 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/nlsat_clause.h
View file

@ -64,7 +64,7 @@ namespace nlsat {
assumption_set assumptions() const { return m_assumptions; }
};
typedef ptr_vector<clause> clause_vector;
typedef std_vector<clause*> clause_vector;
};

6
src/nlsat/nlsat_evaluator.cpp
View file

@ -463,10 +463,12 @@ namespace nlsat {
svector<sign> & signs = m_add_signs_tmp;
roots.reset();
signs.reset();
TRACE(nlsat_evaluator, tout << "x: " << x << " max_var(p): " << m_pm.max_var(p) << "\n";);
TRACE(nlsat_evaluator, m_solver.display(tout << "p: ", polynomial_ref(p, m_pm)) << "\n";tout << "x: " << x << " max_var(p): " << m_pm.max_var(p) << "\n";);
// Note: I added undef_var_assignment in the following statement, to allow us to obtain the infeasible interval sets
// even when the maximal variable is assigned. I need this feature to minimize conflict cores.
m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(m_assignment, x), roots, signs);
auto pr = polynomial_ref(p, m_pm);
auto uass = undef_var_assignment(m_assignment, x);
m_am.isolate_roots(pr, uass, roots, signs);
t.add(roots, signs);
}
}

168
src/nlsat/nlsat_explain.cpp
View file

@ -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) {

2
src/nlsat/nlsat_explain.h
View file

@ -63,7 +63,7 @@ namespace nlsat {
- s_1, ..., s_m do not contain variable x.
- s_1, ..., s_m are false in the current interpretation
*/
void operator()(unsigned n, literal const * ls, scoped_literal_vector & result);
void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result);
/**

4
src/nlsat/nlsat_params.pyg
View file

@ -9,6 +9,7 @@ def_module_params('nlsat',
('lazy', UINT, 0, "how lazy the solver is."),
('reorder', BOOL, True, "reorder variables."),
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
('dump_mathematica', BOOL, False, "display lemmas as matematica"),
('check_lemmas', BOOL, False, "check lemmas on the fly using an independent nlsat solver"),
('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
('minimize_conflicts', BOOL, False, "minimize conflicts"),
@ -17,5 +18,6 @@ def_module_params('nlsat',
('shuffle_vars', BOOL, False, "use a random variable order."),
('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"),
('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution.")
('factor', BOOL, True, "factor polynomials produced during conflict resolution."),
('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only")
))

4
src/nlsat/nlsat_simplify.cpp
View file

@ -30,7 +30,7 @@ namespace nlsat {
// then promote learned to main.
for (auto c : m_learned)
s.del_clause(c);
m_learned.reset();
m_learned.clear();
IF_VERBOSE(3, s.display(verbose_stream() << "before\n"));
unsigned sz = m_clauses.size();
@ -342,7 +342,7 @@ namespace nlsat {
else
m_clauses[j++] = c;
}
m_clauses.shrink(j);
m_clauses.resize(j);
return j < sz;
}

692
src/nlsat/nlsat_solver.cpp
View file

File diff suppressed because it is too large Load diff

5
src/nlsat/nlsat_solver.h
View file

@ -290,6 +290,11 @@ namespace nlsat {
std::ostream& display(std::ostream & out, var x) const;
display_var_proc const & display_proc() const;
std::ostream& display_assignment(std::ostream& out) const;
std::ostream& display_var(std::ostream& out, unsigned j) const;
};
};

2
src/nlsat/nlsat_types.h
View file

@ -94,7 +94,7 @@ namespace nlsat {
void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; }
};
typedef ptr_vector<atom> atom_vector;
typedef std_vector<atom*> atom_vector;
class ineq_atom : public atom {
friend class solver;