From 94b79eefea222f1250e3f569bbd003fb08be0c10 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Mar 2023 20:40:22 -0800
Subject: [PATCH] add back max_occs parameter dependency to solve-eqs

---
 src/ast/simplifiers/solve_eqs.cpp | 42 +++++++++++++++++++++++++++++++
 src/ast/simplifiers/solve_eqs.h   |  7 +++++-
 2 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 65fe8374a..c59ae1e49 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -262,6 +262,48 @@ namespace euf {
         }
     }
 
+    void solve_eqs::collect_num_occs(expr * t, expr_fast_mark1 & visited) {
+        ptr_buffer<app, 128> stack;
+        
+        auto visit = [&](expr* arg) {
+            if (is_uninterp_const(arg)) {                           
+                m_num_occs.insert_if_not_there(arg, 0)++;           
+            }                                                       
+            if (!visited.is_marked(arg) && is_app(arg)) {                          
+                visited.mark(arg, true);                            
+                stack.push_back(to_app(arg));                               
+            }                                                       
+        };
+        
+        visit(t);
+        
+        while (!stack.empty()) {
+            app * t = stack.back();
+            stack.pop_back();
+            for (expr* arg : *t) 
+                visit(arg);
+        }
+    }
+
+    void solve_eqs::collect_num_occs() {
+        if (m_config.m_max_occs == UINT_MAX)
+            return; // no need to compute num occs
+        m_num_occs.reset();
+        expr_fast_mark1 visited;
+        for (unsigned i : indices())
+            collect_num_occs(m_fmls[i].fml(), visited);
+    }
+
+    // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs
+    bool solve_eqs::check_occs(expr * t) const {
+        if (m_config.m_max_occs == UINT_MAX)
+            return true;
+        unsigned num = 0;
+        m_num_occs.find(t, num);
+        TRACE("solve_eqs_check_occs", tout << mk_ismt2_pp(t, m_manager) << " num_occs: " << num << " max: " << m_max_occs << "\n";);
+        return num <= m_config.m_max_occs;
+    }
+
     void solve_eqs::save_subst(vector<dependent_expr> const& old_fmls) {
         if (!m_subst->empty())   
             m_fmls.model_trail().push(m_subst.detach(), old_fmls);                
diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h
index c8fbe3a40..dde42dd94 100644
--- a/src/ast/simplifiers/solve_eqs.h
+++ b/src/ast/simplifiers/solve_eqs.h
@@ -56,10 +56,12 @@ namespace euf {
         expr_mark                     m_unsafe_vars;   // expressions that cannot be replaced
         ptr_vector<expr>              m_todo;
         expr_mark                     m_visited;
+        obj_map<expr, unsigned>       m_num_occs;
+
 
         bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; }
         unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; }
-        bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); }
+        bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e) && check_occs(e); }
         void get_eqs(dep_eq_vector& eqs);
         void filter_unsafe_vars();        
         void extract_subst();
@@ -67,6 +69,9 @@ namespace euf {
         void normalize();
         void apply_subst(vector<dependent_expr>& old_fmls);
         void save_subst(vector<dependent_expr> const& old_fmls);
+        void collect_num_occs(expr * t, expr_fast_mark1 & visited);
+        void collect_num_occs();
+        bool check_occs(expr* t) const;
 
     public: