From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Nov 2020 17:49:59 +0000 (-0600)
Subject: Change UF ho to ppRewrite instead of expand definition (#5499)
X-Git-Tag: cvc5-1.0.0~2557
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6c001e078767a2de6f36a2fa1333b98e39a6ec8;p=cvc5.git

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 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;
 
diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p
index d2977ddb8..e162a63a4 100644
--- 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 edb55d756..313ff68a1 100644
--- 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 5ad693629..d0577dd1f 100644
--- 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
 
 %------------------------------------------------------------------------------