Age | Commit message (Expand) | Author |
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-25 | Use zero in cbqi when not using infinities. | 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-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-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-06-12 | Fix crash in non-linear cbqi. | ajreynol |
2015-04-01 | Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun... | ajreynol |
2015-03-31 | fix no return value warning | Kshitij Bansal |
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 |
2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | 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 |
2014-01-28 | More optimizations of quantifier instantiation data structures. | Andrew Reynolds |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-08-13 | initial modifications for per-ic cbqi | Andrew Reynolds |
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
2013-04-26 | FCSimplex branch merge | Tim King |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters |
2012-12-05 | Improved garbage collection for TheoryArith. The merges all of the code over... | Tim King |
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |