| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-09-24 | Fix infinite loop in datatypes enumerator. Minor work on conjecture generator. | ajreynol |
| 2014-09-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
| 2014-09-23 | Support :no-pattern. | ajreynol |
| 2014-09-23 | Do not throw error when codatatype is not well-founded. Add option for disab... | ajreynol |
| 2014-09-17 | Fix soundness bug for quantifier macros involving Int/Real. | ajreynol |
| 2014-09-17 | Refactor entailment filtering for conjecture generator. Other minor cleanup. | ajreynol |
| 2014-09-17 | More refactoring of conjecture generation. Term generation into own class. | ajreynol |
| 2014-09-16 | Bug fix variable triggers with --inst-max-level : use term in EQC with minima... | ajreynol |
| 2014-09-16 | Refactoring of conjecture generator. Determine subgoals are non-canonical ba... | ajreynol |
| 2014-09-09 | Fix bug for variable term triggers within multi-triggers. | ajreynol |
| 2014-09-09 | Accept user-provided triggers with variable terms. Flush lemmas before quant... | ajreynol |
| 2014-09-03 | Merge remote-tracking branch 'origin/master' | Kshitij Bansal |
| 2014-09-03 | check() optimization | Kshitij Bansal |
| 2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change... | ajreynol |
| 2014-09-03 | Work on conjecture generator : do not generalize subterms with concrete value... | ajreynol |
| 2014-08-29 | Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev... | ajreynol |
