search

kino-mc / rsmt2

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Apache License 2.0
65 stars 14 forks source link

yices2 still wrong binary name #17

Closed aep closed 3 years ago

aep commented 4 years ago

its yices_smt2 or yices_smt2_mt , or yices-smt2, depending on OS and if you build from source or binary,

none of those are "yices2"

aep commented 4 years ago

see https://github.com/SRI-CSL/yices2/issues/213

AdrienChampion commented 4 years ago

Well, rsmt2 is not using the name yices2. You can see this here, in addition to when I told you here. But again, the default command hard-coded in rsmt2 is irrelevant anyway.

Remember that you can change the command by using SmtConf::cmd. Note that the default command is only provided for convenience (mostly mine, for testing), it does not make sense for rsmt2 users to rely on it. If you are writing an application, you need to let users give you the command that runs the solver they want (probably via CLA) and enforce it with the function I mentioned above. Unless you bundle the solver in your application somehow, in which case you can hard-code the command in the call to cmd.

Arguably I should remove default commands altogether to avoid this kind of confusion, or discuss it explicitly in the documentation.

AdrienChampion commented 4 years ago

Woops did not mean to close sorry.

AdrienChampion commented 4 years ago

@aep in the end I acted on what we discussed. I added an example of passing solver commands from the end-user to rsmt2. SolverConf and Solver constructors now take a mandatory command, default commands are still available using constructors prefixed with default_. They now have a big warning in their docs.

You can read more about these changes in the changelog.

I think it's much better and less confusing that way. I did all this because of your feedback, thank you 😃

I would like to release a new version shortly, there are many changes that still live in beta and have probably not been tested by anyone. It would be very helpful if you could let me know what you think of the new version: do the new changes clear the confusion and give enough information, and do you still have problems on your end?

AdrienChampion commented 3 years ago

Let me go ahead and close this. #24 lets solver commands be passed through environment variables, in addition to the constructors taking explicit commands one would get from the user. More information is available in the documentation.