diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 13:34:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 13:34:54 -0600 |
commit | 0f03dbb1378354adcfef635a93f8b13987c2d983 (patch) | |
tree | 6c6dcc0e806b0867d19d01cb045a5a50764bf0e0 /src/theory/quantifiers/relevant_domain.h | |
parent | d107bf9b8b4dd206580681e601a033742029ec79 (diff) |
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.h')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 36364191c..68ffbefe5 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -24,6 +24,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class QuantifiersRegistry; + /** Relevant Domain * * This class computes the relevant domain of @@ -40,7 +42,7 @@ namespace quantifiers { class RelevantDomain : public QuantifiersUtil { public: - RelevantDomain(QuantifiersEngine* qe); + RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr); virtual ~RelevantDomain(); /** Reset. */ bool reset(Theory::Effort e) override; @@ -117,6 +119,8 @@ class RelevantDomain : public QuantifiersUtil std::map< RDomain *, int > d_ri_map; /** Quantifiers engine associated with this utility. */ QuantifiersEngine* d_qe; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** have we computed the relevant domain on this full effort check? */ bool d_is_computed; /** relevant domain literal |