| Age | Commit message (Expand) | Author |
|---|
| 2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol |
| 2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in Th... | ajreynol |
| 2016-07-20 | Infrastructure for storing and printing heap models for separation logic. Ens... | ajreynol |
| 2016-07-06 | Add comment field for model, resolves hack for printing sep logic models. | ajreynol |
| 2016-07-05 | Refactor last call for theories, only create one model when quantifiers are e... | ajreynol |
| 2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
| 2016-04-09 | cardinality operation for finite sets (based on my thesis / ijcar16 paper) | Kshitij Bansal |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2016-03-23 | squash-merge from proof branch | Guy |
| 2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
| 2016-01-28 | Adding listeners to Options. | Tim King |
| 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 |
| 2016-01-05 | Add SmtGlobals Class | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
| 2014-09-03 | check() optimization | Kshitij Bansal |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-09 | more | Kshitij Bansal |
| 2014-03-19 | Fix documentation for Theory::preRegisterTerm(). | Morgan Deters |
| 2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
| 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-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
| 2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
| 2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
| 2013-09-23 | Revert Clark's last commit, at his request; there are some bugs. | Morgan Deters |
| 2013-09-23 | Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h | Clark Barrett |
| 2013-09-18 | Fixes to theoryof-mode; no longer static in Theory class. | Morgan Deters |
| 2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-26 | adding | Dejan Jovanović |
| 2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
| 2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters |
| 2012-12-01 | remove instantiator framework | Morgan Deters |
| 2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
| 2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
| 2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
| 2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett |
| 2012-11-08 | Review of trunk r4525 (TypeNode::getBaseType()): | Morgan Deters |
| 2012-10-31 | cleaning up some of the equality query stuff, implemented a new representativ... | Andrew Reynolds |
| 2012-10-19 | Fix for model building with shared terms for arithmetic. | Tim King |
| 2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
