S (imandra-base.Imandra_interactive.Modular_decomp

type strategy = MD.strategy =

| Classic

| Tracing

| Fair_search

type rec_expansion = MD.rec_expansion =

| Never

| Explicit

| Speculative

val n_regions : decomp -> int

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

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

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

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

Obtain the region associated with this ID

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

Obtain a model for the region

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

Refine a region with additional constraints *

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

Check given region

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

Reasoning state

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

Reasoning state

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

Remove infeasible regions

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

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

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

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

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

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

val (~|) : decomp_ref -> decomp_ref

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