Struct AstVector 

pub struct AstVector { /* private fields */ }

Vector of Z3 AST nodes.

This wraps a Z3-ref-counted vector of asts. This type exists mainly as a high-level compatibility layer for these types from Rust. As this type wraps heterogenous asts, it is analagous to Vec<Dynamic>.

Most users will usually be better off using a Vec; this type primarily exists as a compatibility shim.

Many standard rust collection and iteration traits are implemented on it for convenience.

Implementations

impl AstVector

pub fn new() -> AstVector

Create a new empty AST vector.

pub fn len(&self) -> usize

Get the number of elements in the vector.

pub fn is_empty(&self) -> bool

Check if the vector is empty.

pub fn get(&self, index: usize) -> Dynamic

Get the element at the specified index.

Panics

Panics if the index is out of bounds.

pub fn set(&self, index: usize, ast: &impl Ast)

Set the element at the specified index.

Panics

Panics if the index is out of bounds.

pub fn push(&self, ast: &impl Ast)

Push an element to the end of the vector.

pub fn resize(&self, new_size: usize)

Resize the vector to the specified size.

New elements (if any) are uninitialized.

pub fn to_vec(&self) -> Vec<Dynamic>

Convert the vector to a Vec<Dynamic>.

pub fn translate(&self, target_ctx: &Context) -> AstVector

Translate the AST vector to another context.

pub fn iter(&self) -> AstVectorIter<'_>

Return a borrowing iterator over the elements.

Trait Implementations

impl Debug for AstVector

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for AstVector

fn default() -> Self

Returns the “default value” for a type.

impl Display for AstVector

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Drop for AstVector

fn drop(&mut self)

Executes the destructor for this type.

impl<T: Ast> From<&[T]> for AstVector

Build an AstVector from a borrowed slice, avoiding clones.

fn from(slice: &[T]) -> Self

Converts to this type from the input type.

impl<T: Ast> From<Vec<T>> for AstVector

fn from(v: Vec<T>) -> Self

Converts to this type from the input type.

impl<T: Ast> FromIterator<T> for AstVector

fn from_iter<I: IntoIterator<Item = T>>(iter: I) -> Self

Creates a value from an iterator.

impl<'a> IntoIterator for &'a AstVector

type Item = Dynamic

The type of the elements being iterated over.

type IntoIter = AstVectorIter<'a>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl IntoIterator for AstVector

type Item = Dynamic

The type of the elements being iterated over.

type IntoIter = AstVectorIntoIter

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl TryFrom<AstVector> for Vec<Array>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<BV>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Bool>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Datatype>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Float>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Int>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Real>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Seq>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<Set>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.

impl TryFrom<AstVector> for Vec<String>

type Error = String

The type returned in the event of a conversion error.

fn try_from(v: AstVector) -> Result<Self, Self::Error>

Performs the conversion.