| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
| 2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović |
| 2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
| 2012-05-14 | fixes for shared term registration. previously the type was not considered wh... | Dejan Jovanović |
| 2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
| 2012-04-28 | New LogicInfo functionality. | Morgan Deters |
| 2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
| 2012-04-11 | merge from arrays-clark branch | Morgan Deters |
| 2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović |
