Trait Sorted

pub trait Sorted<'st>: Into<STerm<'st>> {
    type Inner: Sorted<'st>;

    // Required methods
    fn sort(&self) -> Sort<'st>;
    fn is_sort(sort: Sort<'st>) -> bool;
    fn st(&self) -> &'st Storage;

    // Provided methods
    fn sterm(self) -> STerm<'st> { ... }
    fn term(self) -> &'st Term<'st> { ... }
    fn from_dynamic(d: Dynamic<'st>) -> Self
       where Self: From<(STerm<'st>, Sort<'st>)> { ... }
    fn try_from_dynamic(d: Dynamic<'st>) -> Option<Self>
       where Self: From<(STerm<'st>, Sort<'st>)> { ... }
    fn into_dynamic(self) -> Dynamic<'st> { ... }
    fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st> { ... }
    fn _neq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st> { ... }
    fn labeled(self) -> (Label<Self>, Self::Inner)
       where Self::Inner: From<STerm<'st>> { ... }
}

An trait for typing STM-LIB terms.

This trait indicates that a type can construct a Term which is the low-level primitive that is used to define expressions for the SMT solvers to evaluate.

Required Associated Types

type Inner: Sorted<'st>

The inner type of the term. This is used for Const<'st, T> where the inner type is T.

Required Methods

fn sort(&self) -> Sort<'st>

The sort of the term.

fn is_sort(sort: Sort<'st>) -> bool

Check if a sort is of this type.

fn st(&self) -> &'st Storage

The storage associated with any term of this sort.

Provided Methods

fn sterm(self) -> STerm<'st>

Constructy the smtlib AST representation of the term with associated storage.

fn term(self) -> &'st Term<'st>

Construct the smtlib AST representation of term.

fn from_dynamic(d: Dynamic<'st>) -> Self

where Self: From<(STerm<'st>, Sort<'st>)>,

Casts a dynamically typed term into a concrete type

fn try_from_dynamic(d: Dynamic<'st>) -> Option<Self>

where Self: From<(STerm<'st>, Sort<'st>)>,

Casts a dynamically typed term into a concrete type iff the dynamic sort matches

fn into_dynamic(self) -> Dynamic<'st>

Casts the term into a dynamic term which looses static types and stores the sort dynamically.

fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>

Construct the term representing (= self other)

fn _neq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>

Construct the term representing (distinct self other)

fn labeled(self) -> (Label<Self>, Self::Inner)

where Self::Inner: From<STerm<'st>>,

Wraps the term in a a label, which can be used to extract information from models at a later point.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<'st> Sorted<'st> for Dynamic<'st>

type Inner = Dynamic<'st>

impl<'st, T: Sorted<'st>> Sorted<'st> for Const<'st, T>

type Inner = T

impl<'st, T: StaticSorted<'st>> Sorted<'st> for T

type Inner = <T as StaticSorted<'st>>::Inner