projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 14041ad) | patch
Further standardization of datatypes (#5076)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 17 Sep 2020 05:22:20 +0000 (00:22 -0500)
committerGitHub <noreply@github.com>
Thu, 17 Sep 2020 05:22:20 +0000 (22:22 -0700)
commit169a281ca849b7c9fcf61d9ece0c46f728a44cc2
tree0f3c3742f3153bf5556a2b09e8cf3381c39484dctree
parent14041ad14583f670bc03d5eef6535544d86fc9fccommit | diff
Further standardization of datatypes (#5076)

We now have no custom calls to equality engine explain, and only 2 manual calls to equality engine (in its entailment check). This also updates the notify class to the standard one.

This commit makes datatypes ready to start work on proofs.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history