package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

module SeqLim : sig ... end

type check =

| Right
(*
The current model verify the interpretation of the constraint
*)
| Wrong
(*
The current model do not verify the interpretation of the constraint
*)
| NA
(*
I don't know the interpretation of the constraint
*)
| Unknown
(*
I know the interpretation of the constraint but I can't check it
*)

val check_of_bool : bool -> check

Right for true, Wrong for false

type compute =

| Value of Value.t
| NA

module Register : sig ... end

val ty : _ Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t

Iterate on all the possible value of the given type, usually all the values will be reached eventually

val print_value_smt : _ Egraph.t -> Value.t Fmt.t

val interp : Egraph.wt -> Expr.Term.t -> Value.t

interp d e Should be used when the model has been computed. Compute the value of e in the current model. The value of e and the intermediary expression are also stored in the d

module WatchArgs : sig ... end