diff options
Diffstat (limited to 'src/theory/quantifiers/quant_module.h')
| -rw-r--r-- | src/theory/quantifiers/quant_module.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 948f14407..d0c2d024e 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -63,6 +64,7 @@ class QuantifiersModule QuantifiersModule(quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, + quantifiers::TermRegistry& tr, QuantifiersEngine* qe); virtual ~QuantifiersModule() {} /** Presolve. @@ -169,12 +171,14 @@ class QuantifiersModule protected: /** pointer to the quantifiers engine that owns this module */ QuantifiersEngine* d_quantEngine; - /** The state of the quantifiers engine */ + /** Reference to the state of the quantifiers engine */ quantifiers::QuantifiersState& d_qstate; - /** The quantifiers inference manager */ + /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; - /** The quantifiers registry */ + /** Reference to the quantifiers registry */ quantifiers::QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + quantifiers::TermRegistry& d_treg; }; /* class QuantifiersModule */ } // namespace theory |