| Age | Commit message (Expand) | Author |
|---|
| 2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
| 2012-06-14 | fix cout, fix statname, rm deadcode | Kshitij Bansal |
| 2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
| 2012-06-12 | fix ordering issue of --dump-to and --default-dag-thresh. now can be specifi... | Morgan Deters |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-09 | Cleanup and comments for the dag-ifier. Also some unit testing for it. | Morgan Deters |
| 2012-06-09 | Dagification of output expressions. | Morgan Deters |
| 2012-06-08 | The option --arith-presolve-lemmas had previously been renamed --unate-lemmas. | Morgan Deters |
| 2012-06-08 | Extend Printer infrastructure also to the "Result" class, meaning that differ... | Morgan Deters |
| 2012-06-08 | minor fixes, for Mac OS | Morgan Deters |
| 2012-06-08 | threadlocal | Kshitij Bansal |
| 2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal |
| 2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
| 2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
| 2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett |
| 2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
| 2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for arith... | Tim King |
| 2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King |
| 2012-05-17 | Fixed bug 338: | Liana Hadarean |
| 2012-05-14 | in debug builds, -d can be used for trace tags that aren't also debug tags | Morgan Deters |
| 2012-05-13 | fixing build warnings | Dejan Jovanović |
| 2012-05-11 | fix regex in Debug_tags and Trace_tags generation for Mac OS | Morgan Deters |
| 2012-05-11 | fix typo in sed line | Morgan Deters |
| 2012-05-11 | Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory | Clark Barrett |
| 2012-05-11 | Added some ITE rewrites, | Clark Barrett |
| 2012-05-09 | fix an issue which breaks language bindings (so this commit fixes debian nigh... | Morgan Deters |
| 2012-05-09 | --disable-tracing at configure time now disables Trace() and Debug() gestures... | Morgan Deters |
| 2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
| 2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal |
| 2012-05-09 | Fixing the debug tags generation and related methods in configuration.cpp tha... | Dejan Jovanović |
| 2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
| 2012-05-04 | options: fail if the debug or trace tag specified doesn't exist (-d -t) | François Bobot |
| 2012-05-04 | fix: getNumTraceTags, getNumDebugTags | François Bobot |
| 2012-04-30 | Added map from skolem variables to new ite formulas in ite removal. | Clark Barrett |
| 2012-04-27 | This merges in the branch cvc4/branches/arithmetic/matrix into trunk. | Tim King |
| 2012-04-23 | Merge from decision branch -- partially working justification heuristic | Kshitij Bansal |
| 2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
| 2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
| 2012-04-13 | Fix SExpr name qualification for swig, and #include integer and rational head... | Morgan Deters |
| 2012-04-12 | Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds,... | Tim King |
| 2012-04-11 | merge from arrays-clark branch | Morgan Deters |
| 2012-04-06 | * Fix ITEs and functions in CVC language printer. | Morgan Deters |
| 2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean |
| 2012-04-02 | - Merged in the branch cdlist-cleanup. | Tim King |
| 2012-03-28 | fix swig-ignored interface name; hopefully fixes Debian package nightly builds | Morgan Deters |
| 2012-03-26 | Global registry of SAT solvers, where they are registered at compile time. Th... | Dejan Jovanović |
| 2012-03-23 | Removed the variableRemovalEnabled option and d_removedRows from TheoryArith.... | Tim King |
| 2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean |
| 2012-03-21 | Disable nonclausal simplification for QF_SAT benchmarks by default. | Morgan Deters |
| 2012-03-09 | Some work on the dump infrastructure to support portfolio work. | Morgan Deters |
