search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

smt-switch is very tightly bound to a specific, old version of CVC5. #328

Closed kunalsheth closed 1 year ago

kunalsheth commented 1 year ago

Here are a couple specific issues I encountered when trying to use a newer cvc5 (1.0.5+)

1: https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/cvc5/src/cvc5_term.cpp#L271 is not a complete list of enum values e.g.

This causes is_value() to return sometimes erroneously return false, and cause crashes down the line.

2: Several header paths (e.g. cvc5_sort.h, cvc5_kind.h, and api/cpp/..) have changed in newer versions of cvc5.

Ideally, multiple versions of each solver could be supported within one smt-switch build. Though they may not be able to be used simultaneously at runtime.

yoni206 commented 1 year ago

Thank you! If you would like to make a PR that updates cvc5's version in smt-switch, that would be great, and we will be happy to help. Otherwise, we will upgrade to the newest version as soon as we can.

kunalsheth commented 1 year ago

Hello! I would love to write that PR, but I'm unfortunately not sure if I'll be able to get to it until January. I worked on a project a couple months ago that heavily used smt-switch— and Clark asked me to file all of my learnings from that project as issues here before I forget.