From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 22:01:01 +0000 (-0500)
Subject: Check for higher-order variables in TheoryUF::ppRewrite (#7408)
X-Git-Tag: cvc5-1.0.0~1033
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57f8d6c04430277abdb98916b8ac407930abd215;p=cvc5.git

Check for higher-order variables in TheoryUF::ppRewrite (#7408)

Fixes #7000. That sequence of API calls now throws a logic exception.
---

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 096a47c86..fd7cd467e 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env,
 Node HoExtension::ppRewrite(Node node)
 {
   // convert HO_APPLY to APPLY_UF if fully applied
-  if (node[0].getType().getNumChildren() == 2)
+  if (node.getKind() == HO_APPLY)
   {
-    Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
-    Node ret = getApplyUfForHoApply(node);
-    Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
-                   << std::endl;
-    return ret;
+    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 : ppRewrite : " << node << " to " << ret
+                     << std::endl;
+      return ret;
+    }
   }
   return node;
 }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cd974d3e4..ca7dc6a73 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -212,7 +212,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
   Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
                       << std::endl;
   Kind k = node.getKind();
-  if (k == kind::HO_APPLY)
+  if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction()))
   {
     if (!logicInfo().isHigherOrder())
     {
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index d5137393e..a294ad6ca 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -2544,5 +2544,21 @@ TEST_F(TestApiBlackSolver, Output)
   ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
 }
 
+
+TEST_F(TestApiBlackSolver, issue7000)
+{
+  Sort s1 = d_solver.getIntegerSort();
+  Sort s2 = d_solver.mkFunctionSort(s1, s1);
+  Sort s3 = d_solver.getRealSort();
+  Term t4 = d_solver.mkPi();
+  Term t7 = d_solver.mkConst(s3, "_x5");
+  Term t37 = d_solver.mkConst(s2, "_x32");
+  Term t59 = d_solver.mkConst(s2, "_x51");
+  Term t72 = d_solver.mkTerm(EQUAL, t37, t59);
+  Term t74 = d_solver.mkTerm(GT, t4, t7);
+  // throws logic exception since logic is not higher order by default
+  ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5