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

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 : 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 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 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 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 : Stdlib.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