Change UF ho to ppRewrite instead of expand definition (#5499)

UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite.

4 files changed, 11 insertions, 11 deletions

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index d7de0a025..66bcbc76f 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -36,14 +36,14 @@ HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
   d_true = NodeManager::currentNM()->mkConst(true);
 }
 
-Node HoExtension::expandDefinition(Node node)
+Node HoExtension::ppRewrite(Node node)
 {
   // convert HO_APPLY to APPLY_UF if fully applied
   if (node[0].getType().getNumChildren() == 2)
   {
     Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
     Node ret = getApplyUfForHoApply(node);
-    Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret
+    Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
                    << std::endl;
     return ret;
   }
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index fa9c5c612..0e82dbda6 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -54,7 +54,7 @@ class HoExtension
  public:
   HoExtension(TheoryState& state, TheoryInferenceManager& im);
 
-  /** expand definition
+  /** ppRewrite
    *
    * This returns the expanded form of node.
    *
@@ -63,7 +63,7 @@ class HoExtension
    * function variables for function heads that are not variables via the
    * getApplyUfForHoApply method below.
    */
-  Node expandDefinition(Node node);
+  Node ppRewrite(Node node);
 
   /** check higher order
    *
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 099b56a33..6fdc969a4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -204,21 +204,21 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
 }
 //--------------------------------- end standard check
 
-TrustNode TheoryUF::expandDefinition(Node node)
+TrustNode TheoryUF::ppRewrite(TNode node)
 {
-  Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : "
-                      << node << std::endl;
+  Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
+                      << std::endl;
   if( node.getKind()==kind::HO_APPLY ){
     if( !options::ufHo() ){
       std::stringstream ss;
       ss << "Partial function applications are not supported in default mode, try --uf-ho.";
       throw LogicException(ss.str());
     }
-    Node ret = d_ho->expandDefinition(node);
+    Node ret = d_ho->ppRewrite(node);
     if (ret != node)
     {
-      Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: "
-                          << node << " to " << ret << std::endl;
+      Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node
+                          << " to " << ret << std::endl;
       return TrustNode::mkTrustRewrite(node, ret, nullptr);
     }
   }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 4a63d9584..3f76919eb 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -142,7 +142,7 @@ private:
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
-  TrustNode expandDefinition(Node node) override;
+  TrustNode ppRewrite(TNode node) override;
   void preRegisterTerm(TNode term) override;
   TrustNode explain(TNode n) override;