diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-08 16:50:16 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-08 16:50:16 -0600 |
| commit | c198f374972e62db0cebc93d3977fd1e414f431b (patch) | |
| tree | f1180a7bda884d5c91a4bd64044ada8eadaaf333 /src/theory/quantifiers/instantiate.h | |
| parent | ca9705cf0785e3a81fc25995df0bc3dc76e3bd9f (diff) | |
Use quantifiers inference manager for lemma management (#5867)
Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index bbb1a0a44..154cda681 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -78,7 +78,7 @@ class InstantiationRewriter * * Its main interface is ::addInstantiation(...), which is called by many of * the quantifiers modules, which enqueues instantiation lemmas in quantifiers - * engine via calls to QuantifiersEngine::addLemma. + * engine via calls to QuantifiersInferenceManager::addPendingLemma. * * It also has utilities for constructing instantiations, and interfaces for * getting the results of the instantiations produced during check-sat calls. @@ -90,6 +90,7 @@ class Instantiate : public QuantifiersUtil public: Instantiate(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -117,7 +118,7 @@ class Instantiate : public QuantifiersUtil * * This function returns true if the instantiation lemma for quantified * formula q for the substitution specified by m is successfully enqueued - * via a call to QuantifiersEngine::addLemma. + * via a call to QuantifiersInferenceManager::addPendingLemma. * mkRep : whether to take the representatives of the terms in the range of * the substitution m, * modEq : whether to check for duplication modulo equality in instantiation @@ -326,6 +327,8 @@ class Instantiate : public QuantifiersUtil QuantifiersEngine* d_qe; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** cache of term database for quantifiers engine */ |