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.

1 files changed, 17 insertions, 10 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e85d6f2ff..9c56c1ba5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,11 +45,12 @@ QuantifiersEngine::QuantifiersEngine(
       d_model(nullptr),
       d_builder(nullptr),
       d_term_util(new quantifiers::TermUtil),
-      d_term_db(new quantifiers::TermDb(qstate, qim, this)),
+      d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
       d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes),
-      d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)),
+      d_instantiate(
+          new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
       d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
@@ -59,8 +60,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_presolve_cache(qstate.getUserContext())
 {
   //---- utilities
-  // term util must come before the other utilities
-  d_util.push_back(d_term_util.get());
+  // quantifiers registry must come before the other utilities
+  d_util.push_back(&d_qreg);
   d_util.push_back(d_term_db.get());
 
   if (options::sygus() || options::sygusInst())
@@ -88,17 +89,17 @@ QuantifiersEngine::QuantifiersEngine(
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, qstate, "FirstOrderModelFmc"));
+          this, qstate, d_qreg, "FirstOrderModelFmc"));
       d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model.reset(
-          new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+      d_model.reset(new quantifiers::FirstOrderModel(
+          this, qstate, d_qreg, "FirstOrderModel"));
       d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
     }
   }else{
-    d_model.reset(
-        new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+    d_model.reset(new quantifiers::FirstOrderModel(
+        this, qstate, d_qreg, "FirstOrderModel"));
   }
   d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
       qstate, d_term_db.get(), d_model.get()));
@@ -142,6 +143,12 @@ QuantifiersEngine::getInferenceManager()
 {
   return d_qim;
 }
+
+quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
+{
+  return d_qreg;
+}
+
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
   return d_builder.get();
@@ -737,7 +744,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   {
     mdl->assertNode(f);
   }
-  addTermToDatabase(d_term_util->getInstConstantBody(f), true);
+  addTermToDatabase(d_qreg.getInstConstantBody(f), true);
 }
 
 void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)