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_engine.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_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 99e4ad5cc..2fbf6b70f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -28,6 +28,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" @@ -77,6 +78,8 @@ class QuantifiersEngine { quantifiers::QuantifiersState& getState(); /** The quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& getInferenceManager(); + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); //---------------------- end external interface //---------------------- utilities /** get the model builder */ |