| Age | Commit message (Expand) | Author |
|---|
| 2015-06-12 | Merge remote-tracking branch 'origin/master' into experimental | Kshitij Bansal |
| 2015-06-12 | Adding missing new sendAtoms flag in OutputChannel::lemma() into the unit tests. | Tim King |
| 2015-06-11 | Added support for glucose, cryptominisat and riss as eager bit-blasting sat-s... | Liana Hadarean |
| 2015-06-11 | Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St... | ajreynol |
| 2015-06-11 | Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A... | ajreynol |
| 2015-06-11 | Update experimental scripts. Support top-level non-terminals in sygus gramma... | ajreynol |
| 2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
| 2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol |
| 2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol |
| 2015-05-25 | Add missing regression | ajreynol |
| 2015-05-25 | Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report. | ajreynol |
| 2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
| 2015-05-11 | Add missing regression. | ajreynol |
| 2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol |
| 2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
| 2015-04-27 | Disambiguate namespaces in options, fix permissions | Clark Barrett |
| 2015-04-27 | Updating failing unit tests. | Tim King |
| 2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode... | ajreynol |
| 2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm... | ajreynol |
| 2015-04-24 | Fix sygus parser for non-tokenized operators, reenable regression. Fix for --... | ajreynol |
| 2015-04-23 | Merge branch 'master' into google | Clark Barrett |
| 2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
| 2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
| 2015-04-22 | Merge pull request #73 from kbansal/parser-dont-tokenize | Kshitij Bansal |
| 2015-04-21 | Fix file permissions | Clark Barrett |
| 2015-04-21 | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. | ajreynol |
| 2015-04-21 | Adding an example of a tester in SMT2. | Tim King |
| 2015-04-17 | Patch for Kshitij's fix on requriePhase | Tianyi Liang |
| 2015-04-17 | Merge pull request #72 from kbansal/decision-requirephase | Kshitij Bansal |
| 2015-04-16 | disable failing sygus tests | Kshitij Bansal |
| 2015-04-15 | Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2 | Tim King |
| 2015-04-15 | Adding an example that violates an assertion during unconstrained simplificat... | Tim King |
| 2015-04-09 | disable string reqressions timing out after change | Kshitij Bansal |
| 2015-03-23 | Parsing support for define-fun-rec/define-funs-rec. | ajreynol |
| 2015-03-10 | CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig... | ajreynol |
| 2015-02-26 | Robust strategy for single invocation LIA synthesis conjectures. Add regress... | ajreynol |
| 2015-02-14 | Fix unit tests. | ajreynol |
| 2015-02-13 | Handle recursive singleton case for codatatypes, add regression. Simplify im... | ajreynol |
| 2015-02-05 | Minor clean up | Tianyi Liang |
| 2015-02-05 | Improved string performance, thanks to Peter's benchmarks. | Tianyi Liang |
| 2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. Add... | ajreynol |
| 2015-01-19 | Adding tests for get-value output for arithmetic. | Tim King |
| 2015-01-14 | sygus input language and benchmark | Morgan Deters |
| 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-07 | bug fix, thanks to Pierre's report | Tianyi Liang |
| 2014-12-28 | Disable prenex by default when using fmf bound int, minor improvement to data... | ajreynol |
| 2014-12-04 | Relaxed the constant requirement for regular expression loop; | Tianyi Liang |
| 2014-12-03 | Floating point infrastructure. | Martin Brain |
| 2014-11-26 | add intersection rewriting | Tianyi Liang |
