Add array trace printing to incremental SMT2 decision procedure

[thomasspriggs]

This PR includes the functionality from #7066 , but with the additional fixes required to support traces where individual elements of an array are written to.

• 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.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #7078 (0f7b21c) into develop (f4d92f2) will increase coverage by 0.01%.
The diff coverage is 97.95%.

@@             Coverage Diff             @@
##           develop    #7078      +/-   ##
===========================================
+ Coverage    77.85%   77.87%   +0.01%     
===========================================
  Files         1574     1574              
  Lines       181245   181392     +147     
===========================================
+ Hits        141109   141252     +143     
- Misses       40136    40140       +4     

Impacted Files	Coverage Δ
..._incremental/smt2_incremental_decision_procedure.h	75.00% <ø> (ø)
src/solvers/smt2_incremental/smt_solver_process.h	100.00% <ø> (ø)
...lvers/smt2_incremental/smt_response_validation.cpp	95.58% <86.48%> (-2.30%)	⬇️
src/solvers/smt2_incremental/response_or_error.h	100.00% <100.00%> (ø)
...ncremental/smt2_incremental_decision_procedure.cpp	96.72% <100.00%> (+0.73%)	⬆️
src/solvers/smt2_incremental/smt_array_theory.cpp	100.00% <100.00%> (ø)
...rc/solvers/smt2_incremental/smt_solver_process.cpp	69.44% <100.00%> (+0.87%)	⬆️
src/solvers/smt2_incremental/smt_terms.h	100.00% <100.00%> (ø)
...ncremental/smt2_incremental_decision_procedure.cpp	98.09% <100.00%> (+0.08%)	⬆️
...lvers/smt2_incremental/smt_response_validation.cpp	98.42% <100.00%> (+0.63%)	⬆️
... and 2 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[TGWDB]

Can we please have some unit tests for the error conditions both for the map and for arrays? I can think of the following that may not be tested:

1. Identifier type in map is different to type in parse tree
2. Identifier not in the map
3. Multiple instances of the identifier in the map (with different same/types?) -- Does it matter if there is duplication and the types are the same?
4. Array size wrong or unspecified
5. Multiple responses from the solver
6. Error in parsing sub-expression of select (e.g. index is good but value has wrong type?)

[esteffin]

Looks good to me

[thomasspriggs]

Can we please have some unit tests for the error conditions both for the map and for arrays? I can think of the following that may not be tested:

1. Identifier type in map is different to type in parse tree

Identifiers in the parse tree do not have types(sorts). This is the whole reason the identifier map is needed for the validation. Therefore the sorts in the map cannot mismatch the (missing) sorts in the parse tree.

2. Identifier not in the map

Added.

3. Multiple instances of the identifier in the map (with different same/types?) -- Does it matter if there is duplication and the types are the same?

The identifier is used as the key in the unordered map. Therefore the same one cannot be inserted twice.

4. Array size wrong or unspecified

Is this the check on type.is_complete() in smt2_incremental_decision_proceduret::get_expr?

5. Multiple responses from the solver

Which part of this PR does this comment apply to? Extra unrequested responses from the solver could be a potential issue for any part of the new back end which is fetching responses from the solver. Extra responses would not be fetched until the decision procedure issues another command expecting a response. At which point the buffered response will be fetched and the subsequent validation will fail due to the response being of a different nature from that expected.

6. Error in parsing sub-expression of select (e.g. index is good but value has wrong type?)

The parser isn't special cased for select. Is this referring to try_select_validation in smt_response_valildation.cpp? I think this does actually need better validation to report error messages, rather than violate the invariants in smt_array_theoryt::selectt::validate.

[TGWDB]

Can we please have some unit tests for the error conditions both for the map and for arrays? I can think of the following that may not be tested:

1. Identifier type in map is different to type in parse tree

Identifiers in the parse tree do not have types(sorts). This is the whole reason the identifier map is needed for the validation. Therefore the sorts in the map cannot mismatch the (missing) sorts in the parse tree.

I notice there are (now) unit tests for trying to parse SMT output that is invalid, but I was thinking here of unit tests for mismatches. E.g., trying to parse the value of an identifier which is in the map as a bool, but the value in the parse tree is represented as a bitvector or other (non-bool) literal such as 0xFF.

3. Multiple instances of the identifier in the map (with different same/types?) -- Does it matter if there is duplication and the types are the same?

The identifier is used as the key in the unordered map. Therefore the same one cannot be inserted twice.

For some reason I had in mind this was using a map that supports multiple values... my mistake.

4. Array size wrong or unspecified

Is this the check on type.is_complete() in smt2_incremental_decision_proceduret::get_expr?

Looks like it's covered. Other cases I can think of would be catching errors in different parts of the code (e.g. somehow we had the wrong size somewhere), but this would be overly defensive.

5. Multiple responses from the solver

Which part of this PR does this comment apply to? Extra unrequested responses from the solver could be a potential issue for any part of the new back end which is fetching responses from the solver. Extra responses would not be fetched until the decision procedure issues another command expecting a response. At which point the buffered response will be fetched and the subsequent validation will fail due to the response being of a different nature from that expected.

My text here was utterly incomplete - sorry. Your comment addresses some of the possible scenarios - the one I had in mind was whether it is possible for any of the information to change between calls to the solver to solve/get_value in a way that might cause issues? On deeper thought I suspect the answer is that due to the SSA/symex/etc. this is not possible, so we can be confident in the implementation here.

6. Error in parsing sub-expression of select (e.g. index is good but value has wrong type?)

The parser isn't special cased for select. Is this referring to try_select_validation in smt_response_valildation.cpp? I think this does actually need better validation to report error messages, rather than violate the invariants in smt_array_theoryt::selectt::validate.

This seems to be addressed now? I did notice that we at times optimistically continue once one error may have been detected (e.g. smt_response_validation.cpp lines 256 & 7), but this kind of optimisation seems unnecessary here.