Miscellaneous changes from central ee branch (#6687)

Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index fa020e96be1de9b421b827f776c356e21c47b8e3..a355184da03cb26e953137c58cbd9d58a11a0a51 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -19,6 +19,7 @@
 #include "prop/prop_engine.h"
 #include "theory/care_graph.h"
 #include "theory/model_manager.h"
+#include "theory/shared_solver.h"
 #include "theory/theory_engine.h"
 
 namespace cvc5 {
@@ -78,7 +79,7 @@ void CombinationCareGraph::combineTheories()
       Node split = equality.orNode(equality.notNode());
       tsplit = TrustNode::mkTrustLemma(split, nullptr);
     }
-    sendLemma(tsplit, carePair.d_theory);
+    d_sharedSolver->sendLemma(tsplit, carePair.d_theory);
 
     // Could check the equality status here:
     //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 2b35fb97db96a741225fb92fcd5634837a3c6814..da7f0a548d650ee5151d82dfb770c3007f1f6a1a 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -110,11 +110,6 @@ eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
   return nullptr;
 }
 
-void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
-{
-  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
-}
-
 void CombinationEngine::resetRound()
 {
   // compute the relevant terms?

diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 6417b501e9439f63588f26681eae7f599685b39a..7f04ccd7529e9332c378396273fc6f9881b05592 100644 (file)
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -105,8 +105,6 @@ class CombinationEngine
    * who listens to the model's equality engine (if any).
    */
   virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify();
-  /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
-  void sendLemma(TrustNode trn, TheoryId atomsTo);
   /** Reference to the theory engine */
   TheoryEngine& d_te;
   /** Reference to the environment */

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index 95693cafca566c2e6a9a74004071f79aa48baa41..c91c3411559070b7550d3cef0de5535e018fb2f0 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -34,7 +34,8 @@ SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
       d_logicInfo(te.getLogicInfo()),
       d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
       d_preRegistrationVisitor(&te, d_te.getSatContext()),
-      d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext())
+      d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()),
+      d_out(te.theoryOf(THEORY_BUILTIN)->getOutputChannel())
 {
 }
 
@@ -104,9 +105,13 @@ EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b)
   return EQUALITY_UNKNOWN;
 }
 
-void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
+bool SharedSolver::propagateLit(TNode predicate, bool value)
 {
-  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
+  if (value)
+  {
+    return d_out.propagate(predicate);
+  }
+  return d_out.propagate(predicate.notNode());
 }
 
 bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
@@ -130,5 +135,12 @@ bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
 
 bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
 
+void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
+{
+  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
+}
+
+void SharedSolver::sendConflict(TrustNode trn) { d_out.trustedConflict(trn); }
+
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index 9198e504378f2f0f3c3bcf342d66ba28ad5e8a87..396888f66eac6532a21ad8711037f4ccd4960876 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -32,6 +32,7 @@ class TheoryEngine;
 namespace theory {
 
 struct EeSetupInfo;
+class OutputChannel;
 
 /**
  * A base class for shared solver. The shared solver is the component of theory
@@ -107,6 +108,11 @@ class SharedSolver
   /** Is term t a shared term? */
   virtual bool isShared(TNode t) const;
 
+  /**
+   * Propagate the predicate with polarity value on the output channel of this
+   * solver.
+   */
+  bool propagateLit(TNode predicate, bool value);
   /**
    * 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
@@ -118,6 +124,8 @@ class SharedSolver
                                bool value);
   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
   void sendLemma(TrustNode trn, TheoryId atomsTo);
+  /** Send conflict to the theory engine */
+  void sendConflict(TrustNode trn);
 
  protected:
   /** Solver-specific pre-register shared */
@@ -132,6 +140,8 @@ class SharedSolver
   PreRegisterVisitor d_preRegistrationVisitor;
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
+  /** Output channel of theory builtin */
+  OutputChannel& d_out;
 };
 
 }  // namespace theory