diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 4a60e19b..2d9a321a 100644 --- a/z3/src/ast.rs +++ b/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]) -> Bool<'ctx> where Self: Sized, { unsafe { Bool::wrap(ctx, { assert!(values.len() <= 0xffffffff); - let values: Vec = values.iter().map(|nodes| nodes.get_z3_ast()).collect(); + let values: Vec = 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> {