Enum Dynamic

pub enum Dynamic<'a, S: SmtSolver<'a>> {
    BV(S::BV),
    Int(S::Int),
    Bool(S::Bool),
    BvArray(S::BvArray),
}

An expression that is dynamically typed.

Variants

BV(S::BV)

A bitvector.

Int(S::Int)

An integer.

Bool(S::Bool)

A boolean.

BvArray(S::BvArray)

An array.

Implementations

impl<'a, S: SmtSolver<'a>> Dynamic<'a, S>

pub fn from_bv(bv: S::BV) -> Self

Creates a dynamically typed SMT expression from a boolean.

pub fn as_bv(self) -> Option<S::BV>

If the expression is a bitvector, returns the bitvector. Otherwise, returns None.

pub fn as_int(self) -> Option<S::Int>

If the expression is an integer, returns the integer. Otherwise, returns None.

pub fn as_bool(self) -> Option<S::Bool>

If the expression is a bool, returns the bool. Otherwise, returns None.

pub fn as_bv_array(self) -> Option<S::BvArray>

If the expression is a bitvector array, returns the array. Otherwise, returns None.

pub fn sort_kind(&self) -> SortKind

Returns the sort kind of the expression.

pub fn sort(&self) -> Sort

Returns the sort of the expression.

pub fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

pub fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

Panics if the expressions are not of the same type.

pub fn _eq(self, other: Self) -> S::Bool

Returns an SMT expression that performs an equality comparison between the two expressions.

Panics if the expressions are not of the same type.

Trait Implementations

impl<'a, S: SmtSolver<'a>> Clone for Dynamic<'a, S>

fn clone(&self) -> Self

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a, S: SmtSolver<'a>> Debug for Dynamic<'a, S>

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

Formats the value using the given formatter.