projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 697fbbf) | patch
Refactor equality engine setup for arithmetic congruence manager (#6902)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 25 Jul 2021 14:54:28 +0000 (09:54 -0500)
committerGitHub <noreply@github.com>
Sun, 25 Jul 2021 14:54:28 +0000 (14:54 +0000)
commitec1abb0ba86ac06c955848f718fa70d3ffe8e40d
tree6f4555d84543f312ac01b982b6814e477584b5datree
parent697fbbf41621a30c21408f1edeba87f9064ab7decommit | diff
Refactor equality engine setup for arithmetic congruence manager (#6902)

Allows congruence manager to use its own (non-official) equality engine if both it and the arithmetic equality solver are enabled.
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history