Age | Commit message (Expand) | Author |
2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
2012-11-16 | Fix dumping of array-select expressions in CVC native language. | Morgan Deters |
2012-11-14 | Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ... | Tim King |
2012-11-12 | minor bug fixes for quantifiers, added sort inference module (not ready to be... | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-10-06 | * Clean up some options documentation | Morgan Deters |
2012-10-05 | Bug-related: | Morgan Deters |
2012-10-05 | BoolExpr removed and replaced with Expr | Dejan Jovanović |
2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
2012-09-28 | Public interface review items: | Morgan Deters |
2012-09-27 | * Rename SMT parts (printer, parser) to SMT1 | Morgan Deters |
2012-09-26 | Finish off SEXPR kind work. | Morgan Deters |
2012-09-24 | some api changes | Dejan Jovanović |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-09-21 | Fixes for datatype dumping and printing. Add a new test case for dumping. | Morgan Deters |
2012-09-21 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-09-20 | some bugfixes that come as a result of debugging some CASCADE/C stuff.. | Morgan Deters |
2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
2012-09-18 | SMT-LIBv2 compliance regarding outputting "unknown". | Morgan Deters |
2012-09-14 | Fix a few minor issues in options processing, improving usability, consistenc... | Morgan Deters |
2012-09-12 | Adding model assertions after SAT responses. | Morgan Deters |
2012-09-11 | Partially reverting the changes made in 4308. There is now both an Expr and N... | Tim King |
2012-09-10 | modified getValue to return Expr instead of Node | Andrew Reynolds |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-25 | fix unit tests | 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-09 | minor isConst()-related fixes to printing; also add some debugging stuff to s... | Morgan Deters |
2012-08-06 | fix constant printing for datatypes | Dejan Jovanović |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-17 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-07-14 | Applying Dejan's patch for bug #369, which resolves it by adding a new (let..... | Morgan Deters |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot |
2012-06-14 | some changes to make CVC4 work nicely with trace executor for application tra... | Morgan Deters |
2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-11 | fix issue referred to in bug 352 regarding infinite loop between Substitution... | 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-08 | Extend Printer infrastructure also to the "Result" class, meaning that differ... | Morgan Deters |
2012-06-07 | Adding EchoCommand and associated printer and parser rules: | Morgan Deters |
2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King |
2012-05-17 | Fixed bug 338: | Liana Hadarean |
2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
2012-04-06 | * Smt2 printer for datatypes | François Bobot |
2012-04-06 | * Fix ITEs and functions in CVC language printer. | Morgan Deters |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |