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/quantifiers_engine.cpp | |
| 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/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8d8f54768..f1ca0dd9f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -630,6 +630,11 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector d_qim.getInstantiate()->getInstantiationTermVectors(insts); } +void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts) +{ + d_qim.getInstantiate()->getInstantiations(q, insts); +} + void QuantifiersEngine::printSynthSolution( std::ostream& out ) { if (d_qmodules->d_synth_e) { |