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

❌ Patch coverage is 70.40359% with 66 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.00%. Comparing base (15eb10a) to head (0ae286e).

Files with missing lines	Patch %	Lines
src/solvers/flattening/boolbv_quantifier.cpp	70.40%	66 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8224      +/-   ##
===========================================
- Coverage    80.00%   80.00%   -0.01%     
===========================================
  Files         1700     1700              
  Lines       188252   188470     +218     
  Branches        73       73              
===========================================
+ Hits        150613   150783     +170     
- Misses       37639    37687      +48     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[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

[Copilot]

Pull request overview

This PR implements quantifier instantiation via E-matching for cases where eager (enumerative) instantiation cannot be applied. The implementation uses pattern matching on array index expressions to find suitable instantiation values from the solver's cache.

Key changes:

• Added E-matching based quantifier instantiation as a fallback when eager instantiation fails
• Removed the lb > ub check in eager instantiation (correctly handles empty ranges with vacuous truth/false)
• Updated test expectations to reflect that previously unsupported quantifier cases now work

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/solvers/flattening/boolbv_quantifier.cpp	Implements E-matching algorithm via instantiate_one_quantifier function and modifies finish_eager_conversion_quantifiers to apply it
regression/cbmc/Quantifiers-unbounded-array/test.desc	Test descriptor for new unbounded array quantifier test case
regression/cbmc/Quantifiers-unbounded-array/main.c	Test case demonstrating quantifier instantiation with unbounded arrays and loop invariants
regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc	Test descriptor for overflow detection with quantifiers
regression/cbmc/Quantifiers-unbounded-array-overflow/main.c	Test case that validates overflow detection in loop invariants with quantifiers
regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc	Test descriptor for 2D array quantifier handling
regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c	Test case for nested quantifiers over 2D arrays
regression/cbmc/Quantifiers-type/test.desc	Updated test expectations to reflect working quantifier support
regression/cbmc/Quantifiers-invalid-var-range/test.desc	Updated test expectations from KNOWNBUG to CORE status
doc/cprover-manual/cbmc-assertions.md	Updated documentation from "future releases will support" to "CPROVER supports" for quantifiers

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Missing defensive check for quantifier type. Add an assertion or UNREACHABLE statement after the if-else chain to handle the case where q_expr.id() is neither ID_exists nor ID_forall, similar to the pattern used in eager_quantifier_instantiation at line 265.

Suggested change

	else
	return conjunction(instantiations);
	else if(q_expr.id() == ID_forall)
	return conjunction(instantiations);
	UNREACHABLE;
	return {};