build fix

src/ast/expr_substitution.h

@@ -45,6 +45,7 @@ public:
     unsigned size() const { return m_subst.size(); }
     void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
     void erase(expr * s);
+    expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; }
     bool find(expr * s, expr * & def, proof * & def_pr);
     bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
     bool contains(expr * s);

src/ast/simplifiers/extract_eqs.h

@@ -30,7 +30,7 @@ namespace euf {
         app* var;
         expr_ref term;
         expr_dependency* dep;
-        dependent_eq(app* var, expr_ref& term, expr_dependency* d) : var(var), term(term), dep(d) {}
+        dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {}
     };
 
     typedef vector<dependent_eq> dep_eq_vector;

src/ast/simplifiers/solve_eqs.cpp

@@ -20,7 +20,7 @@ Author:
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
-#include "ast/arith_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/simplifiers/solve_eqs.h"
 
@@ -37,7 +37,7 @@ namespace euf {
             sz = std::max(sz, v->get_id());
         m_var2id.resize(sz + 1, UINT_MAX);
         for (auto const& [v, t, d] : eqs) {
-            if (is_var(v))
+            if (is_var(v) || !can_be_var(v))
                 continue;
             m_var2id[v->get_id()] = m_id2var.size();
             m_id2var.push_back(v);
@@ -103,7 +103,9 @@ namespace euf {
     }
 
     void solve_eqs::add_subst(dependent_eq const& eq) {
+        SASSERT(can_be_var(eq.var));
         m_subst->insert(eq.var, eq.term, nullptr, eq.dep);
+        ++m_stats.m_num_elim_vars;
     }
 
     void solve_eqs::normalize() {
@@ -118,10 +120,11 @@ namespace euf {
         proof_ref new_pr(m);
 
         for (unsigned id : m_subst_ids) {
-            // checkpoint();
+            if (!m.inc())
+                break;
             auto const& [v, def, dep] = m_next[id][0];
             rp->operator()(def, new_def, new_pr, new_dep);
-            // m_num_steps += rp->get_num_steps() + 1;
+            m_stats.m_num_steps += rp->get_num_steps() + 1;
             new_dep = m.mk_join(dep, new_dep);
             m_subst->insert(v, new_def, new_pr, new_dep);
             // we updated the substitution, but we don't need to reset rp
@@ -141,6 +144,8 @@ namespace euf {
     }
 
     void solve_eqs::apply_subst() {
+        if (!m.inc())
+            return;
         scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
         rp->set_substitution(m_subst.get());
         expr_ref new_f(m);
@@ -170,6 +175,23 @@ namespace euf {
         advance_qhead(m_fmls.size());
     }
 
+    void solve_eqs::filter_unsafe_vars() {
+        m_unsafe_vars.reset();
+        recfun::util rec(m);
+        for (func_decl* f : rec.get_rec_funs())
+            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m)))
+                m_unsafe_vars.mark(term);
+    }
+
+#if 0
+    model_converter_ref solve_eqs::get_model_converter() {
+        model_converter_ref mc = alloc(gmc, m, "solve-eqs");
+        for (unsigned id : m_subst_ids) 
+            static_cast<gmc*>(mc.get())->add(id2var(id), m_subst->find(v));
+        return mc;
+    }
+#endif
+
     solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : 
         dependent_expr_simplifier(m, fmls), m_rewriter(m) {
         register_extract_eqs(m, m_extract_plugins);
@@ -186,4 +208,9 @@ namespace euf {
 #endif
     }
 
+    void solve_eqs::collect_statistics(statistics& st) const {
+        st.update("solve-eqs-steps", m_stats.m_num_steps);
+        st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars);
+    }
+
 }

src/ast/simplifiers/solve_eqs.h

@@ -26,6 +26,11 @@ Author:
 namespace euf {
 
     class solve_eqs : public dependent_expr_simplifier {
+        struct stats {
+            unsigned m_num_steps = 0;
+            unsigned m_num_elim_vars = 0;
+        };
+
         th_rewriter                   m_rewriter;
         scoped_ptr_vector<extract_eq> m_extract_plugins;
         unsigned_vector               m_var2id, m_id2level, m_subst_ids;
@@ -33,6 +38,9 @@ namespace euf {
         vector<dep_eq_vector>         m_next;  
         scoped_ptr<expr_substitution> m_subst;
 
+        expr_mark                     m_unsafe_vars;   // expressions that cannot be replaced
+        stats                         m_stats;
+
         void add_subst(dependent_eq const& eq);
 
         bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; }
@@ -48,6 +56,8 @@ namespace euf {
                 ex->get_eqs(f, eqs);
         }
 
+        void filter_unsafe_vars();
+        bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); }
         void extract_subst();
         void extract_dep_graph(dep_eq_vector& eqs);
         void normalize();
@@ -62,5 +72,8 @@ namespace euf {
         void reduce() override;
 
         void updt_params(params_ref const& p) override;
+        void collect_statistics(statistics& st) const override;
+
+        // model_converter_ref get_model_converter();
     };
 }

src/tactic/core/solve_eqs_tactic.cpp

@@ -977,14 +977,8 @@ class solve_eqs_tactic : public tactic {
             if (m_produce_models) {
                 if (!mc.get())
                     mc = alloc(gmc, m(), "solve-eqs");
-                for (app* v : m_ordered_vars) {
-                    expr * def = nullptr;
-                    proof * pr;
-                    expr_dependency * dep = nullptr;
-                    m_norm_subst->find(v, def, pr, dep);
-                    SASSERT(def);
-                    static_cast<gmc*>(mc.get())->add(v, def);
-                }
+                for (app* v : m_ordered_vars) 
+                    static_cast<gmc*>(mc.get())->add(v, m_norm_subst->find(v));
             }
         }