summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h3
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback