Adding a New Reduction#
TODO. Sorry, this page is still in development. An example reduction can be seen here.
In general a reduction will subclass the
Reduction base class
and implement the method
reduce_property(self, phi: Expression) -> Iterator[Property],
which takes in a property expression and returns an iterator of
A reduction will likely also require a custom
which must implement
validate_counter_example(self, cex: Any) -> Tuple[bool, Optional[str]].