All SMT solvers are now bundled in the folder smt_solvers.
Currently includes z3, cvc4 and monosat.
The script smt-pnr/util/get_smt_solvers.sh checks if the folder is present
and that it contains all solvers and if its missing any, the script
downloads the whole tarball from
http://web.stanford.edu/~makaim/files/smt_solvers.tar.gz
Then it adds solver directories to the necessary paths.
The folder is cached to speed up the build on subsequent runs.
=================== Why the changes ==============================
These changes are part of incorporating a solver agnostic API that
I've been working on into pnr. This allows us to change the underlying
smt solvers. Currently supports z3 and cvc4.
The API is similar to pySMT but follows SMT-LIB more closely.
Additionally, it will allow us to incorporate optimization or
new theories for multiple solvers in the future.
Using the script to get the smt solvers makes it so we don't have to
change the .travis.yml of the flow every time we add a new smt solver.
All SMT solvers are now bundled in the folder smt_solvers. Currently includes z3, cvc4 and monosat.
The script smt-pnr/util/get_smt_solvers.sh checks if the folder is present and that it contains all solvers and if its missing any, the script downloads the whole tarball from http://web.stanford.edu/~makaim/files/smt_solvers.tar.gz
Then it adds solver directories to the necessary paths.
The folder is cached to speed up the build on subsequent runs.
=================== Why the changes ==============================
These changes are part of incorporating a solver agnostic API that I've been working on into pnr. This allows us to change the underlying smt solvers. Currently supports z3 and cvc4.
The API is similar to pySMT but follows SMT-LIB more closely. Additionally, it will allow us to incorporate optimization or new theories for multiple solvers in the future.
Using the script to get the smt solvers makes it so we don't have to change the .travis.yml of the flow every time we add a new smt solver.
Let me know if there are any comments/concerns!