Age | Commit message (Expand) | Author |
2015-11-26 | Front-end support for get-value of sort cardinality, minor fixes for sygus so... | ajreynol |
2015-10-15 | Change semantics of str.substr to allow endpoint out of bounds, and return em... | ajreynol |
2015-10-13 | remove options infrastructure code which depended on undefined behavior | Kshitij Bansal |
2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
2015-06-30 | fix smt2 parameterized sort printing | Kshitij Bansal |
2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
2015-03-28 | printer change for string smtlib2 | Tianyi Liang |
2015-01-19 | Adding tests for get-value output for arithmetic. | Tim King |
2015-01-11 | adjusted to both v2.0 and v2.5 string literals | Tianyi Liang |
2015-01-09 | blocked unprintable characters in string literals; | Tianyi Liang |
2015-01-08 | switch ascii encoding to unsigned char | Tianyi Liang |
2014-12-06 | Added C++/Java api examples; | Tianyi Liang |
2014-12-03 | Floating point infrastructure. | Martin Brain |
2014-11-17 | Resource-limiting work. | Liana Hadarean |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
2014-10-08 | Add unsat cores support to CVC native language. | Morgan Deters |
2014-10-06 | Print array constants in SMT-LIB models with new syntax. | Morgan Deters |
2014-10-06 | Support for RESET command in CVC native language (and infrastructure for supp... | Morgan Deters |
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 |