| Age | Commit message (Expand) | Author |
|---|
| 2015-05-29 | Do not enforce dt fairness when single invocation sygus. | ajreynol |
| 2015-05-29 | changed resource step options to unsigned | lianah |
| 2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
| 2015-05-22 | Added throw LogicException to method lemma. | Jordy Ruiz |
| 2015-05-15 | Fixes related to cbqi + E-matching. | ajreynol |
| 2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | ajreynol |
| 2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | ajreynol |
| 2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | 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-05-02 | Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add co... | ajreynol |
| 2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
| 2015-04-27 | Disambiguate namespaces in options, fix permissions | Clark Barrett |
| 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-24 | Fix compiler errors due to unbalanced throw specifiers. | Clark Barrett |
| 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-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
| 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-18 | Farkas proof coefficients. | Tim King |
| 2015-04-17 | Patch for Kshitij's fix on requriePhase | Tianyi Liang |
| 2015-04-16 | Fix option --quant-fun-wd. Add mk_starexec script to contrib. | ajreynol |
| 2015-04-16 | Handle (degenerate) case of synthesis conjectures for constants. Disable del... | ajreynol |
| 2015-04-13 | Making CVC4::theory::quantifiers::PrenexQuantMode public for now. | Tim King |
| 2015-04-09 | Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an... | ajreynol |
| 2015-04-09 | Fix performance issue with variable triggers + instantiation restrictions. | ajreynol |
| 2015-04-09 | Bug fix negative contains cache. | ajreynol |
| 2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
| 2015-04-07 | Removing the reference to THEORY_BOOL from the equality engine. This theory | Dejan Jovanovic |
| 2015-04-07 | Minor fixes for cegqi. | ajreynol |
| 2015-04-02 | Merge pull request #71 from kbansal/const-are-triggers | Kshitij Bansal |
| 2015-04-01 | Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun... | ajreynol |
| 2015-03-31 | fix no return value warning | Kshitij Bansal |
| 2015-03-28 | printer change for string smtlib2 | Tianyi Liang |
| 2015-03-25 | change const are triggers from false to true in equality engines | Kshitij Bansal |
| 2015-03-23 | Decouple counter-example guided quantifier instantiation from Sygus. | ajreynol |
| 2015-03-16 | Add requirePhase len(x) = 0. | Tianyi Liang |
| 2015-03-14 | Bug fix for BV | Tianyi Liang |
| 2015-03-14 | Patches for 32-bit ARM | Tianyi Liang |
| 2015-03-11 | Strings split on constant lengths, add length=0 to split lemma for empty string. | ajreynol |
| 2015-03-11 | Minor fixes and improvements to cegqi-si for linear arithmetic. | ajreynol |
| 2015-03-05 | Minor fixes. Extend cegqi-si to real arithmetic. | ajreynol |
| 2015-03-04 | More work on arithmetic single invocation synthesis conjectures. | ajreynol |
| 2015-02-26 | Robust strategy for single invocation LIA synthesis conjectures. Add regress... | ajreynol |
| 2015-02-25 | Switch back to eager loop temporarily. | Tianyi Liang |
| 2015-02-24 | minor fix for internal string print | Tianyi Liang |
