decision_proceduret API with assumptions #7979
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Member
kroening
commented
Oct 27, 2023
•
kroening
commented
- 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.
kroening
force-pushed
the
decision-procedure-API
branch
2 times, most recently
from
1ad4119 to
11f6e8d
Compare
kroening
force-pushed
the
decision-procedure-API
branch
from
11f6e8d to
752b318
Compare
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #7979 +/- ##
========================================
Coverage 79.08% 79.08%
========================================
Files 1696 1697 +1
Lines 196429 196463 +34
========================================
+ Hits 155346 155382 +36
+ Misses 41083 41081 -2 ☔ View full report in Codecov by Sentry. |
kroening
force-pushed
the
decision-procedure-API
branch
2 times, most recently
from
fa810f5 to
7ff8ea9
Compare
kroening
requested review from
peterschrammel,
thomasspriggs,
NlightNFotis,
TGWDB,
esteffin,
martin-cs and
tautschnig
as code owners
martin-cs
approved these changes
Nov 2, 2023
The cbmc/hex_trace test pattern relies on a particular value (0) for an uninitialized local variable. This removes the pattern. See https://github.com/diffblue/cbmc/actions/runs/6672135313/job/18269948126?pr=7979 as an exemplar where this was triggered.
This changes the API offered by decision_proceduret to solving under assumptions. Solving under assumptions has been popularised by MiniSat, and is a state-less alternative to context stacks. This change mimics the transition from check-sat to check-sat-assuming that SMT-LIB is undergoing.
kroening
force-pushed
the
decision-procedure-API
branch
from
7ff8ea9 to
bbedeea
Compare
tautschnig
approved these changes
Dec 18, 2023
| decision_proceduret::~decision_proceduret() | ||
| { | ||
| } | ||
|
|
||
| decision_proceduret::resultt decision_proceduret::operator()() | ||
| { | ||
| return dec_solve(); | ||
| return dec_solve(nil_exprt()); | ||
| } |
There was a problem hiding this comment.
My preference would be to use std::optional at the interface rather than nil.
There was a problem hiding this comment.
I was reluctant to do so since that can't avoid copying the expression.
There was a problem hiding this comment.
Wouldn't const std::optional<exprt> & do the trick?
There was a problem hiding this comment.
No, you'd still need to copy the expression into the optional when creating the optional.
There was a problem hiding this comment.
std::optional< std::reference_wrapper<exprt> > would work, but then it's getting more verbose.
peterschrammel
approved these changes
Dec 18, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.