summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Expand)Author
2014-02-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17type conversionTianyi Liang
2014-02-14partial function charatTianyi Liang
2014-01-29add prefixof, suffixofTianyi Liang
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback