Connect the shared solver to theory engine (#5103)

This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.

It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.

This PR has no intended behavior changes.

FYI @barrettcw

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index d972a4d8e1de937bd6ec78023aa111ea77af9733..32af150547356f324669554f16d0ef8df3628143 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/care_graph.h"
 #include "theory/ee_manager_distributed.h"
 #include "theory/model_manager_distributed.h"
+#include "theory/shared_solver_distributed.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
@@ -31,6 +32,7 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
       d_mmanager(nullptr),
+      d_sharedSolver(nullptr),
       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
                    : nullptr)
 {
@@ -43,8 +45,11 @@ void CombinationEngine::finishInit()
   // create the equality engine, model manager, and shared solver
   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
   {
+    // use the distributed shared solver
+    d_sharedSolver.reset(new SharedSolverDistributed(d_te));
     // make the distributed equality engine manager
-    d_eemanager.reset(new EqEngineManagerDistributed(d_te));
+    d_eemanager.reset(
+        new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
     // make the distributed model manager
     d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
   }
@@ -95,6 +100,10 @@ theory::TheoryModel* CombinationEngine::getModel()
   return d_mmanager->getModel();
 }
 
+SharedSolver* CombinationEngine::getSharedSolver()
+{
+  return d_sharedSolver.get();
+}
 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
 
 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()

diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 886bdc71d1208c2a889fe9e095f8b29904288a2f..daafc1f67d55a98e91c495bcab30888192a34f42 100644 (file)
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -23,6 +23,7 @@
 #include "theory/eager_proof_generator.h"
 #include "theory/ee_manager.h"
 #include "theory/model_manager.h"
+#include "theory/shared_solver.h"
 
 namespace CVC4 {
 
@@ -82,6 +83,11 @@ class CombinationEngine
    */
   TheoryModel* getModel();
   //-------------------------- end model
+  /**
+   * Get the shared solver, which is the active component of theory combination
+   * that TheoryEngine interacts with prior to calling combineTheories.
+   */
+  SharedSolver* getSharedSolver();
   /**
    * Called at the beginning of full effort
    */
@@ -119,6 +125,11 @@ class CombinationEngine
    * model.
    */
   std::unique_ptr<ModelManager> d_mmanager;
+  /**
+   * The shared solver. This class is responsible for performing combination
+   * tasks (e.g. preregistration) during solving.
+   */
+  std::unique_ptr<SharedSolver> d_sharedSolver;
   /**
    * An eager proof generator, if proofs are enabled. This proof generator is
    * responsible for proofs of splitting lemmas generated in combineTheories.

diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp
index e473388f0dfd7686c9925f8354d64464f14fd1f5..697689fb918f4a0024df2c14784800f6dea445f2 100644 (file)
--- a/src/theory/ee_manager.cpp
+++ b/src/theory/ee_manager.cpp
@@ -19,7 +19,10 @@
 namespace CVC4 {
 namespace theory {
 
-EqEngineManager::EqEngineManager(TheoryEngine& te) : d_te(te) {}
+EqEngineManager::EqEngineManager(TheoryEngine& te, SharedSolver& shs)
+    : d_te(te), d_sharedSolver(shs)
+{
+}
 
 const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const
 {

diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h
index 8d65eb2f12fa9b4d122a14940ae71e728f3c6daf..6e40ceb7bdd5fcb23c362939f8a4096f9c2e83ea 100644 (file)
--- a/src/theory/ee_manager.h
+++ b/src/theory/ee_manager.h
@@ -30,6 +30,8 @@ class TheoryEngine;
 
 namespace theory {
 
+class SharedSolver;
+
 /**
  * This is (theory-agnostic) information associated with the management of
  * an equality engine for a single theory. This information is maintained
@@ -51,7 +53,12 @@ struct EeTheoryInfo
 class EqEngineManager
 {
  public:
-  EqEngineManager(TheoryEngine& te);
+   /**
+   * @param te Reference to the theory engine
+   * @param sharedSolver The shared solver that is being used in combination
+   * with this equality engine manager
+    */
+  EqEngineManager(TheoryEngine& te, SharedSolver& shs);
   virtual ~EqEngineManager() {}
   /**
    * Initialize theories, called during TheoryEngine::finishInit after theory
@@ -81,6 +88,8 @@ class EqEngineManager
  protected:
   /** Reference to the theory engine */
   TheoryEngine& d_te;
+  /** Reference to the shared solver */
+  SharedSolver& d_sharedSolver;
   /** Information related to the equality engine, per theory. */
   std::map<TheoryId, EeTheoryInfo> d_einfo;
 };

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 6f6eeb7e716583e31574709fe35cec74f68fa7b7..360b1257bda14c067371b2d2e466c48edf5ecf66 100644 (file)
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -15,13 +15,15 @@
 #include "theory/ee_manager_distributed.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/shared_solver.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te)
-    : EqEngineManager(te), d_masterEENotify(nullptr)
+EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te,
+                                                       SharedSolver& shs)
+    : EqEngineManager(te, shs), d_masterEENotify(nullptr)
 {
 }
 

diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index c233216ea79fca4e2bfac0fad4f39e2256ff0241..90beb0d3b67a6c799d2cc024694875f04fddbfae 100644 (file)
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -45,7 +45,7 @@ namespace theory {
 class EqEngineManagerDistributed : public EqEngineManager
 {
  public:
-  EqEngineManagerDistributed(TheoryEngine& te);
+  EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs);
   ~EqEngineManagerDistributed();
   /**
    * Initialize theories. This method allocates unique equality engines

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a425441fd837bb611f73c2fecf98c6b052c1b05c..47dca7d669ee92135900be4a4b37fa9bf7833af8 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -174,6 +174,8 @@ void TheoryEngine::finishInit() {
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.
   d_tc->finishInit();
+  // get pointer to the shared solver
+  d_sharedSolver = d_tc->getSharedSolver();
 
   // set the core equality engine on quantifiers engine
   if (d_logicInfo.isQuantified())
@@ -223,17 +225,17 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_outMgr(outMgr),
       d_pnm(nullptr),
       d_lazyProof(
-          d_pnm != nullptr ? new LazyCDProof(
-              d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
-                           : nullptr),
+          d_pnm != nullptr
+              ? new LazyCDProof(
+                    d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+              : nullptr),
       d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
-      d_sharedTerms(this, context),
       d_tc(nullptr),
+      d_sharedSolver(nullptr),
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(userContext)),
       d_relManager(nullptr),
       d_preRegistrationVisitor(this, context),
-      d_sharedTermsVisitor(d_sharedTerms),
       d_eager_model_building(false),
       d_inConflict(context, false),
       d_inSatMode(false),
@@ -301,11 +303,6 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       preprocessed = d_preregisterQueue.front();
       d_preregisterQueue.pop();
 
-      if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
-        // When sharing is enabled, we propagate from the shared terms manager also
-        d_sharedTerms.addEqualityToPropagate(preprocessed);
-      }
-
       // the atom should not have free variables
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
@@ -347,11 +344,11 @@ void TheoryEngine::preRegister(TNode preprocessed) {
           }
         }
       }
-      if (multipleTheories) {
-        // Collect the shared terms if there are multiple theories
-        NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor,
-                                             preprocessed);
-      }
+
+      // pre-register with the shared solver, which also handles
+      // calling prepregister on individual theories.
+      Assert(d_sharedSolver != nullptr);
+      d_sharedSolver->preRegisterShared(preprocessed, multipleTheories);
     }
 
     // Leaving pre-register
@@ -961,7 +958,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     Assert(atom.getKind() == kind::EQUAL)
         << "atom should be an EQUALity, not `" << atom << "'";
     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
-      d_sharedTerms.assertEquality(atom, polarity, assertion);
+      // assert to the shared solver
+      d_sharedSolver->assertSharedEquality(atom, polarity, assertion);
     }
     return;
   }
@@ -1052,23 +1050,7 @@ void TheoryEngine::assertFact(TNode literal)
 
   if (d_logicInfo.isSharingEnabled()) {
     // If any shared terms, it's time to do sharing work
-    if (d_sharedTerms.hasSharedTerms(atom)) {
-      // Notify the theories the shared terms
-      SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
-      SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
-      for (; it != it_end; ++ it) {
-        TNode term = *it;
-        theory::TheoryIdSet theories =
-            d_sharedTerms.getTheoriesToNotify(atom, term);
-        for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
-          if (TheoryIdSetUtil::setContains(id, theories))
-          {
-            theoryOf(id)->addSharedTerm(term);
-          }
-        }
-        d_sharedTerms.markNotified(term, theories);
-      }
-    }
+    d_sharedSolver->preNotifySharedFact(atom);
 
     // If it's an equality, assert it to the shared term manager, even though the terms are not
     // yet shared. As the terms become shared later, the shared terms manager will then add them
@@ -1136,15 +1118,7 @@ const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType().isComparableTo(b.getType()));
-  if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
-    if (d_sharedTerms.areEqual(a,b)) {
-      return EQUALITY_TRUE_AND_PROPAGATED;
-    }
-    else if (d_sharedTerms.areDisequal(a,b)) {
-      return EQUALITY_FALSE_AND_PROPAGATED;
-    }
-  }
-  return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+  return d_sharedSolver->getEqualityStatus(a, b);
 }
 
 Node TheoryEngine::getModelValue(TNode var) {
@@ -1153,7 +1127,7 @@ Node TheoryEngine::getModelValue(TNode var) {
     // the model value of a constant must be itself
     return var;
   }
-  Assert(d_sharedTerms.isShared(var));
+  Assert(d_sharedSolver->isShared(var));
   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
 }
 
@@ -1768,20 +1742,9 @@ theory::TrustNode TheoryEngine::getExplanation(
       }
     }
 
-    Node explanation;
-    if (toExplain.d_theory == THEORY_BUILTIN)
-    {
-      explanation = d_sharedTerms.explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
-    }
-    else
-    {
-      TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
-      explanation = texp.getNode();
-      Debug("theory::explain") << "\tTerm was propagated by owner theory: "
-                               << theoryOf(toExplain.d_theory)->getId()
-                               << ". Explanation: " << explanation << std::endl;
-    }
+    TrustNode texp =
+        d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
+    Node explanation = texp.getNode();
 
     Debug("theory::explain")
         << "TheoryEngine::explain(): got explanation " << explanation

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7639afdbf7747b553655285adec42d658c328fd0..cfca03515fc2821b529ced4c128da1f989f0cacb 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -154,14 +154,10 @@ class TheoryEngine {
   /** The proof generator */
   std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
   //--------------------------------- end new proofs
-
-  /**
-   * The database of shared terms.
-   */
-  SharedTermsDatabase d_sharedTerms;
-
   /** The combination manager we are using */
   std::unique_ptr<theory::CombinationEngine> d_tc;
+  /** The shared solver of the above combination engine. */
+  theory::SharedSolver* d_sharedSolver;
   /**
    * The quantifiers engine
    */
@@ -176,9 +172,6 @@ class TheoryEngine {
   /** Default visitor for pre-registration */
   PreRegisterVisitor d_preRegistrationVisitor;
 
-  /** Visitor for collecting shared terms */
-  SharedTermsVisitor d_sharedTermsVisitor;
-
   /** are we in eager model building mode? (see setEagerModelBuilding). */
   bool d_eager_model_building;