Age | Commit message (Expand) | Author |
2011-09-30 | more push/pop infrastructure, some SAT stuff | Morgan Deters |
2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in preparation... | Morgan Deters |
2011-09-29 | build system fixes | Morgan Deters |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-28 | variety of visibility fixes (should clean up some of the many warnings on Mac... | Morgan Deters |
2011-09-16 | include example theory (former "UF-Tim") that's included in the dist but not ... | Morgan Deters |
2011-09-16 | final(?) documentation fixes | Morgan Deters |
2011-09-16 | fix up more documentation | Morgan Deters |
2011-09-16 | fix serious issue with copyright-updating script | Morgan Deters |
2011-09-16 | fix numerous documentation issues; doxygen complains much less, now | Morgan Deters |
2011-09-15 | tim's fixes for context-dependent pre-registration | Dejan Jovanović |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-07 | fixes for uf/equality engine from the quantifiers branch. mainly backtracking... | Dejan Jovanović |
2011-09-03 | removing an assert i forgot to remove that andy found | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
2011-09-02 | * Changing pre-registration to be context dependent -- it is called from the ... | Dejan Jovanović |
2011-08-27 | Removing Theory::registerTerm() as discussed in the meeting. Now pre-register... | Dejan Jovanović |
2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
2011-08-23 | some uf cleanup | Dejan Jovanović |
2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters |
2011-07-11 | fixing out of place typename (error on g++ 4.4.3-4ubuntu5) | Morgan Deters |
2011-07-11 | Adding static_fact_manager | Clark Barrett |
2011-07-11 | Clark's work on array theory - can now solve all QF_AX problems | Clark Barrett |
2011-07-11 | fix some confusing debug output (bogus counter) | Morgan Deters |
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 |