API Reference
Quantifier module
exists(**binds)
Decorates a predicate funcion or another decorator with an existencial quantifier.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
**binds |
The quantified variables. Actually the number of quantified variables is limited to 1. |
{}
|
Returns:
| Type | Description |
|---|---|
Exists
|
An object implementing the property as a callable. |
Warning
Every variable must be quantified over an exhaustible domain.
forall(n_samples: int = 100, **binds)
Decorates a predicate funcion or another decorator with a forall quantifier.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n_samples |
int
|
The number of samples to check. |
100
|
**binds |
The quantified variables. Actually the number of quantified variables is limited to 1. |
{}
|
Returns:
| Type | Description |
|---|---|
ForAll
|
An object implementing the property as a callable. |
Domain module
Domain
Bases: Generic[T]
Domain abstract class
This is the base class for every Domain. It includes some
operations like union.
It also includes the method that to decorate a domain with extra
funcionality. For example: limiting the number of samples that it
will generate.
By default, domains are non exhaustibles. The attribute
is_exhaustible = False. When a domain is or may be exhaustible,
the corresponding class has to explicitly change the attribute
is_exhaustible and, if neccessary, add a parameter to the
__init__ function. And, of course, implement the exhaustible
iterator exhaustible_iter.
__iter__() -> Iterator[T]
Returns the cannonical iterator for a domain.
This is the magic method of any python iterable. The returned iterator is the pbt cannonical one. This iterator will pick and yield random samples from the domain.
exhaustible() -> Iterator[T]
property
Returns an iterator that can be exhausted.
exhaustible_iter() -> Iterator[T]
Returns the non-cannonical, exhaustible iterator for a domain.
The returned iterator is not the pbt cannonical one. Instead of picking random samples, this iterator will pick and yield all the elements of the domain.
NOTE that most domains can not be exhausted because the number of elements is too big, generating them is too costly, or, most of the cases, the number of elements is infinite.
WARNING do not use this method directly, instead use the
property exhaustible.
that(samples_limit: int) -> Domain
Decorate this domain
Returns a decorator of this domain. The decorator will change the behaviour of the domain based on the given parameters.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
samples_limit |
int
|
max number of samples the domain generates |
required |
Returns:
| Type | Description |
|---|---|
Domain
|
the decorated domain |
domain_expr(arg: DomainCoercible, is_exhaustible: Optional[bool] = None) -> Domain
Desugar domain expressions
Converts any expression declaring a domain into a Domain object. The options are:
-
If arg is already a Domain object, returns it. Parameters are not allowed.
-
If arg is any python iterable, returns a Domain object whose elements are the items in the iterable. The programmer may mark the domain as exhaustible when neccessary.
-
If arg is a generator function, equivalent to iterable, taking the elements from the generator returned by the function.
-
If arg is any other python object, returns a Domain containing only one element: arg.