Move implementation of UF rewriter to cpp (#6393)

2 files changed, 216 insertions, 157 deletions

diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp
new file mode 100644
index 000000000..082fe349e
--- /dev/null
+++ b/src/theory/uf/theory_uf_rewriter.cpp
@@ -0,0 +1,205 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Theory UF rewriter
+ */
+
+#include "theory/uf/theory_uf_rewriter.h"
+
+#include "expr/node_algorithm.h"
+#include "options/uf_options.h"
+#include "theory/rewriter.h"
+#include "theory/substitutions.h"
+
+namespace cvc5 {
+namespace theory {
+namespace uf {
+
+RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
+{
+  if (node.getKind() == kind::EQUAL)
+  {
+    if (node[0] == node[1])
+    {
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(true));
+    }
+    else if (node[0].isConst() && node[1].isConst())
+    {
+      // uninterpreted constants are all distinct
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(false));
+    }
+    if (node[0] > node[1])
+    {
+      Node newNode =
+          NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+  }
+  if (node.getKind() == kind::APPLY_UF)
+  {
+    if (node.getOperator().getKind() == kind::LAMBDA)
+    {
+      Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : " << node
+                          << "\n";
+      TNode lambda = node.getOperator();
+      Node ret;
+      // build capture-avoiding substitution since in HOL shadowing may have
+      // been introduced
+      if (options::ufHo())
+      {
+        std::vector<Node> vars;
+        std::vector<Node> subs;
+        for (const Node& v : lambda[0])
+        {
+          vars.push_back(v);
+        }
+        for (const Node& s : node)
+        {
+          subs.push_back(s);
+        }
+        if (Trace.isOn("uf-ho-beta"))
+        {
+          Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
+                              << " vars into " << subs.size() << " terms :\n";
+          for (unsigned i = 0, size = subs.size(); i < size; ++i)
+          {
+            Trace("uf-ho-beta")
+                << "uf-ho-beta: .... " << vars[i] << " |-> " << subs[i] << "\n";
+          }
+        }
+        ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
+        Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
+      }
+      else
+      {
+        std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
+        std::vector<TNode> subs(node.begin(), node.end());
+        ret = lambda[1].substitute(
+            vars.begin(), vars.end(), subs.begin(), subs.end());
+      }
+      return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+    }
+    else if (!canUseAsApplyUfOperator(node.getOperator()))
+    {
+      return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
+    }
+  }
+  else if (node.getKind() == kind::HO_APPLY)
+  {
+    if (node[0].getKind() == kind::LAMBDA)
+    {
+      // resolve one argument of the lambda
+      Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing one argument of : "
+                          << node[0] << " with " << node[1] << "\n";
+
+      // reconstruct the lambda first to avoid variable shadowing
+      Node new_body = node[0][1];
+      if (node[0][0].getNumChildren() > 1)
+      {
+        std::vector<Node> new_vars(node[0][0].begin() + 1, node[0][0].end());
+        std::vector<Node> largs;
+        largs.push_back(
+            NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, new_vars));
+        largs.push_back(new_body);
+        new_body = NodeManager::currentNM()->mkNode(kind::LAMBDA, largs);
+        Trace("uf-ho-beta")
+            << "uf-ho-beta : ....new lambda : " << new_body << "\n";
+      }
+
+      // build capture-avoiding substitution since in HOL shadowing may have
+      // been introduced
+      if (options::ufHo())
+      {
+        Node arg = Rewriter::rewrite(node[1]);
+        Node var = node[0][0][0];
+        new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
+      }
+      else
+      {
+        TNode arg = Rewriter::rewrite(node[1]);
+        TNode var = node[0][0][0];
+        new_body = new_body.substitute(var, arg);
+      }
+      Trace("uf-ho-beta") << "uf-ho-beta : ..new body : " << new_body << "\n";
+      return RewriteResponse(REWRITE_AGAIN_FULL, new_body);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryUfRewriter::preRewrite(TNode node)
+{
+  if (node.getKind() == kind::EQUAL)
+  {
+    if (node[0] == node[1])
+    {
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(true));
+    }
+    else if (node[0].isConst() && node[1].isConst())
+    {
+      // uninterpreted constants are all distinct
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(false));
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n)
+{
+  Assert(n.getKind() == kind::APPLY_UF);
+  Node curr = n.getOperator();
+  for (unsigned i = 0; i < n.getNumChildren(); i++)
+  {
+    curr = NodeManager::currentNM()->mkNode(kind::HO_APPLY, curr, n[i]);
+  }
+  return curr;
+}
+Node TheoryUfRewriter::getApplyUfForHoApply(TNode n)
+{
+  Assert(n.getType().getNumChildren() == 2);
+  std::vector<TNode> children;
+  TNode curr = decomposeHoApply(n, children, true);
+  // if operator is standard
+  if (canUseAsApplyUfOperator(curr))
+  {
+    return NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
+  }
+  // cannot construct APPLY_UF if operator is partially applied or is not
+  // standard
+  return Node::null();
+}
+Node TheoryUfRewriter::decomposeHoApply(TNode n,
+                                        std::vector<TNode>& args,
+                                        bool opInArgs)
+{
+  TNode curr = n;
+  while (curr.getKind() == kind::HO_APPLY)
+  {
+    args.push_back(curr[1]);
+    curr = curr[0];
+  }
+  if (opInArgs)
+  {
+    args.push_back(curr);
+  }
+  std::reverse(args.begin(), args.end());
+  return curr;
+}
+bool TheoryUfRewriter::canUseAsApplyUfOperator(TNode n) { return n.isVar(); }
+
+}  // namespace uf
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 4a06c0322..23576b7a1 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -34,168 +34,24 @@ namespace uf {
 class TheoryUfRewriter : public TheoryRewriter
 {
  public:
-  RewriteResponse postRewrite(TNode node) override
-  {
-    if(node.getKind() == kind::EQUAL) {
-      if(node[0] == node[1]) {
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-      } else if(node[0].isConst() && node[1].isConst()) {
-        // uninterpreted constants are all distinct
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
-      }
-      if (node[0] > node[1]) {
-        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
-        return RewriteResponse(REWRITE_DONE, newNode);
-      }
-    }
-    if(node.getKind() == kind::APPLY_UF) {
-      if( node.getOperator().getKind() == kind::LAMBDA ){
-        Trace("uf-ho-beta")
-          << "uf-ho-beta : beta-reducing all args of : " << node << "\n";
-        TNode lambda = node.getOperator();
-        Node ret;
-        // build capture-avoiding substitution since in HOL shadowing may have
-        // been introduced
-        if (options::ufHo())
-        {
-          std::vector<Node> vars;
-          std::vector<Node> subs;
-          for (const Node& v : lambda[0])
-          {
-            vars.push_back(v);
-          }
-          for (const Node& s : node)
-          {
-            subs.push_back(s);
-          }
-          if (Trace.isOn("uf-ho-beta"))
-          {
-            Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
-                                << " vars into " << subs.size() << " terms :\n";
-            for (unsigned i = 0, size = subs.size(); i < size; ++i)
-            {
-              Trace("uf-ho-beta") << "uf-ho-beta: .... " << vars[i] << " |-> "
-                                  << subs[i] << "\n";
-            }
-          }
-          ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
-          Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
-        }
-        else
-        {
-          std::vector<TNode> vars;
-          std::vector<TNode> subs;
-          for (const TNode& v : lambda[0])
-          {
-            vars.push_back(v);
-          }
-          for (const TNode& s : node)
-          {
-            subs.push_back(s);
-          }
-          ret = lambda[1].substitute(
-              vars.begin(), vars.end(), subs.begin(), subs.end());
-        }
-        return RewriteResponse(REWRITE_AGAIN_FULL, ret);
-      }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
-        return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
-      }
-    }else if( node.getKind() == kind::HO_APPLY ){
-      if( node[0].getKind() == kind::LAMBDA ){
-        // resolve one argument of the lambda
-        Trace("uf-ho-beta")
-            << "uf-ho-beta : beta-reducing one argument of : " << node[0]
-            << " with " << node[1] << "\n";
+  RewriteResponse postRewrite(TNode node) override;
 
-        // reconstruct the lambda first to avoid variable shadowing
-        Node new_body = node[0][1];
-        if( node[0][0].getNumChildren()>1 ){
-          std::vector< Node > new_vars;
-          for( unsigned i=1; i<node[0][0].getNumChildren(); i++ ){
-            new_vars.push_back( node[0][0][i] );
-          }
-          std::vector< Node > largs;
-          largs.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, new_vars ) );
-          largs.push_back( new_body );
-          new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs );
-          Trace("uf-ho-beta")
-            << "uf-ho-beta : ....new lambda : " << new_body << "\n";
-        }
+  RewriteResponse preRewrite(TNode node) override;
 
-        // build capture-avoiding substitution since in HOL shadowing may have
-        // been introduced
-        if (options::ufHo())
-        {
-          Node arg = Rewriter::rewrite(node[1]);
-          Node var = node[0][0][0];
-          new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
-        }
-        else
-        {
-          TNode arg = Rewriter::rewrite(node[1]);
-          TNode var = node[0][0][0];
-          new_body = new_body.substitute(var, arg);
-        }
-        Trace("uf-ho-beta")
-            << "uf-ho-beta : ..new body : " << new_body << "\n";
-        return RewriteResponse( REWRITE_AGAIN_FULL, new_body );
-      }
-    }
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  RewriteResponse preRewrite(TNode node) override
-  {
-    if(node.getKind() == kind::EQUAL) {
-      if(node[0] == node[1]) {
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-      } else if(node[0].isConst() && node[1].isConst()) {
-        // uninterpreted constants are all distinct
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
-      }
-    }
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-public: //conversion between HO_APPLY AND APPLY_UF
-  // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b)
-  static Node getHoApplyForApplyUf(TNode n) {
-    Assert(n.getKind() == kind::APPLY_UF);
-    Node curr = n.getOperator();
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] );     
-    }
-    return curr;
-  }
+ public:  // conversion between HO_APPLY AND APPLY_UF
+  // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a)
+  // b)
+  static Node getHoApplyForApplyUf(TNode n);
   // converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b)
-  static Node getApplyUfForHoApply(TNode n) {
-    Assert(n.getType().getNumChildren() == 2);
-    std::vector< TNode > children;
-    TNode curr = decomposeHoApply( n, children, true );
-    // if operator is standard
-    if( canUseAsApplyUfOperator( curr ) ){
-      return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
-    }
-    // cannot construct APPLY_UF if operator is partially applied or is not standard       
-    return Node::null();
-  }
+  static Node getApplyUfForHoApply(TNode n);
   /**
    * Given a curried HO_APPLY term n, this method adds its arguments into args
    * and returns its operator. If the argument opInArgs is true, then we add
    * its operator to args.
    */
-  static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) {
-    TNode curr = n;
-    while( curr.getKind() == kind::HO_APPLY ){
-      args.push_back( curr[1] );
-      curr = curr[0];        
-    }
-    if( opInArgs ){
-      args.push_back( curr );
-    }
-    std::reverse( args.begin(), args.end() );
-    return curr;
-  }
+  static Node decomposeHoApply(TNode n,
+                               std::vector<TNode>& args,
+                               bool opInArgs = false);
   /** returns true if this node can be used as an operator of an APPLY_UF node.  In higher-order logic,
    * terms can have function types and not just variables. 
    * Currently, we want only free variables to be used as operators of APPLY_UF nodes. This is motivated by
@@ -204,9 +60,7 @@ public: //conversion between HO_APPLY AND APPLY_UF
    * forall x : ( Int -> Int ), y : Int. (x y) = (f 0)
    * Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not.
    */
-  static inline bool canUseAsApplyUfOperator(TNode n){
-    return n.isVar();
-  }
+  static bool canUseAsApplyUfOperator(TNode n);
 }; /* class TheoryUfRewriter */
 
 }  // namespace uf