| Age | Commit message (Expand) | Author |
|---|
| 2015-09-18 | Fix bug in quantifiers engine where model construction could be skipped. | ajreynol |
| 2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ... | 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 | 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-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-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-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
| 2015-06-13 | Avoid instantiating with array constants. | ajreynol |
| 2015-06-13 | Ensure mkRep instantiation strategies do not violate types. | ajreynol |
| 2015-06-09 | Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f... | ajreynol |
| 2015-05-29 | Do not enforce dt fairness when single invocation sygus. | ajreynol |
| 2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
| 2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | 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-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
| 2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode... | ajreynol |
| 2015-04-09 | Fix performance issue with variable triggers + instantiation restrictions. | ajreynol |
| 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-03-11 | Minor fixes and improvements to cegqi-si for linear arithmetic. | ajreynol |
| 2015-02-04 | Refactor sygus_util to TermDb. Initial work on solution reconstruction into ... | ajreynol |
| 2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
| 2015-01-26 | Output solutions for synthesis conjectures with --dump-synth. Minor refactor... | ajreynol |
| 2015-01-24 | Variable patterns only look at eligible terms. Minor refactoring of quantifi... | ajreynol |
| 2015-01-24 | Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in... | ajreynol |
| 2015-01-23 | Rework inst-closure. | ajreynol |
| 2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol |
| 2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to --full-satur... | ajreynol |
| 2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
| 2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. Chang... | ajreynol |
| 2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol |
| 2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
| 2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr... | ajreynol |
| 2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use assertRepre... | ajreynol |
| 2014-10-13 | CEGQI uses model. Enforce fairness in CEGQI natively. | 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-10-10 | Initial draft of CEGQI. | ajreynol |
| 2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
| 2014-10-08 | Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep... | ajreynol |
| 2014-10-07 | Refactor quantifiers attributes. | ajreynol |
