Struct FromSexpWrapper 

pub struct FromSexpWrapper<T: Types, Parser> {
    pub parser: Parser,
    pub _phantom: PhantomData<T>,
    scopes: Vec<IndexSet<String>>,
}

Fields

parser: Parser

_phantom: PhantomData<T>

scopes: Vec<IndexSet<String>>

Implementations

impl<T, Parser: FromSexp<T>> FromSexpWrapper<T, Parser>

where T: Types,

fn parse_bv_size(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError>

pub fn parse_name(&self, sexp: &Sexp) -> Result<T::Var, ParseError>

pub fn parse_bind(&mut self, sexp: &Sexp) -> Result<Bind<T>, ParseError>

fn parse_pred_inner(&mut self, sexp: &Sexp) -> Result<Pred<T>, ParseError>

pub fn parse_kvar(&self, sexp: &Sexp) -> Result<Pred<T>, ParseError>

fn parse_expr_possibly_nested( &mut self, sexp: &Sexp, ) -> Result<Expr<T>, ParseError>

fn parse_is_ctor( &mut self, ctor_name: &str, arg: &Sexp, ) -> Result<Expr<T>, ParseError>

pub fn parse_expr(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_neg(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_not(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_iff(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_imp(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_and(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_or(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_atom(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_app(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_binary_op(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_exists(&mut self, items: &[Sexp]) -> Result<Expr<T>, ParseError>

fn parse_let(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError>

fn parse_list_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError>

pub fn parse_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError>

fn parse_func_sort(&self, items: &[Sexp]) -> Result<Sort<T>, ParseError>

pub fn parse_solution( &mut self, sexp: &Sexp, ) -> Result<(Vec<Sort<T>>, Expr<T>), ParseError>

fn push_scope(&mut self, names: &[String])

fn pop_scope(&mut self)

fn parse_bound_var(&self, name: &str) -> Option<Expr<T>>