#5336

Z3Prover · Jun 16, 2021 · 6b5680f · 6b5680f
1 parent 38fc97d
commit 6b5680f
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp
@@ -328,5 +328,17 @@ namespace recfun {
         }
         return found;
     }
+
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+        if (n->num_args() == 0)
+            dep.insert(n, nullptr);
+        for (auto* k : euf::enode_args(n))
+            dep.add(n, k);
+        return true;
+    }
+
+    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+        values.set(n->get_root_id(), n->get_root()->get_expr());
+    }
 
 }
diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h
@@ -103,6 +103,8 @@ namespace recfun {
         bool unit_propagate() override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool is_shared(euf::theory_var v) const override { return true; }
         void init_search() override {}
         bool should_research(sat::literal_vector const& core) override;