| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-10-17 | Sharing work | Dejan Jovanović |
| 2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
| 2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
| 2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
| 2011-06-01 | minor fix, and better output for type errors | Morgan Deters |
| 2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
| 2011-04-25 | Monday tasks: | Morgan Deters |
| 2011-04-25 | Weekend work. The main points: | Morgan Deters |
