-
Notifications
You must be signed in to change notification settings - Fork 274
Quantifiers with multiple bindings #6585
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
Conversation
kroening
commented
Jan 17, 2022
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
This adds support for pretty-printing forall/exists expressions that have multiple bindings.
This adds support for converting forall/exists expressions that have multiple bindings to SMT2.
This adds convenience constructors for forall/exists expressions with multiple bindings.
The simplifier can now simplify !exists and !forall with multiple bindings.
59205b7
to
b165bf9
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6585 +/- ##
===========================================
+ Coverage 76.19% 76.21% +0.01%
===========================================
Files 1578 1578
Lines 181276 181392 +116
===========================================
+ Hits 138132 138249 +117
+ Misses 43144 43143 -1
Continue to review full report at Codecov.
|
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.
Any chance of some tests of this code?
Tests are coming in the branch model_refinement |