Module `Imandra_surface__Modular_region`

type session_id = int
type id = int
type status = | Unknown | Feasible | Infeasible
type t = private { mreg_session : session_id; mreg_id : id; mreg_constraints : Imandra_surface.Term.t list; mreg_invariant : Imandra_surface.Term.t; mreg_args : Imandra_surface.Var.t list; mreg_status : status; }

val constraints : t -> Imandra_surface.Term.t list
val invariant : t -> Imandra_surface.Term.t
val args : t -> Imandra_surface.Var.t list
val status : t -> status
val update_constraints : f:(Imandra_surface.Term.t list -> Imandra_surface.Term.t list) -> t -> t
val update_invariant : f:(Imandra_surface.Term.t -> Imandra_surface.Term.t) -> t -> t

module Id_map : CCMap.S with type Id_map.key = id