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.

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index d7de0a025d0250dff5274d79715c628d73718bf3..66bcbc76f41bc2bccd13a63fcf5956c79c5c011b 100644 (file)
--- 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 fa9c5c612ca6d7863b74a175eff8c92647bc8b36..0e82dbda64b2c185057c41de793b02c8c711baa8 100644 (file)
--- 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 099b56a33ecbe83b97f3b7f5766ced3bd0fba846..6fdc969a4cce7aea94fd6172471e1bedde3a3a47 100644 (file)
--- 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 4a63d95846aad67396df71b606787ed54b8e50f6..3f76919eb5514b20ff2715992f700125553b6681 100644 (file)
--- 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;
 

diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p
index d2977ddb8e210eb3a76173e7a1048569f4641d8b..e162a63a43de13911e573566af0f275adb895f83 100644 (file)
--- a/test/regress/regress1/ho/NUM925^1.p
+++ b/test/regress/regress1/ho/NUM925^1.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho
+% COMMAND-LINE:  --uf-ho --ho-elim
 % EXPECT: % SZS status Theorem for NUM925^1
 
 %------------------------------------------------------------------------------

diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
index edb55d756a1638337f3392f21d7c3b909db7dab4..313ff68a1e4df2712374c33980e54c1e7b03b3bc 100644 (file)
--- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models
+; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim
 ; EXPECT: unsat
 
 (set-logic ALL)

diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p
index 5ad693629f53eef9e1f018b7c1c38f5a8742db25..d0577dd1f1008d511e43cacaf2c1230adc2e8e99 100644 (file)
--- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p
+++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho
+% COMMAND-LINE:  --uf-ho --ho-elim
 % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3
 
 %------------------------------------------------------------------------------