projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea75c6f) | patch
Refactored the equality engine in order to remove theory-specific logic from equality...
authorGuy <katz911@gmail.com>
Thu, 24 Mar 2016 23:56:13 +0000 (16:56 -0700)
committerGuy <katz911@gmail.com>
Thu, 24 Mar 2016 23:56:13 +0000 (16:56 -0700)
commit399788b6e81f9718e7870ef0b8061a77fb22b9cf
tree5953146e657760a357d1abaf987df049f150a3c3tree
parentea75c6f2b6e3a374efdccbfc9a01074609c13a57commit | diff
Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction
src/Makefile.am diff | blob | history
src/theory/arrays/array_proof_reconstruction.cpp [new file with mode: 0644] blob
src/theory/arrays/array_proof_reconstruction.h [new file with mode: 0644] blob
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history