mirror of
https://github.com/Z3Prover/z3
synced 2026-02-08 01:57:59 +00:00
fix a typo in poly_has_roots
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
60f9edb65f
commit
a19db1f7a7
3 changed files with 289 additions and 3 deletions
|
|
@ -1,4 +1,5 @@
|
|||
{"id":"z3-513","title":"Investigate noDisc optimization when lb and ub are roots of same polynomial","description":"SMT-RAT does noDisc for leaves connected to the section-defining polynomial in the section case. This might extend to sector spanning_tree mode when lb and ub come from the same polynomial but different root functions.\n\nExample: polynomial p has roots at x=1 and x=3, sample at x=2. Then lb is root 1 of p, ub is root 2 of p. A leaf polynomial q connected only to p might not need disc(q) since Res(q,p) constrains q's roots relative to both bounds.\n\nThe previous implementation was unsound because it applied to general leaves connected to any boundary, but discriminants are needed to ensure a polynomial's own roots don't merge/split.\n\nInvestigate whether this optimization is valid when lb and ub are different roots of the same polynomial.","status":"open","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T11:38:28.527265-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T12:00:28.926462-10:00","labels":["enhancement"]}
|
||||
{"id":"z3-76w","title":"Unsound lemma in ppblockterm.t2 with nlsat.check_lemma=true","description":"Running:\nbuild/release/z3 /Users/levnach/dev/data/QF_NIA/20170427-VeryMax/ITS/From_T2__ppblockterm.t2__p7867_terminationG_0.smt2 nlsat.check_lemma=true\n\nexposes an unsound lemma.\n\nThe test case should reconstruct the run of levelwise with these parameters:\n\n=== LEVELWISE input polys\np[0]: x16 + x9\np[1]: x16 x24 + x9 x24 + x13 x19 + x5 x19 + x12 x15 + x10 x15 - 2\np[2]: x4\np[3]: x4 x24 + x2 x19 + x11 x15\n=== END LEVELWISE INPUT (4 polynomials) ===\n\nVariable values at SAMPLE point:\nx0 -\u003e 1\nx1 -\u003e 1\nx2 -\u003e -1\nx3 -\u003e -1\nx4 -\u003e 1\nx5 -\u003e -1\nx6 -\u003e 1\nx7 -\u003e 2\nx8 -\u003e 1\nx9 -\u003e 1\nx10 -\u003e -1\nx11 -\u003e 1\nx12 -\u003e -2\nx13 -\u003e -2\nx14 -\u003e -2\nx15 -\u003e 0\nx16 -\u003e 2\nx17 -\u003e 0\nx18 -\u003e 0\nx19 -\u003e 0\nx20 -\u003e 0\nx21 -\u003e 0\nx22 -\u003e 0\nx23 -\u003e 0\n\nTODO:\n1. Create a test in nlsat.cpp with the same input polynomials and sample point\n2. Reproduce the unsound lemma with test-z3\n3. Fix the unsound lemma","notes":"Investigation findings:\n\n1. Found and fixed typo bug in poly_has_roots(): was 'i \u003c vec_get(...)' instead of 'vec_get(...)'. This caused leading coefficients to be incorrectly omitted for polynomials with index \u003e= 1 at the top level.\n\n2. Added helper function is_point_inside_cell() to check cell membership.\n\n3. The test still fails - counterexample is inside the cell. The cell's projection at level 19 becomes constant (LC=0 at both sample and counterexample). Need further investigation of how nlsat_explain combines cell with conflict literals.","status":"open","priority":1,"issue_type":"bug","owner":"levnach@hotmail.com","created_at":"2026-02-02T13:36:27.350347-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T14:34:21.308632-10:00"}
|
||||
{"id":"z3-a4d","title":"Use commas instead of parentheses in comments","description":"In comments, avoid parenthetical expressions. Use commas for natural flow.\n\nExample:\n// Before: at most one root below v and one root above v (or a single root at v for sections).\n// After: at most one root below v and one root above v, or a single root at v for sections.","status":"tombstone","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T11:16:37.851848-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T12:02:05.512503-10:00","close_reason":"Closed","labels":["style"],"deleted_at":"2026-02-02T12:02:05.512503-10:00","deleted_by":"batch delete","delete_reason":"batch delete","original_type":"task"}
|
||||
{"id":"z3-la5","title":"Refactor add_section_projections to avoid duplicate witness handling code","description":"The if/else branches in add_section_projections have duplicate witness checking logic. Refactor to extract common code:\n\n```cpp\n// Current (duplicate logic):\nif (is_section_poly) {\n polynomial_ref lc(m_pm);\n unsigned deg = m_pm.degree(p, m_level);\n lc = m_pm.coeff(p, m_level, deg);\n \n witness = polynomial_ref(m_pm);\n \n add_projection_for_poly(p, m_level, witness, true, true);\n} else {\n request_factorized(witness, inv_req::sign);\n}\n\n// Consider restructuring to reduce duplication\n```","status":"tombstone","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T07:14:53.827387-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T12:02:05.512503-10:00","close_reason":"Closed","labels":["style"],"deleted_at":"2026-02-02T12:02:05.512503-10:00","deleted_by":"batch delete","delete_reason":"batch delete","original_type":"task"}
|
||||
{"id":"z3-ske","title":"Remove curly braces around single-line if/else statements in levelwise.cpp","description":"Code style cleanup: remove unnecessary curly braces around single-line if/else statements to match Z3's coding style. Example:\n```cpp\n// Before:\nif (both[i].upper_rf \u003c both[p].upper_rf) {\n out_children[i].push_back(p);\n} else {\n out_children[p].push_back(i);\n}\n\n// After:\nif (both[i].upper_rf \u003c both[p].upper_rf)\n out_children[i].push_back(p);\nelse\n out_children[p].push_back(i);\n```","status":"tombstone","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T07:13:28.095639-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T12:02:05.512503-10:00","close_reason":"Closed","labels":["style"],"deleted_at":"2026-02-02T12:02:05.512503-10:00","deleted_by":"batch delete","delete_reason":"batch delete","original_type":"task"}
|
||||
|
|
|
|||
|
|
@ -1277,7 +1277,7 @@ namespace nlsat {
|
|||
process_level_with_mode(mode, have_interval);
|
||||
}
|
||||
|
||||
bool poly_has_roots(unsigned i) { return i < vec_get(m_poly_has_roots, i, false); }
|
||||
bool poly_has_roots(unsigned i) { return vec_get(m_poly_has_roots, i, false); }
|
||||
|
||||
void process_top_level() {
|
||||
TRACE(lws, display_polys_at_level(tout););
|
||||
|
|
|
|||
|
|
@ -28,6 +28,112 @@ Notes:
|
|||
#include <iostream>
|
||||
#include <vector>
|
||||
|
||||
// Helper function to check if a point (given by counter_as) is inside a levelwise cell.
|
||||
// Returns true if the point is inside ALL cell intervals, false otherwise.
|
||||
// Prints diagnostic info about which constraint was violated (if any).
|
||||
static bool is_point_inside_cell(
|
||||
anum_manager& am,
|
||||
polynomial::manager& pm,
|
||||
std_vector<nlsat::levelwise::root_function_interval> const& cell,
|
||||
nlsat::assignment const& counter_as,
|
||||
bool verbose = true)
|
||||
{
|
||||
for (unsigned level = 0; level < cell.size(); ++level) {
|
||||
auto const& interval = cell[level];
|
||||
|
||||
// Skip whole-line sectors - no constraint
|
||||
if (!interval.is_section() && interval.l_inf() && interval.u_inf())
|
||||
continue;
|
||||
|
||||
// Get the value at this level from counter_as
|
||||
if (!counter_as.is_assigned(level))
|
||||
continue; // Variable not assigned in counterexample
|
||||
|
||||
scoped_anum counter_val(am);
|
||||
am.set(counter_val, counter_as.value(level));
|
||||
|
||||
// Build partial assignment up to this level (exclusive) for root isolation
|
||||
nlsat::assignment partial_as(am);
|
||||
for (unsigned j = 0; j < level; ++j) {
|
||||
if (counter_as.is_assigned(j)) {
|
||||
scoped_anum v(am);
|
||||
am.set(v, counter_as.value(j));
|
||||
partial_as.set(j, v);
|
||||
}
|
||||
}
|
||||
|
||||
if (interval.is_section()) {
|
||||
// Section: counter must equal the root
|
||||
polynomial_ref section_p(interval.l, pm);
|
||||
scoped_anum_vector roots(am);
|
||||
am.isolate_roots(section_p, nlsat::undef_var_assignment(partial_as, level), roots);
|
||||
|
||||
if (roots.size() >= interval.l_index) {
|
||||
bool at_root = am.eq(counter_val, roots[interval.l_index - 1]);
|
||||
if (!at_root) {
|
||||
if (verbose) {
|
||||
std::cout << " Level " << level << ": OUTSIDE (not at section root)\n";
|
||||
std::cout << " Section root = ";
|
||||
am.display_decimal(std::cout, roots[interval.l_index - 1], 6);
|
||||
std::cout << ", counter = ";
|
||||
am.display_decimal(std::cout, counter_val, 6);
|
||||
std::cout << "\n";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
// Sector: check lower and upper bounds
|
||||
if (!interval.l_inf()) {
|
||||
polynomial_ref lower_p(interval.l, pm);
|
||||
scoped_anum_vector lower_roots(am);
|
||||
am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, level), lower_roots);
|
||||
|
||||
if (lower_roots.size() >= interval.l_index) {
|
||||
int cmp = am.compare(counter_val, lower_roots[interval.l_index - 1]);
|
||||
if (cmp <= 0) { // counter <= lower bound, violates (lower, ...)
|
||||
if (verbose) {
|
||||
std::cout << " Level " << level << ": OUTSIDE (at or below lower bound)\n";
|
||||
std::cout << " Lower bound = ";
|
||||
am.display_decimal(std::cout, lower_roots[interval.l_index - 1], 6);
|
||||
std::cout << ", counter = ";
|
||||
am.display_decimal(std::cout, counter_val, 6);
|
||||
std::cout << "\n";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!interval.u_inf()) {
|
||||
polynomial_ref upper_p(interval.u, pm);
|
||||
scoped_anum_vector upper_roots(am);
|
||||
am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, level), upper_roots);
|
||||
|
||||
if (upper_roots.size() >= interval.u_index) {
|
||||
int cmp = am.compare(counter_val, upper_roots[interval.u_index - 1]);
|
||||
if (cmp >= 0) { // counter >= upper bound, violates (..., upper)
|
||||
if (verbose) {
|
||||
std::cout << " Level " << level << ": OUTSIDE (at or above upper bound)\n";
|
||||
std::cout << " Upper bound = ";
|
||||
am.display_decimal(std::cout, upper_roots[interval.u_index - 1], 6);
|
||||
std::cout << ", counter = ";
|
||||
am.display_decimal(std::cout, counter_val, 6);
|
||||
std::cout << "\n";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (verbose) {
|
||||
std::cout << " Point is INSIDE the cell (all constraints satisfied)\n";
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
|
||||
nlsat::interval_set_ref const & s2,
|
||||
unsigned expected_num_intervals,
|
||||
|
|
@ -2061,9 +2167,188 @@ static void tst_unsound_lws_disc_zero() {
|
|||
std::cout << "\n=== END tst_unsound_lws_disc_zero ===\n\n";
|
||||
}
|
||||
|
||||
// Test case for unsound lemma from ppblockterm.t2__p7867_terminationG_0.smt2
|
||||
// Issue z3-76w: levelwise produces unsound cell
|
||||
static void tst_unsound_lws_ppblockterm() {
|
||||
std::cout << "=== tst_unsound_lws_ppblockterm ===\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();
|
||||
polynomial::cache cache(pm);
|
||||
|
||||
// Create 25 variables x0 to x24
|
||||
nlsat::var vars[25];
|
||||
polynomial_ref xvars[25] = {
|
||||
polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm),
|
||||
polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm),
|
||||
polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm),
|
||||
polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm),
|
||||
polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm), polynomial_ref(pm)
|
||||
};
|
||||
|
||||
for (unsigned i = 0; i < 25; i++) {
|
||||
vars[i] = s.mk_var(false);
|
||||
xvars[i] = pm.mk_polynomial(vars[i]);
|
||||
}
|
||||
|
||||
// Aliases for readability
|
||||
polynomial_ref &x2 = xvars[2], &x4 = xvars[4], &x5 = xvars[5];
|
||||
polynomial_ref &x9 = xvars[9], &x10 = xvars[10], &x11 = xvars[11];
|
||||
polynomial_ref &x12 = xvars[12], &x13 = xvars[13], &x15 = xvars[15];
|
||||
polynomial_ref &x16 = xvars[16], &x19 = xvars[19], &x24 = xvars[24];
|
||||
|
||||
// p[0]: x16 + x9
|
||||
polynomial_ref p0(pm);
|
||||
p0 = x16 + x9;
|
||||
|
||||
// p[1]: x16 x24 + x9 x24 + x13 x19 + x5 x19 + x12 x15 + x10 x15 - 2
|
||||
polynomial_ref p1(pm);
|
||||
p1 = x16 * x24 + x9 * x24 + x13 * x19 + x5 * x19 + x12 * x15 + x10 * x15 - 2;
|
||||
|
||||
// p[2]: x4
|
||||
polynomial_ref p2(pm);
|
||||
p2 = x4;
|
||||
|
||||
// p[3]: x4 x24 + x2 x19 + x11 x15
|
||||
polynomial_ref p3(pm);
|
||||
p3 = x4 * x24 + x2 * x19 + x11 * x15;
|
||||
|
||||
std::cout << "Input polynomials:\n";
|
||||
std::cout << " p0: " << p0 << "\n";
|
||||
std::cout << " p1: " << p1 << "\n";
|
||||
std::cout << " p2: " << p2 << "\n";
|
||||
std::cout << " p3: " << p3 << "\n\n";
|
||||
|
||||
// Set sample point values
|
||||
// x0->1, x1->1, x2->-1, x3->-1, x4->1, x5->-1, x6->1, x7->2, x8->1
|
||||
// x9->1, x10->-1, x11->1, x12->-2, x13->-2, x14->-2, x15->0, x16->2
|
||||
// x17->0, x18->0, x19->0, x20->0, x21->0, x22->0, x23->0
|
||||
int sample_vals[24] = {1, 1, -1, -1, 1, -1, 1, 2, 1, 1, -1, 1, -2, -2, -2, 0, 2, 0, 0, 0, 0, 0, 0, 0};
|
||||
|
||||
scoped_anum val(am);
|
||||
nlsat::assignment sample_as(am);
|
||||
for (unsigned i = 0; i < 24; i++) {
|
||||
am.set(val, sample_vals[i]);
|
||||
sample_as.set(vars[i], val);
|
||||
}
|
||||
s.set_rvalues(sample_as);
|
||||
|
||||
std::cout << "Sample point (x0..x23):\n";
|
||||
for (unsigned i = 0; i < 24; i++) {
|
||||
std::cout << " x" << i << " -> " << sample_vals[i] << "\n";
|
||||
}
|
||||
std::cout << "\n";
|
||||
|
||||
// Evaluate polynomials at sample (with x24 = 0 for checking)
|
||||
am.set(val, 0);
|
||||
sample_as.set(vars[24], val);
|
||||
std::cout << "Polynomial signs at sample (x24=0):\n";
|
||||
std::cout << " p0 sign: " << am.eval_sign_at(p0, sample_as) << "\n";
|
||||
std::cout << " p1 sign: " << am.eval_sign_at(p1, sample_as) << "\n";
|
||||
std::cout << " p2 sign: " << am.eval_sign_at(p2, sample_as) << "\n";
|
||||
std::cout << " p3 sign: " << am.eval_sign_at(p3, sample_as) << "\n\n";
|
||||
|
||||
// Counterexample from the unsound lemma:
|
||||
// x2=-1, x4=1, x5=0, x9=0, x10=0, x11=-1, x12=-1, x13=-2, x15=3, x16=2, x19=0, x24=3
|
||||
nlsat::assignment counter_as(am);
|
||||
am.set(val, -1); counter_as.set(vars[2], val);
|
||||
am.set(val, 1); counter_as.set(vars[4], val);
|
||||
am.set(val, 0); counter_as.set(vars[5], val);
|
||||
am.set(val, 0); counter_as.set(vars[9], val);
|
||||
am.set(val, 0); counter_as.set(vars[10], val);
|
||||
am.set(val, -1); counter_as.set(vars[11], val);
|
||||
am.set(val, -1); counter_as.set(vars[12], val);
|
||||
am.set(val, -2); counter_as.set(vars[13], val);
|
||||
am.set(val, 3); counter_as.set(vars[15], val);
|
||||
am.set(val, 2); counter_as.set(vars[16], val);
|
||||
am.set(val, 0); counter_as.set(vars[19], val);
|
||||
am.set(val, 3); counter_as.set(vars[24], val);
|
||||
|
||||
std::cout << "Counterexample point:\n";
|
||||
std::cout << " x2=-1, x4=1, x5=0, x9=0, x10=0, x11=-1, x12=-1, x13=-2, x15=3, x16=2, x19=0, x24=3\n\n";
|
||||
|
||||
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";
|
||||
std::cout << " p3 sign: " << am.eval_sign_at(p3, counter_as) << "\n\n";
|
||||
|
||||
// Build polynomial vector
|
||||
polynomial_ref_vector polys(pm);
|
||||
polys.push_back(p0);
|
||||
polys.push_back(p1);
|
||||
polys.push_back(p2);
|
||||
polys.push_back(p3);
|
||||
|
||||
unsigned max_x = vars[24]; // x24 is the highest variable
|
||||
|
||||
std::cout << "Running levelwise with max_x = x24...\n";
|
||||
nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache);
|
||||
auto cell = lws.single_cell();
|
||||
|
||||
if (lws.failed()) {
|
||||
std::cout << "Levelwise FAILED\n";
|
||||
} else {
|
||||
std::cout << "Levelwise succeeded\n";
|
||||
std::cout << "--- LEMMA from levelwise ---\n";
|
||||
for (unsigned i = 0; i < cell.size(); i++) {
|
||||
auto const& interval = cell[i];
|
||||
std::cout << "Level x" << i << ": ";
|
||||
if (interval.is_section()) {
|
||||
std::cout << "section at root[" << interval.l_index << "] of " << interval.l << "\n";
|
||||
} else {
|
||||
if (interval.l_inf())
|
||||
std::cout << "(-oo, ";
|
||||
else
|
||||
std::cout << "(root[" << interval.l_index << "] of " << interval.l << ", ";
|
||||
if (interval.u_inf())
|
||||
std::cout << "+oo)";
|
||||
else
|
||||
std::cout << "root[" << interval.u_index << "] of " << interval.u << ")";
|
||||
std::cout << "\n";
|
||||
}
|
||||
}
|
||||
std::cout << "--- END LEMMA ---\n\n";
|
||||
|
||||
// Check polynomial signs at sample and counterexample
|
||||
int p0_sample = am.eval_sign_at(p0, sample_as);
|
||||
int p1_sample = am.eval_sign_at(p1, sample_as);
|
||||
int p2_sample = am.eval_sign_at(p2, sample_as);
|
||||
int p3_sample = am.eval_sign_at(p3, sample_as);
|
||||
|
||||
int p0_counter = am.eval_sign_at(p0, counter_as);
|
||||
int p1_counter = am.eval_sign_at(p1, counter_as);
|
||||
int p2_counter = am.eval_sign_at(p2, counter_as);
|
||||
int p3_counter = am.eval_sign_at(p3, counter_as);
|
||||
|
||||
bool signs_differ = (p0_sample != p0_counter) || (p1_sample != p1_counter) ||
|
||||
(p2_sample != p2_counter) || (p3_sample != p3_counter);
|
||||
|
||||
if (signs_differ) {
|
||||
std::cout << "Polynomial signs DIFFER between sample and counterexample.\n";
|
||||
} else {
|
||||
std::cout << "Polynomial signs match between sample and counterexample.\n";
|
||||
}
|
||||
|
||||
// Verify that the counterexample is OUTSIDE the cell (cell is sound)
|
||||
std::cout << "\nChecking if counterexample is inside cell:\n";
|
||||
bool inside = is_point_inside_cell(am, pm, cell, counter_as);
|
||||
|
||||
// For a sound cell with differing signs, counterexample must be OUTSIDE
|
||||
ENSURE(!inside);
|
||||
std::cout << "SUCCESS: Counterexample is OUTSIDE the cell (cell is sound)\n";
|
||||
}
|
||||
|
||||
std::cout << "=== END tst_unsound_lws_ppblockterm ===\n\n";
|
||||
}
|
||||
|
||||
void tst_nlsat() {
|
||||
tst_unsound_lws_disc_zero();
|
||||
std::cout << "------------------\n";
|
||||
// TODO: Fix z3-76w - ppblockterm test fails because counterexample is inside cell
|
||||
// tst_unsound_lws_ppblockterm();
|
||||
// std::cout << "------------------\n";
|
||||
tst_unsound_lws_n46();
|
||||
std::cout << "------------------\n";
|
||||
tst_unsound_lws_et4();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue