package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type last_effort_limit =

| Time of float
| Steps of int

val run_exn : 
  ?nodec:unit ->
  ?step_limit:int ->
  ?last_effort_limit:last_effort_limit ->
  ?learning:bool ->
  ?options:Colibri2_core.ForSchedulers.Options.options ->
  theories:(Colibri2_core.Egraph.wt -> unit) list ->
  (Colibri2_core.Egraph.wt -> Colibri2_core.Egraph.wt -> 'a) ->
  'a

run_exn ?nodec ?limit ?learning ~theories add_assertions.

add_assertions d should add the assertions. The resulting function is applied on the environment after propagation and possibly decisions

val run : 
  ?nodec:unit ->
  ?step_limit:int ->
  ?last_effort_limit:last_effort_limit ->
  ?options:Colibri2_core.ForSchedulers.Options.options ->
  theories:(Colibri2_core.Egraph.wt -> unit) list ->
  (Colibri2_core.Egraph.wt -> Colibri2_core.Egraph.wt -> 'a) ->
  [> `Contradiction | `Done of 'a ]

type t

val new_solver : 
  learning:bool ->
  ?last_effort_limit:last_effort_limit ->
  ?options:Colibri2_core.ForSchedulers.Options.options ->
  unit ->
  t

val init_theories : 
  theories:(Colibri2_core.Egraph.wt -> unit) list ->
  t ->
  unit

val add_assertion : t -> (Colibri2_core.Egraph.wt -> unit) -> unit

val check_sat : 
  ?step_limit:int ->
  t ->
  [> `Unsat
  | `Sat of Colibri2_core.Egraph.wt
  | `Unknown of Colibri2_core.Egraph.wt ]

val get_steps : t -> int

val get_context : t -> Colibri2_stdlib.Context.creator

type bp

val push : t -> bp

val pop_to : t -> bp -> unit

module LearnSet : Stdlib.Set.S with type elt = Colibri2_core.Ground.t

exception ReachStepLimit