Support other solvers than z3

AdrienChampion commented 7 years ago

cvc4: should require minor work, mostly testing and adapting a few parsers
mathsat used to be a nightmare as it was not really SMT-LIB 2 compliant, don't know what the status is

aep commented 4 years ago

cvc4 doesnt work out of the box at least. probably because interactive mode echoes back?

Error(ParseError("expected `sat` or `unsat`", "(declare-const n Int)"),

AdrienChampion commented 4 years ago

@aep yeah originally rsmt2 supported cvc4, but it was quite tedious to maintain and until now no one really asked for it.

There used to be a way to remove the prompt completely, but I'm not sure that's the case anymore. I will take a look at adding support for cvc4 back. I will most likely only add support for the latest version, which will provide a template for supporting other versions that behave differently.

aep commented 4 years ago

its "--no-interactive", see my PR

aep commented 4 years ago

any idea how i can run the tests against the other solvers to find the problems?

i could search and replace SmtConf::z3 but that's a temporary solution

AdrienChampion commented 4 years ago

Right, the idea is to extend SmtConf to add a cvc4 "driver" that handles the specifics of interacting with cvc4. Just give me a bit of time, I'll work on it this afternoon to add support for the latest cvc4 I have access to. (Hopefully.)

Once that's done, it will provide a guideline for submitting drivers for other solvers, such as yices or other versions of cvc4.

aep commented 4 years ago

the zz compiler self test suite has half a million lines of smt2.

yices2 works as expected with my PR

AdrienChampion commented 4 years ago

Alright, so cvc4 is actually already supported, at least as far as declarations/assertions/get-model are concerned. Also, get-value segfaults on my version (1.4.2).

Yices 2 mostly works out of the box, but differs in how it outputs models. That is, it writes (= <symbol> <value>) where z3 would write (define-fun <symbol> (<args>) <sort> <value>). (Which implies that Yices 2 does not seem to plan to provide values for non-nullary function symbols.) This forces me to change a few things in the API. Nothing big, but I need a bit more time. This should be taken care of tomorrow.

AdrienChampion commented 4 years ago

In any case, thank you for #11 as it makes it very fast for me to add support for Yices 2 :D

AdrienChampion commented 4 years ago

Done, I released the new version of rsmt2 as beta for now: https://crates.io/crates/rsmt2/0.11.0-beta.0

I think we can close this issue, feel free to open new ones if you run into problems with this beta version.

Thank you again :)

aep commented 4 years ago

how would i use this with yices2-mt?

aep commented 4 years ago

the cvc4 config is still wrong
yices2-smt is the wrong binary name, even for st
--interactive is missing
QF_UFVB missing

after fixing those its working

AdrienChampion commented 4 years ago

tested with the latest version of CVC4 and Yices 2 I could find, if you have specific problems it would be great to discuss them in a dedicated issue.
binary names for CVC4 and Yices 2 are the names used in the releases by the CVC4 and Yices 2 teams. At least the ones I got. You can change the command used to launch them in rsmt2 to match whatever you are using.
I can't add all theories, looking back it did not make much sense to enumerate some of them and force users to use that. I added Solver::set_custom_logic to make it easier to set your own logic.

aep commented 4 years ago

cvc4 needs to --no-interactive as --interactive will echo

you're correct about the yices binary release. no idea why the source build is different. Possibly about to change

still missing --incremental for yices

aep commented 4 years ago

any progress on adding --incremental to yices? i'd like to get rid of the downstream fork

AdrienChampion commented 4 years ago

now using --no-interactive for cvc4 as you recommended, which allowed to remove prompt parsing (no visible change for users)
incrementality is opt-in for yices and all solvers, if you want it you need to use SmtConf::incremental on your solver configuration
in the end I changed the default binary name for yices 2, it is now yices

I'm about to publish rsmt2 0.11.0 which is currently beta. Note that nothing has changed from the user's perspective compared to the beta version from January. (Except the default name for yices' binary.)

I would really appreciate it if you could take the time to give it a try and let me know if you run into any problems before I release 0.11.0. Using rsmt2 = { git = "https://github.com/kino-mc/rsmt2" }.

I think it would be better to have that feedback in a different issue though, if that's ok with you. If you encounter problems for a specific solver, remember to include your operating system and the solver's version :)

Thank you again for your feedback!

kino-mc / rsmt2

Support other solvers than z3 #7