| Age | Commit message (Expand) | Author |
|---|
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds |
| 2018-02-06 | Resolving warnings from -Winconsistent-missing-override on clang. (#1563) | Tim King |
| 2018-01-08 | Removing more miscellaneous throw specifiers. (#1488) | Tim King |
| 2017-11-14 | Make QEffort an enum (#1366) | Andrew Reynolds |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2017-06-15 | Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cb... | 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-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-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
| 2016-09-12 | Remove old implementation of cbqi | ajreynol |
| 2016-09-03 | Option for prenex normal form | ajreynol |
| 2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
| 2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol |
| 2016-08-25 | Options for counterexample guided instantiation. | ajreynol |
| 2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
| 2016-04-20 | update from the master | PaulMeng |
| 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-02-25 | Minor improvement to partial qe. Add options for representative selection in ... | ajreynol |
| 2016-02-17 | Refactor quantifiers attributes. Make quantifier elimination robust to prepro... | ajreynol |
| 2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
| 2015-12-22 | Bug fix for cbqi, do not use model values for terms involving non-enumerable ... | ajreynol |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-23 | Adding a missing delete to InstStrategyCegqi destructor. | Tim King |
| 2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress... | ajreynol |
| 2015-09-26 | Better organization of quantifiers modules, promote full saturation to module... | ajreynol |
| 2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
| 2015-08-27 | Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S... | ajreynol |
| 2015-08-26 | Minor improvements to cbqi, fix bug in solving with vts symbols, round up for... | ajreynol |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
| 2015-08-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 2015-08-19 | Implementation of model-based projection in cbqi, cleanup, add regressions. | ajreynol |
| 2015-08-01 | Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat... | ajreynol |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix soundnes... | ajreynol |
| 2015-07-05 | Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu... | ajreynol |
| 2015-07-02 | On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n... | ajreynol |
| 2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
| 2015-04-01 | Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun... | ajreynol |
| 2015-03-23 | Decouple counter-example guided quantifier instantiation from Sygus. | ajreynol |
| 2015-02-22 | New trigger options. --inst-no-entail on by default. Misc cleanup. | ajreynol |
| 2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
