Miscellaneous changes from central ee branch (#6687)

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

1 files changed, 15 insertions, 3 deletions

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