From 6d8b0c1ab090df93101b5c7fb350b469f7537419 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 May 2020 12:24:02 -0500 Subject: More --- src/theory/theory_engine.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index eba1c5594..955745783 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1606,7 +1606,8 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( proofRecipe->addStep(proofStep); } }); - + // it came directly from the theory, it is ready to be processed + processTrustNode(texplanation); return texplanation; } @@ -1636,16 +1637,16 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( } TrustNode texplanation = getExplanation(vec, proofRecipe); - Node explanation = texplanation.getNode(); - - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; + // the trust node was processed within getExplanation return texplanation; } theory::TrustNode TheoryEngine::getExplanation(TNode node) { LemmaProofRecipe *dontCareRecipe = NULL; + // the trust node was processed within getExplanationAndRecipe return getExplanationAndRecipe(node, dontCareRecipe); } @@ -1911,6 +1912,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Process the explanation TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); + + // TODO: convert proof here? + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); -- cgit v1.2.3