add back max_occs parameter dependency to solve-eqs

Z3Prover · Mar 2, 2023 · 94b79ee · 94b79ee
1 parent acd2eaa
commit 94b79ee
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 1 deletion.
diff --git 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
@@ -56,17 +56,22 @@ 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();
         void extract_dep_graph(dep_eq_vector& eqs);
         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: