From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jan 2021 21:03:23 +0000 (-0600)
Subject: Introduce quantifiers inference manager (#5821)
X-Git-Tag: cvc5-1.0.0~2352
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c34722f830b63bc45a38217943f061912990086d;p=cvc5.git

Introduce quantifiers inference manager (#5821)

This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.

The code for adding lemmas in quantifiers engine will be migrated to this class.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1f7fc8bac..dbf00409c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -721,6 +721,8 @@ libcvc4_add_sources(
   theory/quantifiers/quant_util.h
   theory/quantifiers/quantifiers_attributes.cpp
   theory/quantifiers/quantifiers_attributes.h
+  theory/quantifiers/quantifiers_inference_manager.cpp
+  theory/quantifiers/quantifiers_inference_manager.h
   theory/quantifiers/quantifiers_modules.cpp
   theory/quantifiers/quantifiers_modules.h
   theory/quantifiers/quantifiers_rewriter.cpp
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 539dc1474..980bc1d4b 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -50,8 +50,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
 }
 
 InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
-                                     QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+                                     QuantifiersState& qs,
+                                     QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index f98ea8549..d4b78d306 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -69,7 +69,9 @@ class InstStrategyCegqi : public QuantifiersModule
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 
  public:
-  InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs);
+  InstStrategyCegqi(QuantifiersEngine* qe,
+                    QuantifiersState& qs,
+                    QuantifiersInferenceManager& qim);
   ~InstStrategyCegqi();
 
   /** whether to do counterexample-guided instantiation for quantifier q */
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 2b3bb807a..280c8c511 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,8 +86,9 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
 }
 
 ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
-                                         QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+                                         QuantifiersState& qs,
+                                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_notify(*this),
       d_uequalityEngine(
           d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 79c6f3f29..e45853e12 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -435,7 +435,9 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 
  public:
-  ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs);
+  ConjectureGenerator(QuantifiersEngine* qe,
+                      QuantifiersState& qs,
+                      QuantifiersInferenceManager& qim);
   ~ConjectureGenerator();
 
   /* needs check */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d4904ebe8..382cb233f 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -35,8 +35,9 @@ namespace theory {
 namespace quantifiers {
 
 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
-                                         QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+                                         QuantifiersState& qs,
+                                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index f22da6ec1..f5b999cea 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -48,7 +48,9 @@ class InstantiationEngine : public QuantifiersModule {
   void doInstantiationRound(Theory::Effort effort);
 
  public:
-  InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+  InstantiationEngine(QuantifiersEngine* qe,
+                      QuantifiersState& qs,
+                      QuantifiersInferenceManager& qim);
   ~InstantiationEngine();
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 51f88ad44..0f17bb04a 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -84,8 +84,10 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   return lem;
 }
 
-BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe)
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
+                                 QuantifiersState& qs,
+                                 QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index ff971bc12..685c07d82 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -161,7 +161,9 @@ private:
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
 
  public:
-  BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs);
+  BoundedIntegers(QuantifiersEngine* qe,
+                  QuantifiersState& qs,
+                  QuantifiersInferenceManager& qim);
   virtual ~BoundedIntegers();
 
   void presolve() override;
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 8803fdb2c..3849dc2c6 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -35,8 +35,10 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 //Model Engine constructor
-ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+ModelEngine::ModelEngine(QuantifiersEngine* qe,
+                         QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_incomplete_check(true),
       d_addedLemmas(0),
       d_triedLemmas(0),
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 5616eaf5e..3e212b319 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -43,7 +43,9 @@ private:
   int d_triedLemmas;
   int d_totalLemmas;
 public:
- ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+ ModelEngine(QuantifiersEngine* qe,
+             QuantifiersState& qs,
+             QuantifiersInferenceManager& qim);
  virtual ~ModelEngine();
 
 public:
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index c064819fc..1dff5e000 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -34,8 +34,9 @@ namespace quantifiers {
 
 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
                                    QuantifiersState& qs,
+                                   QuantifiersInferenceManager& qim,
                                    RelevantDomain* rd)
-    : QuantifiersModule(qs, qe), d_rd(rd), d_fullSaturateLimit(-1)
+    : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index a24aeedab..5687624db 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -64,6 +64,7 @@ class InstStrategyEnum : public QuantifiersModule
  public:
   InstStrategyEnum(QuantifiersEngine* qe,
                    QuantifiersState& qs,
+                   QuantifiersInferenceManager& qim,
                    RelevantDomain* rd);
   ~InstStrategyEnum() {}
   /** Presolve */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 23942ba7e..822c9b323 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1838,8 +1838,9 @@ bool MatchGen::isHandled( TNode n ) {
 }
 
 QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
-                                     QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+                                     QuantifiersState& qs,
+                                     QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index f90f1db18..15b3d119a 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -232,7 +232,9 @@ private:  //for equivalence classes
   bool areMatchDisequal( TNode n1, TNode n2 );
 
  public:
-  QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs);
+  QuantConflictFind(QuantifiersEngine* qe,
+                    QuantifiersState& qs,
+                    QuantifiersInferenceManager& qim);
 
   /** register quantifier */
   void registerQuantifier(Node q) override;
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 588d4de76..ad65c06cd 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -25,8 +25,10 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe), d_added_split(qs.getUserContext())
+QuantDSplit::QuantDSplit(QuantifiersEngine* qe,
+                         QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe), d_added_split(qs.getUserContext())
 {
 }
 
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 6f9e74fad..76ac1a974 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -49,7 +49,9 @@ class QuantDSplit : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs);
+  QuantDSplit(QuantifiersEngine* qe,
+              QuantifiersState& qs,
+              QuantifiersInferenceManager& qim);
   /** determine whether this quantified formula will be reduced */
   void checkOwnership(Node q) override;
   /* whether this module needs to check this round */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index cbaa8bfe6..dcf38eccb 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -23,9 +23,11 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-QuantifiersModule::QuantifiersModule(quantifiers::QuantifiersState& qs,
-                                     QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_qstate(qs)
+QuantifiersModule::QuantifiersModule(
+    quantifiers::QuantifiersState& qs,
+    quantifiers::QuantifiersInferenceManager& qim,
+    QuantifiersEngine* qe)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
 {
 }
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 240282d3d..5040bd232 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -21,6 +21,7 @@
 #include <map>
 #include <vector>
 
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -58,7 +59,9 @@ class QuantifiersModule {
   };
 
  public:
-  QuantifiersModule(quantifiers::QuantifiersState& qs, QuantifiersEngine* qe);
+  QuantifiersModule(quantifiers::QuantifiersState& qs,
+                    quantifiers::QuantifiersInferenceManager& qim,
+                    QuantifiersEngine* qe);
   virtual ~QuantifiersModule(){}
   /** Presolve.
    *
@@ -159,6 +162,8 @@ class QuantifiersModule {
   QuantifiersEngine* d_quantEngine;
   /** The state of the quantifiers engine */
   quantifiers::QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& d_qim;
 };/* class QuantifiersModule */
 
 /** Quantifiers utility
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
new file mode 100644
index 000000000..f456dd407
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file quantifiers_inference_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility for quantifiers inference manager
+ **/
+
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersInferenceManager::QuantifiersInferenceManager(
+    Theory& t, QuantifiersState& state, ProofNodeManager* pnm)
+    : InferenceManagerBuffered(t, state, pnm)
+{
+}
+
+QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
new file mode 100644
index 000000000..f89606d75
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file quantifiers_inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility for quantifiers inference manager
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+
+#include "theory/inference_manager_buffered.h"
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * The quantifiers inference manager.
+ */
+class QuantifiersInferenceManager : public InferenceManagerBuffered
+{
+ public:
+  QuantifiersInferenceManager(Theory& t,
+                              QuantifiersState& state,
+                              ProofNodeManager* pnm);
+  ~QuantifiersInferenceManager();
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 719cc3de1..573824b80 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -39,49 +39,50 @@ QuantifiersModules::QuantifiersModules()
 QuantifiersModules::~QuantifiersModules() {}
 void QuantifiersModules::initialize(QuantifiersEngine* qe,
                                     QuantifiersState& qs,
+                                    QuantifiersInferenceManager& qim,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new QuantConflictFind(qe, qs));
+    d_qcf.reset(new QuantConflictFind(qe, qs, qim));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new ConjectureGenerator(qe, qs));
+    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new InstantiationEngine(qe, qs));
+    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs));
+    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim));
     modules.push_back(d_i_cbqi.get());
     qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
   if (options::sygus())
   {
-    d_synth_e.reset(new SynthEngine(qe, qs));
+    d_synth_e.reset(new SynthEngine(qe, qs, qim));
     modules.push_back(d_synth_e.get());
   }
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new BoundedIntegers(qe, qs));
+    d_bint.reset(new BoundedIntegers(qe, qs, qim));
     modules.push_back(d_bint.get());
   }
   if (options::finiteModelFind() || options::fmfBound())
   {
-    d_model_engine.reset(new ModelEngine(qe, qs));
+    d_model_engine.reset(new ModelEngine(qe, qs, qim));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new QuantDSplit(qe, qs));
+    d_qsplit.reset(new QuantDSplit(qe, qs, qim));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAlphaEquiv())
@@ -92,12 +93,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
     d_rel_dom.reset(new RelevantDomain(qe));
-    d_fs.reset(new InstStrategyEnum(qe, qs, d_rel_dom.get()));
+    d_fs.reset(new InstStrategyEnum(qe, qs, qim, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new SygusInst(qe, qs));
+    d_sygus_inst.reset(new SygusInst(qe, qs, qim));
     modules.push_back(d_sygus_inst.get());
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 5aa8cf1d5..ba48cc68b 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -53,6 +53,7 @@ class QuantifiersModules
    */
   void initialize(QuantifiersEngine* qe,
                   QuantifiersState& qs,
+                  QuantifiersInferenceManager& qim,
                   std::vector<QuantifiersModule*>& modules);
 
  private:
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 09a6add1c..fc1bda579 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -30,8 +30,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+SynthEngine::SynthEngine(QuantifiersEngine* qe,
+                         QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_tds(qe->getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index e3cf2e47b..63175cf0c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -33,7 +33,9 @@ class SynthEngine : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  public:
-  SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+  SynthEngine(QuantifiersEngine* qe,
+              QuantifiersState& qs,
+              QuantifiersInferenceManager& qim);
   ~SynthEngine();
   /** presolve
    *
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 210ebb921..728797d85 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -46,9 +46,12 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
   return os;
 }
 
-TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs)
+TermDbSygus::TermDbSygus(QuantifiersEngine* qe,
+                         QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim)
     : d_quantEngine(qe),
       d_qstate(qs),
+      d_qim(qim),
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
       d_eval(new Evaluator),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 1bf6b6ca7..ba09c723f 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -54,7 +54,9 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
-  TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs);
+  TermDbSygus(QuantifiersEngine* qe,
+              QuantifiersState& qs,
+              QuantifiersInferenceManager& qim);
   ~TermDbSygus() {}
   /** Reset this utility */
   bool reset(Theory::Effort e);
@@ -318,6 +320,8 @@ class TermDbSygus {
   QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
 
   //------------------------------utilities
   /** sygus explanation */
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 12ce544d3..c4c722ab2 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -180,8 +180,10 @@ void addSpecialValues(
 
 }  // namespace
 
-SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+SygusInst::SygusInst(QuantifiersEngine* qe,
+                     QuantifiersState& qs,
+                     QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_ce_lemma_added(qs.getUserContext()),
       d_global_terms(qs.getUserContext()),
       d_notified_assertions(qs.getUserContext())
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 10363f5a2..4820398be 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -62,7 +62,9 @@ namespace quantifiers {
 class SygusInst : public QuantifiersModule
 {
  public:
-  SygusInst(QuantifiersEngine* qe, QuantifiersState& qs);
+  SygusInst(QuantifiersEngine* qe,
+            QuantifiersState& qs,
+            QuantifiersInferenceManager& qim);
   ~SygusInst() = default;
 
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 047a3cd41..12cdb1b8c 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -33,8 +33,13 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermDb::TermDb(QuantifiersState& qs, QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_inactive_map(qs.getSatContext())
+TermDb::TermDb(QuantifiersState& qs,
+               QuantifiersInferenceManager& qim,
+               QuantifiersEngine* qe)
+    : d_quantEngine(qe),
+      d_qstate(qs),
+      d_qim(qim),
+      d_inactive_map(qs.getSatContext())
 {
   d_consistent_ee = true;
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index afb8d0c0c..c246ea6fc 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -76,7 +76,9 @@ class TermDb : public QuantifiersUtil {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  public:
-  TermDb(QuantifiersState& qs, QuantifiersEngine* qe);
+  TermDb(QuantifiersState& qs,
+         QuantifiersInferenceManager& qim,
+         QuantifiersEngine* qe);
   ~TermDb();
   /** presolve (called once per user check-sat) */
   void presolve();
@@ -303,6 +305,10 @@ class TermDb : public QuantifiersUtil {
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
+  /** The quantifiers state object */
+  QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** terms processed */
   std::unordered_set< Node, NodeHashFunction > d_processed;
   /** terms processed */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 808c88b78..d01d6a83f 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -36,7 +36,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermUtil::TermUtil(QuantifiersEngine* qe) : d_quantEngine(qe)
+TermUtil::TermUtil()
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index fb982eea8..4033c888f 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -70,11 +70,8 @@ class TermUtil : public QuantifiersUtil
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class Instantiate;
 
- private:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
-public:
-  TermUtil(QuantifiersEngine * qe);
+ public:
+  TermUtil();
   ~TermUtil();
   /** boolean terms */
   Node d_true;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index aaf8f347c..4dd59d12f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -44,7 +44,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
                                      ProofNodeManager* pnm)
     : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
       d_qstate(c, u, valuation),
-      d_qengine(d_qstate, pnm)
+      d_qim(*this, d_qstate, pnm),
+      d_qengine(d_qstate, d_qim, pnm)
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute("qid", this);
@@ -60,6 +61,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   }
   // indicate we are using the quantifiers theory state object
   d_theoryState = &d_qstate;
+  // use the inference manager as the official inference manager
+  d_inferManager = &d_qim;
 
   // Set the pointer to the quantifiers engine, which this theory owns. This
   // pointer will be retreived by TheoryEngine and set to all theories
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 82a588009..8d2366065 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -21,6 +21,7 @@
 
 #include "expr/node.h"
 #include "theory/quantifiers/proof_checker.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
@@ -81,6 +82,8 @@ class TheoryQuantifiers : public Theory {
   QuantifiersProofRuleChecker d_qChecker;
   /** The quantifiers state */
   QuantifiersState d_qstate;
+  /** The quantifiers inference manager */
+  QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
   QuantifiersEngine d_qengine;
 };/* class TheoryQuantifiers */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f60bb724f..fa7e50e1c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,9 +30,12 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate,
-                                     ProofNodeManager* pnm)
+QuantifiersEngine::QuantifiersEngine(
+    quantifiers::QuantifiersState& qstate,
+    quantifiers::QuantifiersInferenceManager& qim,
+    ProofNodeManager* pnm)
     : d_qstate(qstate),
+      d_qim(qim),
       d_te(nullptr),
       d_decManager(nullptr),
       d_masterEqualityEngine(nullptr),
@@ -40,9 +43,9 @@ QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate,
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
-      d_term_util(new quantifiers::TermUtil(this)),
+      d_term_util(new quantifiers::TermUtil),
       d_term_canon(new expr::TermCanonize),
-      d_term_db(new quantifiers::TermDb(qstate, this)),
+      d_term_db(new quantifiers::TermDb(qstate, qim, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
@@ -68,7 +71,7 @@ QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate,
   if (options::sygus() || options::sygusInst())
   {
     // must be constructed here since it is required for datatypes finistInit
-    d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate));
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate, qim));
   }
 
   d_util.push_back(d_instantiate.get());
@@ -128,7 +131,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te,
   d_masterEqualityEngine = mee;
   // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(this, d_qstate, d_modules);
+  d_qmodules->initialize(this, d_qstate, d_qim, d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7ed183342..5a371ff09 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -61,6 +62,7 @@ class QuantifiersEngine {
 
  public:
   QuantifiersEngine(quantifiers::QuantifiersState& qstate,
+                    quantifiers::QuantifiersInferenceManager& qim,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
@@ -337,6 +339,8 @@ public:
  private:
   /** The quantifiers state object */
   quantifiers::QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& d_qim;
   /** Pointer to theory engine object */
   TheoryEngine* d_te;
   /** Reference to the decision manager of the theory engine */