summaryrefslogtreecommitdiff
path: root/src/theory/uf/equality_engine.h
AgeCommit message (Expand)Author
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-20Improved tracing for equivalence classes of EE (#6169)Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2020-12-10Refactor KindMap (#5646)Gereon Kremer
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
2020-08-24Add a few basic extensions for equality engine (#4937)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-12(proof-new) Improving proof-production in Equality Engine (#4871)Haniel Barbosa
2020-08-09Splitting a few utility classes from EqualityEngine to their own file (#4862)Andrew Reynolds
2020-07-15(proof-new) Adding API for converting EqProof into ProofNode (#4747)Haniel Barbosa
2020-06-16Update copyright headers.Aina Niemetz
2020-04-14Remove mergePredicates from EqualityEngine interface (#4305)Andrew Reynolds
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2019-04-17Cache explanations in the equality engine (#2937)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
2017-09-13Modify equality engine to allow operators to be marked as external terms (#1082)Andrew Reynolds
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-07Update copyright headers.Mathias Preiner
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-04-03Updating the copyright headers and scripts.Tim King
2016-04-03Removed the theory-specific merge reason types. Instead, added a mechanism fo...Guy
2016-03-24Refactored the equality engine in order to remove theory-specific logic from ...Guy
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-11-19Making construction of trigger sets not use the global engine state.Dejan Jovanović
2014-07-01Update copyrights.Morgan Deters
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, extends...Andrew Reynolds
2014-02-21add new theory (sets)Kshitij Bansal
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-19possible fix for bug 521Dejan Jovanovic
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback