Simplify (imandra-base.Imandra_interactive.Simplify)

module P = Imandra_protocol

module IFut = Interactive_background_thread.Fut

type mode = Imandra_surface.Top_result.simplify_mode =

`\| Basic`
`\| Dyn_asms`	(* dynamic assumptions for if-then-else *)
`\| Full`	(* forward chaining, rewriting, simplify booleans *)

val top : 
  ?scope:Opentelemetry.Trace.scope ->
  ?asms:Imandra_surface.Term.t list ->
  ?fixpoint:bool ->
  ?basis:string list ->
  mode:Imandra_surface.Top_result.simplify_mode ->
  Imandra_surface.Var.t list ->
  Imandra_surface.Term.t ->
  Imandra_surface.Term.t

val clause : 
  ?scope:Opentelemetry.Trace.scope ->
  ?asms:Imandra_surface.Term.t list ->
  ?fixpoint:bool ->
  ?basis:string list ->
  mode:Imandra_surface.Top_result.simplify_mode ->
  Imandra_surface.Var.t list ->
  Imandra_surface.Term.t ->
  Imandra_surface.Term.t list

`\| Basic`
`\| Dyn_asms`	(* dynamic assumptions for if-then-else *)
`\| Full`	(* forward chaining, rewriting, simplify booleans *)