Struct ConstraintLocalEnv 

struct ConstraintLocalEnv<'a, T: Types> {
    declarations: String,
    symbols: HashMap<String, T::Var>,
    global_symbols: &'a HashMap<String, T::Var>,
}

Declarations active in a single constraint’s solver scope (as a string to send to Z3), and maps to decode its response back to T.

Fields

declarations: String

symbols: HashMap<String, T::Var>

global_symbols: &'a HashMap<String, T::Var>

Implementations

impl<'a, T: Types> ConstraintLocalEnv<'a, T>

fn new( globals: &'a ConstraintGlobalEnv<T>, binder_consts: &[ConstDecl<T>], binders: &[(T::Var, Sort<T>)], ) -> Self

fn symbol(&self, name: &str) -> Option<&T::Var>

fn decode(&self, sexp: &Sexp) -> Result<Expr<T>, SuggestionSolverError>

fn decode_symbol(&self, name: &str) -> Result<Expr<T>, SuggestionSolverError>

fn decode_application( &self, items: &[Sexp], ) -> Result<Expr<T>, SuggestionSolverError>