Module StateVar
State variables
Every state variable is associated with an uninterpreted function symbol that is substituted for the state variable when creating expressions for the SMT solvers.
State variables do not occur directly in terms, but as instances in a particular state, see Var
.
- author
- Christoph Sticksel
Types and hash-consing
Hashtables, maps and sets
val hash_state_var : t -> int
Hashing function on state variables
module StateVarHashtbl : Stdlib.Hashtbl.S with type StateVarHashtbl.key = t
Hash table over state variables
module StateVarSet : sig ... end
Set over state variables
module StateVarMap : Stdlib.Map.S with type StateVarMap.key = t
Map over state variables
Constructor
val mk_state_var : ?is_input:bool -> ?is_const:bool -> ?for_inv_gen:bool -> string -> string list -> Type.t -> t
mk_state_var n s t
declares a state variable of namen
with scopes
, and typet
. The optional labeled arguments?is_input
,?is_const
and?for_inv_gen
flag the variable as an input, as constant and as usable as a candidate for invariant generation, respectively. Their defaults arefalse
,false
andtrue
.Declaring a state variable again with the same signature is harmless and will simply return the previously declared state variable. However, re-declaring a state variable with a different signature will raise an
Invalid_argument
exception.
val mk_init_flag : string list -> t
Creates a scoped init flag.
val mk_depth_input : string list -> t
Creates a scoped depth input.
val mk_max_depth_input : string list -> t
Creates a scoped depth input.
Accessor functions
val state_var_of_string : (string * string list) -> t
Return a previously declared state variable
val state_var_of_long_string : string -> t
Return a previously declared state variable from a string consisting of the concatenation of all scopes and the state variable. Raises
Not_found
if it was not previously declared.
val name_of_state_var : t -> string
Return the name of the state variable
val scope_of_state_var : t -> string list
Return the scope of the state variable
val uf_symbol_of_state_var : t -> UfSymbol.t
Return the uninterpreted function symbol of the variable
val state_var_of_uf_symbol : UfSymbol.t -> t
Return the state variable corresponding to an uninterpreted function symbol
val is_input : t -> bool
Return true if the state variable is an input
val is_const : t -> bool
Return true if the state variable is constant
val for_inv_gen : t -> bool
Return true if state variable is to be used in invariant generation
val set_for_inv_gen : bool -> t -> unit
Set or unset flag to use state variable in invariant generation
Iterators over defined state variables
val fold : (t -> 'a -> 'a) -> 'a -> 'a
fold f a
computes(f sN tN uN ... (f s2 t2 u2 (f s1 t1 u1 a))...)
, wheresI
,tI
anduI
, respectively are the name of the state variable, its types and its associated uninterpreted function symbol.
val iter : (t -> unit) -> unit
iter f
callsf s t u
for every state variable withs
being the name of the variable,t
its type andu
its associated uninterpreted function symbol.
val encode_select : t -> UfSymbol.t
encode array select operation. Encoding select funtion is done byt type (i.e. one select by array type). The select function performs all projections if the array is multidimensional. This means you should have something like
(select_1 m 0 3)
in casem
is a matrix
val get_select_ufs : unit -> UfSymbol.t list
Return select function that were created
Pretty-printing
val pp_print_state_var : Stdlib.Format.formatter -> t -> unit
Pretty-print a state variable
val string_of_state_var : t -> string
Return a string representation of a symbol