| Age | Commit message (Expand) | Author |
|---|
| 2015-11-05 | Merging the google branch back into master. | Tim King |
| 2015-11-05 | Fixes some initialization and desctruction problems in quantifiers. Also rest... | Tim King |
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol |
| 2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol |
| 2015-10-26 | Extend counterexample-guided instantiation to extended theory of Int/Real, mi... | ajreynol |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
| 2015-08-27 | Modify slow regressions. | 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 | Implementation of model-based projection in cbqi, cleanup, add regressions. | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix soundnes... | ajreynol |
| 2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
| 2015-04-21 | Fix file permissions | Clark Barrett |
| 2015-03-23 | Parsing support for define-fun-rec/define-funs-rec. | ajreynol |
| 2014-11-21 | Throw error when pattern is not list of terms. | ajreynol |
| 2014-11-21 | Change default option to --inst-when=full-last-call (interleave instantiation... | ajreynol |
| 2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol |
| 2014-09-17 | Fix soundness bug for quantifier macros involving Int/Real. | ajreynol |
| 2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | ajreynol |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
| 2014-03-05 | Revert "fix naming conflicts in benchmarks" | Kshitij Bansal |
| 2014-02-21 | add new theory (sets) | Kshitij Bansal |
| 2014-02-10 | Fix build (some nonexistent files listed in Makefile) | Morgan Deters |
| 2014-02-09 | More complete guess instantiation strategy, cvc4 now typically times out inst... | Andrew Reynolds |
| 2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | Andrew Reynolds |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
| 2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 suc... | Morgan Deters |
| 2013-09-18 | Support a personal build configuration and make rules. | Morgan Deters |
| 2013-09-13 | Move some regress benchmarks around that took too long, other test cleanup. | Morgan Deters |
| 2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed b... | Andrew Reynolds |
| 2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters |
| 2012-09-18 | SMT-LIBv2 compliance regarding outputting "unknown". | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-28 | fix regression tests for automake 1.11 and automake 1.12---both versions shou... | Morgan Deters |
| 2012-08-27 | * Reversing commit r4258 (which disabled failing regressions). Fixed the pro... | Morgan Deters |
| 2012-08-26 | disabling failing regressions | Kshitij Bansal |
| 2012-07-27 | Minor cleanup after today's commits: | Morgan Deters |
| 2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
| 2012-06-17 | fixing makefile error that brakes build | Dejan Jovanović |
| 2012-06-17 | Fix array bug causing incorrect answers | Clark Barrett |
| 2012-06-11 | distribute an .expect file. fixes a "make check" failure not for svn working... | Morgan Deters |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
