mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-13 07:46:28 +00:00
Code Activity

Improve comments in push/pop scope cleanup code

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c23a0600-90dd-45a1-b64f-c286d041f373

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-03 18:34:43 +00:00 • committed by GitHub
parent 49e5894592
commit 1218520a6c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_clause.h
View file

@ -53,7 +53,7 @@ namespace sat {
unsigned m_inact_rounds:8;
unsigned m_glue:8;
unsigned m_psm:8; // transient field used during gc
unsigned m_scope_lim:2; // user scope level when clause was learned, saturated at 3
unsigned m_scope_lim:2; // user scope level when clause was learned (0-3, saturated: levels >=4 map to 3)
literal m_lits[0];
static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }

7
src/sat/sat_solver.cpp
View file

@ -3724,12 +3724,15 @@ namespace sat {
gc_vars(max_var);
// remove learned clauses that were added during the popped user scopes
// scope_lim is saturated at 3, so clauses at scope > old_sz can be identified when old_sz < 3
// remove learned clauses that were added during the popped user scopes.
// scope_lim is saturated at 3, so when old_sz < 3 we can precisely identify
// and remove clauses learned at scope levels above old_sz.
if (old_sz < 3) {
unsigned j = 0;
for (clause* c : m_learned) {
if (c->scope_lim() > old_sz) {
// pop_to_base_level() ensures no clause is on the reinit stack at base level,
// so it is safe to detach and delete the clause.
SASSERT(!c->on_reinit_stack());
detach_clause(*c);
del_clause(*c);