From d5d526730d11d08c65aa17ea53d0dffb0a72e692 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 23 Mar 2021 15:41:13 -0500
Subject: Passing term registry to ematching utilities (#6190)

Model is now nested into term registry.

This PR also resolves some complications due to namespaces within quantifiers.
---
 src/theory/quantifiers_engine.h | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'src/theory/quantifiers_engine.h')

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b6562caa7..1f1dcc950 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -36,10 +36,12 @@ class DecisionManager;
 class QuantifiersModule;
 class RepSetIterator;
 
+namespace quantifiers {
+
 namespace inst {
 class TriggerTrie;
 }
-namespace quantifiers {
+
 class FirstOrderModel;
 class Instantiate;
 class QModelBuilder;
@@ -67,7 +69,6 @@ class QuantifiersEngine {
                     quantifiers::QuantifiersRegistry& qr,
                     quantifiers::TermRegistry& tr,
                     quantifiers::QuantifiersInferenceManager& qim,
-                    quantifiers::FirstOrderModel* qm,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
@@ -96,7 +97,7 @@ class QuantifiersEngine {
   /** get skolemize utility */
   quantifiers::Skolemize* getSkolemize() const;
   /** get trigger database */
-  inst::TriggerTrie* getTriggerDatabase() const;
+  quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
  private:
   //---------------------- private initialization
@@ -234,7 +235,7 @@ public:
   /** The term registry */
   quantifiers::TermRegistry& d_treg;
   /** all triggers will be stored in this trie */
-  std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+  std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   //------------- end quantifiers utilities
-- 
cgit v1.2.3