summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Expand)Author
2014-01-18strings with new ideasTianyi Liang
2014-01-17Merge branch '1.3.x'Morgan Deters
2014-01-17Fix for quote-escaping in smt2 printerMorgan Deters
2014-01-16adds partial functionsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2013-12-24Merge branch '1.3.x'Morgan Deters
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fixes related to parametric datatype printing.Morgan Deters
2013-12-02SExpr pretty-printing for :all-options and :all-statistics.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-26Fix a segfault in the printer infrastructure when called from API and no lang...Morgan Deters
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-27Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-09another fix for array-store-all printingMorgan Deters
2013-06-09Better array-store-all output for SMT-LIB.Morgan Deters
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-29SMT-LIB printer updates (some missing cases).Morgan Deters
2013-05-14Add support for quantifier patterns in smt2 printer.Andrew Reynolds
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as datatype...Andrew Reynolds
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ...Morgan Deters
2012-12-18Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-15Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
2012-12-01another part of last commitMorgan Deters
2012-11-30internal variables (skolems) aren't printed as part of the modelMorgan Deters
2012-11-30Partial fix for bug 435; still needs some effort.Morgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-11-27Tuples 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-16Fix dumping of array-select expressions in CVC native language.Morgan Deters
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to be...Andrew Reynolds
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback