| Age | Commit message (Expand) | Author |
|---|
| 2014-06-21 | Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ... | Morgan Deters |
| 2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
| 2014-04-14 | Add initial support for co-datatypes. | Andrew Reynolds |
| 2014-04-09 | Minor change to better support parameterized partial/total kinds (for upcomin... | Morgan Deters |
| 2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-11-27 | General pre-release cleanup commit | Morgan Deters |
| 2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
| 2013-09-11 | Theory of strings. | Tianyi Liang |
| 2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters |
| 2013-03-19 | Minor cleanup of sources | Morgan Deters |
| 2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |
| 2012-12-01 | Fix the way abstract values are typed; fixes some compliance issues. | Morgan Deters |
| 2012-11-29 | Fixing function models with Boolean terms. Also, LAMBDA's should not be const. | Clark Barrett |
| 2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-10 | Abstract values for SMT-LIB. | Morgan Deters |
| 2012-09-26 | Fix type checking for define-funs (resolves bug 398). | Morgan Deters |
| 2012-09-26 | The Tuesday Afternoon Catch-All Commit (TACAC): | Morgan Deters |
| 2012-09-24 | some api changes | Dejan Jovanović |
| 2012-09-21 | SMT-LIBv2 compliance updates: | Morgan Deters |
| 2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
| 2012-09-12 | Adding model assertions after SAT responses. | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-27 | * Reversing commit r4258 (which disabled failing regressions). Fixed the pro... | Morgan Deters |
| 2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
| 2012-08-24 | fix get-value output in a couple ways; this fixes bug #378 | Morgan Deters |
| 2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
| 2012-08-13 | Minor cleanup. No performance difference expected. | Morgan Deters |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 2012-08-03 | ArrayStoreAll infrastructure | Morgan Deters |
| 2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
| 2012-08-01 | some fixes for Mac OS | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
| 2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for arith... | Tim King |
| 2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
| 2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
| 2012-02-28 | fix theory "kinds" file documentation for allowed arity of operators | Morgan Deters |
| 2012-02-20 | portfolio merge | Morgan Deters |
| 2012-02-04 | support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now ass... | Andrew Reynolds |
| 2011-11-04 | STRING_TYPE and CONST_STRING and associate type infrastructure implemented. | Morgan Deters |
