mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-07 17:47:58 +00:00
Code Activity

untracking .beads

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-03 08:01:58 -10:00
parent 156a7da4d1
commit 7290df5794
2 changed files with 2 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
.beads/issues.jsonl
View file

@ -1,8 +0,0 @@
{"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.\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"}
{"id":"z3-vzq","title":"Preserve RNG state around check_lemma() in nlsat_solver.cpp","description":"FIXED: Added RNG state preservation around check_lemma() in nlsat_solver.cpp.\n\nChanges:\n1. Added get_seed() method to random_gen class in util.h\n2. Added get_seed() method to interval_set_manager in nlsat_interval_set.h\n3. Modified check_lemma() to save and restore both m_random_seed and m_ism seed\n\nThis ensures that lemma checking doesn't affect the solver's randomized decisions, preserving determinism.","status":"closed","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T12:47:16.372644-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T13:01:35.429703-10:00","closed_at":"2026-02-02T13:01:35.429706-10:00"}
{"id":"z3-x98","title":"Replace SMT-RAT references with theoretical explanations in levelwise.cpp","description":"Comments in levelwise.cpp reference SMT-RAT without explaining why the optimizations are correct. Replace these references with theoretical justifications based on:\n\n- ~/Downloads/pre_proj_del.pdf\n- ~/Downloads/projective_delineability.pdf\n\nThis will make the code self-documenting and not dependent on external implementation references.","status":"tombstone","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T11:02:27.001095-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T12:02:05.512503-10:00","close_reason":"Closed","labels":["documentation"],"deleted_at":"2026-02-02T12:02:05.512503-10:00","deleted_by":"batch delete","delete_reason":"batch delete","original_type":"task"}
{"id":"z3-xxa","title":"Test timeouts when lws=false in nlsat_params.pyg","description":"BUG FIXED: Regression in nlsat_explain.cpp fallback projection.\n\nROOT CAUSE: Extra insert_fresh_factors_in_todo() calls were added in ensure_sign() and normalize() for levelwise support, but these caused polynomial cascade in the fallback projection.\n\nFIX: Made these additions conditional on m_solver.apply_levelwise():\n1. ensure_sign(): Only call insert_fresh_factors_in_todo(p) when levelwise is enabled\n2. normalize(): Only collect m_lower_stage_polys when levelwise is enabled \n3. main(): Only add m_lower_stage_polys to m_ps when levelwise is enabled\n\nThe fallback projection (used by master and when lws=false) handles delineability through its own mechanism and doesn't need these extra polynomials.\n\nAll 5 previously failing benchmarks now pass with lws=false:\n- issue-1658.smt2: 0.01s\n- 7489.smt2: 0.56s\n- 8099.smt2: 0.07s\n- sqrt-bug.smt2: 0.01s\n- issue-1694.smt2: 0.01s","status":"open","priority":2,"issue_type":"task","owner":"levnach@hotmail.com","created_at":"2026-02-02T11:57:01.96032-10:00","created_by":"Lev Nachmanson","updated_at":"2026-02-02T13:01:45.509205-10:00","labels":["bug"]}

2
.gitignore vendored
View file

@ -115,3 +115,5 @@ genaisrc/genblogpost.genai.mts
*.mts
# Bazel generated files
bazel-*
# Local issue tracking
.beads