summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Expand)Author
2014-07-01Update copyrights.Morgan Deters
2014-06-30Merge pull request #47 from kbansal/setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are now...Kshitij Bansal
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-22Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:Morgan Deters
2014-06-22Minor cleanup stuff.Morgan Deters
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-19For casc : print models of functions rewritten by sort inference.ajreynol
2014-06-06Sets translate, and other short fixesKshitij Bansal
2014-06-05When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.Morgan Deters
2014-06-04Add operator support (resolves bug #563).Morgan Deters
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-04-29Fix simplify output for SMT2 printer.Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-03Properly quote symbols in SMT-LIB printer.Morgan Deters
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-19Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.Morgan Deters
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-28add re.nostr for the empty regular expression; add re.allchar for the regular...Tianyi Liang
2014-02-28a new regular expression engine for solving both positive and negative member...Tianyi Liang
2014-02-28rename kind::IN to kind::MEMBER (fixes some windows build conflicts)Kshitij Bansal
2014-02-26smt-lib syntax change: str.contain -> str.contains; add some prefix syntax fo...Tianyi Liang
2014-02-25New translation work, support Z3-str-style string constraints.Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback