diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-11 20:00:18 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 20:00:18 +0100 |
| commit | f5486884229348516ac26300273e4f5458a74208 (patch) | |
| tree | 8e48bd833c3e55b247adca891ec2081fc9077528 /src/theory/arith/inference_manager.cpp | |
| parent | 8fcb59d072b09bfaf8f56334182d425274842461 (diff) | |
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
Diffstat (limited to 'src/theory/arith/inference_manager.cpp')
| -rw-r--r-- | src/theory/arith/inference_manager.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 6a1f898d3..aa0aa4f2a 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -32,7 +32,7 @@ InferenceManager::InferenceManager(TheoryArith& ta, void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma, bool isWaiting) { - Trace("arith::infman") << "Add " << lemma->d_inference << " " << lemma->d_node + Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node << (isWaiting ? " as waiting" : "") << std::endl; if (hasCachedLemma(lemma->d_node, lemma->d_property)) { @@ -81,7 +81,7 @@ void InferenceManager::flushWaitingLemmas() for (auto& lem : d_waitingLem) { Trace("arith::infman") << "Flush waiting lemma to pending: " - << lem->d_inference << " " << lem->d_node + << lem->getId() << " " << lem->d_node << std::endl; d_pendingLem.emplace_back(std::move(lem)); } |