| 2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw |
| 2013-06-25 |
Morgan Deters | Support for abs, to_int, is_int, divisible in SMT-LIB... |
blob | commitdiff | raw |
| 2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
| 2013-03-21 |
lianah | Merge branch 'master' into bv-core |
blob | commitdiff | raw | diff to current |
| 2013-03-21 |
Morgan Deters | Better error in case of nonlinear assertions while... |
blob | commitdiff | raw | diff to current |
| 2013-02-02 |
lianah | merged master into branch |
blob | commitdiff | raw | diff to current |
| 2012-12-15 |
Tim King | Merging in patch from branch '1.0.x'. |
blob | commitdiff | raw | diff to current |
| 2012-12-15 |
Tim King | Merge remote-tracking branch 'main-repo/1.0.x' into... |
blob | commitdiff | raw | diff to current |
| 2012-12-15 |
Tim King | Changing the rewriter to use Boute's Euclidean definiti... |
blob | commitdiff | raw | diff to current |
| 2012-11-12 |
Tim King | Improved error reporting for improperly using non-linea... |
blob | commitdiff | raw | diff to current |
| 2012-11-11 |
Tim King | Fixes for the arithmetic normal form and rewriter to... |
blob | commitdiff | raw | diff to current |
| 2012-11-08 |
Tim King | Improved support for division by zero. This adds the... |
blob | commitdiff | raw | diff to current |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
| 2012-09-10 |
Tim King | Fixed an error in the rewriter Pascal pointed out.... |
blob | commitdiff | raw | diff to current |
| 2012-08-03 |
Morgan Deters | fix uses of getMetaKind() from outside the expr package... |
blob | commitdiff | raw | diff to current |
| 2012-05-15 |
Tim King | This commit removes the CONST_INTEGER kind from nodes... |
blob | commitdiff | raw | diff to current |
| 2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
blob | commitdiff | raw | diff to current |
| 2012-03-28 |
Tim King | Update to the ArithRewriter to remove REWRITE_AGAIN_FUL... |
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-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
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-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-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
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-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
blob | commitdiff | raw | diff to current |
| 2011-03-30 |
Tim King | Added the command line flag --rewrite-arithmetic-equali... |
blob | commitdiff | raw | diff to current |
| 2011-03-17 |
Tim King | - Removes arith_constants.h |
blob | commitdiff | raw | diff to current |
| 2011-02-26 |
Morgan Deters | Commit to fix bug 241 (improper "using namespace std... |
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-10-23 |
Tim King | Removed slack.h, and arith_activity.h. Replaced IsBasic... |
blob | commitdiff | raw | diff to current |
| 2010-09-13 |
Tim King | * New normal form for arithmetic is in place. |
blob | commitdiff | raw |
| 2010-08-19 |
Morgan Deters | UF theory bug fixes, code cleanup, and extra debugging... |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Tim King | Fixes arith rewriter to allow for division by a constan... |
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-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-05-28 |
Tim King | Bug fixes for combining coefficients of rewritten nodes. |
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-26 |
Tim King | Fix for bug 131. Added some additional debugging assert... |
blob | commitdiff | raw | diff to current |
| 2010-05-25 |
Tim King | Added Rational constructors that only take a numerator... |
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