Age | Commit message (Expand) | Author |
2017-11-24 | (Refactor) Instantiate utility (#1387) | Andrew Reynolds |
2017-11-01 | (Refactor) Split term util (#1303) | Andrew Reynolds |
2017-10-09 | Split term database (#1206) | Andrew Reynolds |
2017-07-07 | Update copyright headers. | Mathias Preiner |
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
2016-09-29 | Address some coverity warnings, add another stat. | ajreynol |
2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
2016-05-02 | Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ... | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | 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-30 | Updates to E-matching to avoid entailed instantiations earlier. Minor updates... | ajreynol |
2016-03-22 | Bug fix for define functions + incremental. Minor work on relational triggers. | ajreynol |
2016-03-10 | Faster conditional rewriting for and/or beneath quantifiers. Improvements to ... | ajreynol |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
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 |