summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-02-28minor doxygen build target fixesMorgan Deters
2011-02-28Review 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-26Commit to fix bug 241 (improper "using namespace std" in a header). This cau...Morgan Deters
2011-02-26Merge from theory-break-dependences branch to break Theory and TheoryEngine d...Morgan Deters
2011-02-26fix serious regression breakage (segfaults) caused by an off-by-one error in ...Morgan Deters
2011-02-26adding the variables count to the statistics in the expr managerDejan Jovanović
2011-02-26adding statistics about how many different kinds of expressions we have creat...Dejan Jovanović
2011-02-25- This commit adds some debugging information to ArithPriorityQueue.Tim King
2011-02-25slicing manager is not breaking the old regressions, time to syncDejan Jovanović
2011-02-24- Adds an additional round of checks for a conflict after the difference heur...Tim King
2011-02-24- Adds an additional mode to ArithPriorityQueue, Collection. Collection is a ...Tim King
2011-02-24- Changes ArithPriorityQueue to use stl::vector<>'s plus stl's heap algorithm...Tim King
2011-02-22- Adds column based iterators.Tim King
2011-02-21- Adds the ArithPriorityQueue class. The ArithPriorityQueue class provides an...Tim King
2011-02-21- Adds the statistic d_avgNumRowsNotContainingOnPivot.Tim King
2011-02-19Changes:Tim King
2011-02-18Changes:Tim King
2011-02-17This commit merges the branch branches/arithmetic/quick-row-has into trunk. q...Tim King
2011-02-17This commit is the promised clean up after removing row ejection.Tim King
2011-02-17Removed ActivityMonitor from arithmetic. This was only used for row ejection,...Tim King
2011-02-17Row ejection is now completely disabled. Another commit cleaning this one up ...Tim King
2011-02-17Removed vestigial normal form notes file from src/theory/arith/Makefile.am. S...Tim King
2011-02-17some unit tests to work on slicingDejan Jovanović
2011-02-17I replaced the pattern "x = x + y;" with "x += y;" in a few places in DeltaRa...Tim King
2011-02-17Updates based on the group code review of arithmetic on 2011-02-15. The only...Tim King
2011-02-17Deleting depricated files.Tim King
2011-02-17getting ready for slicing bitvectorsDejan Jovanović
2011-02-16Overview of the changes:Tim King
2011-02-16updates for the rewriter, added some statisticsDejan Jovanović
2011-02-14Reverses the order of the d_possiblyInconsistent queue. (It is that old termi...Tim King
2011-02-133 heuristics were added to arithmetic. A heuristic for detecting an encoding ...Tim King
2011-01-05fix for build errorsDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-17tls.h, rational.h, and integer.h are only re-generated if changed. this obvi...Morgan Deters
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-12-14make some CC module methods private that should not have been publicMorgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-12-14permit PARAMETERIZED operators to be zero-aryMorgan Deters
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan Deters
2010-11-24Changin the get() semantics to a CDQeue-sque semantics. Dejan Jovanović
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-19add statistics support information to --show-configMorgan Deters
2010-11-18small changes to documentation; also, '\''make doc'\'' doesn't build dot grap...Morgan Deters
2010-11-17fix improper CongruenceClosureWhite test by merging from a uf branch; fixes t...Morgan Deters
2010-11-17add some stats to UF/CCMorgan Deters
2010-11-17The "UF engineering issues" release, after much profiling.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback