Age | Commit message (Expand) | Author |
2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol |
2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
2015-04-09 | Fix performance issue with variable triggers + instantiation restrictions. | ajreynol |
2015-01-24 | Variable patterns only look at eligible terms. Minor refactoring of quantifi... | ajreynol |
2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | 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-09-16 | Bug fix variable triggers with --inst-max-level : use term in EQC with minima... | ajreynol |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds |
2014-03-12 | Work on array pf signature, add working example. Add quantifiers proof signa... | Andrew Reynolds |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-01-28 | More optimizations of quantifier instantiation data structures. | Andrew Reynolds |
2014-01-18 | Performance optimization for E-matching, working on using QCF module for prop... | Andrew Reynolds |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option fo... | Andrew Reynolds |
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2012-10-16 | first draft of new inst gen method (still with bugs), some cleanup of quantif... | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-07-31 | Moving some instantiation-related stuff from src/theory to src/theory/quantif... | Morgan Deters |