Minor cleaning of quantifiers engine (#5858)

[cvc5.git] / src / theory / combination_care_graph.cpp

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 9374e7ecbc680a27ad4ae655096e7d582c57578c..1ebffc8c25291c1f69e7f34811ed6f7b2d6f9d2c 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -2,10 +2,10 @@
 /*! \file combination_care_graph.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Dejan Jovanovic
  ** 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.
+ ** 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
  **
@@ -15,6 +15,7 @@
 #include "theory/combination_care_graph.h"
 
 #include "expr/node_visitor.h"
+#include "prop/prop_engine.h"
 #include "theory/care_graph.h"
 #include "theory/theory_engine.h"
 
@@ -22,8 +23,10 @@ namespace CVC4 {
 namespace theory {
 
 CombinationCareGraph::CombinationCareGraph(
-    TheoryEngine& te, const std::vector<Theory*>& paraTheories)
-    : CombinationEngine(te, paraTheories)
+    TheoryEngine& te,
+    const std::vector<Theory*>& paraTheories,
+    ProofNodeManager* pnm)
+    : CombinationEngine(te, paraTheories, pnm)
 {
 }
 
@@ -61,8 +64,18 @@ void CombinationCareGraph::combineTheories()
     Debug("combineTheories")
         << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
 
-    Node split = equality.orNode(equality.notNode());
-    sendLemma(split, carePair.d_theory);
+    TrustNode tsplit;
+    if (isProofEnabled())
+    {
+      // make proof of splitting lemma
+      tsplit = d_cmbsPg->mkTrustNodeSplit(equality);
+    }
+    else
+    {
+      Node split = equality.orNode(equality.notNode());
+      tsplit = TrustNode::mkTrustLemma(split, nullptr);
+    }
+    sendLemma(tsplit, carePair.d_theory);
 
     // Could check the equality status here:
     //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
@@ -73,7 +86,7 @@ void CombinationCareGraph::combineTheories()
     // This is supposed to force preference to follow what the theory models
     // already have but it doesn't seem to make a big difference - need to
     // explore more -Clark
-    Node e = d_te.ensureLiteral(equality);
+    Node e = d_valuation.ensureLiteral(equality);
     propEngine->requirePhase(e, true);
   }
 }