Age | Commit message (Expand) | Author |
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 |
2013-08-13 | initial modifications for per-ic cbqi | 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-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |