Experimental version of smtlib-backends-cvc5
#65
Conversation
There was a problem hiding this comment.
Thanks @goodlyrottenapple!
It looks like a fine contribution.
uses an unstable version of cvc5, hopefully the next release will include the new API
I'll edit the top-level README to mention this backend and remark the experimental nature of it.
due to this bug on macOS https://gitlab.haskell.org/ghc/ghc/-/issues/11829, I've upgraded the nix shell to ghc 9.4.8 as I couldn't get the suggested fix work for the version of ghc in the current shell
Fine by me. Worth mentioning in a new smtlib-backends-cvc5/README.md.
The ParserException type doesn't seem to be exported in the parser API, so parsing errors are caught by a default catch (...) block, potentially giving sub-optimal error messages
This is worth reporting to cvc5 devs. If you open an issue with them, it would be worth linking to it near the catchall.
The tests and likely any downstream executables have to be linked with clang++/g++. Not sure if this is likely to cause any issues?
There is not a problem that I can see for the other backends. Users of smtlib-backends-cvc5 might have to keep it in mind. Worth mentioning in smtlib-backends-cvc5/README.md as well.
| basicUse = | ||
| -- 'CVC5.with' runs a computation using the 'CVC5' backend | ||
| -- it takes a configuration object as argument, whose use we describe in | ||
| -- 'settingOptions' |
There was a problem hiding this comment.
I couldn't find this reference.
There was a problem hiding this comment.
Sorry that was a copy paste from the Z3 library. Have now removed the reference.
… issue in cvc5 api
Perfect timing: cvc5/cvc5#10181 the issue was fixed just before I asked. |
smtlib-backends-cvc5/cbits/cvc5.cpp
Outdated
| // should catch (ParserException& e) here - see https://github.com/cvc5/cvc5/issues/10181 | ||
| catch (...) |
There was a problem hiding this comment.
No need to single out ParserException's then?
There was a problem hiding this comment.
They made the CVC5ApiException a superclass of ParserException now https://github.com/mudathirmahgoub/cvc5/blob/efac45b3a45b75c09625dfd879c588ac609313b1/include/cvc5/cvc5_parser.h#L275
I noticed that CVC5 has recently exported the parser into an API and have an example of parsing and executing SMTLIB commands: https://github.com/cvc5/cvc5/blob/main/examples/api/cpp/parser.cpp
I've implemented an initial version of
smtlib-backends-cvc5to use this API, however, there are a few caveats:ParserExceptiontype doesn't seem to be exported in the parser API, so parsing errors are caught by a defaultcatch (...)block, potentially giving sub-optimal error messages