diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-01 10:14:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 15:14:11 +0000 |
| commit | 8b71d28d4c63b4147429125fae7de3d75fb55bd8 (patch) | |
| tree | 2add2fe642fd2a6e9f7911a76ade8b4dea9dc768 /src | |
| parent | e56900bcacd2698de70172d9c1c79f32a1cbb0eb (diff) | |
Add debug traces to theory inference manager (#6250)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 23 | ||||
| -rw-r--r-- | src/theory/theory_inference_manager.h | 1 |
2 files changed, 14 insertions, 10 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index e6f7fd5eb..031570318 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -113,15 +113,15 @@ void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) void TheoryInferenceManager::conflict(TNode conf, InferenceId id) { - d_conflictIdStats << id; - d_theoryState.notifyInConflict(); - d_out.conflict(conf); - ++d_numConflicts; + TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr); + return trustedConflict(tconf, id); } void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { d_conflictIdStats << id; + Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" + << std::endl; d_theoryState.notifyInConflict(); d_out.trustedConflict(tconf); ++d_numConflicts; @@ -252,6 +252,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, } } d_lemmaIdStats << id; + Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); return true; @@ -338,8 +339,8 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, InferenceId id, TNode exp) { - d_factIdStats << id; - return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr); + return processInternalFact( + atom, pol, id, PfRule::UNKNOWN, {exp}, {}, nullptr); } bool TheoryInferenceManager::assertInternalFact(TNode atom, @@ -350,8 +351,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, const std::vector<Node>& args) { Assert(pfr != PfRule::UNKNOWN); - d_factIdStats << id; - return processInternalFact(atom, pol, pfr, exp, args, nullptr); + return processInternalFact(atom, pol, id, pfr, exp, args, nullptr); } bool TheoryInferenceManager::assertInternalFact(TNode atom, @@ -360,17 +360,20 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom, const std::vector<Node>& exp, ProofGenerator* pg) { - d_factIdStats << id; - return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg); + return processInternalFact(atom, pol, id, PfRule::ASSUME, exp, {}, pg); } bool TheoryInferenceManager::processInternalFact(TNode atom, bool pol, + InferenceId iid, PfRule id, const std::vector<Node>& exp, const std::vector<Node>& args, ProofGenerator* pg) { + d_factIdStats << iid; + Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode()) + << ")" << std::endl; // make the node corresponding to the explanation Node expn = NodeManager::currentNM()->mkAnd(exp); // call the pre-notify fact method with preReg = false, isInternal = true diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index ad92f5380..063b9a008 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -379,6 +379,7 @@ class TheoryInferenceManager */ bool processInternalFact(TNode atom, bool pol, + InferenceId iid, PfRule id, const std::vector<Node>& exp, const std::vector<Node>& args, |