| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw |
| 2012-03-28 |
Dejan Jovanović | enabling the --disable-arithmetic-propagation option... |
blob | commitdiff | raw | diff to current |
| 2012-03-23 |
Tim King | Removed the variableRemovalEnabled option and d_removed... |
blob | commitdiff | raw | diff to current |
| 2012-03-22 |
Dejan Jovanović | * improving arithmetic getEqualityStatus |
blob | commitdiff | raw | diff to current |
| 2012-03-08 |
Dejan Jovanović | Removing QUICK_CHECK, and other unused ones, from the... |
blob | commitdiff | raw | diff to current |
| 2012-03-02 |
Tim King | This commit merges in the changes from branches/arithme... |
blob | commitdiff | raw | diff to current |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
blob | commitdiff | raw | diff to current |
| 2012-03-01 |
Tim King | Fixed a copy paste error where a lower bound was looked... |
blob | commitdiff | raw | diff to current |
| 2012-02-28 |
Tim King | This commit merges in branches/arithmetic/internalbb... |
blob | commitdiff | raw | diff to current |
| 2012-02-25 |
Dejan Jovanović | ppAsert -> ppAssert |
blob | commitdiff | raw | diff to current |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes: |
blob | commitdiff | raw | diff to current |
| 2012-02-22 |
Tim King | Fix for bug 305. |
blob | commitdiff | raw | diff to current |
| 2012-02-22 |
Morgan Deters | Fixes to documentation / fixes for MacOS |
blob | commitdiff | raw | diff to current |
| 2012-02-20 |
Morgan Deters | portfolio merge |
blob | commitdiff | raw | diff to current |
| 2012-02-16 |
Tim King | Last commit accidentally lacked r2778 and r2779 from... |
blob | commitdiff | raw | diff to current |
| 2012-02-15 |
Tim King | This commit merges into trunk the branch branches/arith... |
blob | commitdiff | raw | diff to current |
| 2011-12-15 |
Tim King | Partial fix to bug 295. |
blob | commitdiff | raw | diff to current |
| 2011-12-15 |
Tim King | Fix to the previous commit. |
blob | commitdiff | raw | diff to current |
| 2011-12-15 |
Tim King | Partial fix in arithmetic for propagating shared terms... |
blob | commitdiff | raw | diff to current |
| 2011-11-29 |
Tim King | Merging the branch branches/arithmetic/shared-terms... |
blob | commitdiff | raw | diff to current |
| 2011-10-19 |
Tim King | Merging the branch branches/arithmetic/push-pop-support... |
blob | commitdiff | raw | diff to current |
| 2011-10-17 |
Dejan Jovanović | Sharing work |
blob | commitdiff | raw | diff to current |
| 2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
blob | commitdiff | raw | diff to current |
| 2011-09-15 |
Dejan Jovanović | tim's fixes for context-dependent pre-registration |
blob | commitdiff | raw | diff to current |
| 2011-09-15 |
Dejan Jovanović | additional stuff for sharing, |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
blob | commitdiff | raw | diff to current |
| 2011-08-24 |
Dejan Jovanović | Simplification of the preregister and register throught... |
blob | commitdiff | raw | diff to current |
| 2011-07-06 |
Dejan Jovanović | Fixing two bugs: |
blob | commitdiff | raw | diff to current |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw | diff to current |
| 2011-06-30 |
Morgan Deters | only use theory registration if (1) a theory requests... |
blob | commitdiff | raw | diff to current |
| 2011-05-31 |
Tim King | This commit contains the code for allowing arbitrary... |
blob | commitdiff | raw | diff to current |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Tim King | Removing dead code that came in on commit r1740. |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Tim King | This commit merges the branch arithmetic/propagation... |
blob | commitdiff | raw | diff to current |
| 2011-04-04 |
Tim King | Reverts previous commit r1636. |
blob | commitdiff | raw | diff to current |
| 2011-04-02 |
Tim King | Delayed the addition of unate propagation lemmas until... |
blob | commitdiff | raw | diff to current |
| 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 |
| next |
projects / cvc5.git / history