Age | Commit message (Expand) | Author |
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ć |
2012-09-22 | another fix for the equality class iterator | Dejan Jovanović |
2012-09-19 | fix for bug 370. | Dejan Jovanović |
2012-09-19 | Changing the equality engines's euivalence class iterator. Andy please check ... | Dejan Jovanović |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-17 | fixing wrong assertion | Dejan Jovanović |
2012-06-14 | changing to a more natural propagation order in uf, seems to pay off | Dejan Jovanović |
2012-06-14 | some changes to the uf engine | Dejan Jovanović |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-10 | fixes for bug347 | Dejan Jovanović |
2012-06-07 | fixing the wrong results. arrays equality adaptor had a missing case when pro... | Dejan Jovanović |
2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-05-27 | some reordering to keep invariants | Dejan Jovanović |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the regr... | Dejan Jovanović |
2012-05-24 | Significant changes to the internals of the equality engine. Equality is not ... | Dejan Jovanović |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-16 | adding simple-minded handling of (dis-)equalities where constants are involved | Dejan Jovanović |
2012-05-10 | Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now ... | Tim King |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |