Enum Sort

pub enum Sort<'st> {
    Static(Sort<'st>),
    Dynamic {
        st: &'st Storage,
        name: &'st str,
        index: &'st [Index<'st>],
        parameters: &'st [Sort<'st>],
    },
}

A SMT-LIB sort.

Variants

Static(Sort<'st>)

A built-in sort.

Dynamic

A user-defined sort.

Fields

st: &'st Storage

smtlib storage

name: &'st str

The name of the sort.

index: &'st [Index<'st>]

The index of the sort.

parameters: &'st [Sort<'st>]

The parameters of the sort.

Implementations

impl<'st> Sort<'st>

pub fn new(st: &'st Storage, name: impl Into<String>) -> Self

Create a new dynamic sort.

pub fn new_parametric( st: &'st Storage, name: impl Into<String>, parameters: &[Sort<'st>], ) -> Self

Create a new dynamic sort with parameters.

pub fn new_indexed( st: &'st Storage, name: impl Into<String>, index: &[Index<'st>], ) -> Self

Create a new dynamic sort with index.

pub fn ast(self) -> Sort<'st>

Get the smtlib AST representation of the sort.

pub fn new_const( &self, st: &'st Storage, name: impl Into<String>, ) -> Const<'st, Dynamic<'st>>

Create a new constant of this sort.

Trait Implementations

impl<'st> Clone for Sort<'st>

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

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'st> Debug for Sort<'st>

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

Formats the value using the given formatter.

impl Display for Sort<'_>

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

Formats the value using the given formatter.

impl<'st> From<Sort<'st>> for Sort<'st>

fn from(sort: Sort<'st>) -> Self

Converts to this type from the input type.

impl<'st> PartialEq for Sort<'st>

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'st> Copy for Sort<'st>

impl<'st> Eq for Sort<'st>

impl<'st> StructuralPartialEq for Sort<'st>