Fix SMT2 encoding of array_comprehension_exprt
#5973
Conversation
SaswatPadhi
added
SMT Backend Interface
bugfix
aws
SaswatPadhi
requested review from
allredj,
martin-cs,
peterschrammel and
romainbrenguier
as code owners
SaswatPadhi
force-pushed
the
smt2_array_comprehension
branch
from
e99097e to
1a5a4d3
Compare
SaswatPadhi
changed the title
array_comprehension_exprt
Codecov Report
@@ Coverage Diff @@
## develop #5973 +/- ##
===========================================
+ Coverage 75.12% 75.14% +0.02%
===========================================
Files 1435 1444 +9
Lines 156301 157307 +1006
===========================================
+ Hits 117416 118207 +791
- Misses 38885 39100 +215
Continue to review full report at Codecov.
|
|
If you can use an SMT-LIB expression that maps directly onto what you want to translate, you no longer need the |
There was a problem hiding this comment.
- Is you think it fixes other things, please can you take the time to find out what they are? Someone will have to do this at some point and it would be better that it is connected with the change that fixes them.
- I'm pretty sure
lambdaisn't in SMT-LIB 2. It has been /proposed/ for SMT-LIB 3 but we shouldn't be outputting it in an SMT-LIB 2.0 back-end.
src/solvers/smt2/smt2_conv.cpp
Outdated
|
|
||
| const irep_idt id = | ||
| "array_comprehension." + std::to_string(defined_expressions.size()); | ||
| out << "(define-fun " << id << " () "; |
There was a problem hiding this comment.
Why are you creating a function with no arguments that returns a lambda?
There was a problem hiding this comment.
Unless I have got the wrong end of the stick completely, I think you can implement this without the lambda.
There was a problem hiding this comment.
Arrays are infinite maps in SMT and are represented just like key -> value functions. The function with no arguments returns a lambda, because we want to return an array.
This has been tested with both Z3 -- you can run the attached regression test with cbmc --smt2.
I am not super sure about the official status of lambda within SMTLIB2 vs SMTLIB3, but Z3 supports it for a while now.
AFAIK, the only other way to implement array comprehension would be to use quantifiers, but that did not work even for the simpler case of array_of where the lambda expression was a constant (independent of the index).
There was a problem hiding this comment.
I will make this translation solver-specific then -- only emit SMT2 output using lambda if solver is Z3. Otherwise, fall back to quantifier-based initialization.
[Also, more info about lambda handling here: Z3Prover/z3/issues/2221]
SaswatPadhi
force-pushed
the
smt2_array_comprehension
branch
from
1a5a4d3 to
0e2e339
Compare
|
I have tested this (the attached regression test) locally with both However, with CVC4 (and other solvers that don't allow |
|
Thanks for taking a look, @martin-cs. I agree with not changing the default logic to allow quantifiers. I opened #5977 to discuss more about this issue. |
SaswatPadhi
force-pushed
the
smt2_array_comprehension
branch
3 times, most recently
from
7037b93 to
0c4f8b3
Compare
Z3 treats arrays and lambdas as identical structures, so we use lambdas in the z3-specific encoding of `array_comprehension_exprt`. For other solvers, we fall back to a universally quantified expression to initialize the array.
SaswatPadhi
force-pushed
the
smt2_array_comprehension
branch
from
0c4f8b3 to
c499ff7
Compare
The SMT conversion routines were missing a rule for translating
array_comprehension_exprt.This PR creates a new translation rule leveraging the
lambdaconstruct in SMTLIB2.NOTE: There may be several other
broken-smt-backendregression tests that may be fixed by this change; I haven't checked (there are too many!).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.