From b551a2b5d950f495d9309cb754c9c89abda95ffa Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 28 Apr 2022 20:08:43 +0300
Subject: [PATCH] int-blaster: not allowing higher order functions (#8674)

Currently we throw an OptionException if higher order logic is enabled, but we only check this once we reach an APPLY_FUN node.
This PR does the check regardless of APPLY_FUN, thus capturing, e.g. BAG_MAP.
Fixes cvc5/cvc5-projects#415.
The PR also includes a simplified version of the test from that issue.
---
 src/theory/bv/int_blaster.cpp                 | 38 ++++++++++---------
 test/regress/cli/CMakeLists.txt               |  1 +
 .../cli/regress0/bv/bv_to_int_415.smt2        |  9 +++++
 3 files changed, 31 insertions(+), 17 deletions(-)
 create mode 100644 test/regress/cli/regress0/bv/bv_to_int_415.smt2

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 85159a424..1c348a071 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -273,6 +273,17 @@ Node IntBlaster::translateWithChildren(
   // Store the translated node
   Node returnNode;
 
+   /**
+    * higher order logic allows comparing between functions
+    * The translation does not support this,
+    * as the translated functions may be different outside
+    * of the bounds that were relevant for the original
+    * bit-vectors.
+    */
+   if (childrenTypesChanged(original) && logicInfo().isHigherOrder())
+   {
+     throw OptionException("bv-to-int does not support higher order logic ");
+   }
   // Translate according to the kind of the original node.
   switch (oldKind)
   {
@@ -534,17 +545,6 @@ Node IntBlaster::translateWithChildren(
     }
     case kind::APPLY_UF:
     {
-      /**
-       * higher order logic allows comparing between functions
-       * The translation does not support this,
-       * as the translated functions may be different outside
-       * of the bounds that were relevant for the original
-       * bit-vectors.
-       */
-      if (childrenTypesChanged(original) && logicInfo().isHigherOrder())
-      {
-        throw OptionException("bv-to-int does not support higher order logic ");
-      }
       // Insert the translated application term to the cache
       returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children);
       // Add range constraints if necessary.
@@ -816,13 +816,17 @@ bool IntBlaster::childrenTypesChanged(Node n)
   bool result = false;
   for (const Node& child : n)
   {
-    TypeNode originalType = child.getType();
-    Assert(d_intblastCache.find(child) != d_intblastCache.end());
-    TypeNode newType = d_intblastCache[child].get().getType();
-    if (!newType.isSubtypeOf(originalType))
+    // the child's type has changed only if it has been
+    // processed already
+    if (d_intblastCache.find(child) != d_intblastCache.end())
     {
-      result = true;
-      break;
+      TypeNode originalType = child.getType();
+      TypeNode newType = d_intblastCache[child].get().getType();
+      if (!newType.isSubtypeOf(originalType))
+      {
+        result = true;
+        break;
+      }
     }
   }
   return result;
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 464304bcb..5712c5c0b 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -270,6 +270,7 @@ set(regress_0_tests
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bv_to_int1.smt2
+  regress0/bv/bv_to_int_415.smt2
   regress0/bv/bv_to_int_5230_binary.smt2
   regress0/bv/bv_to_int_5230_missing_op.smt2
   regress0/bv/bv_to_int_5230_shift_const.smt2
diff --git a/test/regress/cli/regress0/bv/bv_to_int_415.smt2 b/test/regress/cli/regress0/bv/bv_to_int_415.smt2
new file mode 100644
index 000000000..a6e96f9f7
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_415.smt2
@@ -0,0 +1,9 @@
+; EXPECT: 
+; SCRUBBER: grep -v "higher.order"
+; EXIT: 1
+(set-option :solve-bv-as-int sum)
+(set-logic HO_ALL)
+(declare-const _x108 (Bag (_ BitVec 4)) )
+(declare-fun _x113 ((_ BitVec 4)) (_ BitVec 4))
+(assert (= (bag.map _x113 _x108) (as bag.empty (Bag (_ BitVec 4)))))
+(check-sat)
-- 
2.30.2