summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ...Dejan Jovanović
2011-08-24Simplification of the preregister and register throught a NodeVisitor class. ...Dejan Jovanović
2011-07-06Fixing two bugs:Dejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30Merging the playground branch upto r1957 into trunk.Tim King
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's m...Morgan Deters
2011-05-31This commit contains the code for allowing arbitrary equalities in the theory...Tim King
2011-05-26apply arithmetic static learner's miplibtrick in a consistent order (for easi...Morgan Deters
2011-05-06Deleting dead code.Tim King
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-04-25Monday tasks:Morgan Deters
2011-04-25Weekend work. The main points:Morgan Deters
2011-04-18Removing dead code that came in on commit r1740.Tim King
2011-04-18This commit merges the branch arithmetic/propagation-again into trunk.Tim King
2011-04-04Reverts previous commit r1636.Tim King
2011-04-02Delayed the addition of unate propagation lemmas until propagation is called....Tim King
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-30Added the command line flag --rewrite-arithmetic-equalities. This sets a sta...Tim King
2011-03-30Merged the branch sparse-tableau into trunk.Tim King
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-22Merges the small changes on the queue-period branch into trunk. This branch ...Tim King
2011-03-19Merges 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-17Switched SimplexDecisionProcedure::d_delayedLemmas from a vector to a queue.Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback