Age | Commit message (Expand) | Author |
2014-04-14 | Add initial support for co-datatypes. | Andrew Reynolds |
2014-04-10 | Fix the build; --check-proof works for UF but not for the new UFC logic. | Morgan Deters |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-04-10 | Boolean terms conversion fix for datatypes, fixes a problem Andy discovered o... | Morgan Deters |
2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
2014-04-09 | fix get-info error-behavior | Kshitij Bansal |
2014-04-04 | For security, add --no-filesystem-access option, which disables SMT-LIB scrip... | Morgan Deters |
2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann... | Morgan Deters |
2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal |
2014-03-20 | cleanup | Kshitij Bansal |
2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
2014-03-19 | Set dumping options from (set-option..) and API more directly. | Morgan Deters |
2014-03-11 | Fix for (get-assignment), resolves bug 553. | Morgan Deters |
2014-03-11 | Merge branch '1.3.x' | Morgan Deters |
2014-03-11 | Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok. | Morgan Deters |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi... | Morgan Deters |
2014-03-07 | Fix bug 554 (nominally). | Morgan Deters |
2014-03-07 | Fix strings-exp setting. | Morgan Deters |
2014-03-04 | Guard java-specific swig code with SWIGJAVA. | Thomas Hunger |
2014-02-28 | a new regular expression engine for solving both positive and negative member... | Tianyi Liang |
2014-02-21 | portfolio: fix export of emptyset | Kshitij Bansal |
2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q... | Andrew Reynolds |
2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang |
2014-02-17 | bring back the commits which is lost accidentally. | Tianyi Liang |
2014-02-17 | add str2int | Tianyi Liang |
2014-02-17 | Fix for strings-exp: enable quantifiers | Morgan Deters |
2014-02-17 | Fix strings preprocessing for justification heuristic | Morgan Deters |
2014-02-17 | type conversion | Tianyi Liang |
2014-02-13 | fix expanding def | Tianyi Liang |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang |
2014-01-22 | Some minor fixes to SmtEngine strings settings. | Morgan Deters |
2014-01-22 | add warning for using strings in ALL_SUPPORTED | Tianyi Liang |
2014-01-22 | Smarter options, but still have a bug | Tianyi Liang |
2014-01-18 | strings with new ideas | Tianyi Liang |
2014-01-16 | adds partial functions | Tianyi Liang |
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters |
2013-12-16 | Fix for bug 544. | Morgan Deters |
2013-12-10 | Whitespace. | Morgan Deters |
2013-12-10 | Remove "NodeValue width" output | Morgan Deters |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-12-05 | Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now wor... | Morgan Deters |
2013-12-04 | Partial kind branch merge, including new --rewrite-apply-to-const feature. | Morgan Deters |
2013-12-04 | Don't put define-funs in model output; bug 411 testcase no longer relevant. | Morgan Deters |
2013-12-02 | Another fix to Java destruction order issues. Thanks to Zheng Manchun for th... | Morgan Deters |