kdrag.hypothesis

Helper functions for the hypothesis property based testing library.

This can be useful for: - Giving counterexamples to poorly stated theorems before you spend much effort on them - Sanity checking axioms - Connecting formal models to other code - Testing Knuckledragger facilities - Testing Z3 intended meaning

Functions

`binop`(children, op)
`binops`(children)
`compares`(strat)
`quickcheck`(thm[, deadline])	Run a hypothesis test to check that an instantiated forall is equivalent to the original forall.
`smt_datatype_val`(s)
`smt_generic_val`(sort[, maxiter])	A hypothesis search strateegy that uses smt model generation to generate a value of a given SMT sort.
`smt_seq_val`(s)
`sort_occurs`(s, s2[, visited])	Check if a sort occurs in the datatype.
`val_of_sort`(s[, knot_tie, slow_generic])	Make a search strategy of values of a given SMT sort.
`z3_array_val`(dom, ran)

kdrag.hypothesis.binop(children, op) → SearchStrategy

Return type:: SearchStrategy

kdrag.hypothesis.binops(children) → SearchStrategy

Return type:: SearchStrategy

kdrag.hypothesis.compares(strat) → SearchStrategy

Return type:: SearchStrategy

kdrag.hypothesis.quickcheck(thm: QuantifierRef, deadline=100, **hyp_settings)

Run a hypothesis test to check that an instantiated forall is equivalent to the original forall.

Parameters:: thm (QuantifierRef)

kdrag.hypothesis.smt_datatype_val(s: DatatypeSortRef) → SearchStrategy[DatatypeRef]

Parameters:: s (DatatypeSortRef)
Return type:: SearchStrategy[DatatypeRef]

kdrag.hypothesis.smt_generic_val(sort: SortRef, maxiter=4) → SearchStrategy[ExprRef]

A hypothesis search strateegy that uses smt model generation to generate a value of a given SMT sort. It is slower and will have worse shrinkage. To be used as a fallback.

Parameters:: sort (SortRef)
Return type:: SearchStrategy[ExprRef]

kdrag.hypothesis.smt_seq_val(s: SortRef) → SearchStrategy[SeqRef]

Parameters:: s (SortRef)
Return type:: SearchStrategy[SeqRef]

kdrag.hypothesis.sort_occurs(s, s2, visited=None)

Check if a sort occurs in the datatype.

>>> import kdrag.theories.list as list
>>> sort_occurs(smt.IntSort(), list.List(smt.IntSort()))
True
>>> sort_occurs(smt.IntSort(), list.List(smt.BoolSort()))
False
>>> sort_occurs(smt.IntSort(), smt.IntSort())
True

kdrag.hypothesis.val_of_sort(s: SortRef, knot_tie: tuple[SortRef, SearchStrategy[ExprRef]] | None = None, slow_generic=False) → SearchStrategy[ExprRef]

Make a search strategy of values of a given SMT sort.

Parameters:

s (SortRef)
knot_tie (tuple[SortRef, SearchStrategy[ExprRef]] | None)

Return type:

SearchStrategy[ExprRef]

kdrag.hypothesis.z3_array_val(dom: SearchStrategy[ExprRef], ran: SearchStrategy[ExprRef]) → SearchStrategy[ArrayRef]

Parameters:

dom (SearchStrategy[ExprRef])
ran (SearchStrategy[ExprRef])

Return type:

SearchStrategy[ArrayRef]