diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-30 10:05:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-30 15:05:29 +0000 |
| commit | 4948485775b04d95dbf69eee311bf452d0bfac3d (patch) | |
| tree | 536a017cc5a8cce04cd9863c8fb0671cc9f7f5e1 /src/theory/builtin | |
| parent | 05db3e9511c1c485b27a8e3467bcae74659dfd9a (diff) | |
Implement simple tracking of instantiation lemmas (#6077)
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
Diffstat (limited to 'src/theory/builtin')
0 files changed, 0 insertions, 0 deletions