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 1f7fc8bac2c38970532a951c681b75a7381cc511..dbf00409cb9a65f98451e9d9ec2e7152296f1153 100644 (file)
--- 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 539dc1474da15c8c52604695675f09d191070213..980bc1d4b0b759988d8abc44fbcc3d16f93718e7 100644 (file)
--- 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 f98ea8549ccdb07e1ab8193a285f66d94112a04d..d4b78d3068f117dee5f0f07a05a28d280919b8ec 100644 (file)
--- 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 2b3bb807afea0e0e12948bccceed727fcc219399..280c8c511ba2977fd50408bd949f3817adec19a5 100644 (file)
--- 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 79c6f3f29fb1a6e84132382a87ebb6c201889fe5..e45853e121ca12a71b9275db3a21c2acf3cc90d2 100644 (file)
--- 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 d4904ebe8696626b4993b038098751544856acf4..382cb233f462f1eba75c7b809c1808d970764ab8 100644 (file)
--- 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 f22da6ec17350b54f2cbb0b906a818c05c78952b..f5b999ceaba9f69933d0ce7de0af61fd345ff2e0 100644 (file)
--- 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 51f88ad449f7552302b75c554931dcda965e38c3..0f17bb04a4711362f7da308b61106ff56de30b63 100644 (file)
--- 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 ff971bc12b0eb4a15114898474e37a58c1a46cbc..685c07d82234aedbbe063ba268e389433d4339c8 100644 (file)
--- 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 8803fdb2c1704520596025ce8590a095c45e5d67..3849dc2c657a7f621e51528d5cba27f6fe516bdf 100644 (file)
--- 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 5616eaf5e51b3fc925bcbdda1ef9817b219e4cc0..3e212b3192e3b1b67ff0e4155fa7bab4781b59c2 100644 (file)
--- 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 c064819fca6029a209c7b22e59a6d7cb0ae76390..1dff5e00029f4628cd8b89e3d6172ccf1f342002 100644 (file)
--- 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 a24aeedabfef6304416ba73ed5c4521aaa13d1b5..5687624db3074ba28cf63fb2b7cf9e1b683484d2 100644 (file)
--- 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 23942ba7e3b98a124f4f96ffa265788bf9d01558..822c9b3233b3d71864d583323d57aaa969c3a3c2 100644 (file)
--- 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 f90f1db18321e141b39cbef503d7e49622d9bc3c..15b3d119a0761727b0dcaf755ae90b6c8eb63ee3 100644 (file)
--- 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 588d4de7663118b5559a3c7c045c56df193d7bb9..ad65c06cdfaa44098f561837a9afcbba262ac644 100644 (file)
--- 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 6f9e74fadbaa87dcec5d382648bac4928eaf93a7..76ac1a974fb1f6608b91875009b10cc178308e25 100644 (file)
--- 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 cbaa8bfe6a01cd959e8f021a4d9393ef0626b7ae..dcf38eccb1da177c49496635208718273b591ffb 100644 (file)
--- 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 240282d3d22231917ba0ac4f198b7b559ad15431..5040bd2323184b085ac7b9b45bef16e919859623 100644 (file)
--- 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 (file)
index 0000000..f456dd4
--- /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 (file)
index 0000000..f89606d
--- /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 719cc3de1c1ace052928c7f14374b653c515ea86..573824b80bcdb89739bdfa69be7b800b7944a639 100644 (file)
--- 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 5aa8cf1d50f45ce004172e4b3940846ec07e4a36..ba48cc68b0ca1b5d5d0a31b7bf2ef22df4c963db 100644 (file)
--- 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 09a6add1caf3f18dc7a8409e4feee85b78c01fc8..fc1bda5794ac341583a606e9889c6952f4a46906 100644 (file)
--- 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 e3cf2e47b4d4a4333be90edf364a2bd2be1b87aa..63175cf0cd0ec5e5a0b2f514a26542c69b004fe4 100644 (file)
--- 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 210ebb921a4dc6bd6d6953d9446f1169ab7ca3b8..728797d85e6ec84fe1f199717580f54cf20e4875 100644 (file)
--- 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 1bf6b6ca7e44b793eb26dcb1b4066ea16fccd819..ba09c723f9de41f86f3af2c8add047e123256bf7 100644 (file)
--- 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 12ce544d3b7aa1822b664cb0108efc5a39e74dd8..c4c722ab253fa6dc9a6ea9488853593f7976381c 100644 (file)
--- 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 10363f5a2d9cba145a803e73210323bba4db6311..4820398be3afb1e669301a64cb808a2dbec7f559 100644 (file)
--- 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 047a3cd41ffcebee0773ae8f904caf622b1ad927..12cdb1b8c8193ba2282c467f03a8f77e0e1c8c61 100644 (file)
--- 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 afb8d0c0c14aecdca15a2034daa136ef72e8296f..c246ea6fce39606b484c661dd9a69d77c80a18ac 100644 (file)
--- 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 808c88b7806262f02278a3f38d7102f88fe8dfe9..d01d6a83f4ebd6facf50b1183a25d29fae057230 100644 (file)
--- 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 fb982eea8e352f5ce80a1e2da0e012ffb1b211b8..4033c888ff6a70e2da450ca259becb603c8e30cf 100644 (file)
--- 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 aaf8f347c3987cc166e951feda11aa584d2838d1..4dd59d12fd7fb825e5b15d2453af4168929cb8fc 100644 (file)
--- 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 82a5880090c5cfc581a37bdebbabe9b92cddb6b9..8d236606526b102abb4ee5b0a44db621237146e2 100644 (file)
--- 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 f60bb724f241dc36e8fc8f787a85ad1c5f4a8263..fa7e50e1cecfd25e80f518ca720310754ded2a83 100644 (file)
--- 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 7ed183342c00945d9dcb06d94bbbf2c80cd10625..5a371ff09e0c61db58c1d2954027dd54c4b03633 100644 (file)
--- 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 */