Simplifier breaks propagation
Issue #799
invalid
This is an issue in MinisatID.
However, one IDP test is disabled because of this issue.
Please close this issue and put the test back as soon as the corresponding issue
https://bitbucket.org/krr/minisatid/issue/56/simplifier-breaks-propagation
is fixed.
Comments (3)
-
reporter -
reporter Extra uitleg.
De simplifier werkt momenteel als volgt: cache alle input voor de solver. Zodra hij signaal krijgt dat de grounding klaar is, vereenvoudig theorie en geef hem door naar propagatoren etcetera.
Dit is niet compatibel met het idee om unsat al snel naar de grounder toe te propageren zodat hij snel kan stoppen
-
reporter - changed status to invalid
This is the expected behaviour of the simplifier
- Log in to comment
Removed unsatsolvertest
see
#799→ <<cset 60df43bbe3cc>>