Trait move_model::exp_generator::ExpGenerator

source · [−]
pub trait ExpGenerator<'env> {

Show 35 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;

    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_address_const(&self, value: BigUint) -> 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> { ... }

}
Expand description

A trait that defines a generator for Exp.

Required methods

Get the functional environment

Get the current location

Set the current location

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

Get the type of a local given at temp index

Provided methods

Get the global environment

Sets the default location from a node id.

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

Allocates a new temporary.

Make a boolean constant expression.

Make an address constant.

Makes a Call expression.

Makes a Call expression with type instantiation.

Makes an if-then-else expression.

Makes a Call expression with boolean result type.

Make a boolean not expression.

Make an equality expression.

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

Make an and expression.

Make an or expression.

Make an implies expression.

Make an iff expression.

Make a numerical expression for some of the builtin constants.

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

Join two boolean optional expression with binary operator.

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.

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

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;

Makes a local variable declaration.

Makes a symbol from a string.

Makes a type domain expression.

Makes an expression which selects a field from a struct.

Makes an expression for a temporary.

Makes an expression for a named local.

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

Implementors