summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2011-03-17SimplexDecisionProcedure no longer takes an OutputChannel as a parameter.Tim King
2011-03-17- Removes arith_constants.hTim King
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-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-03-08- Merges queue-interrogation branch into the trunk. This branch adds extra ph...Tim King
2011-03-07Merges 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-05Enables the PreferenceFunction minBoundAndRowCount.Tim King
2011-03-05- Adds "PreferenceFunction" to SimplexDecisionProcedure. A PreferenceFunctio...Tim King
2011-03-03- Creates a queue for lemmas discovered during the simplex procedure. Lemmas ...Tim King
2011-03-03Merged the tableau-copy branch into trunk. This adds a copy constructor and o...Tim King
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-25- This commit adds some debugging information to ArithPriorityQueue.Tim King
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-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-16Overview of the changes:Tim King
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-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-11-16Added Theory::presolve().Tim King
2010-11-15cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in...Morgan Deters
2010-11-15This commit merges the arith-prop-opt branch into the main trunk. This was do...Tim King
2010-11-12Some bug fixes in the SAT for lemmas, and an experiment with a more complete ...Dejan Jovanović
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-04This commit adds the ejected and un-ejected statistics.Tim King
2010-11-03Adds size() to RowVector.Tim King
2010-11-03Adds statistics for the number of Uservariables and Slack variables used by a...Tim King
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-30Adds a hueristic from Alberto's thesis. For a fixed window the row count is u...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback