projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec1abb0) | patch
Changes to datatypes in preparation for central equality engine (#6901)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 25 Jul 2021 16:04:00 +0000 (11:04 -0500)
committerGitHub <noreply@github.com>
Sun, 25 Jul 2021 16:04:00 +0000 (16:04 +0000)
commit74acadc8e7aebd9cd7d41bed64d67e42f45de640
treea0166b2ee6d8f87371fd959befa5a7e5c27d5498tree
parentec1abb0ba86ac06c955848f718fa70d3ffe8e40dcommit | diff
Changes to datatypes in preparation for central equality engine (#6901)

This adds changes from the centralEeDev branch for datatypes.

The changes in behavior are that the inference manager clears its pending inferences when the state is in conflict, and preCheck processes pending facts immediately (which may have been enqueued prior to the call to check via ee merges). These are required to make datatypes robust to the order in which check / merge / backtracks can occur.
src/theory/datatypes/inference_manager.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history