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/ematching/inst_strategy.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/ematching/inst_strategy.h')
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 916790d9c..3baa25fa0 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -29,6 +29,7 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersState; +class QuantifiersInferenceManager; /** A status response to process */ enum class InstStrategyStatus @@ -45,8 +46,10 @@ enum class InstStrategyStatus class InstStrategy { public: - InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs) - : d_quantEngine(qe), d_qstate(qs) + InstStrategy(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim) { } virtual ~InstStrategy() {} @@ -64,6 +67,8 @@ class InstStrategy QuantifiersEngine* d_quantEngine; /** The quantifiers state object */ QuantifiersState& d_qstate; + /** The quantifiers inference manager object */ + QuantifiersInferenceManager& d_qim; }; /* class InstStrategy */ } // namespace quantifiers |