Age | Commit message (Expand) | Author |
2015-01-22 | Do not drop patterns during boolean term rewriting. Narrow sygus search space... | ajreynol |
2015-01-21 | Initial work on sygusNormalForm. | ajreynol |
2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. Add... | ajreynol |
2015-01-20 | Handle miniscoping of conjunctions in synthesis properties. Refactor constru... | ajreynol |
2015-01-16 | Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de... | ajreynol |
2015-01-16 | Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus... | ajreynol |
2015-01-14 | sygus input language and benchmark | Morgan Deters |
2014-12-28 | Disable prenex by default when using fmf bound int, minor improvement to data... | ajreynol |
2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
2014-12-22 | Add misc trigger options. | ajreynol |
2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to --full-satur... | ajreynol |
2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
2014-11-21 | Throw error when pattern is not list of terms. | ajreynol |
2014-11-21 | Change default option to --inst-when=full-last-call (interleave instantiation... | ajreynol |
2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol |
2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | ajreynol |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol |
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
2014-11-13 | More preparation for filtering relevant terms in TermDb. | ajreynol |
2014-11-11 | Work on synchronizing decision=justification and E-matching. | ajreynol |
2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements to... | ajreynol |
2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr... | ajreynol |
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use assertRepre... | ajreynol |
2014-11-05 | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. | ajreynol |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
2014-11-01 | Fix cegqi for synthesis without syntax. | ajreynol |
2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ... | ajreynol |
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | ajreynol |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
2014-10-28 | Improve stats in conjecture generator, minor cleanup. | ajreynol |
2014-10-25 | Minor fix for --user-pat=resort | ajreynol |
2014-10-24 | Fix typo. | Morgan Deters |
2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | ajreynol |
2014-10-18 | Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi... | ajreynol |
2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by CE... | ajreynol |
2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, a... | Morgan Deters |
2014-10-13 | CEGQI uses model. Enforce fairness in CEGQI natively. | ajreynol |
2014-10-13 | Model building into quantifiers engine. Simplify axiom-inst mode. | ajreynol |
2014-10-13 | Refactor model builder from model engine to quant engine. Work on fairness s... | ajreynol |
2014-10-10 | Initial draft of CEGQI. | ajreynol |
2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
2014-10-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | ajreynol |
2014-10-08 | Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep... | ajreynol |
2014-10-07 | Refactor quantifiers attributes. | ajreynol |
2014-10-01 | Option for more aggressive merging in UEE. | ajreynol |
2014-09-29 | Add option for aggressive model filtering in conjecture generator (enumerate ... | ajreynol |