Minor updates to shared terms database for central equality engine (#6929)

Includes proper set up of the proof equality engine it uses (which may be shared over multiple theories). Also makes its assertEquality method robust to non-equality atoms.

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index 4786d6fc9776861d21b24c874970713bcb9bb076..e2cda0fbc927624a4e038172e66a7399dd7e18ce 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -95,17 +95,15 @@ class SharedSolver
    */
   virtual TrustNode explain(TNode literal, TheoryId id) = 0;
   /**
-   * Assert equality to the shared terms database.
+   * Assert n 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.
+   * maintain this fact. In the distributed equality engine architecture,
+   * 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;
+  virtual void assertShared(TNode n, bool polarity, TNode reason) = 0;
   /** Is term t a shared term? */
   virtual bool isShared(TNode t) const;
 

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 58a5b4f6c9978e5232c993acc80986a9ddc4b645..3c78a75f897944c37bf4a09f783948e8114dc7f8 100644 (file)
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -86,11 +86,9 @@ TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id)
   return texp;
 }
 
-void SharedSolverDistributed::assertSharedEquality(TNode equality,
-                                                   bool polarity,
-                                                   TNode reason)
+void SharedSolverDistributed::assertShared(TNode n, bool polarity, TNode reason)
 {
-  d_sharedTerms.assertEquality(equality, polarity, reason);
+  d_sharedTerms.assertShared(n, polarity, reason);
 }
 
 }  // namespace theory

diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h
index dab1902641a0461f5ddb6e7043f8e1135cd47229..f9a00230ba16504d3f116b9093940d4e59e45bbc 100644 (file)
--- a/src/theory/shared_solver_distributed.h
+++ b/src/theory/shared_solver_distributed.h
@@ -42,10 +42,8 @@ class SharedSolverDistributed : public SharedSolver
   /** 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;
+  /** Assert n to the shared terms database. */
+  void assertShared(TNode n, bool polarity, TNode reason) override;
   /**
    * Get equality status based on the equality engine of shared terms database
    */

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 0e17f50a96d8ea1a64e1ec3d0a04a5946a5235ad..a4a846e053ae63671768b2cdd42e1b6b130a6b9b 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -51,18 +51,24 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
 {
   Assert(ee != nullptr);
   d_equalityEngine = ee;
-  // if proofs are enabled, make the proof equality engine
+  // if proofs are enabled, make the proof equality engine if necessary
   if (d_pnm != nullptr)
   {
-    d_pfee.reset(
-        new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
+    d_pfee = d_equalityEngine->getProofEqualityEngine();
+    if (d_pfee == nullptr)
+    {
+      d_pfeeAlloc.reset(
+          new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
+      d_pfee = d_pfeeAlloc.get();
+      d_equalityEngine->setProofEqualityEngine(d_pfee);
+    }
   }
 }
 
 bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_EENotify;
-  esi.d_name = "SharedTermsDatabase";
+  esi.d_name = "shared::ee";
   return true;
 }
 
@@ -243,12 +249,21 @@ theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
   return d_equalityEngine;
 }
 
-void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason)
+void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
 {
   Assert(d_equalityEngine != nullptr);
-  Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
+  Debug("shared-terms-database::assert")
+      << "SharedTermsDatabase::assertShared(" << n << ", "
+      << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
   // Add it to the equality engine
-  d_equalityEngine->assertEquality(equality, polarity, reason);
+  if (n.getKind() == kind::EQUAL)
+  {
+    d_equalityEngine->assertEquality(n, polarity, reason);
+  }
+  else
+  {
+    d_equalityEngine->assertPredicate(n, polarity, reason);
+  }
   // Check for conflict
   checkForConflict();
 }

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 4e09ac23ff0974baddadd66d43fbffa382623a0c..ddb1a4043bcbc46238ee4e864974f589203a3d44 100644 (file)
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -174,9 +174,9 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   //-------------------------------------------- end initialization
 
   /**
-   * Asserts the equality to the shared terms database,
+   * Asserts n to the shared terms database with given polarity and reason
    */
-  void assertEquality(TNode equality, bool polarity, TNode reason);
+  void assertShared(TNode n, bool polarity, TNode reason);
 
   /**
    * Return whether the equality is alreday known to the engine
@@ -271,8 +271,10 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   context::UserContext* d_userContext;
   /** Equality engine */
   theory::eq::EqualityEngine* d_equalityEngine;
-  /** Proof equality engine */
-  std::unique_ptr<theory::eq::ProofEqEngine> d_pfee;
+  /** Proof equality engine, if we allocated one */
+  std::unique_ptr<theory::eq::ProofEqEngine> d_pfeeAlloc;
+  /** The proof equality engine we are using */
+  theory::eq::ProofEqEngine* d_pfee;
   /** The proof node manager */
   ProofNodeManager* d_pnm;
 };

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f98f1cb6cc4fdae6901f7da518e51788db593119..58014b06b1d3cfd50f46bcb7f506fbfb969eeaaf 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -919,7 +919,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       // assert to the shared solver
       bool polarity = assertion.getKind() != kind::NOT;
       TNode atom = polarity ? assertion : assertion[0];
-      d_sharedSolver->assertSharedEquality(atom, polarity, assertion);
+      d_sharedSolver->assertShared(atom, polarity, assertion);
     }
     return;
   }