Module Logtk.Test_propSource

Test Properties

Test universal properties that use defined functions, within some "reasonable" bound (e.g. smallcheck/quickcheck).

This is used to test a property semantically (by evaluation) before trying the costly proof by induction; if the property is false there is no need to try to prove it.

Sourcetype term = Term.t
Sourcetype lit = Literal.t
Sourcetype form = Literals.t list
Sourcetype res =
  1. | R_ok
  2. | R_fail of Subst.t
Sourceval normalize_form : form -> form

Use rewriting to normalize the formula

Sourceval 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.

Sourceval default_limit : int