Add incremental SMT2 sort checked construction of bit vector predicate application and application of core theory functions #6256
Conversation
This file contains hidden or 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
Codecov Report
@@ Coverage Diff @@
## develop #6256 +/- ##
===========================================
+ Coverage 76.18% 76.21% +0.02%
===========================================
Files 1484 1490 +6
Lines 162092 162500 +408
===========================================
+ Hits 123495 123844 +349
- Misses 38597 38656 +59
Continue to review full report at Codecov.
|
|
This PR relates to #6134 |
TGWDB
reviewed
Jul 28, 2021
thomasspriggs
force-pushed
the
tas/smt_function_factories
branch
from
3f670cc to
d9fd299
Compare
For checking parameterised sorts.
thomasspriggs
force-pushed
the
tas/smt_function_factories
branch
from
c878207 to
652ca69
Compare
thomasspriggs
requested review from
chrisr-diffblue,
kroening,
NlightNFotis,
peterschrammel and
tautschnig
as code owners
thomasspriggs
changed the title
TGWDB
approved these changes
Jul 30, 2021
thomasspriggs
force-pushed
the
tas/smt_function_factories
branch
2 times, most recently
from
2061d96 to
d46aaab
Compare
| { | ||
| INVARIANT( | ||
| parameter_sorts.size() == arguments.size(), | ||
| "Number of parameters and number of arguments must the the same."); |
There was a problem hiding this comment.
"must the the same" => "must be the same"
| @@ -94,3 +95,15 @@ TEST_CASE("smt_set_option_commandt getter", "[core][smt2_incremental]") | |||
| CHECK(smt_set_option_commandt{models_on}.option() == models_on); | |||
| CHECK(smt_set_option_commandt{models_off}.option() == models_off); | |||
| } | |||
|
|
|||
| TEST_CASE("SMT2 function application factory tests", "[core][smt2_incremental]") | |||
There was a problem hiding this comment.
No CHECKs in this test? Whats its purpose?
There was a problem hiding this comment.
The checks were missing because I got distracted adding other functionality to this PR, before I finished writing this test. Thanks for spotting this oversight. I have now added some checks.
So that function specific INVARIANTS can be checked.
For consistency with how the functions for the bit vector theory are defined. Note that the factory is called `make_not` rather than `not`, because not is a keyword in C++ which is equivalent to the `!` operator.
To prevent construction of function application without checking that the given arguments are valid for the given function.
thomasspriggs
force-pushed
the
tas/smt_function_factories
branch
from
d46aaab to
686ba37
Compare
chrisr-diffblue
approved these changes
Aug 4, 2021
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.
Add incremental SMT2 sort checked construction of bit vector predicate application and application of core theory functions.