Enum smt2::Term

pub enum Term<E: Environment> {
    Const(E::Constant),
    Var {
        index: usize,
        id: E::Ident,
    },
    Let {
        bindings: Vec<Binding<E>>,
        body: Box<Typed<Term<E>>>,
    },
    Forall {
        vars: Vec<SortedVar<E>>,
        body: Box<Typed<Term<E>>>,
    },
    Exists {
        vars: Vec<SortedVar<E>>,
        body: Box<Typed<Term<E>>>,
    },
    Match {
        term: Box<Typed<Term<E>>>,
        cases: Vec<MatchCase<E>>,
    },
    Apply {
        fun: E::Function,
        args: Box<Vec<Typed<Term<E>>>>,
    },
}

A term.

Variants

Const(E::Constant)

Var

Fields of Var

index: usize

unique identified in the current variable environment.

id: E::Ident

non-unique identifier.

Let

Fields of Let

bindings: Vec<Binding<E>>body: Box<Typed<Term<E>>>

Forall

Fields of Forall

vars: Vec<SortedVar<E>>body: Box<Typed<Term<E>>>

Exists

Fields of Exists

vars: Vec<SortedVar<E>>body: Box<Typed<Term<E>>>

Match

Fields of Match

term: Box<Typed<Term<E>>>cases: Vec<MatchCase<E>>

Apply

Fields of Apply

fun: E::Functionargs: Box<Vec<Typed<Term<E>>>>

Implementations

impl<E: Environment> Term<E>

pub fn apply(
    fun: E::Function,
    args: Vec<Typed<Term<E>>>,
    sort: GroundSort<E::Sort>
) -> Typed<Term<E>>

Trait Implementations

impl<E: Environment> Display for Term<E> where
    E::Constant: Display,
    E::Ident: Display,
    E::Function: Display,
    E::Sort: Display, 

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

Formats the value using the given formatter.

impl<E: Environment> From<Term<E>> for Located<Term> where
    E::Constant: Display,
    E::Ident: Display,
    E::Function: Display,
    E::Sort: Display, 

fn from(term: Term<E>) -> Self

Performs the conversion.

impl<E: Environment> Typable for Term<E>

type Sort = E::Sort

type Environment = E

fn type_decoration(
    &mut self,
    checker: &mut TypeChecker<E::Sort>,
    env: &E,
    this_type: TypeRef<E::Sort>
)