summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Expand)Author
2015-01-19Adding tests for get-value output for arithmetic.Tim King
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2015-01-08switch ascii encoding to unsigned charTianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-03Floating point infrastructure.Martin Brain
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-08Add unsat cores support to CVC native language.Morgan Deters
2014-10-06Print array constants in SMT-LIB models with new syntax.Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks Christo...Morgan Deters
2014-10-03More array constants and parsing: better error messages, extend to CVC presen...Morgan Deters
2014-10-03Minor fixes to CVC printer.Morgan Deters
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-23Unsat core printing.Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-22Fix operator-printing issue in SMT2.Morgan Deters
2014-07-10membership cvc token changed to `IS_IN' to avoid conflict with IN used for letKshitij Bansal
2014-07-09sets cvc printerKshitij Bansal
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback