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.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index b5fa79cd0f30aea203d20484a18f9cc7f259f97e..f95160df700fe9531f7e87df73bf0a19e86ad466 100644 (file)
--- 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 94e6fc5188dbc88abb88e89d8d1e21db6d313076..533a0365716723ff986ee88c71c82423db883437 100644 (file)
--- 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 8eb0ef6866a57bc6c69a8e84b3d48db2cd021057..c2baf8be6ee5c51f185d6df87a993b4d2e3caf31 100644 (file)
--- 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 ad08dfa84dc4f7d198a739029cf276b39f1c6ad3..64c9f3f04e3d4fa91b97e17475c1f28ab1f87819 100644 (file)
--- 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