Var (kind2dev@731decdf5fb1.Var)

Types and hash-consing

type t

Hashconsed variable

Hashtables, maps and sets

val compare_vars : t -> t -> int

Comparison function on variables

val equal_vars : t -> t -> bool

Equality function on variables

val hash_var : t -> int

Hashing function on variables

module VarHashtbl : Stdlib.Hashtbl.S with type key = t

Hash table over variables

module VarSet : Stdlib.Set.S with type elt = t

Set over variables

module VarMap : Stdlib.Map.S with type key = t

Map over variables

Constructors

val mk_const_state_var : StateVar.t -> t

Return a constant state variable.

The state variable must be constant.

val mk_state_var_instance : StateVar.t -> Numeral.t -> t

Return an instance of a state variable.

The state variable may also be constant, in which case a variable created by mk_const_state_var is returned.

val mk_free_var : HString.t -> Type.t -> t

Return a free variable

val mk_fresh_var : Type.t -> t

Return a fresh free variable

val mk_binder_var : Type.t -> int -> t

mk_binder_var t d is the variable standing for the variable of type t of a binder at binding depth d, used to open that binder. Memoized: the same t and d always give the same variable.

val is_binder_var : t -> bool

Return true if the variable was made by mk_binder_var, and so stands for the variable of an opened binder rather than for a variable of the term that binder occurs in.

val import : t -> t

Import a variable from a different instance into this hashcons table

Accessor functions

val type_of_var : t -> Type.t

Return the type of the variable

val state_var_of_state_var_instance : t -> StateVar.t

Return the state variable of a state variable instance

val offset_of_state_var_instance : t -> Numeral.t

Return the offset of a state variable instance

val hstring_of_free_var : t -> HString.t

Return a string for a free variable

val is_state_var_instance : t -> bool

Return true if the variable is an instance of a state variable

val is_const_state_var : t -> bool

Return true if the variable is a constant state variable

val is_free_var : t -> bool

Return true if the variable is a free variable

Construct Variables of Variables

val bump_offset_of_state_var_instance : t -> Numeral.t -> t

Return a new variable with the offset of the state variable instance incremented by the given value

bump_offset_of_state_var_instance v i returns a new variable, where the value i is added to the offset of the v if it is a state variable instance. The value i may be negative.

If v is a constant state variable or a free variable, it is returned unchanged.

val set_offset_of_state_var_instance : t -> Numeral.t -> t

Return a new variable with the offset of the state variable instance set to the given value

set_offset_of_state_var_instance v i returns a new variable, where the offset of the state variable v is set to i, if v is a state variable instance.

If v is a constant state variable or a free variable, it is returned unchanged.

val map_state_var : (StateVar.t -> StateVar.t) -> t -> t

Return a new variable with the state variable replaced

map_state_var v f returns a new variable where the state variable s is replaced by the result of the evaluation f s if v is a state variable instance or a constant state variable.

If v is a free variable, it is returned unchanged.

Pretty-printing

val pp_print_var : Stdlib.Format.formatter -> t -> unit

Pretty-print a hashconsed variable

val print_var : t -> unit

Pretty-print a hashconsed variable to the standard formatter

val string_of_var : t -> string

Return a string representation of a hashconsed variable

val stats : unit -> int * int * int * int * int * int

val state_var_instance_of_symbol : Symbol.t -> t

Gets the state var instance associated with a constant unrolled uf. Throws Not_found if the uf is unknown.

val state_var_instance_of_uf_symbol : UfSymbol.t -> t

Gets the state var instance associated with a constant unrolled uf. Throws Not_found if the uf is unknown.

val unrolled_uf_of_state_var_instance : t -> UfSymbol.t

val declare_constant_vars : (UfSymbol.t -> unit) -> t list -> unit

Declares constant variables as constant ufsymbols using the provided function.

val declare_vars : (UfSymbol.t -> unit) -> t list -> unit

Declares non constant variables as constant ufsymbols using the provided function.

val encode_select : t -> UfSymbol.t

encode array select operation