Module `Logtk.Test_prop`

Test Properties

type term = Term.t
type lit = Literal.t
type form = Literals.t list
type res = | R_ok | R_fail of Subst.t

val normalize_form : form -> form: Use rewriting to normalize the formula

val check_form : ?⁠limit:int -> form -> res

check_form rules form returns R_ok if the property seems to hold up to depth, or R_fail subst if subst makes form evaluate to false

parameter limit: a limit on how many "steps" are done (for some notion of steps). The higher, the more expensive, but also the more accurate this is.

val default_limit : int