mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 13:41:27 +00:00
Code Activity

remve add_zero_assumption from pcs()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-21 07:09:43 -10:00
parent b8fb10ecc6
commit d6a4c9199b
2 changed files with 14 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/nlsat/nlsat_explain.cpp
View file

@ -310,7 +310,7 @@ namespace nlsat {
break; break;
} }
if (root_idx == 0) if (root_idx == 0)
return; // there are no root functions and therefore no constraints aer generated return; // there are no root functions and therefore no constraints are generated
TRACE(nlsat_explain, TRACE(nlsat_explain,
tout << "adding zero-assumption root literal for "; tout << "adding zero-assumption root literal for ";
@ -318,7 +318,7 @@ namespace nlsat {
add_root_literal(atom::ROOT_EQ, maxx, root_idx, q); add_root_literal(atom::ROOT_EQ, maxx, root_idx, q);
} }
void add_simple_assumption(atom::kind k, poly * p, bool sign = false) { void add_assumption(atom::kind k, poly * p, bool sign = false) {
SASSERT(k == atom::EQ || k == atom::LT || k == atom::GT); SASSERT(k == atom::EQ || k == atom::LT || k == atom::GT);
bool is_even = false; bool is_even = false;
bool_var b = m_solver.mk_ineq_atom(k, 1, &p, &is_even); bool_var b = m_solver.mk_ineq_atom(k, 1, &p, &is_even);
@ -326,10 +326,6 @@ namespace nlsat {
add_literal(l); add_literal(l);
} }
void add_assumption(atom::kind k, poly * p, bool sign = false) {
// TODO: factor
add_simple_assumption(k, p, sign);
}
/** /**
\brief Eliminate "vanishing leading coefficients" of p. \brief Eliminate "vanishing leading coefficients" of p.
@ -372,6 +368,7 @@ namespace nlsat {
// and were added as assumptions. // and were added as assumptions.
p = m_pm.mk_zero(); p = m_pm.mk_zero();
TRACE(nlsat_explain, tout << "all coefficients of p vanished\n";); TRACE(nlsat_explain, tout << "all coefficients of p vanished\n";);
VERIFY(m_add_all_coeffs); // need to fall back to Collins projection otherwise
return; return;
} }
k--; k--;
@ -448,13 +445,13 @@ namespace nlsat {
SASSERT(max_var(p) < max); SASSERT(max_var(p) < max);
// factor p is a lower stage polynomial, so we should add assumption to justify p being eliminated // factor p is a lower stage polynomial, so we should add assumption to justify p being eliminated
if (s == 0) if (s == 0)
add_simple_assumption(atom::EQ, p); // add assumption p = 0 add_assumption(atom::EQ, p); // add assumption p = 0
else if (a->is_even(i)) else if (a->is_even(i))
add_simple_assumption(atom::EQ, p, true); // add assumption p != 0 add_assumption(atom::EQ, p, true); // add assumption p != 0
else if (s < 0) else if (s < 0)
add_simple_assumption(atom::LT, p); // add assumption p < 0 add_assumption(atom::LT, p); // add assumption p < 0
else else
add_simple_assumption(atom::GT, p); // add assumption p > 0 add_assumption(atom::GT, p); // add assumption p > 0
} }
if (s == 0) { if (s == 0) {
bool atom_val = a->get_kind() == atom::EQ; bool atom_val = a->get_kind() == atom::EQ;
@ -660,7 +657,7 @@ namespace nlsat {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
polynomial_ref coeff(m_pm); polynomial_ref coeff(m_pm);
bool sqf = !m_add_all_coeffs && is_square_free(ps, x); bool only_lc = !m_add_all_coeffs && is_square_free(ps, x);
// Add the leading or all coeffs, depening on being square-free // Add the leading or all coeffs, depening on being square-free
for (unsigned i = 0; i < ps.size(); i++) { for (unsigned i = 0; i < ps.size(); i++) {
p = ps.get(i); p = ps.get(i);
@ -668,11 +665,11 @@ namespace nlsat {
if (k_deg == 0) continue; if (k_deg == 0) continue;
// p depends on x // p depends on x
TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";); TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { for (int j_coeff_deg = k_deg; j_coeff_deg >= 0; j_coeff_deg--) {
coeff = m_pm.coeff(p, x, j_coeff_deg); coeff = m_pm.coeff(p, x, j_coeff_deg);
TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";); TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
insert_fresh_factors_in_todo(coeff); insert_fresh_factors_in_todo(coeff);
if (sqf) if (only_lc)
break; break;
} }
} }
@ -762,11 +759,6 @@ namespace nlsat {
TRACE(nlsat_explain, tout << "done, psc is a constant\n";); TRACE(nlsat_explain, tout << "done, psc is a constant\n";);
return; return;
} }
if (is_zero(sign(s))) {
TRACE(nlsat_explain, tout << "psc vanished, adding zero assumption\n";);
add_zero_assumption(s);
continue;
}
TRACE(nlsat_explain, TRACE(nlsat_explain,
tout << "adding v-psc of\n"; tout << "adding v-psc of\n";
display(tout, p); display(tout, p);
@ -953,7 +945,7 @@ namespace nlsat {
int s = sign(p); int s = sign(p);
if (!is_const(p)) { if (!is_const(p)) {
TRACE(nlsat_explain, tout << p << "\n";); TRACE(nlsat_explain, tout << p << "\n";);
add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
} }
return s; return s;
#endif #endif
@ -985,7 +977,7 @@ namespace nlsat {
UNREACHABLE(); UNREACHABLE();
break; break;
} }
add_simple_assumption(k, p, lsign); add_assumption(k, p, lsign);
} }
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) { void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {

4
src/nlsat/nlsat_params.pyg
View file

@ -9,7 +9,7 @@ def_module_params('nlsat',
('lazy', UINT, 0, "how lazy the solver is."), ('lazy', UINT, 0, "how lazy the solver is."),
('reorder', BOOL, True, "reorder variables."), ('reorder', BOOL, True, "reorder variables."),
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
('log_lemma_smtrat', BOOL, True, "use indexed SMT-LIB root expressions when logging lemmas"), ('log_lemma_smtrat', BOOL, False, "use indexed SMT-LIB root expressions when logging lemmas"),
('dump_mathematica', BOOL, False, "display lemmas as matematica"), ('dump_mathematica', BOOL, False, "display lemmas as matematica"),
('check_lemmas', BOOL, False, "check lemmas on the fly using an independent nlsat solver"), ('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."), ('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
@ -20,6 +20,6 @@ def_module_params('nlsat',
('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"),
('seed', UINT, 0, "random seed."), ('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution."), ('factor', BOOL, True, "factor polynomials produced during conflict resolution."),
('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."), ('add_all_coeffs', BOOL, True, "add all polynomial coefficients during projection."),
('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only") ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only")
)) ))