From 9d09064ad08211bfb436b02bf08ee7cc0ee56ce1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Nov 2022 18:01:38 -0800
Subject: [PATCH] add comments to elim_unconstrained and remove unused function

---
 src/ast/simplifiers/elim_unconstrained.cpp | 16 ++++++++--------
 src/ast/simplifiers/elim_unconstrained.h   |  4 ----
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index cbd575b6a..2cdca3074 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -103,12 +103,6 @@ void elim_unconstrained::eliminate() {
     }
 }
 
-void elim_unconstrained::add_term(expr* t) {
-    expr_ref_vector terms(m);
-    terms.push_back(t);
-    init_terms(terms);
-}
-
 expr* elim_unconstrained::get_parent(unsigned n) const {
     for (expr* p : get_node(n).m_parents)
         if (get_node(p).m_refcount > 0 && get_node(p).m_term == get_node(p).m_orig)
@@ -128,20 +122,23 @@ void elim_unconstrained::init_nodes() {
         terms.push_back(m_fmls[i].fml());
     m_trail.append(terms);
     m_heap.reset();
+    m_frozen.reset();
 
+    // initialize nodes for terms in the original goal
     init_terms(terms);
 
+    // top-level terms have reference count > 0
     for (expr* e : terms)
         inc_ref(e);
 
-    // freeze subterms before the head.
+    // freeze subterms before the already processed head
     terms.reset();
     for (unsigned i = 0; i < m_qhead; ++i)
         terms.push_back(m_fmls[i].fml());
     for (expr* e : subterms::all(terms))
         m_frozen.mark(e, true);    
 
-    
+    // freeze subterms that occur with recursive function definitions
     recfun::util rec(m);
     if (rec.has_rec_defs()) {
         for (func_decl* f : rec.get_rec_funs()) {
@@ -152,6 +149,9 @@ void elim_unconstrained::init_nodes() {
     }
 }
 
+/**
+* Create nodes for all terms in the goal
+*/
 void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
     unsigned max_id = 0;
     for (expr* e : subterms::all(terms))
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index 327ceeff0..67d64027b 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -58,14 +58,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
     void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
     void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
     void gc(expr* t);
-
     expr* get_parent(unsigned n) const;
     void init_refcounts();
     void dec_refcounts(expr* t);
-
-    void add_term(expr* t);
     void init_terms(expr_ref_vector const& terms);
-
     void init_nodes();
     void eliminate();
     void reconstruct_terms();