projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 17eb04b) | patch
Arithmetic equality solver (#6876)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 15 Jul 2021 13:25:28 +0000 (08:25 -0500)
committerGitHub <noreply@github.com>
Thu, 15 Jul 2021 13:25:28 +0000 (13:25 +0000)
commitbe1f03037110e8334bb2e73e9b6afb76eee959e2
tree7e7a9bdd010f7ec0324cae431bfb05bb70d7a770tree
parent17eb04b4e06a8b6d6ac18098d9efa961c49f6863commit | diff
Arithmetic equality solver (#6876)

This is work towards the central equality engine. This adds a module of arithmetic that uses the equality engine in the default way.

This class will be incorporated into theory_arith.cpp. It will be the replacement for CongruenceManager when we use the central equality engine architecture.
src/theory/arith/equality_solver.cpp [new file with mode: 0644] blob
src/theory/arith/equality_solver.h [new file with mode: 0644] blob