projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8562fbe) | patch
Ignore isInConflict when adding conflicts (#5995)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 4 Mar 2021 14:24:21 +0000 (15:24 +0100)
committerGitHub <noreply@github.com>
Thu, 4 Mar 2021 14:24:21 +0000 (15:24 +0100)
commitc3d58e3bdd194372421ce7d7c8a6f8d1f4deecfa
treede191404275e801ac9bc7857fa94583a89b2baf6tree
parent8562fbebb7bcc6b6c07938d6866b4092715c2a55commit | 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.
src/theory/theory_inference_manager.cpp diff | blob | history