Fix static lib repacking for cvc5

[makaimann]

In smt-switch, we try to pack all the (nonstandard) dependencies into the static library when compiled with --static. This is more convenient from a user perspective, because smt-switch wraps other solvers and you don't want to keep track of all the dependencies. After updating to cvc5, this broke because of the dependencies on cadical and poly.

Example: Say smt-switch is compiled as a static library, and you write a program using cvc5 through smt-switch. If you link that program against libsmt-switch-cvc5.a and libsmt-switch.a before this change, there will be errors about missing symbols from cadical and poly. The user would have to link those static libraries in directly. Instead, we want to pack all those into the same library (libsmt-switch-cvc5.a) so users don't need to think about the dependency tree.

I tried just adding them to the existing approach in cvc5/CMakeLists.txt, but it created a static library that was still missing symbols. The only way I could get this to work is use the appropriate tool for Mac vs Linux. On Mac, libtool (note: this is different than the GNU libtool) works well. On Linux, using an MRI script with ar is best. The scripts/repack-static-lib.sh script detects the OS and uses the appropriate technique.

[makaimann]

Hey @4tXJ7f, I was wondering if you'd mind reviewing this for me? It's related to cvc5. No rush and if not, I can find someone else. Additionally, please let me know if you know of a better way and/or if I can explain anything further.

[makaimann]

Hey @ahmed-irfan, would you mind taking a look at this? You would be a good person, because it's needed for cvc5 support in pono.

[ahmed-irfan]

The api in current mainline of cvc5 has changed. Do you want to also make change here:

[ 21%] Building CXX object cvc5/CMakeFiles/smt-switch-cvc5.dir/src/cvc5_solver.cpp.o
/Users/ahmed/git/smt-switch/cvc5/src/cvc5_solver.cpp:36:28: error: no member named 'PLUS' in namespace 'cvc5::api'
      { Plus, ::cvc5::api::PLUS },
              ~~~~~~~~~~~~~^
/Users/ahmed/git/smt-switch/cvc5/src/cvc5_solver.cpp:37:29: error: no member named 'MINUS' in namespace 'cvc5::api'
      { Minus, ::cvc5::api::MINUS },
               ~~~~~~~~~~~~~^
/Users/ahmed/git/smt-switch/cvc5/src/cvc5_solver.cpp:38:30: error: no member named 'UMINUS' in namespace 'cvc5::api'
      { Negate, ::cvc5::api::UMINUS },
                ~~~~~~~~~~~~~^
/Users/ahmed/git/smt-switch/cvc5/src/cvc5_solver.cpp:1004:38: error: no member named 'BOUND_VAR_LIST' in namespace 'cvc5::api'
            solver.mkTerm(cvc5::api::BOUND_VAR_LIST, cterms.back());
                          ~~~~~~~~~~~^

[makaimann]

Thanks for the review! Good to know. Made the update with 29ad33d902d81e133d8af36e90643099f0825c9e. Let's see if CI passes.

[makaimann]

Hey @ahmed-irfan, sorry for the delay in getting to this. It required updating cvc5 further which also changed the interface. It should be working now. Let's see if it passes tests.