Fix SMT2 encoding of array_of_exprt
#5974
Conversation
SaswatPadhi
added
SMT Backend Interface
bugfix
aws
SaswatPadhi
requested review from
martin-cs,
peterschrammel and
romainbrenguier
as code owners
SaswatPadhi
changed the title
array_of_exprtarray_of_exprt
SaswatPadhi
changed the title
array_of_exprtarray_of_exprt
|
Hmm ... CI is failing because CPROVER SMT2 doesn't understand |
|
Likewise here: you no longer need defined_expressions -- simply emit the required SMT-LIB expression directly. |
src/solvers/smt2/smt2_conv.cpp
Outdated
| #endif | ||
| out << "(define-fun " << id << " () "; | ||
| convert_type(array_of_expr.type()); | ||
| out << " ((as const "; |
There was a problem hiding this comment.
I'm pretty sure as const isn't in SMT-LIB.
There was a problem hiding this comment.
I am not sure about the status of as const in SMTLIB2 standard, but both Z3 and CVC4 accept as const. We anyway didn't have a working solution for this with quantifiers, and I have tested array initialization with as const for both solvers.
There was a problem hiding this comment.
I will make this translation solver-specific then -- only emit SMT2 output if solver is either Z3 or CVC4.
There was a problem hiding this comment.
Yes, it is fine to use extensions but they must not be in the default. Z3 and CVC4 are not the only solvers, they are not even the only solvers that people use with CBMC.
There was a problem hiding this comment.
I agree. Please take another look and see if the changes look okay. I introduced the use_as_const field to track solvers that support as const.
SaswatPadhi
force-pushed
the
smt2_array_of
branch
from
01d1ec5 to
fa1f769
Compare
|
Marking as draft until #5976 is merged. |
SaswatPadhi
force-pushed
the
smt2_array_of
branch
from
fa1f769 to
ebef52d
Compare
Instead of using quantifers to encode array_of expressions -- which, as indicated in the comments, doesn't seem to work on existing solvers -- we can use the `as const` construct for CVC4 and Z3.
SaswatPadhi
force-pushed
the
smt2_array_of
branch
from
ebef52d to
aaa7a3a
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5974 +/- ##
===========================================
- Coverage 75.02% 75.01% -0.01%
===========================================
Files 1431 1433 +2
Lines 155595 155738 +143
===========================================
+ Hits 116734 116834 +100
- Misses 38861 38904 +43
Continue to review full report at Codecov.
|
|
It would be awesome to identify the tests that work after this change, and remove the 'broken' flag from these! |
#5958 will help with this, but I need to do my homework first... |
|
I will create a separate PR for the |
This commit fixes an error introduced in diffblue#5974 where quantifiers were produced for all SMT2 solvers despite only being supported by Z3 and CVC4. The fix here reverts to the older behaviour for other solvers. Fixes diffblue#6263
This commit fixes an error introduced in diffblue#5974 where quantifiers were produced for all SMT2 solvers despite only being supported by Z3 and CVC4. The fix here reverts to the older behaviour for other solvers. Fixes diffblue#6263
The SMT conversion routines were broken for
array_comprehension_exprt. They used quantifiers to initialize constant arrays, but that encoding didn't seem to work with existing SMT solvers.This PR fixes the translation rule by using the
as constconstruct in SMTLIB2.NOTE: I am not sure which regression test is directly affected by this, I just noticed this issue while fixing another bug [#5973]. I'd be happy to add a new regression test, but there must be some
broken-smt-backendregression test blocked on this one.Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.