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