Fix push/pop scopes affecting performance of subsequent proofs

Add a 2-bit scope_lim field to the SAT clause struct to track the user scope
level at which each learned clause was created. When user_pop is called, learned
clauses that were added during the popped user scopes are removed.

The root cause was that learned clauses accumulated during inner push/pop scopes
were persisting after pop, polluting the clause database and biasing the search
for subsequent proofs.

- sat_clause.h: Add m_scope_lim:2 bitfield and set_scope_lim/scope_lim accessors
- sat_clause.cpp: Initialize m_scope_lim=0 in constructor, copy in copy_clause
- sat_solver.cpp (mk_nary_clause): Set scope_lim when adding learned clauses
- sat_solver.cpp (user_pop): After gc_vars, remove learned clauses with
  scope_lim > new scope level (handles up to 3 levels of nesting precisely)

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/sat/sat_clause.cpp

@@ -34,7 +34,8 @@ namespace sat {
         m_reinit_stack(false),
         m_inact_rounds(0),
         m_glue(255),
-        m_psm(255) {
+        m_psm(255),
+        m_scope_lim(0) {
         memcpy(m_lits, lits, sizeof(literal) * sz);
         mark_strengthened();
         SASSERT(check_approx());
@@ -192,6 +193,7 @@ namespace sat {
         cls->m_psm    = other.psm();
         cls->m_frozen = other.frozen();
         cls->m_approx = other.approx();
+        cls->m_scope_lim = other.scope_lim();
         return cls;
     }
 

src/sat/sat_clause.h

@@ -53,6 +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
         literal            m_lits[0];
 
         static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
@@ -103,6 +104,8 @@ namespace sat {
 
         bool on_reinit_stack() const { return m_reinit_stack; }
         void set_reinit_stack(bool f) { m_reinit_stack = f; }
+        unsigned scope_lim() const { return m_scope_lim; }
+        void set_scope_lim(unsigned lim) { m_scope_lim = lim > 3 ? 3 : lim; }
     };
 
     std::ostream & operator<<(std::ostream & out, clause_vector const & cs);

src/sat/sat_solver.cpp

@@ -549,8 +549,10 @@ namespace sat {
  
         if (reinit || has_variables_to_reinit(*r)) 
             push_reinit_stack(*r);
-        if (st.is_redundant()) 
+        if (st.is_redundant()) {
+            r->set_scope_lim(m_user_scope_literals.size());
             m_learned.push_back(r);
+        }
         else 
             m_clauses.push_back(r);
         if (m_config.m_drat) 
@@ -3721,6 +3723,22 @@ namespace sat {
             m_ext->user_pop(num_scopes);
     
         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
+        if (old_sz < 3) {
+            unsigned j = 0;
+            for (clause* c : m_learned) {
+                if (c->scope_lim() > old_sz) {
+                    SASSERT(!c->on_reinit_stack());
+                    detach_clause(*c);
+                    del_clause(*c);
+                }
+                else
+                    m_learned[j++] = c;
+            }
+            m_learned.shrink(j);
+        }
         TRACE(sat, display(tout););
 
         m_qhead = 0;