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 Property objects. A reduction will likely also require a custom Property type which must implement validate_counter_example(self, cex: Any) -> Tuple[bool, Optional[str]].