| Age | Commit message (Expand) | Author |
|---|
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
| 2015-09-18 | Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quan... | ajreynol |
| 2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ... | ajreynol |
| 2015-09-10 | Models for codatatypes. Fixes bug 662. | ajreynol |
| 2015-09-09 | Fix bug in strings rewriter regarding lengths of substr terms. | ajreynol |
| 2015-09-05 | Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug... | ajreynol |
| 2015-09-04 | Fix bugs 605 and 667. | ajreynol |
| 2015-09-02 | fix regressions | Kshitij Bansal |
| 2015-08-27 | Modify slow regressions. | ajreynol |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
| 2015-08-19 | fix bug 605 | Kshitij Bansal |
| 2015-08-19 | Implementation of model-based projection in cbqi, cleanup, add regressions. | ajreynol |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-08-01 | Support for default grammar for datatypes in sygus. Support vts for infinity. | ajreynol |
| 2015-08-01 | Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. | ajreynol |
| 2015-07-31 | Sygus support for inductive datatypes. | ajreynol |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix soundnes... | ajreynol |
| 2015-07-27 | Disable bug590.smt2 | Tianyi Liang |
| 2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
| 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 |
