summaryrefslogtreecommitdiff
path: root/src/theory/uf/equality_engine.cpp
AgeCommit message (Expand)Author
2020-07-17Improving equality engine tracing (#4770)Haniel Barbosa
2020-07-15(proof-new) Adding API for converting EqProof into ProofNode (#4747)Haniel Barbosa
2020-06-16Update copyright headers.Aina Niemetz
2020-04-18Improving EqProof printing (#4329)Haniel Barbosa
2020-04-14Remove mergePredicates from EqualityEngine interface (#4305)Andrew Reynolds
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-04-18 Less aggressive caching in equality engine when proofs are enabled (#2964)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
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-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ć
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback