| Age | Commit message (Expand) | Author |
|---|
| 2011-03-20 | more bugfixes for bitvectors | Dejan Jovanović |
| 2011-03-20 | fixing the failure from last nigth, due to using a reference to an element in... | Dejan Jovanović |
| 2011-03-20 | missed one case | Dejan Jovanović |
| 2011-03-20 | commit for the version of bitvectors that passes all the unit tests | Dejan Jovanović |
| 2011-03-19 | Merges the pqueue-set branch into trunk. During VarOrder mode and Collection... | Tim King |
| 2011-03-18 | - The learned clauses from the miplib trick were being added twice. This was ... | Tim King |
| 2011-03-17 | Switched SimplexDecisionProcedure::d_delayedLemmas from a vector to a queue. | Tim King |
| 2011-03-17 | SimplexDecisionProcedure no longer takes an OutputChannel as a parameter. | Tim King |
| 2011-03-17 | - Removes arith_constants.h | Tim King |
| 2011-03-17 | Adds debugging output to EngineOutputChannel::lemma. | Tim King |
| 2011-03-17 | Fix for the bug introduced in 1477. The stuff that was added to CVC4ostream:... | Tim King |
| 2011-03-17 | push and pop manipulators for output stream so that one can indent the output | Dejan Jovanović |
| 2011-03-16 | - Turns on the excluded middle assertions during the miplibTrick. If it is kn... | Tim King |
| 2011-03-16 | - Turns on the miplibTrick. This detects during the static learning phase a ... | Tim King |
| 2011-03-15 | real fix for bug 245, previous one was faulty | Dejan Jovanović |
| 2011-03-15 | small fixes for run_regression script to workaround bug in old mktemp, was ca... | Morgan Deters |
| 2011-03-15 | fix for bug 254, lemmas were propagating at lower levels, and the conflict cl... | Dejan Jovanović |
| 2011-03-15 | Merge from cudd branch. This mostly just adds support for linking | Morgan Deters |
| 2011-03-14 | adding support for google performance tools to the build sytem, it can be ena... | Dejan Jovanović |
| 2011-03-14 | change to the run_regression script to better manage temporary files; hopeful... | Morgan Deters |
| 2011-03-14 | Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array b... | Morgan Deters |
| 2011-03-10 | Fix bug 246 (occasional buffer overflow related to varargs in assertion-failu... | Morgan Deters |
| 2011-03-10 | ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds. F... | Morgan Deters |
| 2011-03-08 | Clean up Theory base class as per code review bug #60; also fixes to CodeTime... | Morgan Deters |
| 2011-03-08 | - Merges queue-interrogation branch into the trunk. This branch adds extra ph... | Tim King |
| 2011-03-07 | Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now ... | Tim King |
| 2011-03-05 | - Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The d... | Tim King |
| 2011-03-05 | Enables the PreferenceFunction minBoundAndRowCount. | Tim King |
| 2011-03-05 | - Adds "PreferenceFunction" to SimplexDecisionProcedure. A PreferenceFunctio... | Tim King |
| 2011-03-05 | - Made Rational::sgn() function const. | Tim King |
| 2011-03-05 | adding three features to CVC parser that drastically improve its support for ... | Morgan Deters |
| 2011-03-03 | fix for bug #244, "Segfault if file cannot be found and --stats is on" | Morgan Deters |
| 2011-03-03 | - Creates a queue for lemmas discovered during the simplex procedure. Lemmas ... | Tim King |
| 2011-03-03 | resurrecting triple.h from r1023 (after which it was removed) | Morgan Deters |
| 2011-03-03 | Merged the tableau-copy branch into trunk. This adds a copy constructor and o... | Tim King |
| 2011-03-03 | fixing a type that caused the segfaults in the regressions | Dejan Jovanović |
| 2011-03-02 | fixing the big with lemma reallocation in minisat garbage collection | Dejan Jovanović |
| 2011-02-28 | CongruenceClosure module now should support nullary congruence operators (now... | Morgan Deters |
| 2011-02-28 | Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts... | Morgan Deters |
| 2011-02-28 | minor doxygen build target fixes | Morgan Deters |
| 2011-02-28 | Review of statistics code. Added lots of documentation, and fixed an issue (... | Morgan Deters |
| 2011-02-27 | - Adds a path for Theory to be passed a reference to Options. | Tim King |
| 2011-02-27 | - Makes VarCoeffPair a class instead of a typedef of pair<ArithVar, Rational>... | Tim King |
| 2011-02-27 | - Adds a buffer to the ReducedRowVector addRowTimesConstant operation to redu... | Tim King |
| 2011-02-26 | - Merged RowVector and ReducedRowVector. | Tim King |
| 2011-02-26 | Commit to fix bug 241 (improper "using namespace std" in a header). This cau... | Morgan Deters |
| 2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
| 2011-02-26 | fix serious regression breakage (segfaults) caused by an off-by-one error in ... | Morgan Deters |
| 2011-02-26 | adding the variables count to the statistics in the expr manager | Dejan Jovanović |
| 2011-02-26 | adding statistics about how many different kinds of expressions we have creat... | Dejan Jovanović |
