summaryrefslogtreecommitdiff
path: root/src/theory/uf/equality_engine.cpp
AgeCommit message (Expand)Author
2017-07-07Update copyright headers.Mathias Preiner
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-09-16Handling a corner case where a ROW's guard is a constant disequality.Guy
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-07-06A few proof bugs fixedGuy
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-28Minor cleanup from last commit (quant util, equality infer). Do not set fmfBo...ajreynol
2016-03-24Refactored the equality engine in order to remove theory-specific logic from ...Guy
2016-03-23squash-merge from proof branchGuy
2016-02-05Changing the way the equality engine explains disequalities.guykatzz
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-04-07Removing the reference to THEORY_BOOL from the equality engine. This theoryDejan Jovanovic
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-03Revert "Disable constants sharing in eq engine, disable hack in theory engine."Kshitij Bansal
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. Chang...ajreynol
2014-11-19Making construction of trigger sets not use the global engine state.Dejan Jovanović
2014-07-01Update copyrights.Morgan Deters
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : h...Andrew Reynolds
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, extends...Andrew Reynolds
2014-01-07minor fix, bring back the assertion.Tianyi Liang
2014-01-07string contain changesTianyi Liang
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-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
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21fixing markings of internal nodes in equality engineDejan Jovanović
2013-03-21more equality constant evaluationDejan Jovanović
2013-03-21fixing constant evaluation bugsDejan Jovanović
2013-03-19Adding evaluation of constant terms to the equality engine. Evaluation on a p...Dejan Jovanović
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-16fixing and refactoring the equality iteratorDejan Jovanović
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-09More fixes to model codeClark Barrett
2012-10-09adding mergePredicates method to the equality engine to be able toDejan Jovanović
2012-09-22another fix for the equality class iterator Dejan Jovanović
2012-09-19fix for bug 370.Dejan Jovanović
2012-09-19Changing the equality engines's euivalence class iterator. Andy please check ...Dejan Jovanović
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-17fixing wrong assertionDejan Jovanović
2012-06-14changing to a more natural propagation order in uf, seems to pay offDejan Jovanović
2012-06-14some changes to the uf engineDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback