From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 4 Mar 2021 14:24:21 +0000 (+0100)
Subject: Ignore isInConflict when adding conflicts (#5995)
X-Git-Tag: cvc5-1.0.0~2156
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3d58e3bdd194372421ce7d7c8a6f8d1f4deecfa;p=cvc5.git

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.
---

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,