StateVar (kind2dev@731decdf5fb1.StateVar)

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 key = t

Hash table over state variables

module StateVarSet : sig ... end

Set over state variables

module StateVarMap : Stdlib.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 modify_state_var : 
  ?is_input:bool ->
  ?is_const:bool ->
  ?for_inv_gen:bool ->
  ?state_var_name:string ->
  ?state_var_scope:string list ->
  ?state_var_type:Type.t ->
  t ->
  t

modify_state_var s creates a copy of the state variable s, with the specified changes applied. The optional labeled arguments ?is_input, ?is_const, ?for_inv_gen, ?state_var_name, ?state_var_scope, and ?state_var_type specify the changes to be made. If left un-specified the previous value will be copied.

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 uid : t -> int

Return a unique numerical identifier

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 set_const : bool -> t -> unit

Set or unset flag that determines 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 pp_print_state_var_debug : Stdlib.Format.formatter -> t -> unit

val string_of_state_var : t -> string

Return a string representation of a symbol

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