Age | Commit message (Expand) | Author |
2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
2014-04-29 | Fix simplify output for SMT2 printer. | Morgan Deters |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-04-03 | Properly quote symbols in SMT-LIB printer. | Morgan Deters |
2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang |
2014-03-27 | adds new feature: re.loop | Tianyi Liang |
2014-03-19 | Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting. | Morgan Deters |
2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King |
2014-02-28 | add re.nostr for the empty regular expression; add re.allchar for the regular... | Tianyi Liang |
2014-02-28 | a new regular expression engine for solving both positive and negative member... | Tianyi Liang |
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal |
2014-02-26 | smt-lib syntax change: str.contain -> str.contains; add some prefix syntax fo... | Tianyi Liang |
2014-02-25 | New translation work, support Z3-str-style string constraints. | Morgan Deters |
2014-02-21 | add new theory (sets) | Kshitij Bansal |
2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang |
2014-02-17 | type conversion | Tianyi Liang |
2014-02-14 | partial function charat | Tianyi Liang |
2014-01-29 | add prefixof, suffixof | Tianyi Liang |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang |
2014-01-18 | strings with new ideas | Tianyi Liang |
2014-01-17 | Merge branch '1.3.x' | Morgan Deters |
2014-01-17 | Fix for quote-escaping in smt2 printer | Morgan Deters |
2014-01-16 | adds partial functions | Tianyi Liang |
2014-01-15 | adds smt2 print for strings | Tianyi Liang |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters |
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-12-05 | Fixes related to parametric datatype printing. | Morgan Deters |
2013-12-02 | SExpr pretty-printing for :all-options and :all-statistics. | Morgan Deters |
2013-11-27 | General pre-release cleanup commit | Morgan Deters |
2013-11-26 | Fix a segfault in the printer infrastructure when called from API and no lang... | Morgan Deters |
2013-11-19 | Add fair strategy for finite model finding multiple sorts --uf-ss-fair. | Andrew Reynolds |
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 |