Add trace for combination splits (#6862)

Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index a355184da03cb26e953137c58cbd9d58a11a0a51..4b0adf56b53ec3b2230b42b0e665a499e417745f 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -79,7 +79,8 @@ void CombinationCareGraph::combineTheories()
       Node split = equality.orNode(equality.notNode());
       tsplit = TrustNode::mkTrustLemma(split, nullptr);
     }
-    d_sharedSolver->sendLemma(tsplit, carePair.d_theory);
+    d_sharedSolver->sendLemma(
+        tsplit, carePair.d_theory, InferenceId::COMBINATION_SPLIT);
 
     // Could check the equality status here:
     //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 2cbba6b3385c1f816ffe27fbad3feafc60852fa9..0ef0ad6bd5ef089998b019407f58cad0a2e58bca 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -25,6 +25,7 @@ const char* toString(InferenceId i)
   switch (i)
   {
     case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE";
+    case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT";
     case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX";
     case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ";
     case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f8bc35e087898061255fba034be36e19bd052d4d..ba268b39684ac3e34c8e59c6fb4f262511a4b842 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -41,6 +41,8 @@ enum class InferenceId
   // ---------------------------------- core
   // a conflict when two constants merge in the equality engine (of any theory)
   EQ_CONSTANT_MERGE,
+  // a split from theory combination
+  COMBINATION_SPLIT,
   // ---------------------------------- arith theory
   //-------------------- linear core
   // black box conflicts. It's magic.

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index c91c3411559070b7550d3cef0de5535e018fb2f0..f2266c23696107b9adef8166f4c28d5c776d5cbf 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -135,8 +135,9 @@ bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
 
 bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
 
-void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
+void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id)
 {
+  Trace("im") << "(lemma " << id << " " << trn.getProven() << ")" << std::endl;
   d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
 }
 

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index 396888f66eac6532a21ad8711037f4ccd4960876..4786d6fc9776861d21b24c874970713bcb9bb076 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__SHARED_SOLVER__H
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
@@ -123,7 +124,7 @@ class SharedSolver
                                TNode b,
                                bool value);
   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
-  void sendLemma(TrustNode trn, TheoryId atomsTo);
+  void sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id);
   /** Send conflict to the theory engine */
   void sendConflict(TrustNode trn);