remove assignments to lambdas, exposed by Z3Prover#4169

Author: NikolajBjorner

src/smt/smt_context.cpp

@@ -62,6 +62,7 @@ namespace smt {
         m_fingerprints(m, m_region),
         m_b_internalized_stack(m),
         m_e_internalized_stack(m),
+        m_l_internalized_stack(m),
         m_final_check_idx(0),
         m_is_auxiliary(false),
         m_par(nullptr),

src/smt/smt_context.h

@@ -107,6 +107,7 @@ namespace smt {
         // enodes. Examples: boolean expression nested in an
         // uninterpreted function.
         expr_ref_vector             m_e_internalized_stack; // stack of the expressions already internalized as enodes.
+        quantifier_ref_vector       m_l_internalized_stack;
 
         ptr_vector<justification>   m_justifications;
 
@@ -776,19 +777,25 @@ namespace smt {
             void undo(context & ctx) override { ctx.undo_mk_bool_var(); }
         };
         mk_bool_var_trail   m_mk_bool_var_trail;
-
         void undo_mk_bool_var();
 
         friend class mk_enode_trail;
         class mk_enode_trail : public trail<context> {
         public:
             void undo(context & ctx) override { ctx.undo_mk_enode(); }
         };
-
         mk_enode_trail   m_mk_enode_trail;
-
         void undo_mk_enode();
 
+        friend class mk_lambda_trail;
+        class mk_lambda_trail : public trail<context> {
+        public:
+            void undo(context & ctx) override { ctx.undo_mk_lambda(); }
+        };
+        mk_lambda_trail   m_mk_lambda_trail;
+        void undo_mk_lambda();
+
+
         void apply_sort_cnstr(app * term, enode * e);
 
         bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits);

src/smt/smt_internalizer.cpp

@@ -575,6 +575,8 @@ namespace smt {
         internalize_quantifier(fa, true);
         if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name);
         m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
+        m_l_internalized_stack.push_back(q);
+        m_trail_stack.push_back(&m_mk_lambda_trail);
     }
 
     /**
@@ -992,6 +994,14 @@ namespace smt {
         return e;
     }
 
+    void context::undo_mk_lambda() {
+        SASSERT(!m_l_internalized_stack.empty());
+        m_stats.m_num_del_enode++;
+        quantifier * n         = m_l_internalized_stack.back();
+        m_app2enode[n->get_id()] = nullptr;
+        m_l_internalized_stack.pop_back();
+    }
+
     void context::undo_mk_enode() {
         SASSERT(!m_e_internalized_stack.empty());
         m_stats.m_num_del_enode++;
@@ -1001,7 +1011,7 @@ namespace smt {
         unsigned n_id         = n->get_id();
         SASSERT(is_app(n));
         enode * e             = m_app2enode[n_id];
-        m_app2enode[n_id]     = 0;
+        m_app2enode[n_id]     = nullptr;
         if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
             SASSERT(m_cg_table.contains_ptr(e));
             m_cg_table.erase(e);