Trait move_model::exp_generator::ExpGenerator

pub trait ExpGenerator<'env> {
    // Required methods
    fn function_env(&self) -> &FunctionEnv<'env>;
    fn get_current_loc(&self) -> Loc;
    fn set_loc(&mut self, loc: Loc);
    fn add_local(&mut self, ty: Type) -> TempIndex;
    fn get_local_type(&self, temp: TempIndex) -> Type;

    // Provided methods
    fn global_env(&self) -> &'env GlobalEnv { ... }
    fn set_loc_from_node(&mut self, node_id: NodeId) { ... }
    fn new_node(&self, ty: Type, inst_opt: Option<Vec<Type>>) -> NodeId { ... }
    fn new_temp(&mut self, ty: Type) -> TempIndex { ... }
    fn mk_bool_const(&self, value: bool) -> Exp { ... }
    fn mk_call(&self, ty: &Type, oper: Operation, args: Vec<Exp>) -> Exp { ... }
    fn mk_call_with_inst(
        &self,
        ty: &Type,
        inst: Vec<Type>,
        oper: Operation,
        args: Vec<Exp>
    ) -> Exp { ... }
    fn mk_ite(&self, cond: ExpData, if_true: ExpData, if_false: ExpData) -> Exp { ... }
    fn mk_bool_call(&self, oper: Operation, args: Vec<Exp>) -> Exp { ... }
    fn mk_not(&self, arg: Exp) -> Exp { ... }
    fn mk_eq(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_identical(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_and(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_or(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_implies(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_iff(&self, arg1: Exp, arg2: Exp) -> Exp { ... }
    fn mk_builtin_num_const(&self, oper: Operation) -> Exp { ... }
    fn mk_join_bool(
        &self,
        oper: Operation,
        args: impl Iterator<Item = Exp>
    ) -> Option<Exp> { ... }
    fn mk_join_opt_bool(
        &self,
        oper: Operation,
        arg1: Option<Exp>,
        arg2: Option<Exp>
    ) -> Option<Exp> { ... }
    fn mk_vector_quant_opt<F>(
        &self,
        kind: QuantKind,
        vector: Exp,
        elem_ty: &Type,
        f: &mut F
    ) -> Option<Exp>
       where F: FnMut(Exp) -> Option<Exp> { ... }
    fn mk_mem_quant_opt<F>(
        &self,
        kind: QuantKind,
        mem: QualifiedId<StructId>,
        f: &mut F
    ) -> Option<ExpData>
       where F: FnMut(Exp) -> Option<Exp> { ... }
    fn mk_inst_mem_quant_opt<F>(
        &self,
        kind: QuantKind,
        mem: &QualifiedInstId<StructId>,
        f: &mut F
    ) -> Option<Exp>
       where F: FnMut(Exp) -> Option<Exp> { ... }
    fn mk_decl(&self, name: Symbol, ty: Type, binding: Option<Exp>) -> LocalVarDecl { ... }
    fn mk_symbol(&self, str: &str) -> Symbol { ... }
    fn mk_type_domain(&self, ty: Type) -> Exp { ... }
    fn mk_field_select(
        &self,
        field_env: &FieldEnv<'_>,
        targs: &[Type],
        exp: Exp
    ) -> Exp { ... }
    fn mk_temporary(&self, temp: TempIndex) -> Exp { ... }
    fn mk_local(&self, name: &str, ty: Type) -> Exp { ... }
    fn get_memory_of_node(&self, node_id: NodeId) -> QualifiedInstId<StructId> { ... }
}

A trait that defines a generator for Exp.

Required Methods

fn function_env(&self) -> &FunctionEnv<'env>

Get the functional environment

fn get_current_loc(&self) -> Loc

Get the current location

fn set_loc(&mut self, loc: Loc)

Set the current location

fn add_local(&mut self, ty: Type) -> TempIndex

Add a local variable with given type, return the local index.

fn get_local_type(&self, temp: TempIndex) -> Type

Get the type of a local given at temp index

Provided Methods

fn global_env(&self) -> &'env GlobalEnv

Get the global environment

fn set_loc_from_node(&mut self, node_id: NodeId)

Sets the default location from a node id.

fn new_node(&self, ty: Type, inst_opt: Option<Vec<Type>>) -> NodeId

Creates a new expression node id, using current default location, provided type, and optional instantiation.

fn new_temp(&mut self, ty: Type) -> TempIndex

Allocates a new temporary.

fn mk_bool_const(&self, value: bool) -> Exp

Make a boolean constant expression.

fn mk_call(&self, ty: &Type, oper: Operation, args: Vec<Exp>) -> Exp

Makes a Call expression.

fn mk_call_with_inst( &self, ty: &Type, inst: Vec<Type>, oper: Operation, args: Vec<Exp> ) -> Exp

Makes a Call expression with type instantiation.

fn mk_ite(&self, cond: ExpData, if_true: ExpData, if_false: ExpData) -> Exp

Makes an if-then-else expression.

fn mk_bool_call(&self, oper: Operation, args: Vec<Exp>) -> Exp

Makes a Call expression with boolean result type.

fn mk_not(&self, arg: Exp) -> Exp

Make a boolean not expression.

fn mk_eq(&self, arg1: Exp, arg2: Exp) -> Exp

Make an equality expression.

fn mk_identical(&self, arg1: Exp, arg2: Exp) -> Exp

Make an identical equality expression. This is stronger than make_equal because it requires the exact same representation, not only interpretation.

fn mk_and(&self, arg1: Exp, arg2: Exp) -> Exp

Make an and expression.

fn mk_or(&self, arg1: Exp, arg2: Exp) -> Exp

Make an or expression.

fn mk_implies(&self, arg1: Exp, arg2: Exp) -> Exp

Make an implies expression.

fn mk_iff(&self, arg1: Exp, arg2: Exp) -> Exp

Make an iff expression.

fn mk_builtin_num_const(&self, oper: Operation) -> Exp

Make a numerical expression for some of the builtin constants.

fn mk_join_bool( &self, oper: Operation, args: impl Iterator<Item = Exp> ) -> Option<Exp>

Join an iterator of boolean expressions with a boolean binary operator.

fn mk_join_opt_bool( &self, oper: Operation, arg1: Option<Exp>, arg2: Option<Exp> ) -> Option<Exp>

Join two boolean optional expression with binary operator.

fn mk_vector_quant_opt<F>( &self, kind: QuantKind, vector: Exp, elem_ty: &Type, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of a vector. The passed function f receives an expression representing an element of the vector and returns the quantifiers predicate; if it returns None, this function will also return None, otherwise the quantifier will be returned.

fn mk_mem_quant_opt<F>( &self, kind: QuantKind, mem: QualifiedId<StructId>, f: &mut F ) -> Option<ExpData>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of memory. The passed function f receives

fn mk_inst_mem_quant_opt<F>( &self, kind: QuantKind, mem: &QualifiedInstId<StructId>, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of instantiated memory. The passed function f receives an expression representing a value in memory and returns the quantifiers predicate;

fn mk_decl(&self, name: Symbol, ty: Type, binding: Option<Exp>) -> LocalVarDecl

Makes a local variable declaration.

fn mk_symbol(&self, str: &str) -> Symbol

Makes a symbol from a string.

fn mk_type_domain(&self, ty: Type) -> Exp

Makes a type domain expression.

fn mk_field_select( &self, field_env: &FieldEnv<'_>, targs: &[Type], exp: Exp ) -> Exp

Makes an expression which selects a field from a struct.

fn mk_temporary(&self, temp: TempIndex) -> Exp

Makes an expression for a temporary.

fn mk_local(&self, name: &str, ty: Type) -> Exp

Makes an expression for a named local.

fn get_memory_of_node(&self, node_id: NodeId) -> QualifiedInstId<StructId>

Get’s the memory associated with a Call(Global,..) or Call(Exists, ..) node. Crashes if the the node is not typed as expected.

Implementors