mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

add new polynomials from handle_nullified to m_todo

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-18 10:54:39 -10:00
parent df419c137d
commit d8f2b5ca01
4 changed files with 31 additions and 162 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/levelwise.cpp
View file

@ -1217,12 +1217,18 @@ namespace nlsat {
// Line 10/11: detect nullification + pick a non-zero coefficient witness per p.
m_witnesses.clear();
m_witnesses.reserve(m_level_ps.size());
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
// Fixpoint loop: handle_nullified_poly may add more polynomials back at m_level
// via request_factorized. Drain them from m_todo into m_level_ps and
// compute witnesses for the new entries until no more appear.
for (unsigned i = 0; i < m_level_ps.size(); i++) {
polynomial_ref p(m_level_ps.get(i), m_pm);
polynomial_ref w = choose_nonzero_coeff(p, m_level);
if (!w)
handle_nullified_poly(p);
m_witnesses.push_back(w);
// Absorb any same-level polys that handle_nullified_poly added to m_todo
if (i + 1 == m_level_ps.size())
m_todo.extract_polys_at_level(m_level, m_level_ps);
}
}

21
src/nlsat/nlsat_common.cpp
View file

@ -112,6 +112,27 @@ namespace nlsat {
return x;
}
unsigned todo_set::extract_polys_at_level(var x, polynomial_ref_vector& out) {
pmanager& pm = m_set.m();
unsigned sz = m_set.size();
unsigned j = 0;
unsigned count = 0;
for (unsigned i = 0; i < sz; i++) {
poly* p = m_set.get(i);
if (pm.max_var(p) == x) {
out.push_back(p);
m_in_set[pm.id(p)] = false;
++count;
}
else {
m_set.set(j, p);
j++;
}
}
m_set.shrink(j);
return count;
}
/**
\brief Wrapper for factorization
*/

3
src/nlsat/nlsat_common.h
View file

@ -44,6 +44,9 @@ namespace nlsat {
them in max_polys. Return the maximal variable
*/
var extract_max_polys(polynomial_ref_vector& max_polys);
// Extract polynomials whose max_var equals \c x, appending them to \c out.
// Returns the number of polynomials extracted.
unsigned extract_polys_at_level(var x, polynomial_ref_vector& out);
};
inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) {

161
src/test/nlsat.cpp
View file

@ -2167,165 +2167,6 @@ static void tst_unsound_gh8397() {
std::cout << "\n=== END tst_unsound_gh8397 ===\n\n";
}
// Test case for unsound lemma from p6236_terminationG_0.smt2
// Levelwise produces cell that's too large when polynomial is nullified.
// Polynomials:
// p[0]: - x9
// p[1]: - x9 x15 - x10 x14 + x5 x11 x13 + x3 x4 x11 + 2
// p[2]: x15 + x6 x13 + x0 x4
// Sample: x0=1, x1=-1, x2=1, x3=-1, x4=2, x5=0, x6=0, x7=0, x8=0, x9=1, x10=0, x11=1/2, x12=1, x13=-4, x14=2
// Counterexample: x0=0, x3=-1, x4=1, x5=0, x6=0, x9=1, x10=0, x11=3, x13=0, x14=0, x15=0
static void tst_unsound_lws_p6236() {
std::cout << "=== tst_unsound_lws_p6236 ===\n";
params_ref ps;
ps.set_bool("lws", true);
reslimit rlim;
nlsat::solver s(rlim, ps, false);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment sample_as(am);
nlsat::assignment counter_as(am);
polynomial::cache cache(pm);
// Create 16 variables x0-x15
nlsat::var x0 = s.mk_var(false);
nlsat::var x1 = s.mk_var(false);
nlsat::var x2 = s.mk_var(false);
nlsat::var x3 = s.mk_var(false);
nlsat::var x4 = s.mk_var(false);
nlsat::var x5 = s.mk_var(false);
nlsat::var x6 = s.mk_var(false);
nlsat::var x7 = s.mk_var(false);
nlsat::var x8 = s.mk_var(false);
nlsat::var x9 = s.mk_var(false);
nlsat::var x10 = s.mk_var(false);
nlsat::var x11 = s.mk_var(false);
nlsat::var x12 = s.mk_var(false);
nlsat::var x13 = s.mk_var(false);
nlsat::var x14 = s.mk_var(false);
nlsat::var x15 = s.mk_var(false);
polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(pm), _x7(pm);
polynomial_ref _x8(pm), _x9(pm), _x10(pm), _x11(pm), _x12(pm), _x13(pm), _x14(pm), _x15(pm);
_x0 = pm.mk_polynomial(x0);
_x1 = pm.mk_polynomial(x1);
_x2 = pm.mk_polynomial(x2);
_x3 = pm.mk_polynomial(x3);
_x4 = pm.mk_polynomial(x4);
_x5 = pm.mk_polynomial(x5);
_x6 = pm.mk_polynomial(x6);
_x7 = pm.mk_polynomial(x7);
_x8 = pm.mk_polynomial(x8);
_x9 = pm.mk_polynomial(x9);
_x10 = pm.mk_polynomial(x10);
_x11 = pm.mk_polynomial(x11);
_x12 = pm.mk_polynomial(x12);
_x13 = pm.mk_polynomial(x13);
_x14 = pm.mk_polynomial(x14);
_x15 = pm.mk_polynomial(x15);
(void)_x1; (void)_x2; (void)_x7; (void)_x8; (void)_x12;
// p[0]: -x9
polynomial_ref p0(pm);
p0 = -_x9;
// p[1]: -x9*x15 - x10*x14 + x5*x11*x13 + x3*x4*x11 + 2
polynomial_ref p1(pm);
p1 = -_x9 * _x15 - _x10 * _x14 + _x5 * _x11 * _x13 + _x3 * _x4 * _x11 + 2;
// p[2]: x15 + x6*x13 + x0*x4
polynomial_ref p2(pm);
p2 = _x15 + _x6 * _x13 + _x0 * _x4;
std::cout << "Input polynomials:\n";
std::cout << " p0: " << p0 << "\n";
std::cout << " p1: " << p1 << "\n";
std::cout << " p2: " << p2 << "\n\n";
// Sample: x0=1, x1=-1, x2=1, x3=-1, x4=2, x5=0, x6=0, x7=0, x8=0, x9=1, x10=0, x11=1/2, x12=1, x13=-4, x14=2
scoped_anum val(am);
rational half(1, 2);
am.set(val, 1); sample_as.set(x0, val);
am.set(val, -1); sample_as.set(x1, val);
am.set(val, 1); sample_as.set(x2, val);
am.set(val, -1); sample_as.set(x3, val);
am.set(val, 2); sample_as.set(x4, val);
am.set(val, 0); sample_as.set(x5, val);
am.set(val, 0); sample_as.set(x6, val);
am.set(val, 0); sample_as.set(x7, val);
am.set(val, 0); sample_as.set(x8, val);
am.set(val, 1); sample_as.set(x9, val);
am.set(val, 0); sample_as.set(x10, val);
am.set(val, half.to_mpq()); sample_as.set(x11, val);
am.set(val, 1); sample_as.set(x12, val);
am.set(val, -4); sample_as.set(x13, val);
am.set(val, 2); sample_as.set(x14, val);
// Counterexample: x0=0, x3=-1, x4=1, x5=0, x6=0, x9=1, x10=0, x11=3, x13=0, x14=0, x15=0
// (use sample values for variables not mentioned in counterexample)
am.set(val, 0); counter_as.set(x0, val);
am.set(val, -1); counter_as.set(x1, val);
am.set(val, 1); counter_as.set(x2, val);
am.set(val, -1); counter_as.set(x3, val);
am.set(val, 1); counter_as.set(x4, val);
am.set(val, 0); counter_as.set(x5, val);
am.set(val, 0); counter_as.set(x6, val);
am.set(val, 0); counter_as.set(x7, val);
am.set(val, 0); counter_as.set(x8, val);
am.set(val, 1); counter_as.set(x9, val);
am.set(val, 0); counter_as.set(x10, val);
am.set(val, 3); counter_as.set(x11, val);
am.set(val, 1); counter_as.set(x12, val);
am.set(val, 0); counter_as.set(x13, val);
am.set(val, 0); counter_as.set(x14, val);
am.set(val, 0); counter_as.set(x15, val);
std::cout << "Sample: x0=1,x1=-1,x2=1,x3=-1,x4=2,x5=0,x6=0,x7=0,x8=0,x9=1,x10=0,x11=1/2,x12=1,x13=-4,x14=2\n";
std::cout << "Counterexample: x0=0,x3=-1,x4=1,x5=0,x6=0,x9=1,x10=0,x11=3,x13=0,x14=0,x15=0\n\n";
// Verify polynomial signs differ between sample and counterexample
// At counterexample: p2 = x15 + x6*x13 + x0*x4 = 0 + 0 + 0 = 0
// The lemma says p2 > 0, but counterexample has p2 = 0
std::cout << "Polynomial signs at COUNTEREXAMPLE:\n";
std::cout << " p0 sign: " << am.eval_sign_at(p0, counter_as) << "\n";
std::cout << " p1 sign: " << am.eval_sign_at(p1, counter_as) << "\n";
std::cout << " p2 sign: " << am.eval_sign_at(p2, counter_as) << "\n\n";
// Set solver assignment for levelwise (x0..x14, not x15)
s.set_rvalues(sample_as);
// Build polynomial vector
polynomial_ref_vector polys(pm);
polys.push_back(p0);
polys.push_back(p1);
polys.push_back(p2);
nlsat::var max_x = x15;
std::cout << "Running levelwise with max_x = x15\n";
// Run levelwise
nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache);
auto cell = lws.single_cell();
std::cout << "Cell intervals (count=" << cell.size() << "):\n";
for (unsigned i = 0; i < cell.size(); ++i) {
std::cout << " Level " << i << ": ";
nlsat::display(std::cout, s, cell[i]) << "\n";
}
// Check if counterexample is inside the cell
std::cout << "\n--- Checking if counterexample is in cell ---\n";
bool counterexample_outside_cell = is_point_inside_cell(am, pm, cell, counter_as);
// For a sound cell, the counterexample must be OUTSIDE the cell.
ENSURE(counterexample_outside_cell);
std::cout << "SUCCESS: Counterexample is OUTSIDE the cell (cell is sound)\n";
std::cout << "=== END tst_unsound_lws_p6236 ===\n\n";
}
// Test case for unsound lemma - nullified polynomial in levelwise
// Polynomials:
@ -2653,8 +2494,6 @@ static void tst_explain_p6236() {
void tst_nlsat() {
tst_explain_p6236();
std::cout << "------------------\n";
tst_unsound_lws_p6236();
std::cout << "------------------\n";
tst_unsound_lws_disc_zero();
std::cout << "------------------\n";
tst_unsound_lws_nullified2();