package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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