package colibri2

  1. Overview
  2. Docs
type ctx
type state = Dolmen_loop.State.t
val handle_exn_with_error : 'a -> Stdlib.Printexc.raw_backtrace -> exn -> 'b
val handle_exn_with_exit : state -> Stdlib.Printexc.raw_backtrace -> exn -> 'b
val get_ctx : state -> ctx
val get_state : state -> [ `Sat of Colibri2_core.Egraph.wt | `Unknown of Colibri2_core.Egraph.wt | `Search | `Unsat | `StepLimitReached ]
val read : ?show_check_sat_result:bool -> ?show_steps:bool -> ?check_status: [< `COLIBRI2 | `No | `SMTLIB | `Sat | `StepLimitReached | `Unknown | `Unsat No ] -> set_true:(Colibri2_core.Egraph.wt -> Colibri2_core.Node.t -> unit) -> handle_exn:(state -> Stdlib.Printexc.raw_backtrace -> exn -> unit) -> state -> unit
val mk_state : ?gc:bool -> ?gc_opt:Stdlib.Gc.control -> ?bt:bool -> ?colors:bool -> ?time_limit:float -> ?size_limit:float -> ?step_limit:int -> ?input_lang:Dolmen_loop.Logic.language -> ?input_mode:[ `Full | `Incremental ] -> input:[< `File of string | `Stdin ] -> ?header_check:bool -> ?header_licenses:string list -> ?header_lang_version:string option -> ?type_check:bool -> ?debug:bool -> ?max_warn:int -> ?learning:bool -> ?last_effort_limit:Scheduler.last_effort_limit -> ?print_success:bool -> ?negate_goal:bool -> ?options:Colibri2_core.ForSchedulers.Options.options -> (Colibri2_core.Egraph.wt -> unit) list -> state
OCaml

Innovation. Community. Security.