Struct Sort 

pub struct Sort {
    pub head: SortHead,
    pub arguments: SArc<[SortArgument]>,
}

The sort of a term.

Sort represent the semantic notion of sort of a term, i.e. its type. Sorts are represented by the application of some arguments to a function, called sort constructor, whose range must be Sort::sort(), the sort of sorts.

In contrast to Term, sorts can be constructed directly and are not uniqued.

Most methods that would accept a Sort accept instead a generic instance of the ToSort trait. See its documentation for details.

Fields

head: SortHead

The sort constructor that is being applied.

arguments: SArc<[SortArgument]>

The sort’s arguments.

Implementations

impl Sort

pub fn of(term: &Term) -> Result<Sort>

Alias for term.type_check(ctx) which provide a better notation.

impl Sort

pub const fn sort() -> Sort

The sort of sorts.

Sort::sort() returns a special sort, not provided by any theory, which is the sort of terms representing sorts. In other words, a sort term such as (Array Int Real) has sort Sort::sort().

let mut solver = Solver::new(&Config::default().logic("ALIA"))?;

// construct and resolve the term
let array = solver.lookup(term!(Array Int Int), Role::Sort)?;
let sort = Sort::of(&array)?; // deduce the sort of the term

assert_eq!(sort, Sort::sort()); // the resulting sort is `Sort::sort()`

Trait Implementations

impl Clone for Sort

fn clone(&self) -> Self

Returns a duplicate 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 Display for Sort

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

Formats the value using the given formatter.

impl Eq for Sort

impl From<Identifier<'_>> for Sort

fn from(value: Identifier<'_>) -> Self

Converts to this type from the input type.

impl From<Sort> for Sort

fn from(value: Sort) -> Self

Converts to this type from the input type.

impl<T: Into<Function>> From<T> for Sort

fn from(value: T) -> Self

Converts to this type from the input type.

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, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<'t> Into<Sort> for UFLIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for UFLRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for LIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for LRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for LIRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for NIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for NRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_UFLIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_UFLRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_UFNIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_UFNRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_LIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_LRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_NIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_NRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_LIRA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for ALIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_ALIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for UFALIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for QF_UFALIA_Sort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl Into<Sort> for CoreSort

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl Into<Sort> for RealsSort

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl Into<Sort> for IntsSort

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl Into<Sort> for RealsIntsSort

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl<'t> Into<Sort> for ArraysSort<'t>

fn into(self) -> Sort

Converts this type into the (usually inferred) input type.

impl PartialEq for Sort

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

Equality operator ==.

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

Inequality operator !=.

impl Pretty for Sort

fn pretty(&self) -> RcDoc<'static>

impl Resolve for Sort

fn resolve(&self, env: &Env, pool: &dyn TermPool, role: Role) -> Result<Self>

Perform name resolution on self.

impl StructuralPartialEq for Sort

impl ToTerm for Sort

fn into_term_in(self, pool: &dyn TermPool) -> Term

Convert the object into a Term by uniquing in the given TermPool.

fn to_term_in(&self, pool: &dyn TermPool) -> Term

Convert the object (by reference) into a Term by uniquing in the given TermPool.

impl<'t> TryFrom<&'t Sort> for UFLIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for UFLRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for LIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for LRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for LIRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for NIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for NRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_UFLIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_UFLRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_UFNIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_UFNRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_LIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_LRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_NIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_NRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_LIRA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for ALIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_ALIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for UFALIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for QF_UFALIA_Sort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<Self, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for CoreSort

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<CoreSort, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for RealsSort

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<RealsSort, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for IntsSort

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<IntsSort, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for RealsIntsSort

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<RealsIntsSort, Self::Error>

Performs the conversion.

impl<'t> TryFrom<&'t Sort> for ArraysSort<'t>

type Error = &'t Sort

The type returned in the event of a conversion error.

fn try_from(sort: &'t Sort) -> Result<ArraysSort<'t>, Self::Error>

Performs the conversion.

impl TryFrom<Infer> for Sort

type Error = Diagnostic

The type returned in the event of a conversion error.

fn try_from(_value: Infer) -> Result<Self, Diagnostic>

Performs the conversion.

impl TryFrom<Term> for Sort

type Error = InvalidSortTerm

The type returned in the event of a conversion error.

fn try_from(term: Term) -> Result<Sort, InvalidSortTerm>

Performs the conversion.

impl TypeCheck for Sort

fn type_check(&self) -> Result<Sort>