Age | Commit message (Expand) | Author |
2011-07-11 | if running in QF_AX, equalities over terms of uninterpreted sort go to arrays... | Morgan Deters |
2011-07-11 | adding disequality propagation | Dejan Jovanović |
2011-07-11 | merge from symmetry branch | Morgan Deters |
2011-07-10 | Reverting mistaken check-in | Clark Barrett |
2011-07-10 | Fixed bug in default solve - wasn't returning when it was supposed to | Clark Barrett |
2011-07-10 | another typo | Dejan Jovanović |
2011-07-10 | yet another uf bug fix, hopefully the last | Dejan Jovanović |
2011-07-10 | another bugfix for uf | Dejan Jovanović |
2011-07-09 | some immediate bug fixes | Dejan Jovanović |
2011-07-09 | minor fixups | Morgan Deters |
2011-07-09 | surprize surprize | Dejan Jovanović |
2011-07-06 | Fixing two bugs: | Dejan Jovanović |
2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
2011-06-30 | Merging the playground branch upto r1957 into trunk. | Tim King |
2011-06-30 | only use theory registration if (1) a theory requests it, or (2) if there's m... | Morgan Deters |
2011-06-03 | fixed various bugs related to ambiguous parametric datatype constructors, par... | Andrew Reynolds |
2011-06-03 | datatypes work | Morgan Deters |
2011-06-02 | added (temporary) support for ensuring that all ambiguously typed constructor... | Andrew Reynolds |
2011-06-01 | minor fix, and better output for type errors | Morgan Deters |
2011-06-01 | type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT] | Morgan Deters |
2011-05-31 | This commit contains the code for allowing arbitrary equalities in the theory... | Tim King |
2011-05-26 | apply arithmetic static learner's miplibtrick in a consistent order (for easi... | Morgan Deters |
2011-05-23 | fixes for "make dist" and "make doc", minor cleanups | Morgan Deters |
2011-05-23 | Merge from arrays2 branch. | Morgan Deters |
2011-05-14 | fix production-build compiler warning | Morgan Deters |
2011-05-14 | add AscriptionType stuff to support nullary parameterized datatypes; also, re... | Morgan Deters |
2011-05-13 | added support for parametric datatypes, updated cvc parser to handle parametr... | Andrew Reynolds |
2011-05-13 | * fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio | Morgan Deters |
2011-05-06 | Deleting dead code. | Tim King |
2011-05-06 | significant revisions/improvements to code for theory datatypes solver | Andrew Reynolds |
2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
2011-05-04 | Stronger support for zero-performance-penalty output, and fixes and | Morgan Deters |
2011-05-02 | minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closu... | Andrew Reynolds |
2011-05-02 | updates for bitvectors | Dejan Jovanović |
2011-04-29 | refactoring to datatypes theory, added working prototype for proof/explanatio... | Andrew Reynolds |
2011-04-28 | more fixes/improvements to datatypes theory and transitive closure | Andrew Reynolds |
2011-04-27 | cleaned up some of the hacks in the datatypes theory solver, working on using... | Andrew Reynolds |
2011-04-25 | Monday tasks: | Morgan Deters |
2011-04-25 | Weekend work. The main points: | Morgan Deters |
2011-04-22 | added fixes for datatype theory solver to account for rewriting before finite... | Andrew Reynolds |
2011-04-20 | numerous bugfixes | Morgan Deters |
2011-04-20 | Minor mixed-bag commit. Expected performance impact negligible. | Morgan Deters |
2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
2011-04-18 | Removing dead code that came in on commit r1740. | Tim King |
2011-04-18 | This commit merges the branch arithmetic/propagation-again into trunk. | Tim King |
2011-04-18 | Partial merge from datatypes-merge branch: | Morgan Deters |
2011-04-14 | Three things: | Morgan Deters |
2011-04-10 | Add -lprofiler when --with-google-perftools is offered; also fix some newswir... | Morgan Deters |
2011-04-07 | Made Valuation::getValue() and Valuation::getSatValue() const. | Tim King |
2011-04-05 | Minor adjustments to the Registrar commit in 1644, documentation. | Morgan Deters |