Age | Commit message (Expand) | Author |
2016-12-02 | Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --... | ajreynol |
2016-12-01 | Improvement and bug fix for str.indexof reduction, add regression. Other mino... | ajreynol |
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation l... | 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 | Minor cleanup and additions to quantifiers statistics. | ajreynol |
2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
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-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
2016-06-01 | Initial infrastructure for bounded set quantification (disabled). Refactoring... | ajreynol |
2016-05-06 | Minor clean up, fixes related to sygus. | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-13 | Minor improvements for alpha equivalence and partial quantifier elimination i... | ajreynol |
2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
2016-04-10 | More work on instantiation propagation. Enable external filtering of instanti... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-16 | Change internal representative selection for finite domains that do not invol... | ajreynol |
2016-01-15 | Type enumerators take optional argument indicating fixed cardinalities of uni... | ajreynol |
2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-12-10 | Add option fmf-empty-sorts. | ajreynol |
2015-09-26 | Better organization of quantifiers modules, promote full saturation to module... | ajreynol |
2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol |
2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | ajreynol |
2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm... | ajreynol |
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | 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-09-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ... | ajreynol |
2014-07-21 | initialization in model_engine | Kshitij Bansal |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
2014-04-28 | Optimizations for datatypes: check for clashes modulo equality. Avoid buildi... | ajreynol |
2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ... | Andrew Reynolds |
2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds |
2014-01-28 | More optimizations of quantifier instantiation data structures. | Andrew Reynolds |
2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | Andrew Reynolds |
2014-01-10 | Add stats to quantifiers conflict find. Added option for qcf. Working on ha... | Andrew Reynolds |
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
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 |