package colibri2

  1. Overview
  2. Docs
package colibri2
Legend:
Library
Module
Module type
Parameter
Class
Class type
val check : Egraph.wt -> (Egraph.rt -> Ground.t -> check) -> unit

Check the value of the arguments corresponds to the the one of the of the ground term according to its interpretation

val check_closed_quantifier : Egraph.wt -> (Egraph.rt -> Ground.ClosedQuantifier.t -> check) -> unit

Check the interpretation of the closed quantifier in the current model

val check_not_totally_applied : Egraph.wt -> (Egraph.rt -> Ground.NotTotallyApplied.t -> check) -> unit

Check the interpretation for this partial application or lambdas

val compute : Egraph.wt -> (Egraph.rt -> Ground.t -> compute) -> unit
val compute_closed_quantifier : Egraph.wt -> (Egraph.rt -> Ground.ClosedQuantifier.t -> compute) -> unit
val compute_not_totally_applied : Egraph.wt -> (Egraph.rt -> Ground.NotTotallyApplied.t -> compute) -> unit
val node : Egraph.wt -> ((Egraph.wt -> Node.t -> Value.t SeqLim.t) -> Egraph.wt -> Node.t -> Value.t SeqLim.t option) -> unit

Register the computation of possible values for a node using the information on the domains. It could ask the computation of other nodes

val ty : Egraph.wt -> (Egraph.rt -> Ground.Ty.t -> Value.t SeqLim.t option) -> unit

Register iterators on all the possible value of some types, all the values must be reached eventually

val print_value_smt : (_, 'a) Value.Kind.t -> (Egraph.rt -> 'a Fmt.t) -> unit
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