From e1074c87769d079936b52a8e8ea33cc03f8b4638 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Dec 2019 15:02:28 -0600
Subject: [PATCH] Use the evaluator utility in the function definition
 evaluator (#3576)

Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.
---
 src/theory/evaluator.cpp                     | 6 +++---
 src/theory/evaluator.h                       | 6 +++---
 src/theory/quantifiers/fun_def_evaluator.cpp | 8 +++-----
 src/theory/quantifiers/fun_def_evaluator.h   | 3 +++
 4 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index b5fa79cd0..f95160df7 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -116,7 +116,7 @@ Node EvalResult::toNode() const
 
 Node Evaluator::eval(TNode n,
                      const std::vector<Node>& args,
-                     const std::vector<Node>& vals)
+                     const std::vector<Node>& vals) const
 {
   Trace("evaluator") << "Evaluating " << n << " under substitution " << args
                      << " " << vals << std::endl;
@@ -142,7 +142,7 @@ EvalResult Evaluator::evalInternal(
     TNode n,
     const std::vector<Node>& args,
     const std::vector<Node>& vals,
-    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode)
+    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const
 {
   std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
   std::vector<TNode> queue;
@@ -793,7 +793,7 @@ EvalResult Evaluator::evalInternal(
 Node Evaluator::reconstruct(
     TNode n,
     std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
-    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode)
+    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const
 {
   if (n.getNumChildren() == 0)
   {
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 94e6fc518..533a03657 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -94,7 +94,7 @@ class Evaluator
    */
   Node eval(TNode n,
             const std::vector<Node>& args,
-            const std::vector<Node>& vals);
+            const std::vector<Node>& vals) const;
 
  private:
   /**
@@ -117,7 +117,7 @@ class Evaluator
       TNode n,
       const std::vector<Node>& args,
       const std::vector<Node>& vals,
-      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode);
+      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
   /** reconstruct
    *
    * This function reconstructs the result of evaluating n using a combination
@@ -130,7 +130,7 @@ class Evaluator
   Node reconstruct(
       TNode n,
       std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
-      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode);
+      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
 };
 
 }  // namespace theory
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 8eb0ef686..c2baf8be6 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -181,11 +181,8 @@ Node FunDefEvaluator::evaluate(Node n) const
           const std::vector<Node>& args = itf->second.d_args;
           if (!args.empty())
           {
-            // invoke it on arguments
-            sbody = sbody.substitute(
-                args.begin(), args.end(), children.begin(), children.end());
-            // rewrite it
-            sbody = Rewriter::rewrite(sbody);
+            // invoke it on arguments using the evaluator
+            sbody = d_eval.eval(sbody, args, children);
             if (Trace.isOn("fd-eval-debug2"))
             {
               Trace("fd-eval-debug2")
@@ -197,6 +194,7 @@ Node FunDefEvaluator::evaluate(Node n) const
               Trace("fd-eval-debug2")
                   << "FunDefEvaluator: results in " << sbody << "\n";
             }
+            Assert(!sbody.isNull());
           }
           // our result is the result of the body
           visited[cur] = sbody;
diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h
index ad08dfa84..64c9f3f04 100644
--- a/src/theory/quantifiers/fun_def_evaluator.h
+++ b/src/theory/quantifiers/fun_def_evaluator.h
@@ -20,6 +20,7 @@
 #include <map>
 #include <vector>
 #include "expr/node.h"
+#include "theory/evaluator.h"
 
 namespace CVC4 {
 namespace theory {
@@ -63,6 +64,8 @@ class FunDefEvaluator
   };
   /** maps functions to the above information */
   std::map<Node, FunDefInfo> d_funDefMap;
+  /** evaluator utility */
+  Evaluator d_eval;
 };
 
 }  // namespace quantifiers
-- 
2.30.2