is_const_array and Distinct with &[impl Borrow<Self>]

z3/src/ast.rs

@@ -264,14 +264,17 @@ pub trait Ast<'ctx>: fmt::Debug {
     /// `Ast`s being compared must all be the same type.
     //
     // Note that we can't use the varop! macro because of the `pub` keyword on it
-    fn distinct(ctx: &'ctx Context, values: &[&Self]) -> Bool<'ctx>
+    fn distinct(ctx: &'ctx Context, values: &[impl Borrow<Self>]) -> Bool<'ctx>
     where
         Self: Sized,
     {
         unsafe {
             Bool::wrap(ctx, {
                 assert!(values.len() <= 0xffffffff);
-                let values: Vec<Z3_ast> = values.iter().map(|nodes| nodes.get_z3_ast()).collect();
+                let values: Vec<Z3_ast> = values
+                    .iter()
+                    .map(|nodes| nodes.borrow().get_z3_ast())
+                    .collect();
                 Z3_mk_distinct(ctx.z3_ctx, values.len() as u32, values.as_ptr())
             })
         }
@@ -1525,6 +1528,27 @@ impl<'ctx> Array<'ctx> {
             })
         }
     }
+
+    /// Returns true if the array is a const array (i.e. a.is_const_array() => exists v, forall i. select(a, i) == v)
+    ///
+    /// # Examples
+    /// ```
+    /// # use z3::{ast, Config, Context, ast::{Array, Int}, Sort};
+    /// # use z3::ast::Ast;
+    /// # use std::convert::TryInto;
+    /// # let cfg = Config::new();
+    /// # let ctx = Context::new(&cfg);
+    /// let arr = Array::const_array(&ctx, &Sort::int(&ctx), &Int::from_u64(&ctx, 9));
+    /// assert!(arr.is_const_array());
+    /// let arr2 = Array::fresh_const(&ctx, "a", &Sort::int(&ctx), &Sort::int(&ctx));
+    /// assert!(!arr2.is_const_array());
+    /// ```
+    pub fn is_const_array(&self) -> bool {
+        // python:
+        // is_app_of(a, Z3_OP_CONST_ARRAY)
+        // >> is_app(a) and a.decl().kind() == Z3_OP_CONST_ARRAY
+        self.is_app() && matches!(self.decl().kind(), DeclKind::CONST_ARRAY)
+    }
 }
 
 impl<'ctx> Set<'ctx> {