Module `Var`

Variables in terms

A variable is an instance of a state variable (see StateVar) in a state relative to an initial state. A variable can also be a free variable that is to be bound in a let expression.

author: Christoph Sticksel

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 VarHashtbl.key = t: Hash table over variables

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

module VarMap : Stdlib.Map.S with type VarMap.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 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