Age | Commit message (Expand) | Author |
2014-10-03 | Merge branch '1.4.x' | Morgan Deters |
2014-10-03 | Fix output of integer-valued real constants in SMT-LIB models (thanks Christo... | Morgan Deters |
2014-10-03 | More array constants and parsing: better error messages, extend to CVC presen... | Morgan Deters |
2014-10-03 | Minor fixes to CVC printer. | Morgan Deters |
2014-08-26 | Improved SMT-LIBv2 language support for unsat cores. | Morgan Deters |
2014-08-23 | Unsat core printing. | Morgan Deters |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters |
2014-08-22 | Fix operator-printing issue in SMT2. | Morgan Deters |
2014-07-10 | membership cvc token changed to `IS_IN' to avoid conflict with IN used for let | Kshitij Bansal |
2014-07-09 | sets cvc printer | Kshitij Bansal |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-06-30 | Merge pull request #47 from kbansal/sets | Kshitij Bansal |
2014-06-29 | sets: "insert" operator | Kshitij Bansal |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are now... | Kshitij Bansal |
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij Bansal |
2014-06-22 | Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3: | Morgan Deters |
2014-06-22 | Minor cleanup stuff. | Morgan Deters |
2014-06-21 | Some minor cleanup and documentation. | Morgan Deters |
2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol |
2014-06-06 | Sets translate, and other short fixes | Kshitij Bansal |
2014-06-05 | When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary. | Morgan Deters |
2014-06-04 | Add operator support (resolves bug #563). | Morgan Deters |
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 |