Add support for quantifiers #3993
Conversation
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
tests/expected/quantifiers/expected
Outdated
| @@ -0,0 +1 @@ | |||
| VERIFICATION:- SUCCESSFUL | |||
There was a problem hiding this comment.
That by itself would not really make for a useful use of expected - can we check for particular properties that are being reported as proved, please?
There was a problem hiding this comment.
Reviving this comment--please write expected tests instead that show that the quantifier is being evaluated and its properties are successful, and then I'll review.
There was a problem hiding this comment.
I've only looked at the tests so far. I'm not sure that this makes sense to merge if the only kinds of harnesses that we can run are the ones in no_array.rs. IMO the main benefit of quantifiers is quantifying over some collection (array, vector, ...), so we should either block this PR until that's possible, or I would expect to see some expected tests to prove that it works.
Also, can we move the tests to expected and have some assertions about particular properties that are being checked?
tests/kani/Quantifiers/even_fixme.rs
Outdated
| fn quantifier_even_harness() { | ||
| let j: isize = kani::any(); | ||
| kani::assume(j % 2 == 0 && j < 2000 && j > -2000); | ||
| kani::assert(kani::exists!(|i in (-1000, 1000)| i + i == j), ""); |
There was a problem hiding this comment.
I am surprised this one is a "fixme" test - what is holding us up on this one? (Also, this one does not include a link to an issue.)
This PR add support for quantifiers. Especially, we inline function calls in quantified expressions so that the result statement-expression can be accepted by the CBMC backend.
RFC: RFC 0010-quantifiers.
Resolves #2546 and #836.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.