Module Logtk_arbitrary.ArTerm

Arbitrary Typed Terms and Formulas

type 'a arbitrary = 'a QCheck.arbitrary
type 'a gen = 'a QCheck.Gen.t
val shrink : Logtk.Term.t QCheck.Shrink.t
val default_g : Logtk.Term.t gen
val default_fuel : int -> Logtk.Term.t gen
val default : Logtk.Term.t arbitrary

Default polymorphic term

val default_ho_g : Logtk.Term.t gen
val default_lfho_g : Logtk.Term.t gen
val default_ho : Logtk.Term.t arbitrary

Default polymorphic term, with lambdas

val default_lfho : Logtk.Term.t arbitrary
val default_ho_fuel : int -> Logtk.Term.t gen
val ground_g : Logtk.Term.t gen
val ground : Logtk.Term.t arbitrary

Default ground monomorphic term

val pred : Logtk.Term.t arbitrary

predicates (type "o")

val pos : Logtk.Term.t -> Logtk.Position.t gen

Random valid position in the term

S Terms

module PT : sig ... end