| Age | Commit message (Expand) | Author |
|---|
| 2016-02-18 | Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug ... | ajreynol |
| 2016-02-17 | Refactor quantifiers attributes. Make quantifier elimination robust to prepro... | ajreynol |
| 2016-02-15 | More simplification to internal implementation of tuples and records. | ajreynol |
| 2016-02-09 | Fix regression, minor change to output. | ajreynol |
| 2016-02-08 | Updates related to finite model finding and (co)datatypes. Bug fix enumerator... | ajreynol |
| 2016-02-01 | Simplify fmc model construction, add regression. Improve FMF debug assertions. | ajreynol |
| 2015-12-30 | Shuffling around public vs. private headers | Tim King |
| 2015-12-22 | Always split on constructor types for datatypes involving uninterpreted sorts... | ajreynol |
| 2015-12-22 | Bug fix for cbqi, do not use model values for terms involving non-enumerable ... | ajreynol |
| 2015-12-18 | Modifying emptyset.h and sexpr. Adding SetLanguage. | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-25 | Infrastructure for partially single invocation properties. Bug fix for uncons... | ajreynol |
| 2015-11-12 | Minor fixes and improvements to purify quant, relational triggers. | ajreynol |
| 2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol |
| 2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol |
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress... | ajreynol |
| 2015-09-28 | Improve quantifiers engine wrt incremental presolve. Add regressions. | ajreynol |
| 2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
| 2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ... | ajreynol |
| 2015-09-11 | Minor cleanup related to codatatypes. | ajreynol |
| 2015-09-06 | Improve quantifiers rewriter, minor refactoring. | ajreynol |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-08-21 | Minor changes related to codatatypes for 1.5 release. | ajreynol |
| 2015-08-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 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-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-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-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 | 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-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | 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-16 | Fix option --quant-fun-wd. Add mk_starexec script to contrib. | ajreynol |
| 2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
