diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-04 16:55:00 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-04 16:55:00 -0600 |
| commit | 0bcaeb9cd75ec2268b6fe237bc037865d5122b5a (patch) | |
| tree | f0d5efa61e6c839720d5494b33113520e59a5cd8 /src/theory/quantifiers/inst_strategy_enumerative.cpp | |
| parent | d89ff37c2dfbd91dd89169ad5dda06b5cc8f0a7b (diff) | |
Introduce quantifiers registry utility (#5829)
This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_enumerative.cpp')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c0f294528..f22e67815 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -35,8 +35,9 @@ namespace quantifiers { InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() @@ -130,7 +131,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) for (unsigned i = 0; i < nquant; i++) { Node q = fm->getAssertedQuantifier(i, true); - bool doProcess = d_quantEngine->hasOwnership(q, this) + bool doProcess = d_qreg.hasOwnership(q, this) && fm->isQuantifierActive(q) && alreadyProc.find(q) == alreadyProc.end(); if (doProcess) |