| Age | Commit message (Expand) | Author |
|---|
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-29 | To the build system: | Morgan Deters |
| 2012-08-26 | Array constants finished and working. Unit tests for array constants. | Clark Barrett |
| 2012-08-25 | fix unit tests | Morgan Deters |
| 2012-08-22 | Cap finite cardinalities at 2^64, as discussed in the meeting last week. | Morgan Deters |
| 2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ... | Morgan Deters |
| 2012-08-16 | ArrayStoreAll should (for now) only allow constant expressions, as it is itse... | Morgan Deters |
| 2012-08-14 | Fixes to integer wrapper classes: | Morgan Deters |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 2012-08-04 | isConst() rule for datatypes | Morgan Deters |
| 2012-08-03 | Comparisons for LogicInfos, and associated tests | Morgan Deters |
| 2012-08-03 | ArrayStoreAll infrastructure | Morgan Deters |
| 2012-08-01 | fixes to some *clean targets | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-27 | removing unecessary files | Andrew Reynolds |
| 2012-07-26 | Datatype enumerator work. This version is not a "fair" enumerator, but I got... | Morgan Deters |
| 2012-07-16 | now passes "make distcheck", which does important checks for the release (e.g... | Morgan Deters |
| 2012-07-16 | fix compiler warning in unit test | Morgan Deters |
| 2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
| 2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
| 2012-07-14 | fix a warning in unit test compilation | Morgan Deters |
| 2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | 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-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
| 2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
| 2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
| 2012-05-17 | Fixing an issue with LogicInfo::isPure() that turned off simplification in QF... | Morgan Deters |
| 2012-05-15 | Implement TypeNode::isComparableTo() and add a unit test for it. | Morgan Deters |
| 2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
| 2012-05-15 | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively | Liana Hadarean |
| 2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
| 2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
| 2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
| 2012-04-28 | New LogicInfo functionality. | Morgan Deters |
| 2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
| 2012-04-02 | Fix for broken unit tests from the previous commit. | Tim King |
| 2012-04-02 | - Merged in the branch cdlist-cleanup. | Tim King |
| 2012-03-26 | More cleaning up. | Dejan Jovanović |
| 2012-03-26 | forgot to commit this one, fixing build errors | Dejan Jovanović |
| 2012-03-08 | Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. | Dejan Jovanović |
| 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-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
| 2012-02-22 | Added OutputChannel::propagateAsDecision() functionality, allowing a theory | Morgan Deters |
| 2012-02-06 | Fixing a bug in the integer unit tests when configured for GMP with assertion... | Tim King |
| 2011-12-06 | LemmaStatus changes, as agreed to during 12/2 meeting. | 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 |
