From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Jul 2021 18:15:48 +0000 (-0500)
Subject: Add trace for combination splits (#6862)
X-Git-Tag: cvc5-1.0.0~1505
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e01ae3a87f4e1dc4b4511e8bd028d5c0838ccedc;p=cvc5.git

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 a355184da..4b0adf56b 100644
--- 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 2cbba6b33..0ef0ad6bd 100644
--- 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 f8bc35e08..ba268b396 100644
--- 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 c91c34115..f2266c236 100644
--- 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 396888f66..4786d6fc9 100644
--- 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);