search

exo-lang / exo

Exocompilation for productive programming of hardware accelerators
https://exo-lang.dev
MIT License
290 stars 28 forks source link

Switch Backend to Directly Use Z3 instead of PySMT #138

Open gilbo opened 2 years ago

gilbo commented 2 years ago

We're currently relying on the Z3.py interface to get things to run anyway, so we won't be incurring a new dependency. Given the amount of trouble I've run into with PySMT, it would be good to just eliminate it as a dependency overall.

Additionally, doing this change will give us access to SMT-LIB's div and mod functions, and we can see if Z3 can handle these details for us more seamlessly than we currently are.

gilbo commented 11 months ago

@rachitnigam FYI, In the new_analysis_core.py file, everything should just be using Z3 instead of SMT (PySMT) already. It should be possible to entirely remove PySMT from that file and have everything work fine. In that respect, this issue should be considered merely a cleanup issue.

However, effectcheck.py does still rely on PySMT. So, someone would have to go through that file and migrate it to use the Z3 interface instead if we want to fully jettison the PySMT dependency.

This issue is low priority regardless. The effectcheck ought to be rewritten/replaced in the course of program analysis overhaul (further steps beyond getting abstract interpretation working). So if we ignore this issue it is likely that it will eventually become obsolete anyway.