CODEWITHSUNDEEP
z3
Andreas Morgenstern
Andreas Morgenstern

Reputation: 299

Does Z3 Support Craig Interpolation

Can Z3 generate Craig interpolants (at least for propositional logic ?). I have not found it in the documentation of Z3.

Upvotes: 5

Views: 784

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

No, Z3 does not support Craig interpolants, but it generates proofs. The interpolants can be extracted from the proofs. Ken Mcmillan is developing an interpolant generator on top of Z3 using this approach.

Upvotes: 4

Related Questions