| 2013-01-31 |
Tim King | Adding a heuristic to more eagerly split bounded intege... |
blob | commitdiff | raw |
| 2013-01-28 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-27 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-23 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-22 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-22 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-19 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2012-12-22 |
Dejan Jovanović | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2012-12-18 |
Morgan Deters | Merge branch '1.0.x' |
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-12 |
Dejan Jovanović | Merge pull request #2 from CVC4/1.0.x |
blob | commitdiff | raw | diff to current |
| 2012-12-11 |
Morgan Deters | Merge branch '1.0.x', getting fix for bug 480 |
blob | commitdiff | raw | diff to current |
| 2012-12-11 |
Morgan Deters | Merge branch '1.0.x' (getting fix for bug 479) |
blob | commitdiff | raw | diff to current |
| 2012-12-11 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2012-12-08 |
Morgan Deters | Merge from 1.0.x (bugfix for 476). |
blob | commitdiff | raw | diff to current |
| 2012-12-07 |
François Bobot | Merge release branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2012-12-06 |
François Bobot | Merge branch 'release-1.0.x' |
blob | commitdiff | raw | diff to current |
| 2012-12-05 |
Tim King | Improved garbage collection for TheoryArith. The merge... |
blob | commitdiff | raw | diff to current |
| 2012-12-05 |
Tim King | This commit merges in CDTrailHashMap and CDInsertHashMa... |
blob | commitdiff | raw | diff to current |
| 2012-12-01 |
Andrew Reynolds | drastic simplification of quantifiers code regarding... |
blob | commitdiff | raw | diff to current |
| 2012-11-26 |
Dejan Jovanović | Adding support for a master equality engine. Each theor... |
blob | commitdiff | raw | diff to current |
| 2012-11-21 |
Tim King | - Removes getDeltaValueWithNonlinear() entirely |
blob | commitdiff | raw | diff to current |
| 2012-11-19 |
Tim King | Fix for bug452. |
blob | commitdiff | raw | diff to current |
| 2012-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code revie... |
blob | commitdiff | raw | diff to current |
| 2012-11-12 |
Tim King | Delta is now generated in arithmetic to keep consistent... |
blob | commitdiff | raw | diff to current |
| 2012-11-10 |
Tim King | Fix for bug 439. Delta computation now includes disequa... |
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-24 |
Tim King | Updated the ArithStaticLearner to be user context depen... |
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-29 |
Tim King | Calling the setIncompleteness() flag on all full checks... |
blob | commitdiff | raw | diff to current |
| 2012-09-29 |
Tim King | This commit add interpretation by lemma for INTS_DIVISI... |
blob | commitdiff | raw | diff to current |
| 2012-09-22 |
Morgan Deters | Separate public-facing and internal-facing interfaces... |
blob | commitdiff | raw | diff to current |
| 2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
blob | commitdiff | raw | diff to current |
| 2012-07-07 |
Morgan Deters | Various fixes to documentation---typos, some incomplete... |
blob | commitdiff | raw | diff to current |
| 2012-06-27 |
Tim King | This adds TheoryArith::safeToReset(). This fixes bug... |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Tim King | Fixing a bug related to explaining propagations with... |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Tim King | Fixed arithmetic consistency issue. The simplex confli... |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Tim King | Brings the tuning branch into trunk. This includes... |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Tim King | - Added a loop to internally assert constraints that... |
blob | commitdiff | raw | diff to current |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
| 2012-05-22 |
Tim King | This commit merges in the branch arithmetic/cprop. |
blob | commitdiff | raw | diff to current |
| 2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
blob | commitdiff | raw | diff to current |
| 2012-05-17 |
Tim King | This fixes a fascinating segfault. This is the sequenc... |
blob | commitdiff | raw | diff to current |
| 2012-05-04 |
Tim King | - This fixes a problem where simplex produced the same... |
blob | commitdiff | raw | diff to current |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
blob | commitdiff | raw | diff to current |
| 2012-04-27 |
Tim King | This merges in the branch cvc4/branches/arithmetic... |
blob | commitdiff | raw | diff to current |
| 2012-04-24 |
Tim King | This commit merges in the branch branches/arithmetic... |
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-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-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-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-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-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ć | 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-09-02 |
Dejan Jovanović | * Changing pre-registration to be context dependent... |
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-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 | 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-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
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-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 | Merged the tableau-copy branch into trunk. This adds... |
blob | commitdiff | raw | diff to current |
| 2011-02-27 |
Tim King | - Adds a path for Theory to be passed a reference to... |
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-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 | Removed ActivityMonitor from arithmetic. This was only... |
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-16 |
Tim King | Added Theory::presolve(). |
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-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
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-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-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
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 |
| next |
projects / cvc5.git / history