Age | Commit message (Expand) | Author |
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 |
2012-03-07 | fix some Java compatibility-layer interface problems; also fix some Mac OS X ... | Morgan Deters |
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
2012-02-28 | This commit merges in branches/arithmetic/internalbb up to revision 2831. Th... | Tim King |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2012-02-22 | Fixes to documentation / fixes for MacOS | Morgan Deters |
2012-02-21 | fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on platf... | Morgan Deters |
2012-02-21 | don't require libboost_thread (its presence is detected at configure-time), a... | Morgan Deters |
2012-02-20 | fix "make dist" | Morgan Deters |
2012-02-20 | portfolio merge | Morgan Deters |
2012-02-20 | By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1 | Morgan Deters |