From c3d58e3bdd194372421ce7d7c8a6f8d1f4deecfa Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 4 Mar 2021 15:24:21 +0100 Subject: [PATCH] Ignore isInConflict when adding conflicts (#5995) Right now, the inference manager infrastructure drops conflicts (and literal propagations) if the solver already is in a conflict. This PR removes this behavior. The current setup in linear arithmetic requires adding conflicts, even when already in conflict, and experiments showed a small but beneficial effect of this change. --- src/theory/theory_inference_manager.cpp | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 810f31ce5..c96666cab 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -107,23 +107,17 @@ void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) void TheoryInferenceManager::conflict(TNode conf, InferenceId id) { - if (!d_theoryState.isInConflict()) - { - d_conflictIdStats << id; - d_theoryState.notifyInConflict(); - d_out.conflict(conf); - ++d_numConflicts; - } + d_conflictIdStats << id; + d_theoryState.notifyInConflict(); + d_out.conflict(conf); + ++d_numConflicts; } void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { - if (!d_theoryState.isInConflict()) - { - d_conflictIdStats << id; - d_theoryState.notifyInConflict(); - d_out.trustedConflict(tconf); - } + d_conflictIdStats << id; + d_theoryState.notifyInConflict(); + d_out.trustedConflict(tconf); } void TheoryInferenceManager::conflictExp(InferenceId id, -- 2.30.2