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/term_database.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/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index b2f964a3a..89d77e169 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -33,8 +33,9 @@ class QuantifiersEngine; namespace quantifiers { -class ConjectureGenerator; -class TermGenEnv; +class QuantifiersState; +class QuantifiersInferenceManager; +class QuantifiersRegistry; /** Context-dependent list of nodes */ class DbList @@ -76,6 +77,7 @@ class TermDb : public QuantifiersUtil { public: TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, QuantifiersEngine* qe); ~TermDb(); /** presolve (called once per user check-sat) */ @@ -295,6 +297,8 @@ class TermDb : public QuantifiersUtil { QuantifiersState& d_qstate; /** The quantifiers inference manager */ QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** A context for the data structures below, when not context-dependent */ context::Context d_termsContext; /** The context we are using for the data structures below */ |