| Age | Commit message (Expand) | Author |
|---|
| 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 | Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat... | 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-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-07-12 | Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms. | ajreynol |
| 2015-07-05 | Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu... | ajreynol |
| 2015-07-02 | On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n... | ajreynol |
| 2015-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | ajreynol |
| 2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
| 2015-06-25 | Do not assert fail for fmf empty domains. Fixes bug 644. | ajreynol |
| 2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
| 2015-06-16 | Avoid completion for large finite types. Fix bug for --fmf-fun. | ajreynol |
| 2015-06-15 | Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-stable | ajreynol |
| 2015-06-12 | Fix crash in non-linear cbqi. | ajreynol |
| 2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
| 2015-06-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | 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-10 | Parse support for sygus LetGTerm. | ajreynol |
| 2015-06-09 | Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f... | ajreynol |
| 2015-06-04 | Minor changes to smt comp script for quantified arith. Add option --cbqi-sat... | ajreynol |
| 2015-06-03 | Refactoring of sygus parsing, properly parse Constant/Variable constructors. | ajreynol |
| 2015-05-29 | Do not enforce dt fairness when single invocation sygus. | ajreynol |
| 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-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 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
| 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-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 |
