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

preserve random seed in nlsat_solver::check_lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-02 13:31:33 -10:00
parent f1a6f85ae5
commit 60f9edb65f
6 changed files with 32 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

12
.beads/issues.jsonl
View file

@ -1,5 +1,7 @@
{"id":"z3-513","title":"Investigate noDisc optimization for spanning_tree when lb == ub","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 are the same polynomial.\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 == ub (same polynomial defines both bounds).","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-02T11:38:28.527265-10:00","labels":["enhancement"]}
{"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":"closed","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-02T11:21:14.339946-10:00","closed_at":"2026-02-02T11:21:14.339946-10:00","close_reason":"Closed","labels":["style"]}
{"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":"closed","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-02T07:17:55.710403-10:00","closed_at":"2026-02-02T07:17:55.710403-10:00","close_reason":"Closed","labels":["style"]}
{"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":"closed","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-02T07:18:00.76593-10:00","closed_at":"2026-02-02T07:18:00.76593-10:00","close_reason":"Closed","labels":["style"]}
{"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":"closed","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-02T11:05:03.133153-10:00","closed_at":"2026-02-02T11:05:03.133153-10:00","close_reason":"Closed","labels":["documentation"]}
{"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-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"]}

5
.gitattributes vendored
View file

@ -3,4 +3,7 @@
src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf
.github/workflows/*.lock.yml linguist-generated=true merge=ours
.github/workflows/*.lock.yml linguist-generated=true merge=ours
# Use bd merge for beads JSONL files
.beads/issues.jsonl merge=beads

1
src/nlsat/nlsat_explain.cpp
View file

@ -361,7 +361,6 @@ namespace nlsat {
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
insert_fresh_factors_in_todo(lc);
if (!is_zero(lc) && sign(lc)) {
insert_fresh_factors_in_todo(lc);
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return;
}

1
src/nlsat/nlsat_interval_set.h
View file

@ -35,6 +35,7 @@ namespace nlsat {
interval_set_manager(anum_manager & m, small_object_allocator & a);
void set_seed(unsigned s) { m_rand.set_seed(s); }
unsigned get_seed() const { return m_rand.get_seed(); }
/**
\brief Return the empty set.

22
src/nlsat/nlsat_solver.cpp
View file

@ -1141,6 +1141,10 @@ namespace nlsat {
TRACE(nlsat, display(tout << "check lemma: ", n, cls) << "\n";
display(tout););
// Save RNG state before check_lemma to ensure determinism
unsigned saved_random_seed = m_random_seed;
unsigned saved_ism_seed = m_ism.get_seed();
try {
// Create a separate reslimit for the checker with 10 second timeout
reslimit checker_rlimit;
@ -1157,11 +1161,19 @@ namespace nlsat {
checker.m_apply_lws = false; // Disable levelwise for checker to avoid recursive issues
scoped_bool_vars tr(checker);
if (!setup_checker(checker, tr, n, cls, a))
if (!setup_checker(checker, tr, n, cls, a)) {
// Restore RNG state
m_random_seed = saved_random_seed;
m_ism.set_seed(saved_ism_seed);
return; // Lemma contains untranslatable atoms, skip check
}
lbool r = checker.check();
if (r == l_undef) // Checker timed out - skip this lemma check
return;
if (r == l_undef) {
// Restore RNG state
m_random_seed = saved_random_seed;
m_ism.set_seed(saved_ism_seed);
return; // Checker timed out - skip this lemma check
}
if (r == l_true) {
// Before reporting unsound, dump the lemma to see what we're checking
@ -1175,6 +1187,10 @@ namespace nlsat {
catch (...) {
// Ignore exceptions from the checker - just skip this lemma check
}
// Restore RNG state after check_lemma
m_random_seed = saved_random_seed;
m_ism.set_seed(saved_ism_seed);
}
void log_lemma(std::ostream& out, clause const& cls, std::string annotation) {

1
src/util/util.h
View file

@ -345,6 +345,7 @@ public:
}
void set_seed(unsigned s) { m_data = s; }
unsigned get_seed() const { return m_data; }
int operator()() {
return ((m_data = m_data * 214013L + 2531011L) >> 16) & 0x7fff;