Reasoning_proxy (imandra-base.Imandra_interactive.Reasoning

Interface to backend

module P = Imandra_protocol

val raise_async_error : 
  ( exn -> Stdlib.Printexc.raw_backtrace option -> unit ) Stdlib.ref

val top : 
  ( ?cancel:Imandra_util.Switch.t ->
    assume_ok:bool ->
    finally:( unit -> unit ) ->
    P.Query.t ->
    P.Response.response Imandra_thread_util.Fut.t )
    Stdlib.ref

type scope = Opentelemetry.Trace.scope

module Remote_ref : sig ... end

module Builtin : sig ... end

module Define_check : sig ... end

module Verify : sig ... end

module Simplify : sig ... end

module Load_plugin : sig ... end

module Instance : sig ... end

module Debug : sig ... end

module Modular_decomp : sig ... end

module Abstractor : sig ... end

module Snapshot : sig ... end

module Ext_solver : sig ... end

module Extract : sig ... end

module Cache : sig ... end

module Basis : sig ... end

module Exec_ops : sig ... end

module Loading_prelude : sig ... end

module Sync : sig ... end

module Gc : sig ... end

module Custom : sig ... end

val send_pconfig_ops : 
  scope:scope option ->
  Imandra_util.Pconfig.op list ->
  unit

val interrupt : scope:scope option -> P.Query.t -> unit

val reply_to_server_q : 
  P.Server_query.t ->
  P.Client_response.t Imandra_thread_util.Fut.t * bool