Trait rsmt2::print::FunDef

source · [−]
pub trait FunDef<Info = ()> {
    type FunSym: Sym2Smt<Info>;
    type SortedSym: SymAndSort<Info>;
    type ArgsIter: Iterator<Item = Self::SortedSym>;
    type OutSort: Sort2Smt;
    type Body: Expr2Smt<Info>;

    fn fun_sym(&self) -> &Self::FunSym;
    fn args(&self) -> Self::ArgsIter;
    fn out_sort(&self) -> &Self::OutSort;
    fn body(&self) -> &Self::Body;
}
Expand description

Function definition data.

Used by Solver::define_funs_rec and Solver::define_funs_rec.

Required Associated Types

Type of the function’s symbol (name).

Type of the arguments (name, sort).

Type of the iterator over the arguments.

Type of the function’s output sort.

Type of the body.

Required Methods

Function name accessor.

Arguments accessor.

Output sort accessor.

Function’s body accessor.

Implementations on Foreign Types

Implementors