Modular_decomp (imandra-base.Imandra_interactive.Modular

Modular decomp

module type S = Modular_decomp_intf.S

include S

type strategy = Imandra_interactive.Modular_decomp_intf.MD.strategy =

| Classic

| Tracing

| Fair_search

type rec_expansion = Imandra_interactive.Modular_decomp_intf.MD.rec_expansion =

| Never

| Explicit

| Speculative

val n_regions : Modular_decomp_intf.decomp -> int

val n_regions_ref : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  int

val get_concrete : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp

Get a concrete, ref-free, local version of the decomposition. This can incur serialization costs.

val get_region : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Imandra_interactive.Modular_decomp_intf.MR.id ->
  Modular_decomp_intf.region_ref

Obtain the region associated with this ID

val get_model : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.region_ref ->
  Imandra_surface.Term.Model.t

Obtain a model for the region

val refine : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.region_ref ->
  Imandra_surface.Term.t list ->
  Modular_decomp_intf.region_ref option

Refine a region with additional constraints *

val check_region : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.region_ref ->
  Imandra_interactive.Modular_decomp_intf.MR.status

Check given region

val rstate : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.rstate_ref

Reasoning state

val mdstate : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.mdstate_ref

Reasoning state

val prune : 
  ?scope:Modular_decomp_intf.scope ->
  ?use_jobs:bool ->
  ?hints:Imandra_surface.Uid.t Imandra_surface.Hints.t ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref

Remove infeasible regions

val get_regions : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.region_ref list

val get_concrete_regions : 
  ?scope:Modular_decomp_intf.scope ->
  Modular_decomp_intf.decomp_ref ->
  Imandra_interactive.Modular_decomp_intf.MR.t list

val (<<) : 
  ?use_jobs:bool ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref

val (<|<) : 
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref

val (<<!) : 
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref

val (<|<!) : 
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref ->
  Modular_decomp_intf.decomp_ref

val (~|) : Modular_decomp_intf.decomp_ref -> Modular_decomp_intf.decomp_ref

val top : 
  ?scope:Modular_decomp_intf.scope ->
  ?prune:bool ->
  ?prune_use_jobs:bool ->
  ?rule_specs:string list ->
  ?strategy:strategy ->
  ?rec_expansion:rec_expansion ->
  ?st:Modular_decomp_intf.mdstate_ref ->
  ?max_rounds:int ->
  ?stop_at:int ->
  ?assuming:string ->
  ?basis:string list ->
  ?ctx_simp:bool ->
  string ->
  Modular_decomp_intf.decomp_ref

val make : ?st:Modular_decomp_intf.mdstate_ref -> unit -> (module S)