| Age | Commit message (Expand) | Author |
|---|
| 2016-05-18 | Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino... | ajreynol |
| 2016-05-16 | Enable --sygus-direct-eval by default, limit to terms that do not induce Bool... | ajreynol |
| 2016-05-15 | Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En... | ajreynol |
| 2016-05-05 | Compute term indices lazily in TermDb. Optimization for qcf to recognize irre... | ajreynol |
| 2016-05-02 | Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ... | ajreynol |
| 2016-04-28 | More work on inst propagate. Optimization for qcf to check instances eagerly... | ajreynol |
| 2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
| 2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ... | ajreynol |
| 2016-04-07 | Refactor trigger selection, revisions to --relational-trigger. Properly proce... | ajreynol |
| 2016-04-04 | New options for trigger selection, add option --strict-triggers. Do not infer... | ajreynol |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2016-03-31 | Improvements to trigger selection, min triggers by default. Optimizations for... | ajreynol |
| 2016-03-28 | Implement equality inference module for arithmetic terms. Optimization for e... | ajreynol |
| 2016-03-16 | Change internal representative selection for finite domains that do not invol... | ajreynol |
| 2016-03-10 | Faster conditional rewriting for and/or beneath quantifiers. Improvements to ... | ajreynol |
| 2016-02-25 | Minor improvement to partial qe. Add options for representative selection in ... | ajreynol |
| 2016-02-23 | Fix term database for non-equal, congruent terms in master equality engine. D... | ajreynol |
| 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-01 | Simplify fmc model construction, add regression. Improve FMF debug assertions. | ajreynol |
| 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-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
| 2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | 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-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | 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-20 | Squashed merge of SygusComp 2015 branch. | 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-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | ajreynol |
| 2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
| 2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
| 2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
| 2015-02-11 | Move si solution reconstruction to own file, make more robust. Other refactor... | ajreynol |
| 2015-02-06 | Handle missing cases for single inv solution reconstruction. Minor fixes. Re... | ajreynol |
| 2015-02-05 | Working version of sygus solution reconstruction from single inv cegqi. Heur... | ajreynol |
| 2015-02-04 | Work on solution reconstruction for single inv. Fix compiler error found by ... | ajreynol |
| 2015-02-04 | Refactor sygus_util to TermDb. Initial work on solution reconstruction into ... | ajreynol |
| 2015-02-04 | Start work on simplifying single inv solutions. Minor. | ajreynol |
