-
Notifications
You must be signed in to change notification settings - Fork 38
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
Remove SBV from the SMT backend #93
Conversation
…references are prestate)
I took it upon myself to just go ahead and commit all the redundant parentheses I encountered since that seemed like a no-brainer 🙃 still one other suggestion open though and may add more. Looks very good in general though, I'm really just nitpicking. |
Co-authored-by: MrChico <[email protected]>
Co-authored-by: Jack Ek <[email protected]>
this is really nice! Can we add a test for #58 now that it works? |
Co-authored-by: Jack Ek <[email protected]>
done. |
I already approved before the new test so I can't do it again but looks great :) |
|
||
invariants | ||
|
||
b[a] == 1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!!
This PR rewrites the SMT backend to remove the usage of the sbv library. We now generate smt2 directly in
SMT.hs
without going through an additional abstraction layer.The primary motivation for this change was to allow the encoding of mappings in act as arrays in SMT. Doing this with sbv was surprisingly hard (sbv uses tuples for array indicies, act uses a nonempty list), and would have required either extensive modifications to the structure of the AST, significant additional boilerplate, or template haskell.
There are some additional benefits regarding auditability and debugging: the new SMT backend is less than 500 lines (compared to many thousand for sbv), and the resulting queries are significantly more readable.
The big disadvantage here is that we have to keep the sbv based code around for interfacing with
hevm
(which still relies on sbv for now), this is unfortunate, but seems to be a price worth paying given the alternatives.CLI output is currently very rough, and counterexamples are currently not generated, I intend to work on this next.
This PR closes the following issues: #62, #72, #91, #58