Add the shared solver (#4982)

This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine.

In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase.

In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral).

FYI @barrettcw

7 files changed, 433 insertions, 0 deletions

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
new file mode 100644
index 000000000..794d3ca7c
--- /dev/null
+++ b/src/theory/shared_solver.cpp
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file shared_solver.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 The shared solver base class
+ **/
+
+#include "theory/shared_solver.h"
+
+#include "expr/node_visitor.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+// Always creates shared terms database. In all cases, shared terms
+// database is used as a way of tracking which calls to Theory::addSharedTerm
+// we need to make in preNotifySharedFact.
+// In distributed equality engine management, shared terms database also
+// maintains an equality engine. In central equality engine management,
+// it does not.
+SharedSolver::SharedSolver(TheoryEngine& te)
+    : d_te(te),
+      d_logicInfo(te.getLogicInfo()),
+      d_sharedTerms(&d_te, d_te.getSatContext()),
+      d_sharedTermsVisitor(d_sharedTerms)
+{
+}
+
+bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi)
+{
+  return false;
+}
+
+void SharedSolver::preRegisterShared(TNode t, bool multipleTheories)
+{
+  // register it with the equality engine manager if sharing is enabled
+  if (d_logicInfo.isSharingEnabled())
+  {
+    preRegisterSharedInternal(t);
+  }
+  // if multiple theories are present in t
+  if (multipleTheories)
+  {
+    // Collect the shared terms if there are multiple theories
+    // This calls Theory::addSharedTerm, possibly multiple times
+    NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, t);
+  }
+}
+
+void SharedSolver::preNotifySharedFact(TNode atom)
+{
+  if (d_sharedTerms.hasSharedTerms(atom))
+  {
+    // Always notify the theories of the shared terms, which is independent of
+    // the architecture currently.
+    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;
+      TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term);
+      for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
+      {
+        if (TheoryIdSetUtil::setContains(id, theories))
+        {
+          Theory* t = d_te.theoryOf(id);
+          // call the add shared term method
+          t->addSharedTerm(term);
+        }
+      }
+      d_sharedTerms.markNotified(term, theories);
+    }
+  }
+}
+
+EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b)
+{
+  return EQUALITY_UNKNOWN;
+}
+
+void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
+{
+  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
+}
+
+bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
+                                           TNode a,
+                                           TNode b,
+                                           bool value)
+{
+  // Propagate equality between shared terms to the one who asked for it
+  Node equality = a.eqNode(b);
+  if (value)
+  {
+    d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN);
+  }
+  else
+  {
+    d_te.assertToTheory(
+        equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
+  }
+  return true;
+}
+
+bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
new file mode 100644
index 000000000..d3604faca
--- /dev/null
+++ b/src/theory/shared_solver.h
@@ -0,0 +1,133 @@
+/*********************                                                        */
+/*! \file shared_solver.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 Base class for shared solver
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SHARED_SOLVER__H
+#define CVC4__THEORY__SHARED_SOLVER__H
+
+#include "expr/node.h"
+#include "theory/ee_setup_info.h"
+#include "theory/logic_info.h"
+#include "theory/shared_terms_database.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+/**
+ * A base class for shared solver. The shared solver is the component of theory
+ * engine that behaves like a theory solver, and whose purpose is to ensure the
+ * main theory combination method can be performed in CombinationEngine.
+ * Its role is to:
+ * (1) Notify the individual theories of shared terms via addSharedTerms,
+ * (2) Be the official interface for equality statuses,
+ * (3) Propagate equalities to TheoryEngine when necessary and explain them.
+ */
+class SharedSolver
+{
+ public:
+  SharedSolver(TheoryEngine& te);
+  virtual ~SharedSolver() {}
+  //------------------------------------- initialization
+  /**
+   * Returns true if we need an equality engine, this has the same contract
+   * as Theory::needsEqualityEngine.
+   */
+  virtual bool needsEqualityEngine(theory::EeSetupInfo& esi);
+  /**
+   * Set the equality engine. This should be called by equality engine manager
+   * during EqEngineManager::initializeTheories.
+   */
+  virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0;
+  //------------------------------------- end initialization
+  /**
+   * Called when the given term t is pre-registered in TheoryEngine.
+   *
+   * This adds t as an equality to propagate in the shared terms database
+   * if it is an equality, or adds its shared terms if it involves multiple
+   * theories.
+   *
+   * @param t The term to preregister
+   * @param multipleTheories Whether multiple theories are present in t.
+   */
+  void preRegisterShared(TNode t, bool multipleTheories);
+  /**
+   * Pre-notify assertion fact with the given atom. This is called when any
+   * fact is asserted in TheoryEngine, just before it is dispatched to the
+   * appropriate theory.
+   *
+   * This calls Theory::notifySharedTerm for the shared terms of the atom.
+   */
+  void preNotifySharedFact(TNode atom);
+  /**
+   * Get the equality status of a and b.
+   *
+   * This method is used by theories via Valuation mostly for determining their
+   * care graph.
+   */
+  virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
+  /**
+   * Explain literal, which returns a conjunction of literals that entail
+   * the given one.
+   */
+  virtual TrustNode explain(TNode literal, TheoryId id) = 0;
+  /**
+   * Assert equality to the shared terms database.
+   *
+   * This method is called by TheoryEngine when a fact has been marked to
+   * send to THEORY_BUILTIN, meaning that shared terms database should
+   * maintain this fact. This is the case when either an equality is
+   * asserted from the SAT solver or a theory propagates an equality between
+   * shared terms.
+   */
+  virtual void assertSharedEquality(TNode equality,
+                                    bool polarity,
+                                    TNode reason) = 0;
+  /** Is term t a shared term? */
+  virtual bool isShared(TNode t) const;
+
+  /**
+   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b
+   * are shared with the theory. Returns false if there is a direct conflict
+   * (via rewrite for example).
+   */
+  bool propagateSharedEquality(theory::TheoryId theory,
+                               TNode a,
+                               TNode b,
+                               bool value);
+  /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
+  void sendLemma(TrustNode trn, TheoryId atomsTo);
+
+ protected:
+  /** Solver-specific pre-register shared */
+  virtual void preRegisterSharedInternal(TNode t) = 0;
+  /** Reference to the theory engine */
+  TheoryEngine& d_te;
+  /** Logic info of theory engine (cached) */
+  const LogicInfo& d_logicInfo;
+  /** The database of shared terms.*/
+  SharedTermsDatabase d_sharedTerms;
+  /** Visitor for collecting shared terms */
+  SharedTermsVisitor d_sharedTermsVisitor;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SHARED_SOLVER__H */
diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
new file mode 100644
index 000000000..873c81db1
--- /dev/null
+++ b/src/theory/shared_solver_distributed.cpp
@@ -0,0 +1,95 @@
+/*********************                                                        */
+/*! \file shared_solver_distributed.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 Shared solver in the distributed architecture
+ **/
+
+#include "theory/shared_solver_distributed.h"
+
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te)
+    : SharedSolver(te)
+{
+}
+
+bool SharedSolverDistributed::needsEqualityEngine(theory::EeSetupInfo& esi)
+{
+  return d_sharedTerms.needsEqualityEngine(esi);
+}
+
+void SharedSolverDistributed::setEqualityEngine(eq::EqualityEngine* ee)
+{
+  d_sharedTerms.setEqualityEngine(ee);
+}
+
+void SharedSolverDistributed::preRegisterSharedInternal(TNode t)
+{
+  if (t.getKind() == kind::EQUAL)
+  {
+    // When sharing is enabled, we propagate from the shared terms manager also
+    d_sharedTerms.addEqualityToPropagate(t);
+  }
+}
+
+EqualityStatus SharedSolverDistributed::getEqualityStatus(TNode a, TNode b)
+{
+  // if we're using a shared terms database, ask its status if a and b are
+  // shared.
+  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;
+    }
+  }
+  // otherwise, ask the theory
+  return d_te.theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+}
+
+TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id)
+{
+  TrustNode texp;
+  if (id == THEORY_BUILTIN)
+  {
+    // explanation using the shared terms database
+    Node exp = d_sharedTerms.explain(literal);
+    texp = TrustNode::mkTrustPropExp(literal, exp, nullptr);
+    Trace("shared-solver")
+        << "\tTerm was propagated by THEORY_BUILTIN. Explanation: "
+        << texp.getNode() << std::endl;
+  }
+  else
+  {
+    // By default, we ask the individual theory for the explanation.
+    texp = d_te.theoryOf(id)->explain(literal);
+    Trace("shared-solver") << "\tTerm was propagated by owner theory: " << id
+                           << ". Explanation: " << texp.getNode() << std::endl;
+  }
+  return texp;
+}
+
+void SharedSolverDistributed::assertSharedEquality(TNode equality,
+                                                   bool polarity,
+                                                   TNode reason)
+{
+  d_sharedTerms.assertEquality(equality, polarity, reason);
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h
new file mode 100644
index 000000000..45c7eafb3
--- /dev/null
+++ b/src/theory/shared_solver_distributed.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file shared_solver_distributed.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 Shared solver in the distributed architecture.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
+#define CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
+
+#include "expr/node.h"
+#include "theory/shared_solver.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * The shared solver in the distributed architecture. This class uses the
+ * SharedTermsDatabase for implementing the core methods of a shared solver.
+ */
+class SharedSolverDistributed : public SharedSolver
+{
+ public:
+  SharedSolverDistributed(TheoryEngine& te);
+  virtual ~SharedSolverDistributed() {}
+  //------------------------------------- initialization
+  /**
+   * Returns true if we need an equality engine, this has the same contract
+   * as Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(theory::EeSetupInfo& esi) override;
+  /** Set equality engine in the shared terms database */
+  void setEqualityEngine(eq::EqualityEngine* ee) override;
+  //------------------------------------- end initialization
+  /** Assert equality to the shared terms database. */
+  void assertSharedEquality(TNode equality,
+                            bool polarity,
+                            TNode reason) override;
+  /**
+   * Get equality status based on the equality engine of shared terms database
+   */
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  /** Explain literal that was propagated by a theory or using shared terms
+   * database */
+  TrustNode explain(TNode literal, TheoryId id) override;
+
+ protected:
+  /** If t is an equality, add it as one that may be propagated */
+  void preRegisterSharedInternal(TNode t) override;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H */
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index b01cef377..034401b9a 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -44,6 +44,18 @@ SharedTermsDatabase::~SharedTermsDatabase()
   smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
 }
 
+void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
+{
+  // TODO (project #39): dynamic allocation of equality engine here
+}
+
+bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_EENotify;
+  esi.d_name = "SharedTermsDatabase";
+  return true;
+}
+
 void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
   d_registeredEqualities.insert(equality);
   d_equalityEngine.addTriggerPredicate(equality);
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index ca4f6c183..1a50224e1 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "theory/ee_setup_info.h"
 #include "theory/theory_id.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
@@ -158,6 +159,16 @@ public:
   SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
   ~SharedTermsDatabase();
 
+  //-------------------------------------------- initialization
+  /** Called to set the equality engine. */
+  void setEqualityEngine(theory::eq::EqualityEngine* ee);
+  /**
+   * Returns true if we need an equality engine, this has the same contract
+   * as Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(theory::EeSetupInfo& esi);
+  //-------------------------------------------- end initialization
+
   /**
    * Asserts the equality to the shared terms database,
    */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a6258b7d6..fda32206b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -87,6 +87,7 @@ struct NodeTheoryPairHashFunction {
 namespace theory {
 class TheoryModel;
 class CombinationEngine;
+class SharedSolver;
 class DecisionManager;
 class RelevanceManager;
 
@@ -113,6 +114,7 @@ class TheoryEngine {
   friend class theory::CombinationEngine;
   friend class theory::EngineOutputChannel;
   friend class theory::CombinationEngine;
+  friend class theory::SharedSolver;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;