projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 52c5c28) | patch
Significant changes to the internals of the equality engine. Equality is not handled...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 24 May 2012 05:54:39 +0000 (05:54 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 24 May 2012 05:54:39 +0000 (05:54 +0000)
commit13e7de0006e9c34cc715521fc9f1866c25682113
tree29d83cdfcb0ebd618f630496bc6050d16a0cdc66tree
parent52c5c282f47448856e0dec8a7d4e5de612a8dcc3commit | diff
Significant changes to the internals of the equality engine. Equality is not handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected.
src/theory/uf/Makefile.am diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
src/theory/uf/equality_engine_types.h [new file with mode: 0644] blob
src/theory/uf/theory_uf.cpp diff | blob | history