Module `Model`

module MIL : Stdlib.Map.S with type MIL.key = int list

type value = | Term of Term.t | Lambda of Term.lambda | Map of Term.t MIL.t: Term or lambda expression

type t = value Var.VarHashtbl.t: A model is a list of variables and assignemnts

type path = value list StateVar.StateVarHashtbl.t: A path is a map of state variables to assignments

val equal_value : value -> value -> bool: Equality over values of model

val path_offset : Numeral.t: Offset of the variables at each step of a path.

val pp_print_value : ?⁠as_type:Type.t -> Stdlib.Format.formatter -> value -> unit: Pretty-print a value

val pp_print_value_xml : ?⁠as_type:Type.t -> Stdlib.Format.formatter -> value -> unit: Pretty-print a value in xml format

val pp_print_value_json : ?⁠as_type:Type.t -> Stdlib.Format.formatter -> value -> unit: Pretty-print a value in json format

val pp_print_model : Stdlib.Format.formatter -> t -> unit: Pretty-print a model

val pp_print_path : Stdlib.Format.formatter -> path -> unit: Pretty-print a path

val create : int -> t: Create a model of the given size

val create_path : int -> path: Create a path of the given size

val import_value : value -> value: Import a variable assignment from a different instance

val of_list : (Var.t * value) list -> t: Create a model of an association list

val to_list : t -> (Var.t * value) list: Return an association list with the assignments in the model

val path_to_list : path -> (StateVar.t * value list) list: Return an association list with the assignments in the model

val path_of_list : (StateVar.t * value list) list -> path: Create a model of an association list

val path_of_term_list : (StateVar.t * Term.t list) list -> path: Create a model of an association list

val path_from_model : StateVar.t list -> t -> Numeral.t -> path

Convert a model to a path

path_from_model s m k extracts from the model m a path of values for each of the state variables in s from the offset zero up to k. The lists of values for each state variable are of equal length. Values that are not defined in the model are filled with TermLib.default_of_type.

val path_length : path -> int

Return the length of the value paths

All value paths are of equal lengths.

val model_at_k_of_path : path -> Numeral.t -> t: Extract values at instant k from the path and return a model

val models_of_path : path -> t list: Return a list of models, one for each step on the path

val exists_on_path : (t -> bool) -> path -> bool: Return true if the predicate p applies at one step of the path

val for_all_on_path : (t -> bool) -> path -> bool: Return true if the predicate p applies at each step of the path

val bump_var : Numeral.t -> t -> t: Add k to offset of all variables in model

val set_var_offset : Numeral.t -> t -> t: Set offset of all variables in model to k

val merge : t -> t -> t: Combine assignments of two models into one. If a variable has an assignment in both models, it gets the assignment in the second model.

val bump_and_merge : Numeral.t -> t -> t -> t: Combine assignments of two models into one as in merge, but bump the variables in the second model by the given offset before merging.

val dimension_of_map : Term.t MIL.t -> int list: Returns the bounds / dimension of the array value represented by the map in the model