| Age | Commit message (Expand) | Author |
|---|
| 2015-08-26 | Minor improvements to cbqi, fix bug in solving with vts symbols, round up for... | ajreynol |
| 2015-08-25 | Use zero in cbqi when not using infinities. | ajreynol |
| 2015-08-24 | Added threshold for core bv cardinality lemmas | Liana Hadarean |
| 2015-08-24 | Fix for bv core cardinality lemma generation | Liana Hadarean |
| 2015-08-24 | eager bit-blasting gives models for boolean variables too (fixes bug618) | Liana Hadarean |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
| 2015-08-21 | Minor changes related to codatatypes for 1.5 release. | ajreynol |
| 2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
| 2015-08-20 | fix to bug659 due to algebraic solver model building | Liana Hadarean |
| 2015-08-20 | fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero | Liana Hadarean |
| 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-17 | fix for bug663 | Tianyi Liang |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-08-01 | Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat... | ajreynol |
| 2015-08-01 | Support for default grammar for datatypes in sygus. Support vts for infinity. | ajreynol |
| 2015-08-01 | Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. | ajreynol |
| 2015-07-31 | Sygus support for inductive datatypes. | ajreynol |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix soundnes... | ajreynol |
| 2015-07-27 | minor change to the last fix | Tianyi Liang |
| 2015-07-27 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang |
| 2015-07-27 | Hotfix for substr function. | Tianyi Liang |
| 2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-07-12 | Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms. | ajreynol |
| 2015-07-08 | fix bug 650 | Kshitij Bansal |
| 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-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | ajreynol |
| 2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
| 2015-06-25 | Do not assert fail for fmf empty domains. Fixes bug 644. | ajreynol |
| 2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
| 2015-06-16 | Avoid completion for large finite types. Fix bug for --fmf-fun. | ajreynol |
| 2015-06-15 | Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-stable | ajreynol |
| 2015-06-15 | Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr... | Tim King |
| 2015-06-14 | Handing the case in replay where a cut is directly in conflict with an existi... | Tim King |
| 2015-06-14 | Fixes for shared term normalization in replay for constraint construction. | Tim King |
| 2015-06-14 | Turning off aggressive arith ite simplifications during incremental solving. | Tim King |
| 2015-06-13 | Robust check to avoid store all instantiations. Fix prior commit for sort inf... | ajreynol |
| 2015-06-13 | Restricting TheoryArith to computeRelevantTerms. | Tim King |
| 2015-06-13 | Fixed bug in iteSimp | Clark Barrett |
| 2015-06-13 | Fix for assertion failure: | Clark Barrett |
| 2015-06-13 | A return value for an ApproxGLPK::loadVB() failure case was incorrect. | Tim King |
| 2015-06-13 | Avoid instantiating with array constants. | ajreynol |
| 2015-06-13 | Ensure mkRep instantiation strategies do not violate types. | ajreynol |
| 2015-06-12 | Fix crash in non-linear cbqi. | ajreynol |
| 2015-06-12 | In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n... | Tim King |
| 2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
