diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-24 13:55:50 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-24 13:55:50 -0600 |
| commit | ae541bb35e7b627f28b13eede29f5870f42b078e (patch) | |
| tree | 75ca1e6a099d55ba22fa74d95fd49bcb8b4b86e6 /src/theory/quantifiers/quant_relevance.h | |
| parent | 36b5281d3a4d58df5a4e68eca3d41568f1650769 (diff) | |
Initial cleaning of e-matching instantiation strategy (#5796)
In preparation for splitting this into multiple files.
No behavior changes in this PR.
Diffstat (limited to 'src/theory/quantifiers/quant_relevance.h')
| -rw-r--r-- | src/theory/quantifiers/quant_relevance.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 3396c2099..a16985d82 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -48,10 +48,7 @@ class QuantRelevance : public QuantifiersUtil /** identify */ std::string identify() const override { return "QuantRelevance"; } /** get number of quantifiers for symbol s */ - unsigned getNumQuantifiersForSymbol(Node s) - { - return d_syms_quants[s].size(); - } + size_t getNumQuantifiersForSymbol(Node s) const; private: /** map from quantifiers to symbols they contain */ |