mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-08 10:07:59 +00:00
Code Activity

add lc(p) and disc(p) for a rootless p in section case

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-02 16:39:30 -10:00
parent a19db1f7a7
commit 4587ecec9c
3 changed files with 19 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.beads/issues.jsonl
View file

@ -1,5 +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-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.\n\n\nKey finding from check_lemma output:\n\nThe original conflict is:\n\nThe lemma says: within cell, either x24 \u003c root[1](p1) OR p3 \u003e 0.\n\nBut the checker found a point INSIDE the cell where:\n- x24 \u003e= root[1](p1)\n- p3 \u003c= 0\n\nThis means the cell doesn't preserve the conflict. The issue may be that levelwise treats polynomials for SIGN preservation, but the conflict involves ROOT ATOMS.","status":"closed","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-02T16:00:23.824841-10:00","closed_at":"2026-02-02T16:00:23.824841-10:00","close_reason":"Fixed: polynomials without roots at section level need LC+disc for delineability"}
{"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"}

25
src/nlsat/levelwise.cpp
View file

@ -1106,27 +1106,34 @@ namespace nlsat {
bool is_section() { return m_I[m_level].is_section();}
// Section case: only the section-defining polynomial needs disc and lc projections.
//
// Theory: For a section (sample on a root), sign-invariance of other polynomials
// is ensured by resultants with the section-defining polynomial. Their leading
// coefficients and discriminants are not needed because:
// - Resultant Res(p, q) being order-invariant ensures relative root ordering (Thm 2.2 in [1])
// - The section polynomial's delineability (via its disc/lc) anchors the cell
// Section case: the section-defining polynomial needs disc and lc projections.
// For polynomials WITH roots: resultants with section polynomial ensure root ordering.
// For polynomials WITHOUT roots: they need LC + disc to ensure they don't gain roots.
//
// Theory: For a section (sample on a root), sign-invariance of polynomials with roots
// is ensured by resultants with the section-defining polynomial (Thm 2.2 in [1]).
// But polynomials without roots need delineability (LC + disc) to stay root-free.
//
// [1] Nalbach et al., "Projective Delineability for Single Cell Construction", SC² 2025
void add_section_projections() {
poly* section_poly = m_I[m_level].l;
SASSERT(section_poly);
// Build set of polynomial indices that have roots at this level
std::set<unsigned> has_roots;
for (auto const& rf : m_rel.m_rfunc)
has_roots.insert(rf.ps_idx);
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
polynomial_ref p(m_level_ps.get(i), m_pm);
polynomial_ref witness = m_witnesses[i];
if (m_level_ps.get(i) == section_poly)
add_projection_for_poly(p, m_level, witness, /*add_lc=*/true, /*add_disc=*/true);
add_projection_for_poly(p, m_level, witness, true, true); // section poly: full projection
else if (has_roots.find(i) == has_roots.end())
add_projection_for_poly(p, m_level, witness, true, true); // no roots: need LC+disc for delineability
else if (witness && !is_const(witness))
request_factorized(witness, inv_req::sign);
request_factorized(witness, inv_req::sign); // has roots: witness only
}
}

5
src/test/nlsat.cpp
View file

@ -2346,9 +2346,8 @@ static void tst_unsound_lws_ppblockterm() {
}
void tst_nlsat() {
// TODO: Fix z3-76w - ppblockterm test fails because counterexample is inside cell
// tst_unsound_lws_ppblockterm();
// std::cout << "------------------\n";
tst_unsound_lws_ppblockterm();
std::cout << "------------------\n";
tst_unsound_lws_n46();
std::cout << "------------------\n";
tst_unsound_lws_et4();