Add datatype support for z3

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.

Other

103 stars 40 forks source link

Closed farmerzhang1 closed 6 months ago

farmerzhang1 commented 6 months ago

Hi all,

I'm trying to play with smt-switch and decide to add z3 backend support for datatypes. Any feedback is welcome.

farmerzhang1 commented 6 months ago

Hi Yoni, I've add some z3-specific tests and try to mirror the cvc5 datatype files as much as possible. Maybe you can check them again?