Module Reasoning_proxy.Modular_decomp

module MR = Imandra_surface.Modular_region
module MD = Imandra_surface.Modular_decomposition
type region_id = MR.id
val top : scope:scope option -> P.Modular_decomp.Query.params -> MD.RRef.t
val get_decomp_full : scope:scope option -> MD.RRef.t -> MD.concrete
val get_region : scope:scope option -> MD.RRef.t -> region_id -> MR.RRef.t
val get_regions : scope:scope option -> MD.RRef.t -> MR.RRef.t list
val check_region : scope:scope option -> MR.RRef.t -> MR.status

Check satisfiability of a region

val get_state_ref : scope:scope option -> MD.RRef.t -> Reasoning_state_ref.t
val get_mdstate_ref : scope:scope option -> MD.RRef.t -> Modular_decomp_state_ref.t
val get_model : scope:scope option -> MR.RRef.t -> Imandra_surface.Term.Model.t
val prune : scope:scope option -> ?use_jobs:bool -> ?hints:Imandra_surface.Uid.t Imandra_surface.Hints.t -> MD.RRef.t -> MD.RRef.t

Return a pruned modular decomp, directly.

  • parameter use_jobs

    if true, pruning is done in background jobs, potentially in parallel.

val refine : scope:scope option -> MR.RRef.t -> Imandra_surface.Term.t list -> MR.RRef.t option
val flat_merge : ?use_jobs:bool -> scope:scope option -> MD.RRef.t -> MD.RRef.t -> MD.RRef.t
val compound_merge : scope:scope option -> MD.RRef.t -> MD.RRef.t -> MD.RRef.t
val flat_force_merge : scope:scope option -> MD.RRef.t -> MD.RRef.t -> MD.RRef.t
val compound_force_merge : scope:scope option -> MD.RRef.t -> MD.RRef.t -> MD.RRef.t
val combine : scope:scope option -> MD.RRef.t -> MD.RRef.t
val mr_of_ref : scope:scope option -> Imandra_util.Remote_id.t -> MR.RRef.t