Struct z3::ast::Array [−][src]
pub struct Array<'ctx> { /* fields omitted */ }
Expand description
Ast
node representing an array value.
An array in Z3 is a mapping from indices to values.
Implementations
Create an Array
which maps from indices of the domain
Sort
to
values of the range
Sort
.
All values in the Array
will be unconstrained.
pub fn fresh_const(
ctx: &'ctx Context,
prefix: &str,
domain: &Sort<'ctx>,
range: &Sort<'ctx>
) -> Array<'ctx>
Create a “constant array”, that is, an Array
initialized so that all of the
indices in the domain
map to the given value val
Get the value at a given index in the array.
Note that the index
must be of the array’s domain
sort.
The return type will be of the array’s range
sort.
Trait Implementations
Compare this Ast
with another Ast
, and get a Result. Errors if the sort does not
match for the two values. Read more
Simplify the Ast
. Returns a new Ast
which is equivalent,
but simplified using algebraic simplification rules, such as
constant propagation. Read more
Performs substitution on the Ast
. The slice substitutions
contains a
list of pairs with a “from” Ast
that will be substituted by a “to” Ast
. Read more
Return the number of children of this Ast
. Read more
Return the n
th child of this Ast
. Read more
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Array<'ctx>
impl<'ctx> UnwindSafe for Array<'ctx>
Blanket Implementations
Mutably borrows from an owned value. Read more