Module StateVar

module StateVar: sig .. end
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(s): Christoph Sticksel



Types and hash-consing


type state_var = private string * string list 
State variable

A state state variable is a pair of its identifier and its scope, which is a list of identifiers.

type t 
Hashconsed state variable

Hashtables, maps and sets


val compare_state_vars : t -> t -> int
Comparison function on state variables
val equal_state_vars : t -> t -> bool
Equality function on state variables
val hash_state_var : t -> int
Hashing function on state variables
module StateVarHashtbl: Hashtbl.S  with type key = t
Hash table over state variables
module StateVarSet: sig .. end
Set over state variables
module StateVarMap: Map.S  with type 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 name n with scope s, and type t. 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 are false, false and true.

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.
val import : t -> t
Import a state variable from a different instance into this hashcons table

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 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 type_of_state_var : t -> Type.t
Return the type of the variable
val change_type_of_state_var : t -> Type.t -> unit
Change the type of a 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))...)
, where sI, tI and uI, respectively are the name of the state variable, its types and its associated uninterpreted function symbol.
val iter : (t -> unit) -> unit
iter f calls f s t u for every state variable with s being the name of the variable, t its type and u 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 case m is a matrix
val get_select_ufs : unit -> UfSymbol.t list
Return select function that were created

Pretty-printing


val pp_print_state_var : Format.formatter -> t -> unit
Pretty-print a state variable
val string_of_state_var : t -> string
Return a string representation of a symbol
val stats : unit -> int * int * int * int * int * int