Struct gf::smt::Sort

pub struct Sort { /* fields omitted */ }

🟢 Sort.

Sorts are reference-counted: the Clone implementation increments the counter, and the Drop implementation decrements it, freeing the sort when it is no longer used.

Implementations

impl Sort

pub fn new_bit_vec(bit_len: usize) -> Self

Construct a bit vector sort of given length.

pub fn new_fn<I>(args: I, result: Sort) -> Self where
    I: IntoIterator<Item = Sort>, 

Construct a function sort.

pub fn from_value(value: &ExprValue) -> Self

Construct sort from a value.

pub fn kind(&self) -> &SortKind

Return the sort kind.

pub fn is_bit_vec(&self) -> bool

Return whether the sort is a bit vector sort.

pub fn is_bit_vec_bool(&self) -> bool

Return whether the sort is a bit vector sort of length 1.

pub fn is_bit_vec_of_len(&self, bit_len: usize) -> bool

Return whether the sort is a bit vector sort of length bit_len.

pub fn is_fn(&self) -> bool

Return whether the sort is a function sort.

pub fn bit_vec_len(&self) -> usize

Return bit vector sort length.

Errors

• Panics if the sort is not a bit vector sort.

pub fn fn_arg_sorts(&self) -> &[Sort]

Return function argument sorts.

Errors

• Panics if the sort is not a function sort.

pub fn fn_result_sort(&self) -> &Sort

Return function result sort.

Errors

• Panics if the sort is not a function sort.

Trait Implementations

impl Clone for Sort

fn clone(&self) -> Sort

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Sort

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

Formats the value using the given formatter.

impl Eq for Sort

impl Hash for Sort

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl PartialEq<Sort> for Sort

fn eq(&self, other: &Sort) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Sort) -> bool

This method tests for !=.

impl StructuralEq for Sort

impl StructuralPartialEq for Sort