| 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-30 |
lianah | fixed merge conflicts |
blob | commitdiff | raw | diff to current |
| 2013-04-26 |
Tim King | FCSimplex branch merge |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Tim King | Making arithmetic model reversion on unsat checks an... |
blob | commitdiff | raw | diff to current |
| 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-04-01 |
Tim King | Cleaning up the demand restart code. |
blob | commitdiff | raw | diff to current |
| 2013-04-01 |
Tim King | Adding a restart test strategy to integers. |
blob | commitdiff | raw | diff to current |
| 2013-03-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-14 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-01 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-26 |
lianah | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-17 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-16 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-15 |
Tim King | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-08 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-05 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-02 |
lianah | merged master into branch |
blob | commitdiff | raw | diff to current |
| 2013-02-01 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-31 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-01-31 |
Tim King | Adding a heuristic to more eagerly split bounded intege... |
blob | commitdiff | raw | diff to current |
| 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 |
Tim King | Adding substitution size cap. |
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-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-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-11-26 |
Dejan Jovanović | Adding support for a master equality engine. Each theor... |
blob | commitdiff | raw | diff to current |
| 2012-11-26 |
Tim King | Improving arithmetic debugging output. |
blob | commitdiff | raw | diff to current |
| 2012-11-25 |
Tim King | This commit fixes two incompleteness bugs (461, 459... |
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-14 |
Andrew Reynolds | replaced all static member data from rewrite rule trigg... |
blob | commitdiff | raw | diff to current |
| 2012-11-14 |
Tim King | Fixed a typo in r4576 |
blob | commitdiff | raw | diff to current |
| 2012-11-14 |
Tim King | Fix to bug449. Adds shared constants to the set of... |
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-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 | Turns on TheoryUF when non-linear arithmetic is turned... |
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-11-07 |
Tim King | Fix to a bug in integer mod lemmas. |
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-19 |
Tim King | Fix for model building with shared terms for arithmetic. |
blob | commitdiff | raw | diff to current |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
| 2012-10-02 |
Morgan Deters | * re-enable some Z3 extended commands: |
blob | commitdiff | raw | diff to current |
| 2012-09-30 |
Morgan Deters | minor changes to arithmetic assertions involving nonlin... |
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-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
| 2012-08-14 |
Tim King | Implements TheoryArith::collectModelInfo(). The curren... |
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-07-31 |
Morgan Deters | Options merge. This commit: |
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-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
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 | Fixing a bug in proof production for the DioSolver. |
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-16 |
Tim King | Fixing if condition for trivial equalities in arithmeti... |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Tim King | Fixing a case for explanation of non-normal form equali... |
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 |
Morgan Deters | The "no-tears-in-competition-mode" commit. Change... |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Kshitij Bansal | fix cout, fix statname, rm deadcode |
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 witnesses to Constraints. |
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 |
Tim King | Fix to term normalization of integer equalities. Adds... |
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-17 |
Tim King | This fixes a fascinating segfault. This is the sequenc... |
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-05-14 |
Dejan Jovanović | fixes for shared term registration. previously the... |
blob | commitdiff | raw | diff to current |
| 2012-05-11 |
Tim King | Partially fixes something-like-a-problem with TheoryAri... |
blob | commitdiff | raw | diff to current |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
blob | commitdiff | raw | diff to current |
| 2012-05-07 |
Tim King | Fixing a bug with TheoryArith::ppAssert() and shared... |
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 |
| next |
projects / cvc5.git / history