| Age | Commit message (Expand) | Author |
|---|
| 2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
| 2016-01-05 | Add SmtGlobals Class | Tim King |
| 2016-01-01 | Added propagation rule for array ext lemmas to aid proofs | Clark Barrett |
| 2015-12-22 | Bug fix uf-ss-totality. | ajreynol |
| 2015-12-15 | Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference. | ajreynol |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-26 | Front-end support for get-value of sort cardinality, minor fixes for sygus so... | ajreynol |
| 2015-11-09 | Replacing an inefficient use of std::find(...) to use std::set's find() instead. | Tim King |
| 2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
| 2015-10-08 | Minor improvements to strings. Refactor rewriter. Enable fairness for multipl... | ajreynol |
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress... | ajreynol |
| 2015-09-05 | Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug... | ajreynol |
| 2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
| 2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
| 2015-04-07 | Removing the reference to THEORY_BOOL from the equality engine. This theory | Dejan Jovanovic |
| 2015-03-25 | change const are triggers from false to true in equality engines | Kshitij Bansal |
| 2015-03-14 | Patches for 32-bit ARM | Tianyi Liang |
| 2015-01-16 | Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus... | ajreynol |
| 2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
| 2014-12-12 | Add cvc parsing support for cardinality constraints. Bug fix for enumerating... | ajreynol |
| 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-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
| 2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol |
| 2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
| 2014-09-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
| 2014-09-03 | check() optimization | Kshitij Bansal |
| 2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-20 | UF kinds documentation | Morgan Deters |
| 2014-05-02 | Simplification of EqualityEngine::areDisequal. Comparison for production : h... | Andrew Reynolds |
| 2014-04-29 | Fix compiler warning re: TheoryUF destructor. | Morgan Deters |
| 2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
| 2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
| 2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ... | Andrew Reynolds |
| 2014-03-14 | Add ability to provide theory-specific proof rules to EqualityEngine, extends... | Andrew Reynolds |
| 2014-02-21 | Merge branch '1.3.x' | Morgan Deters |
| 2014-02-21 | No diamond-breaking under quantifiers (resolves bug #550). | Morgan Deters |
| 2014-02-21 | add new theory (sets) | Kshitij Bansal |
| 2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
| 2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
| 2014-01-07 | minor fix, bring back the assertion. | Tianyi Liang |
| 2014-01-07 | string contain changes | Tianyi Liang |
| 2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
| 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-11-27 | General pre-release cleanup commit | Morgan Deters |
| 2013-11-19 | Bug fix for previous commit | Andrew Reynolds |
| 2013-11-19 | Add fair strategy for finite model finding multiple sorts --uf-ss-fair. | Andrew Reynolds |
