Struct SortChecker 

pub struct SortChecker<'a>(/* private fields */);

Trait Implementations

impl<'a> Debug for SortChecker<'a>

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

Formats the value using the given formatter.

impl<L: Logic> Folder<L> for SortChecker<'_>

type Output = ISort

Type produced by the transformation. If Output = Term<T>, implement IntraLogicFolder instead. If Output = Term<U> for some U: Logic, implement InterLogicFolder instead.

type Error = UnknownSort<Term<L>>

Type of errors that the folder may run into.

fn fold_const(&mut self, constant: IConst) -> Result<Self::Output, Self::Error>

Transforms a constant.

fn fold_var(&mut self, var: IVar<L::Var>) -> Result<Self::Output, Self::Error>

Transforms a variable.

fn fold_core_op(&mut self, op: ICoreOp<L>) -> Result<Self::Output, Self::Error>

Transforms an SMT-LIB Core operation, recursively folding its arguments.

fn fold_theory_op(&mut self, op: IOp<L>) -> Result<Self::Output, Self::Error>

Transforms a non-core operation, recursively folding its arguments.

fn fold_uninterpreted_func( &mut self, uf: IUF<L>, ) -> Result<Self::Output, Self::Error>

Transforms an uninterpreted function, recursively folding its arguments.

fn fold_let(&mut self, l: ILet<L>) -> Result<Self::Output, Self::Error>

Transforms a let binder, recursively folding its arguments.

fn fold_match(&mut self, m: IMatch<L>) -> Result<Self::Output, Self::Error>

Transforms a match binder, recursively folding its arguments.

fn fold_quantifier( &mut self, quantifier: IQuantifier<L>, ) -> Result<Self::Output, Self::Error>

Transforms a quantifier, recursively folding its arguments.

fn context(&self) -> Option<&Ctx>

Gets the context tracked by the folder, if applicable. Tracking context enables things like determining the sorts of expressions and which variables are free/bound, but a folder that doesn’t need that information can leave this method defaulted, which will return None.

fn context_mut(&mut self) -> Option<&mut Ctx>

Gets a mutable reference to the context tracked by the folder, if applicable. Tracking context enables things like determining the sorts of expressions and which variables are free/bound, but a folder that doesn’t need that information can leave this method defaulted, which will return None.

fn fold_term(&mut self, term: Term<T>) -> Result<Self::Output, Self::Error>

Transforms a term, recursively transforming its contents. By default, calls SuperFold::super_fold_with.

fn fold_set_logic( &mut self, logic: ISymbol, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a set-logic command. By default, returns as-is.

fn fold_assert( &mut self, asserted: Term<T>, ) -> Result<Command<Self::Output>, Self::Error>

Transforms an asserted term. By default, calls Self::fold_term.

fn fold_declare_const( &mut self, symbol: ISymbol, sort: ISort, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a constant declaration. By default, returns as-is.

fn fold_declare_fun( &mut self, symbol: ISymbol, parameters: Vec<ISort>, sort: ISort, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a function declaration. By default, returns as-is.

fn fold_declare_sort( &mut self, symbol: ISymbol, arity: Numeral, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a sort declaration. By default, returns as-is.

fn fold_define_fun( &mut self, sig: FunctionDec, body: Term<T>, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a function definition. By default, recursively transforms the function body with Self::fold_term.

fn fold_define_fun_rec( &mut self, sig: FunctionDec, body: Term<T>, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a recursive function definition. By default, recursively transforms the function body with Self::fold_term.

fn fold_define_funs_rec( &mut self, funs: Vec<(FunctionDec, Term<T>)>, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a set of recursive function definition. By default, recursively transforms each function body with Self::fold_term.

fn fold_define_sort( &mut self, symbol: ISymbol, parameters: Vec<ISymbol>, sort: ISort, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a sort definition. By default, returns as-is.

fn fold_get_value( &mut self, terms: Vec<Term<T>>, ) -> Result<Command<Self::Output>, Self::Error>

Transforms a get-value call. By default, recursively transforms each term with Self::fold_term.