Add ite_bv_array

liblisa/src/smt/cache.rs

@@ -913,6 +913,13 @@ impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBool<'ctx, CachedSolver
         }
     }
 
+    fn ite_bv_array(self, lhs: CacheBVArray<'ctx, S>, rhs: CacheBVArray<'ctx, S>) -> CacheBVArray<'ctx, S> {
+        CacheBVArray {
+            inner: self.inner.ite_bv_array(lhs.inner, rhs.inner),
+            tree: Tree::Ite(Box::new([self.tree, lhs.tree, rhs.tree])),
+        }
+    }
+
     fn as_bool(&self) -> Option<bool> {
         self.inner.as_bool()
     }

liblisa/src/smt/solver.rs

@@ -310,6 +310,11 @@ pub trait SmtBool<'a, S: SmtSolver<'a, Bool = Self>>:
     /// `lhs` is returned if the boolean value is true, `rhs` if it is false.
     fn ite_bool(self, lhs: S::Bool, rhs: S::Bool) -> S::Bool;
 
+    /// Creates an If-Then-Else expression that returns bitvector arrays.
+    ///
+    /// `lhs` is returned if the boolean value is true, `rhs` if it is false.
+    fn ite_bv_array(self, lhs: S::BvArray, rhs: S::BvArray) -> S::BvArray;
+
     /// Creates an If-Then-Else expression that returns [`Dynamic`]s.
     ///
     /// `lhs` is returned if the boolean value is true, `rhs` if it is false.
@@ -318,6 +323,7 @@ pub trait SmtBool<'a, S: SmtSolver<'a, Bool = Self>>:
             (Dynamic::BV(a), Dynamic::BV(b)) => self.ite_bv(a, b).into_dynamic(),
             (Dynamic::Int(a), Dynamic::Int(b)) => self.ite_int(a, b).into_dynamic(),
             (Dynamic::Bool(a), Dynamic::Bool(b)) => self.ite_bool(a, b).into_dynamic(),
+            (Dynamic::BvArray(a), Dynamic::BvArray(b)) => self.ite_bv_array(a, b).into_dynamic(),
             (a, b) => panic!("ITE branches must have same sort: {a:?} vs {b:?}"),
         }
     }

liblisa/src/smt/z3/mod.rs

@@ -505,6 +505,22 @@ impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx> {
         Bool(self.0.ite(&lhs.0, &rhs.0))
     }
 
+    fn ite_bv_array(self, lhs: BvArray<'ctx>, rhs: BvArray<'ctx>) -> BvArray<'ctx> {
+        assert_eq!(
+            lhs.element_size, rhs.element_size,
+            "element size mismatch in ite_bv_array({lhs:?}, {rhs:?})"
+        );
+        assert_eq!(
+            lhs.index_size, rhs.index_size,
+            "index size mismatch in ite_bv_array({lhs:?}, {rhs:?})"
+        );
+        BvArray {
+            element_size: lhs.element_size,
+            index_size: lhs.index_size,
+            inner: self.0.ite(&lhs.inner, &rhs.inner),
+        }
+    }
+
     fn is_identical(&self, other: &Self) -> bool {
         self.to_string() == other.to_string()
     }