diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-04 15:24:21 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-04 15:24:21 +0100 |
| commit | c3d58e3bdd194372421ce7d7c8a6f8d1f4deecfa (patch) | |
| tree | de191404275e801ac9bc7857fa94583a89b2baf6 /src/theory | |
| parent | 8562fbebb7bcc6b6c07938d6866b4092715c2a55 (diff) | |
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.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 20 |
1 files 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, |