| 2018-08-25 |
Andrew Reynolds | Clean up quantifiers engine initialization. (#2371) |
blob | commitdiff | raw |
| 2018-08-22 |
Andrew Reynolds | More unused code elimination (#2358) |
blob | commitdiff | raw | diff to current |
| 2018-08-21 |
Andrew Reynolds | More unused code elimination (#2339) |
blob | commitdiff | raw | diff to current |
| 2018-07-03 |
Andrew Reynolds | Remove miscellaneous dead and unused code from quantifi... |
blob | commitdiff | raw | diff to current |
| 2018-06-28 |
Andrew Reynolds | Split and document ceg theory instantiators (#2094) |
blob | commitdiff | raw | diff to current |
| 2018-06-26 |
Andrew Reynolds | Remove unnecessary code in register quantifier internal... |
blob | commitdiff | raw | diff to current |
| 2018-06-25 |
Aina Niemetz | Updated copyright headers. |
blob | commitdiff | raw | diff to current |
| 2018-06-01 |
Andrew Reynolds | Fix quantifiers conflict lemma handling (#2043) |
blob | commitdiff | raw | diff to current |
| 2018-06-01 |
Andrew Reynolds | Reduce before preregister. (#2025) |
blob | commitdiff | raw | diff to current |
| 2018-05-30 |
Andrew Reynolds | Fixes for quantifiers + incremental (#2009) |
blob | commitdiff | raw | diff to current |
| 2018-05-27 |
Andrew Reynolds | Fix cegqi assertions for quantified non-linear cases... |
blob | commitdiff | raw | diff to current |
| 2018-05-21 |
Andrew Reynolds | Refactor sygus eval unfold (#1946) |
blob | commitdiff | raw | diff to current |
| 2018-03-23 |
Andrew Reynolds | Remove unused code (#1700) |
blob | commitdiff | raw | diff to current |
| 2018-03-06 |
Andrew Reynolds | Simplify initialization of quantifiers engine (#1641) |
blob | commitdiff | raw | diff to current |
| 2018-02-14 |
Andrew Reynolds | Quantifiers subdirectories (#1608) |
blob | commitdiff | raw | diff to current |
| 2018-02-02 |
Haniel Barbosa | Option to check solutions produced by SyGuS solver... |
blob | commitdiff | raw | diff to current |
| 2017-12-08 |
Andrew Reynolds | Make collect model info return a Bool (#1421) |
blob | commitdiff | raw | diff to current |
| 2017-11-25 |
Andrew Reynolds | (Refactor) Instantiate utility (#1387) |
blob | commitdiff | raw | diff to current |
| 2017-11-15 |
Andrew Reynolds | Make QEffort an enum (#1366) |
blob | commitdiff | raw | diff to current |
| 2017-11-09 |
Andrew Reynolds | Decouple sygus term database and term database. (... |
blob | commitdiff | raw | diff to current |
| 2017-11-02 |
Andrew Reynolds | (Move-only) Split quant util (#1306) |
blob | commitdiff | raw | diff to current |
| 2017-11-01 |
Andrew Reynolds | (Refactor) Split term util (#1303) |
blob | commitdiff | raw | diff to current |
| 2017-10-28 |
Andrew Reynolds | (Move only) Move enumerative instantiation strategy... |
blob | commitdiff | raw | diff to current |
| 2017-10-28 |
Andrew Reynolds | Document term db (#1220) |
blob | commitdiff | raw | diff to current |
| 2017-10-27 |
Andrew Reynolds | Refactor theory model (#1236) |
blob | commitdiff | raw | diff to current |
| 2017-10-10 |
Andres Noetzli | Fix memory leak in quantifiers engine (#1219) |
blob | commitdiff | raw | diff to current |
| 2017-10-10 |
Andrew Reynolds | Split term database (#1206) |
blob | commitdiff | raw | diff to current |
| 2017-09-29 |
Andrew Reynolds | Simplify representation of inversion Skolems for bv... |
blob | commitdiff | raw | diff to current |
| 2017-09-27 |
Andrew Reynolds | Minor fixes for partial quantifier elimination. (#1147) |
blob | commitdiff | raw | diff to current |
| 2017-08-24 |
Andrew Reynolds | Merge pull request #191 from timothy-king/cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-08-17 |
ajreynol | Add mbqi interleave option, change option fs-inst to... |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Merge branch 'master' into cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Moving from the gnu extensions for hash maps to the... |
blob | commitdiff | raw | diff to current |
| 2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2017-06-01 |
ajreynol | Minor optimizations related to cbqi. |
blob | commitdiff | raw | diff to current |
| 2017-05-17 |
Clark Barrett | Merge pull request #155 from makaimann/conditional_coverage |
blob | commitdiff | raw | diff to current |
| 2017-05-16 |
Andrew Reynolds | Merge pull request #156 from 4tXJ7f/fix_safe_print |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #159 from 4tXJ7f/fix_set_types |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #158 from 4tXJ7f/fix_sets_rewriter |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #157 from 4tXJ7f/fix_iterator |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
ajreynol | Make conflict-based instantiation abort if a ground... |
blob | commitdiff | raw | diff to current |
| 2017-03-29 |
ajreynol | Add quantifiers options related to model and master... |
blob | commitdiff | raw | diff to current |
| 2017-03-27 |
Clark Barrett | Merge pull request #137 from 4tXJ7f/throw_quals |
blob | commitdiff | raw | diff to current |
| 2017-03-27 |
Tim King | Making ppNotifyAssertions take a const vector. |
blob | commitdiff | raw | diff to current |
| 2017-03-24 |
ajreynol | Refactor model building for quantifiers to be a single... |
blob | commitdiff | raw | diff to current |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
blob | commitdiff | raw | diff to current |
| 2017-02-16 |
ajreynol | Fixes for sets+rels check. Minor. |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
ajreynol | Refactoring, generalization of bounded inference module... |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
Tim King | Merge pull request #95 from 4tXJ7f/fix_sierra_build |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
Clark Barrett | Merge pull request #113 from 4tXJ7f/remove_extract_rule |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
ajreynol | Refactor preprocessing of models in fmf. Fix options... |
blob | commitdiff | raw | diff to current |
| 2016-11-21 |
ajreynol | Refactoring related to track instantiation option. |
blob | commitdiff | raw | diff to current |
| 2016-11-03 |
ajreynol | Add priorities to getNextDecision. Properly handle... |
blob | commitdiff | raw | diff to current |
| 2016-10-28 |
ajreynol | Add get instantiations utilities to API. |
blob | commitdiff | raw | diff to current |
| 2016-10-11 |
Paul Meng | Merge branch 'origin' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-10-01 |
Tim King | Merge pull request #93 from timothy-king/clang-format |
blob | commitdiff | raw | diff to current |
| 2016-09-29 |
ajreynol | Address some coverity warnings, add another stat. |
blob | commitdiff | raw | diff to current |
| 2016-09-29 |
ajreynol | Minor cleanup and additions to quantifiers statistics. |
blob | commitdiff | raw | diff to current |
| 2016-09-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options... |
blob | commitdiff | raw | diff to current |
| 2016-09-15 |
ajreynol | Refactor setIncomplete in quantifiers. |
blob | commitdiff | raw | diff to current |
| 2016-09-14 |
ajreynol | Lemma cache in theory sep. Minor optimization for sets... |
blob | commitdiff | raw | diff to current |
| 2016-09-13 |
ajreynol | Minor changes to sep logic, epr, quantifier splitting. |
blob | commitdiff | raw | diff to current |
| 2016-09-12 |
ajreynol | Remove old implementation of cbqi |
blob | commitdiff | raw | diff to current |
| 2016-09-09 |
ajreynol | Support for separation logic + EPR. Refactor preprocess... |
blob | commitdiff | raw | diff to current |
| 2016-09-08 |
ajreynol | Refactor seplog preprocess. Handle case where sep data... |
blob | commitdiff | raw | diff to current |
| 2016-09-02 |
Tim King | Merge pull request #91 from timothy-king/no-throw |
blob | commitdiff | raw | diff to current |
| 2016-09-01 |
ajreynol | Cleanup quantifier elimination in smt engine. |
blob | commitdiff | raw | diff to current |
| 2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to... |
blob | commitdiff | raw | diff to current |
| 2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup. |
blob | commitdiff | raw | diff to current |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
blob | commitdiff | raw | diff to current |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
blob | commitdiff | raw | diff to current |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-07-26 |
ajreynol | Add option to minimize sygus solutions based on using... |
blob | commitdiff | raw | diff to current |
| 2016-07-20 |
ajreynol | Infrastructure for storing and printing heap models... |
blob | commitdiff | raw | diff to current |
| 2016-07-20 |
ajreynol | Print only instantiations that are in the unsat core... |
blob | commitdiff | raw | diff to current |
| 2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
blob | commitdiff | raw | diff to current |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-06-17 |
ajreynol | Support for separation logic. Enable cbqi by default... |
blob | commitdiff | raw | diff to current |
| 2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification... |
blob | commitdiff | raw | diff to current |
| 2016-05-24 |
ajreynol | Improvements to symmetry breaking in sygus search.... |
blob | commitdiff | raw | diff to current |
| 2016-05-18 |
ajreynol | Refactor modes for sygus+single invocation. Add option... |
blob | commitdiff | raw | diff to current |
| 2016-05-16 |
ajreynol | Enable --sygus-direct-eval by default, limit to terms... |
blob | commitdiff | raw | diff to current |
| 2016-05-10 |
ajreynol | Fix for --inst-max-level |
blob | commitdiff | raw | diff to current |
| 2016-05-06 |
ajreynol | Minor clean up, fixes related to sygus. |
blob | commitdiff | raw | diff to current |
| 2016-05-05 |
ajreynol | Compute term indices lazily in TermDb. Optimization... |
blob | commitdiff | raw | diff to current |
| 2016-04-28 |
ajreynol | More work on inst propagate. Optimization for qcf... |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
| 2016-04-13 |
ajreynol | Minor improvements for alpha equivalence and partial... |
blob | commitdiff | raw | diff to current |
| 2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of varia... |
blob | commitdiff | raw | diff to current |
| 2016-04-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip. |
blob | commitdiff | raw | diff to current |
| 2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external... |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers... |
blob | commitdiff | raw | diff to current |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
ajreynol | New options for trigger selection, add option --strict... |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-04-01 |
ajreynol | Improvements to equality inference module: add missing... |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history