| Age | Commit message (Expand) | Author |
|---|
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds |
| 2017-11-16 | (Refactor) Arithmetic monomial sum (#1381) | Andrew Reynolds |
| 2017-11-14 | Make QEffort an enum (#1366) | Andrew Reynolds |
| 2017-11-13 | (Refactor) Decouple rep set iterator and quantifiers (#1339) | Andrew Reynolds |
| 2017-11-01 | (Refactor) Split term util (#1303) | Andrew Reynolds |
| 2017-10-27 | Refactor theory model (#1236) | Andrew Reynolds |
| 2017-10-09 | Split term database (#1206) | Andrew Reynolds |
| 2017-07-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ... | ajreynol |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ... | ajreynol |
| 2017-03-22 | Minor fix for bounded integers. | ajreynol |
| 2017-03-02 | Fixes related to sets. | ajreynol |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
| 2017-02-15 | Minimization modes for fmf bound. | ajreynol |
| 2017-02-07 | Generalize finite bound inference to unifiable variables in set membership li... | ajreynol |
| 2017-01-11 | Fix for when variables are (partially) bound in multiple ways, add regression... | ajreynol |
| 2016-12-07 | Add sets regression, fixes bug 754. Minor fix to regexp in strings. | ajreynol |
| 2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of re... | ajreynol |
| 2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + un... | ajreynol |
| 2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
| 2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng |
| 2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
| 2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
| 2016-06-01 | Initial infrastructure for bounded set quantification (disabled). Refactoring... | ajreynol |
| 2016-04-20 | update from the master | PaulMeng |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-06-09 | Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f... | ajreynol |
| 2015-03-04 | More work on arithmetic single invocation synthesis conjectures. | ajreynol |
| 2015-02-02 | Single invocation module for counterexample guided quantifier instantiation -... | ajreynol |
| 2014-10-18 | Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi... | ajreynol |
| 2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | ajreynol |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
| 2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
| 2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi... | Morgan Deters |
| 2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r... | Morgan Deters |
| 2014-01-18 | Fixed non-termination issue in bounded integers. | Andrew Reynolds |
| 2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-11-26 | Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ... | Andrew Reynolds |
| 2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to tu... | Andrew Reynolds |
| 2013-09-27 | Add new symmetry breaking technique for finite model finding. Improvements t... | Andrew Reynolds |
| 2013-09-15 | Change default option of simple ite lifting within quantifier bodies. add so... | Andrew Reynolds |
| 2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
| 2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
| 2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds |
| 2013-06-25 | Refactoring of model engine to separate individual implementations of model b... | Andrew Reynolds |
| 2013-06-04 | Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ... | Andrew Reynolds |
