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.

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 85159a4240b05a714fa18b10b0619bb1a163b1ba..1c348a0718373a8e46dddd9d2d8b46bdce3d95f0 100644 (file)
--- 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 464304bcbc2b6ffe8b75637aa96af1fe7300f80d..5712c5c0b9620591b853d20dc1e60cee125d82a6 100644 (file)
--- 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 (file)
index 0000000..a6e96f9
--- /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)