Region_idx (imandra-tools.Imandra_tools.Region

module type Args = sig ... end

Argument types of the decomposed function, as a tuple *

val synthesize : 
  ?loc:Imandra_util.Iloc.t ->
  ?compound:bool ->
  Imandra_surface.Modular_region.t list ->
  (int * Imandra_surface.Modular_region.t) list * string

Takes a list of regions and returns an int -> region index, and code to map arguments to the decomposed function to the index of the region the arguments belong to If the arguments belong to no region in the region list, returns -1 *

val indexer_f_for : 
  ?scope:Opentelemetry.Trace.scope ->
  ?loc:Imandra_util.Iloc.t ->
  ?assuming:string ->
  Imandra_surface.Modular_region.t list ->
  (int * Imandra_surface.Modular_region.t) list * string

Like synthesize, but insted of returning code it returns a function name for the indexer *

val indexer_for : 
  (module Args with type args = 'a) ->
  ?assuming:string ->
  Imandra_surface.Modular_region.t list ->
  (int * Imandra_surface.Modular_region.t) list * ( 'a -> int )

Same as indexer_f_for, but returns a first class function instead of a function name, the arguments to the indexer are passed as a tuple, whose type must match the args type in the first class module argument. If the arguments belong to no region in the region list, throws Not_found *