-
Notifications
You must be signed in to change notification settings - Fork 14
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Decouple supported SMT solvers #8
Comments
Thank you for your interest in The short answer is that what you're asking for is the very goal of this library, and this is already supported in a more streamlined fashion than what you describe, at least in theory.
They're actually not hard-wired at all, So in theory, as long as your solver respects the SMT-LIB 2.* standard and can read from Anyway, in practice things are a bit different. OptionsThe first difference is that different solver will want different options to do different things. CVC4 wants the While users can specify whatever options they want when creating the CommandsThe second problem is that different solvers tend to implement the SMT-LIB standard slightly differently. Until recently for instance Z3 only supported the
would yield an error while the non-SMT-LIB
would work. Also, CVC4 used to return models differently from Z3, without the (Current) SolutionThe current approach is to use a (Eventually The idea is that whatever special option or special syntax (for models, The annoying thing is that as a user you need to know what kind of solver you're using, but as a result you don't need to worry about the basic options too much. The idea is that when users create a binary with your_super_binary --cvc4 "my_cvc4_version -m --incremental" ...
# Users of the binary have to know/discover you use get-model and push/pop and your_super_binary --z3 "my_z3_version -smt2 -in"
# Users of the binary have to know/discover z3 does not read from stdin by default
# Also, (I'm pretty sure) older version of z3 don't read their input in SMT-LIB 2 by default I think having a uniform API at This is just my vision though, if you disagree with this usage do let me know and let's talk about it :) Long story short there should be no need to create specific crates for each solver, just enrich I'm not saying this workflow is perfect, and I'm completely open for better ideas. |
I will try my best to add support for CVC4 soon-ish since (thanks to you) I just realized it's now much closer to Z3 commands/answers-wise than it used to be. As a result |
Thank you very much for your fast and comprehensive response! I am not sure if I understand enough about the SMT interfaces of concrete solvers to summarize my ideas of my visions. So please take all my suggestions with a grain of salt. :) You told that all solvers behave differently with their respective CLI, and So in the end result I hope you got the idea and I hope I got it all right. :) |
Okay, I see what you're saying, I'll think about it and get back to you :) |
No problem, and please take everything I said with a grain of salt since I am not sure if I have understood the problem you want to solve with rsmt2, either. ;) As far as I understood it my suggestion isn't very far away from the current project. It just pin points to a slight different direction in how to achieve the same things. With my suggested decoupling the ecosystem would be more stable. Adding a new SMT solver implementation or changing the implementation of another one would require no updates to |
I haven't forgotten about you :) I going to give it a try, by creating a different crate, probably named I'm still worried about a few things regarding your suggestion. I understand having to update rsmt2 whenever a new solver is added can be tedious to some (I personally don't mind, especially since there's not that many solvers around). But with this new workflow, changes in the main crate's API will potentially break all other crates. Arguably, that's only a problem until some stable API is reached so it's probably worth it in the long run. But, because of the lack of feedback, I'm not sure how convenient/natural the current workflow is. Anyway, I'll try to find something generic enough that makes sense. |
You might be right that this might become a huge project and you also might be right about the fact that the SMT solver area isn't very big. I do not want to enforce this idea since it involves a lot of work especially on your side and especially if done right. There are countless theories that should be supported in the end. For my personal project I simply want access to an efficient SMTLib2 parser that is flexible enough and has enough customization points available to let me integrate it efficiently with my own data structures or at least without performance penalties upon using them. It is up to you whether you want to actually start this project. I like having standardized and ecosystem wide APIs - so I favor your library over me implementing my own stuff as all other SMT solver did in the past. The existence of SMTLib2 is a good thing and so is the existence of a flexible ecosystem wide wrapper around it. :) |
Let me go ahead and close this for a mix of
(Mostly the second reason though.) The OP and newcomers are welcome to re-open this issue or create a new one to +1 this idea. |
As far as I understood the crate, it enables SMT solver front-ends to use a diverse set of SMT solvers implementing its interfaces. This is awesome and I would love to implement this for my SMT solver to use its SMTLibv2 parsing support so that I do not have to reinvent the wheel another time.
However, it seems that the SMT solvers that implement the interfaces of
rsmt2
are hard-wired into the library.Would it be possible to separate implementors (Z3, CVC4) from the actual interfaces?
The end result would be like that:
rsmt2
is now the crate providing the interfaces that the SMT clients use and the SMT solvers implementrsmt2-z3
is the crate that provides the implementation ofrsmt2
for the Z3 solver.rsmt2-cvc4
is the crate that provides the implementation ofrsmt2
for the CVC4 solver.rsmt2-stevia
is the crate that provides the implementation ofrsmt2
for the Stevia solver.etc.
A client would then simply depend on one of the
rsmt2-*
crates for a direct support of the associated SMT solver.I think you got the idea. :)
So the question: Is this even possible?
The text was updated successfully, but these errors were encountered: