Quantifier instantiation via simplistic E-matching

[tautschnig]

Use E-matching on index expressions to instantiate quantifiers when eager instantiation (aka enumerative instantiation) cannot be applied.

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

[tautschnig]

Despite this being a "draft" PR I would like to ask for feedback on the following aspects:

• @remi-delmas-3000 on the overall PR and specifically on the Quantifiers-unbounded-array-overflow test case: we'll have to clean this up to make clear what assertions we really expect to fail.
• @kroening and @martin-cs : the expression matching implementation is really crude. Any and all suggestions would be most appreciated.

[codecov]

Codecov Report

Attention: Patch coverage is 76.66667% with 14 lines in your changes missing coverage. Please review.

Project coverage is 78.34%. Comparing base (629dbcd) to head (e076dab).

Files	Patch %	Lines
src/solvers/flattening/boolbv_quantifier.cpp	76.66%	14 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8224      +/-   ##
===========================================
- Coverage    78.35%   78.34%   -0.01%     
===========================================
  Files         1726     1726              
  Lines       188424   188497      +73     
  Branches     18248    18258      +10     
===========================================
+ Hits        147631   147686      +55     
- Misses       40793    40811      +18     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

• @remi-delmas-3000 on the overall PR and specifically on the Quantifiers-unbounded-array-overflow test case: we'll have to clean this up to make clear what assertions we really expect to fail.

This is now done, comment explaining the (expected) verification failure is now included.

[kroening]

This needs serious consideration: failing quantifier instantiation is the leading source of proof brittleness, and we are opening the door to that here.

[kroening]

I would much prefer a more deterministic, predictable and robust solution to this.

[martin-cs]

Hard maybe?

So, it would be good but there is going to be a limit on how much we can do like this. Unless we put a refinement loop around the solver and do something like MBQI. Getting that stable and reliable is tricky. Given the amount of work that has gone into E-matching in Z3 and Andy's decade+ of work on quantifiers in cvc5, I wonder whether it would be more efficient (in terms of dev-hours / things proved) to improve our SMT integration.

To actually answer the question you asked, things that might help:

• Make sure both the terms in the quantifiers and the expressions you are using as context are rewritten.
• Use a union-find so that "up to equality" is handled. The modern approach might be to use an E-Graph data structure for both this and previous.
• You can do a number of optimisations if the quantified variable(s) are only used once in the body or are only used in one atom. That should handle the simple cases but when you have \forall x, y, z . p(x,y) && q(y,z) && r(x,z) I think you need to get into term indexing and ordering the matching.

HTH