Pythonic API
This API is missing some features from cvc5 and Z3Py.
It does not (currently) support these cvc5 features:
-
The theories of strings, sequences and bags
-
unsatisfiable cores
-
syntax-guided synthesis (SyGuS)
It does not (currently) support the following features of Z3Py:
-
Patterns for quantifier instantiation
-
Pseudo-boolean counting constraints: AtMost, AtLeast, …
-
Special relation classes: PartialOrder, LinearOrder, …
-
HTML integration
-
Hooks for user-defined propagation and probing
-
Fixedpoint API
-
Finite domains
-
SMT2 file parsing