Age | Commit message (Expand) | Author |
2011-10-28 | Adding a check in Polynomial::parsePolynomial to better enforce the arithmeti... | Tim King |
2011-10-23 | Implement changes from yesterday morning's meeting (10/21/2011): | Morgan Deters |
2011-10-19 | Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 i... | Tim King |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-10-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
2011-10-05 | ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t... | Morgan Deters |
2011-10-05 | remove some debugging code that slowed down last night's regressions | Morgan Deters |
2011-10-04 | fixes to context-dependent caching substitutions | Morgan Deters |
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 |