projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a8f1f0e) | patch
some changes to the uf engine
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 06:44:49 +0000 (06:44 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 06:44:49 +0000 (06:44 +0000)
commit4dad25f2c1377603ff1f035887acce3b30d40d56
tree14fa02b4205a2de1971c5600aa6280e6383be8c4tree
parenta8f1f0e2cef69acd278f859fe32a2df7852256e0commit | diff
some changes to the uf engine
* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine_types.h diff | blob | history