Module Logtk_arbitrary.ArForm

Arbitrary Basic Terms

type 'a arbitrary = 'a QCheck.arbitrary
type 'a gen = 'a QCheck.Gen.t
type form = Logtk.TypedSTerm.t
val atom_g : form gen
val atom : form arbitrary

Atomic formula

val clause_g : form list gen
val clause : form list arbitrary

clause

val default : form arbitrary

polymorphic formula with connectives (DB-closed)

val default_fuel : int -> form gen