| Age | Commit message (Expand) | Author |
|---|
| 2019-10-30 | Unify 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-17 | Cache explanations in the equality engine (#2937) | Andrew Reynolds |
| 2019-03-26 | Update copyright headers. | Aina Niemetz |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz |
| 2017-10-25 | Switching EqProof to use shared_ptr everywhere. (#1217) | Tim King |
| 2017-09-13 | Modify equality engine to allow operators to be marked as external terms (#1082) | Andrew Reynolds |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
| 2016-09-16 | Handling a corner case where a ROW's guard is a constant disequality. | Guy |
| 2016-09-01 | Relaxing the throw specifiers for the destructors for Node, TypeNode, the con... | Tim King |
| 2016-07-06 | A few proof bugs fixed | Guy |
| 2016-06-01 | Merge from proof branch | Guy |
| 2016-06-01 | Revert "Merging proof branch" | Guy |
| 2016-06-01 | Merging proof branch | Guy |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2016-04-03 | Removed the theory-specific merge reason types. Instead, added a mechanism fo... | Guy |
| 2016-03-28 | Minor cleanup from last commit (quant util, equality infer). Do not set fmfBo... | ajreynol |
| 2016-03-24 | Refactored the equality engine in order to remove theory-specific logic from ... | Guy |
| 2016-03-23 | squash-merge from proof branch | Guy |
| 2016-02-05 | Changing the way the equality engine explains disequalities. | guykatzz |
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
| 2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
| 2015-04-07 | Removing the reference to THEORY_BOOL from the equality engine. This theory | Dejan Jovanovic |
| 2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
| 2014-12-03 | Revert "Disable constants sharing in eq engine, disable hack in theory engine." | Kshitij Bansal |
| 2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. Chang... | ajreynol |
| 2014-11-19 | Making construction of trigger sets not use the global engine state. | Dejan Jovanović |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-05-02 | Simplification of EqualityEngine::areDisequal. Comparison for production : h... | Andrew Reynolds |
| 2014-03-14 | Add ability to provide theory-specific proof rules to EqualityEngine, extends... | Andrew Reynolds |
| 2014-01-07 | minor fix, bring back the assertion. | Tianyi Liang |
| 2014-01-07 | string contain changes | Tianyi Liang |
| 2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-07-19 | possible fix for bug 521 | Dejan Jovanovic |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-04-01 | Merging some cleanup work: | Morgan Deters |
| 2013-03-21 | another typo/bugfix for equality constant evaluation | Dejan Jovanović |
| 2013-03-21 | fixing markings of internal nodes in equality engine | Dejan Jovanović |
| 2013-03-21 | more equality constant evaluation | Dejan Jovanović |
| 2013-03-21 | fixing constant evaluation bugs | Dejan Jovanović |
| 2013-03-19 | Adding evaluation of constant terms to the equality engine. Evaluation on a p... | Dejan Jovanović |
| 2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
| 2012-11-16 | fixing and refactoring the equality iterator | Dejan Jovanović |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-09 | More fixes to model code | Clark Barrett |
| 2012-10-09 | adding mergePredicates method to the equality engine to be able to | Dejan Jovanović |
