Age | Commit message (Expand) | Author |
2011-09-16 | fix an oversight in the language printers | Morgan Deters |
2011-09-15 | tim's fixes for context-dependent pre-registration | Dejan Jovanović |
2011-09-15 | adding --show-debug-tags to list all available debug tracing tags | 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 | Disable a warning to address bug 277. (This doesn't really resolve the issue... | Morgan Deters |
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 | Ensure that assignment gestures through CDMap iterators like: | 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-30 | Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK wil... | 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 | changing the sat solver remove clauses constants | Dejan Jovanović |
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-07 | removing duplicate clauses in ite cnf conversion | 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 | Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x), | Morgan Deters |
2011-06-30 | Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 1... | Tim King |
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-30 | some things I had laying around in a directory but never got committed; minor... | Morgan Deters |
2011-06-29 | Fixed spelling mistake and documentation for --enable-variable-removal. | Tim King |
2011-06-18 | Some fixes inspired by Fedora 15: | Morgan Deters |
2011-06-06 | compilation fix for x86 (from previous commit) | Morgan Deters |
2011-06-06 | Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on... | 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 |