| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-04-20 | numerous bugfixes | Morgan Deters |
| 2011-04-18 | Partial merge from datatypes-merge branch: | Morgan Deters |
| 2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
| 2011-02-26 | Commit to fix bug 241 (improper "using namespace std" in a header). This cau... | Morgan Deters |
| 2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
| 2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
| 2010-11-19 | Merge from ufprop branch, including: | Morgan Deters |
| 2010-11-16 | Added Theory::presolve(). | Tim King |
| 2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ... | Morgan Deters |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
| 2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ... | Morgan Deters |
