From e8333750e5932ab5ce9a8a491b53aef4ffa4b0aa Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 11 Feb 2021 21:25:50 +0100 Subject: Make most methods of TheoryInferenceManager expect an InferenceId. (#5897) This PR makes most methods of the TheoryInferenceManager expect an InferenceId. All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere. In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs. The InferenceIds are not yet used, but will be used for statistics and debug output. --- src/theory/strings/inference_manager.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/theory/strings') diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index a348585e7..8c487d7c1 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -299,7 +299,7 @@ void InferenceManager::processConflict(const InferInfo& ii) Trace("strings-assert") << "(assert (not " << tconf.getNode() << ")) ; conflict " << ii.getId() << std::endl; // send the trusted conflict - trustedConflict(tconf); + trustedConflict(tconf, ii.getId()); } bool InferenceManager::processFact(InferInfo& ii) @@ -342,13 +342,13 @@ bool InferenceManager::processFact(InferInfo& ii) // current SAT context d_ipc->notifyFact(ii); // now, assert the internal fact with d_ipc as proof generator - curRet = assertInternalFact(atom, polarity, exp, d_ipc.get()); + curRet = assertInternalFact(atom, polarity, ii.getId(), exp, d_ipc.get()); } else { Node cexp = utils::mkAnd(exp); // without proof generator - curRet = assertInternalFact(atom, polarity, cexp); + curRet = assertInternalFact(atom, polarity, ii.getId(), cexp); } ret = ret || curRet; // may be in conflict @@ -420,7 +420,7 @@ bool InferenceManager::processLemma(InferInfo& ii) ++(d_statistics.d_lemmasInfer); // call the trusted lemma, without caching - return trustedLemma(tlem, p, false); + return trustedLemma(tlem, ii.getId(), p, false); } } // namespace strings -- cgit v1.2.3