| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
| 2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to tu... | Andrew Reynolds |
| 2013-10-24 | Fix for bug515 | Clark Barrett |
| 2013-10-03 | Added support for converting unsorted problems to multi-sorted problems via s... | Andrew Reynolds |
| 2013-09-30 | Bug fixes and improvements for symmetry breaking, it now supports multiple so... | Andrew Reynolds |
| 2013-09-27 | Add new symmetry breaking technique for finite model finding. Improvements t... | Andrew Reynolds |
| 2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
