| 2011-04-02 |
Tim King | Delayed the addition of unate propagation lemmas until... |
blob | commitdiff | raw |
| 2011-03-30 |
Tim King | Merged the branch sparse-tableau into trunk. |
blob | commitdiff | raw | diff to current |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
| 2011-03-17 |
Tim King | SimplexDecisionProcedure no longer takes an OutputChann... |
blob | commitdiff | raw | diff to current |
| 2011-03-17 |
Tim King | - Removes arith_constants.h |
blob | commitdiff | raw | diff to current |
| 2011-03-16 |
Tim King | - Turns on the excluded middle assertions during the... |
blob | commitdiff | raw | diff to current |
| 2011-03-16 |
Tim King | - Turns on the miplibTrick. This detects during the... |
blob | commitdiff | raw | diff to current |
| 2011-03-15 |
Morgan Deters | Merge from cudd branch. This mostly just adds support... |
blob | commitdiff | raw | diff to current |
| 2011-03-07 |
Tim King | Merges branches/arithmetic/tableau-reset into the trunk... |
blob | commitdiff | raw | diff to current |
| 2011-03-03 |
Tim King | - Creates a queue for lemmas discovered during the... |
blob | commitdiff | raw | diff to current |
| 2011-03-03 |
Tim King | Merged the tableau-copy branch into trunk. This adds... |
blob | commitdiff | raw | diff to current |
| 2011-02-26 |
Morgan Deters | Merge from theory-break-dependences branch to break... |
blob | commitdiff | raw | diff to current |
| 2011-02-21 |
Tim King | - Adds the statistic d_avgNumRowsNotContainingOnPivot. |
blob | commitdiff | raw | diff to current |
| 2011-02-19 |
Tim King | Changes: |
blob | commitdiff | raw | diff to current |
| 2011-02-18 |
Tim King | Changes: |
blob | commitdiff | raw | diff to current |
| 2011-02-17 |
Tim King | This commit is the promised clean up after removing... |
blob | commitdiff | raw | diff to current |
| 2011-02-17 |
Tim King | Removed ActivityMonitor from arithmetic. This was only... |
blob | commitdiff | raw | diff to current |
| 2011-02-17 |
Tim King | Row ejection is now completely disabled. Another commit... |
blob | commitdiff | raw | diff to current |
| 2011-02-16 |
Tim King | Overview of the changes: |
blob | commitdiff | raw | diff to current |
| 2011-02-13 |
Tim King | 3 heuristics were added to arithmetic. A heuristic... |
blob | commitdiff | raw | diff to current |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-11-15 |
Tim King | This commit merges the arith-prop-opt branch into the... |
blob | commitdiff | raw | diff to current |
| 2010-11-12 |
Dejan Jovanović | Some bug fixes in the SAT for lemmas, and an experiment... |
blob | commitdiff | raw | diff to current |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
blob | commitdiff | raw | diff to current |
| 2010-11-03 |
Tim King | Adds statistics for the number of Uservariables and... |
blob | commitdiff | raw | diff to current |
| 2010-10-29 |
Tim King | Factors out the QF_LRA decision procedure from TheoryAr... |
blob | commitdiff | raw | diff to current |
| 2010-10-28 |
Tim King | The Row implementation has no been replaced by RowVecto... |
blob | commitdiff | raw | diff to current |
| 2010-10-23 |
Tim King | Removed slack.h, and arith_activity.h. Replaced IsBasic... |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Tim King | Code cleanup for TheoryArith. |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Tim King | Fixes to getValue for TheoryArith. |
blob | commitdiff | raw | diff to current |
| 2010-10-14 |
Tim King | Fixed computation of infinitesimals for arithmetic... |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Tim King | IDENTITY has been removed. |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Tim King | Small tableau optimization. |
blob | commitdiff | raw | diff to current |
| 2010-10-04 |
Tim King | Fix to bug 211. ArithVar is now typedefed to uint32_t. |
blob | commitdiff | raw | diff to current |
| 2010-10-02 |
Tim King | branches/arith-indexed-variables merged into the main... |
blob | commitdiff | raw | diff to current |
| 2010-09-21 |
Morgan Deters | part of review (bug #197): coding conventions, file... |
blob | commitdiff | raw | diff to current |
| 2010-09-13 |
Tim King | * New normal form for arithmetic is in place. |
blob | commitdiff | raw | diff to current |
| 2010-08-19 |
Morgan Deters | UF theory bug fixes, code cleanup, and extra debugging... |
blob | commitdiff | raw | diff to current |
| 2010-07-09 |
Dejan Jovanović | the tableaux optimization |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | Considerably simplified the way output streams are... |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | With "-d extra-checking", rewrites are now checked... |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | re-generated comment headers of source files |
blob | commitdiff | raw | diff to current |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
| 2010-06-29 |
Tim King | This commit merges the decaying-rows branch into the... |
blob | commitdiff | raw | diff to current |
| 2010-06-29 |
Tim King | Merging the unate-propagator branch into the trunk... |
blob | commitdiff | raw | diff to current |
| 2010-06-22 |
Tim King | Made ~Stat() virtual. Added some additional statistics... |
blob | commitdiff | raw | diff to current |
| 2010-06-18 |
Tim King | Merging the statistics branch into the main trunk.... |
blob | commitdiff | raw | diff to current |
| 2010-06-16 |
Tim King | Added the experimental. +bool TheoryArith::AssertEquali... |
blob | commitdiff | raw | diff to current |
| 2010-06-16 |
Tim King | More assorted changes to arithmetic in preparation... |
blob | commitdiff | raw | diff to current |
| 2010-06-16 |
Tim King | This commit just contains miscellaneous arithmetic... |
blob | commitdiff | raw | diff to current |
| 2010-06-14 |
Tim King | Fix to arith to make sure it only attempts to report... |
blob | commitdiff | raw | diff to current |
| 2010-06-06 |
Tim King | Some assorted fixes and local optimizations for theory... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Tim King | Changed how assignments are saved during check. These... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-06-03 |
Tim King | Fixes 2 issues with assignments. The first is construct... |
blob | commitdiff | raw | diff to current |
| 2010-06-01 |
Tim King | This commit adds a debugTagIsOn() guard around some... |
blob | commitdiff | raw | diff to current |
| 2010-05-29 |
Tim King | Couple of fixes to theory arith. pivotAndUpdate now... |
blob | commitdiff | raw | diff to current |
| 2010-05-28 |
Tim King | This update enables TheoryArith to accept assertions... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Tim King | Preregistration has been turned on. Highly experimental... |
blob | commitdiff | raw | diff to current |
| 2010-05-26 |
Tim King | . '+Outstanding case split in theory arith' |
blob | commitdiff | raw | diff to current |
| 2010-05-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand. |
blob | commitdiff | raw | diff to current |
| 2010-05-21 |
Tim King | Small fixes to TheoryArith. Added a hack to make Integ... |
blob | commitdiff | raw | diff to current |
| 2010-05-20 |
Tim King | Added the division symbol to the parser, and minimal... |
blob | commitdiff | raw | diff to current |
| 2010-05-19 |
Tim King | Significant revision to theory/arith. The new draft... |
blob | commitdiff | raw | diff to current |
| 2010-04-28 |
Tim King | Merging the arithmetic theory draft (lra-init) back... |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history