Module GeneratedIdentifiers

module StringMap = HString.HStringMap
module StringSet = HString.HStringSet
type source =
  1. | Local
  2. | Input
  3. | Output
  4. | Ghost
  5. | ClockedOutput of LustreAst.expr
    (*

    Output of an equation pulled out of a when-block branch; the expression is the (polarity-adjusted) conjunction of the enclosing when-block guards. Node calls in such an equation must be activated on that clock.

    *)
type t = {
  1. node_args : (HString.t * bool * LustreAst.lustre_type * LustreAst.expr) list;
  2. locals : LustreAst.lustre_type StringMap.t;
  3. free_constants : (HString.t * LustreAst.lustre_type) list;
  4. contract_calls : (Lib.position * (Lib.position * NodeId.t) list * LustreAst.contract_node_equation list) StringMap.t;
  5. oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list;
  6. ib_oracles : (HString.t * LustreAst.lustre_type) list;
  7. calls : (Lib.position * HString.t * LustreAst.expr * LustreAst.expr * HString.t option * NodeId.t * LustreAst.expr list * LustreAst.expr list option * bool) list;
  8. refinement_type_constraints : (source * Lib.position * HString.t * LustreAst.expr * NodeId.t option) list;
  9. selector_obligations : (Lib.position * HString.t * LustreAst.expr) list;
  10. empty_maps : (HString.t * LustreAst.lustre_type * LustreAst.lustre_type) list;
  11. empty_sets : (HString.t * LustreAst.lustre_type) list;
  12. map_element_updates : (HString.t * LustreAst.expr * LustreAst.expr * LustreAst.expr * HString.t * LustreAst.lustre_type * LustreAst.lustre_type) list;
  13. map_subtractions : (HString.t * LustreAst.expr * LustreAst.expr * HString.t * LustreAst.lustre_type * LustreAst.lustre_type) list;
  14. set_insertions : (HString.t * LustreAst.expr * LustreAst.expr * HString.t * LustreAst.lustre_type) list;
  15. set_binops : (HString.t * LustreAst.expr * LustreAst.expr * HString.t * LustreAst.binary_operator * LustreAst.lustre_type) list;
  16. expanded_variables : StringSet.t;
  17. equations : (LustreAst.typed_ident list * (Lib.position * NodeId.t) list * LustreAst.eq_lhs * LustreAst.expr * source option) list;
  18. nonvacuity_props : StringSet.t;
  19. clocked_call_ties : (HString.t * HString.t option * HString.t * HString.t) list;
    (*

    Tuples (tie, init_tie, t, x) where x is a when-block variable whose off-branch holds its previous value, t is the local bound to the output of the node call activated on the when-block guard, tie is a generated boolean local defined as x = t, and init_tie, if any, is a generated boolean local defined as x = init, where init is the initial value of x. Used to generate candidate invariants tying the held variable to the (frozen) call output.

    *)
  20. array_literal_vars : StringSet.t;
  21. expr_source_map : LustreAst.expr StringMap.t;
  22. prop_source_map : LustreAst.expr StringMap.t;
  23. type_ascription_exprs : LustreAst.expr NodeId.Map.t;
  24. history_vars : HString.t StringMap.t;
}
val iboracle : string
val ctr_id : HString.t
val var_is_iboracle : HString.t -> bool

Checks if a variable name corresponds to an iboracle

val discarded_output : string
val var_is_discarded_output : HString.t -> bool

Checks if a variable name corresponds to a discarded call-statement result

val last_local : string
val var_is_last_local : HString.t -> bool

Checks if a variable name corresponds to a 'last'-operator local

val clocked_call_output : string
val clocked_call_tie : string
val block_guard : string
val empty : unit -> t
val union : t -> t -> t
val union_keys : 'a -> 'b option -> 'b option -> 'b option
val union_keys2 : 'a -> t option -> t option -> t option