Age | Commit message (Expand) | Author |
2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters |
2013-09-05 | Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se... | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters |
2013-06-27 | Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod". | Morgan Deters |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-09 | another fix for array-store-all printing | Morgan Deters |
2013-06-09 | Better array-store-all output for SMT-LIB. | Morgan Deters |
2013-05-29 | Merge branch '1.2.x' | Morgan Deters |
2013-05-29 | SMT-LIB printer updates (some missing cases). | Morgan Deters |
2013-05-14 | Add support for quantifier patterns in smt2 printer. | Andrew Reynolds |
2013-05-01 | Fix to dumping re: boolean terms, datatypes | Morgan Deters |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters |
2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters |
2013-03-21 | Some model and printing fixes for defined functions in input. | Morgan Deters |
2013-03-20 | Properly |quote| symbols in SMT-LIBv2 output. | Morgan Deters |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters |
2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |
2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as datatype... | Andrew Reynolds |
2013-01-08 | SMT-LIB get-model output now is easier to machine-parse: contains (model...) ... | Morgan Deters |
2012-12-18 | Fix printing of EXISTS in CVC language printer | Morgan Deters |
2012-12-15 | Fix printing of EXISTS in CVC language printer | Morgan Deters |
2012-12-12 | * fixed bug 481 by adding check for division by 0 in bit-vector division circuit | lianah |
2012-12-01 | another part of last commit | Morgan Deters |
2012-11-30 | internal variables (skolems) aren't printed as part of the model | Morgan Deters |
2012-11-30 | Partial fix for bug 435; still needs some effort. | Morgan Deters |
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters |
2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters |
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 |