Add datatype support for z3

[farmerzhang1]

Hi all,

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

[yoni206]

Thank you very much for this PR. It would be great to have support for z3 datatypes!
I've made some initial comments/questions inline.

In addition to them -- I wonder -- would it make sense to add tests that are specific to z3 datatypes? Perhaps here?
https://github.com/stanford-centaur/smt-switch/tree/main/tests/z3

We are already in good shape because I can see that CI ran the general datatypes tests, but I still wonder whether there is anything specific to test in the z3 API side.

[farmerzhang1]

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?

[yoni206]

Thanks for the changes. Looks like the new tests are passing, and also the old ones, also after adding datatypes to the list of supported theories of z3, which is great.

Just one last question inline.

[yoni206]

Why is this needed?

[farmerzhang1]

This is basically doing the classic

cd build
cmake ..
make

In the first command, -S . means source is in the current directory, -B build means the build directory, and the rest is just to make sure we build the binary we want, which is optimized static library, we don't need the shared one so I turn it off.

The second one is designating the build directory and build the target in parallel

[yoni206]

Thanks again for this valuable contribution!