package colibri2

  1. Overview
  2. Docs
package colibri2
Legend:
Library
Module
Module type
Parameter
Class
Class type
type last_effort_limit =
  1. | Time of float
  2. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct