| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-02-16 | Last commit accidentally lacked r2778 and r2779 from integer2. I have manual... | Tim King |
| 2012-02-15 | This commit merges into trunk the branch branches/arithmetic/integers2 from r... | Tim King |
| 2012-02-12 | copyright year updated to 2012 | Morgan Deters |
| 2011-12-14 | added minor documentation for parametric datatypes, for bug 283 | Andrew Reynolds |
| 2011-11-22 | More language bindings work: | Morgan Deters |
| 2011-11-16 | Addressed many of the concerns raised in the public interface review of CVC4 ... | Morgan Deters |
| 2011-11-15 | Bindings work (ocaml bindings are now sort of working); also minor cleanup | Morgan Deters |
| 2011-11-15 | additional minor changes to get python binding on better footing | Morgan Deters |
| 2011-11-15 | fixes for python language binding, added python example | Morgan Deters |
| 2011-11-06 | datatype stuff in compatibility interface implemented | Morgan Deters |
| 2011-11-04 | STRING_TYPE and CONST_STRING and associate type infrastructure implemented. | Morgan Deters |
| 2011-11-02 | Only print a shortlist of most-commonly-used options on option processing err... | Morgan Deters |
| 2011-11-02 | give an option error if the user specifies --proof in a non-proof-enabled build | Morgan Deters |
| 2011-11-02 | better Integer asserts when there's overflow on conversion to unsigned long /... | Morgan Deters |
| 2011-10-31 | fixes to assertions in GMP to match CLN behavior | Morgan Deters |
| 2011-10-31 | Added assertions to the CLN implementation of Integer for getLong() and getUn... | Tim King |
| 2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |
| 2011-10-28 | * ability to output NodeBuilders without first converting them to Nodes---use... | Morgan Deters |
| 2011-10-28 | merged the proofgen3 branch into trunk: | Liana Hadarean |
| 2011-10-25 | Initialize resource limit and millisecond limit options | Kshitij Bansal |
| 2011-10-23 | Implement changes from yesterday morning's meeting (10/21/2011): | Morgan Deters |
| 2011-10-21 | add gcc version information to Configuration, and warn when building with v4.... | Morgan Deters |
| 2011-10-17 | Sharing work | Dejan Jovanović |
