Module Modular_decomp.Query

type params = {
basis : string list option;
assuming : string option;
rule_specs : string list;
f : string;
max_rounds : int option;
stop_at : int option;
strategy : Imandra_surface.Modular_decomposition.strategy;
rec_expansion : Imandra_surface.Modular_decomposition.rec_expansion option;
ctx_simp : bool option;
state_from : Modular_decomp_state_ref.t option;
}
val pp_params : Ppx_deriving_runtime.Format.formatter -> params -> Ppx_deriving_runtime.unit
val show_params : params -> Ppx_deriving_runtime.string
type merge_strategy =
| Flat
| Compound
| Flat_force
| Compound_force
val pp_merge_strategy : Ppx_deriving_runtime.Format.formatter -> merge_strategy -> Ppx_deriving_runtime.unit
val show_merge_strategy : merge_strategy -> Ppx_deriving_runtime.string
type t =
| Q_start of params
| Q_get_region of {
d_ref : decomp_ref;
id : region_id;
}
| Q_get_regions of {
d_ref : decomp_ref;
}
| Q_get_decomp_full of {
d_ref : decomp_ref;
}
| Q_check_region of {
r_ref : region_ref;
}
| Q_get_model of {
r_ref : region_ref;
}
| Q_refine_region of {
r_ref : region_ref;
terms : Imandra_surface.Term.t list;
}
| Q_merge of {
d_tgt : decomp_ref;
d_src : decomp_ref;
strategy : merge_strategy;
use_jobs : bool;
}
| Q_combine of {
d_ref : decomp_ref;
}
| Q_state of {
d_ref : decomp_ref;
}		(*

return reasoning state for this decomp

*)
| Q_md_state of {
d_ref : decomp_ref;
}		(*

return MD state for this decomp

*)
| Q_prune of {
d_ref : decomp_ref;
hints : Imandra_surface.Uid.t Imandra_surface.Hints.t option;
use_jobs : bool;(*

Use background jobs to perform the pruning?

*)
}
val kind : t -> string
val pp : Fmt.t -> t -> Ppx_deriving_runtime.unit
val show : t -> string
val make_params : ?max_rounds:int -> ?stop_at:int -> ?basis:string list -> ?state_from:Modular_decomp_state_ref.t -> ?rec_expansion:Imandra_surface.Modular_decomposition.rec_expansion -> rule_specs:string list -> strategy:Imandra_surface.Modular_decomposition.strategy -> assuming:string option -> ?ctx_simp:bool -> string -> params
val make : params -> t