From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 4 Jun 2021 21:05:43 +0000 (-0500)
Subject: Miscellaneous changes from central ee branch (#6687)
X-Git-Tag: cvc5-1.0.0~1639
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=760874731c70e2aa32c3591c67a08f3ea85dcafd;p=cvc5.git

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 fa020e96b..a355184da 100644
--- 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 2b35fb97d..da7f0a548 100644
--- 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 6417b501e..7f04ccd75 100644
--- 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 95693cafc..c91c34115 100644
--- 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 9198e5043..396888f66 100644
--- 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