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 096a47c8678cab0009b9b06d8d4cf7593e557c09..fd7cd467e6bceee1a4a31add1edca26774d134d0 100644 (file)
--- 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 cd974d3e42027eb6c8eae6ff54ad70f7af8dba21..ca7dc6a73adc5e1ace1952d319a7ccf1b2a7f52a 100644 (file)
--- 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 d5137393e5fce358f415f4825396833f8fba3e97..a294ad6cac437b21e062f406e95c7b7d5b587850 100644 (file)
--- 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