From: Andrew Reynolds 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);