package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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