| 2021-03-09 |
Aina Niemetz | Update copyright headers to 2021. (#6081) |
blob | commitdiff | raw |
| 2021-02-09 |
Haniel Barbosa | [quantifiers] Fix prenex computation (#5879) |
blob | commitdiff | raw | diff to current |
| 2020-12-16 |
Andrew Reynolds | (proof-new) Use bound variable manager (#5679) |
blob | commitdiff | raw | diff to current |
| 2020-12-07 |
Andrew Reynolds | Fix issue with free variables introduced by quantifier... |
blob | commitdiff | raw | diff to current |
| 2020-09-22 |
Mathias Preiner | Update copyright header script to support CMake and... |
blob | commitdiff | raw | diff to current |
| 2020-09-03 |
Andrew Reynolds | (proof-new) Support proofs of quantifier instantiation... |
blob | commitdiff | raw | diff to current |
| 2020-06-16 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2020-06-03 |
Andrew Reynolds | Use prenex normal form when using cegqi-nested-qe ... |
blob | commitdiff | raw | diff to current |
| 2020-02-29 |
Andrew Reynolds | Replace conditional rewrite pass in quantifiers with... |
blob | commitdiff | raw | diff to current |
| 2020-02-28 |
Andrew Reynolds | Use enum for quantifiers rewrite steps (#3840) |
blob | commitdiff | raw | diff to current |
| 2020-02-14 |
Andrew Reynolds | Remove quantifiers rewrite rules infrastructure (#3754) |
blob | commitdiff | raw | diff to current |
| 2020-02-06 |
Andrew Reynolds | Generalize containsQuantifiers to hasClosure (#3722) |
blob | commitdiff | raw | diff to current |
| 2019-12-09 |
Andres Noetzli | Make theory rewriters non-static (#3547) |
blob | commitdiff | raw | diff to current |
| 2019-10-01 |
Andrew Reynolds | Trivial solve method for single invocation sygus (... |
blob | commitdiff | raw | diff to current |
| 2019-08-23 |
Andrew Reynolds | Update dynamic splitting strategy for quantifiers ... |
blob | commitdiff | raw | diff to current |
| 2019-08-05 |
Andrew Reynolds | Remove forward declarations in quantifiers engine ... |
blob | commitdiff | raw | diff to current |
| 2019-06-27 |
Andrew Reynolds | Variable elimination rewrite for quantified strings... |
blob | commitdiff | raw | diff to current |
| 2019-04-24 |
Mathias Preiner | Do not use __ prefix for header guards. (#2974) |
blob | commitdiff | raw | diff to current |
| 2019-03-26 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2018-09-06 |
Andrew Reynolds | Refactor and document quantifiers variable elimination... |
blob | commitdiff | raw | diff to current |
| 2018-08-17 |
Andrew Reynolds | Remove miscellaneous unused code (#2333) |
blob | commitdiff | raw | diff to current |
| 2018-06-25 |
Aina Niemetz | Updated copyright headers. |
blob | commitdiff | raw | diff to current |
| 2018-04-04 |
Andrew Reynolds | Option to turn arbitrary input into sygus (#1704) |
blob | commitdiff | raw | diff to current |
| 2018-01-08 |
Andrew Reynolds | Improvements to quant+BV/Bool variable elimination... |
blob | commitdiff | raw | diff to current |
| 2017-11-19 |
Tim King | Names the Effort enum of QuantConflictFind class. ... |
blob | commitdiff | raw | diff to current |
| 2017-07-10 |
ajreynol | Merge datatype shared selectors/sygus comp 2017 branch... |
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-04-28 |
ajreynol | Do not eliminate non-standard arithmetic operators... |
blob | commitdiff | raw | diff to current |
| 2016-10-13 |
Tim King | Revert "Merge branch 'origin' of https://github.com... |
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-09-12 |
ajreynol | Refactor prenex modes. |
blob | commitdiff | raw | diff to current |
| 2016-09-03 |
ajreynol | Miniscope top level conjunctions for prenex normal... |
blob | commitdiff | raw | diff to current |
| 2016-09-03 |
ajreynol | Option for prenex normal form |
blob | commitdiff | raw | diff to current |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
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-08 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-06-06 |
guykatzz | Merge pull request #85 from CVC4/master_for_proof_merge |
blob | commitdiff | raw | diff to current |
| 2016-06-03 |
ajreynol | Reduce number of passes in quantifiers rewriter. |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
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-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-02-17 |
ajreynol | Refactor quantifiers attributes. Make quantifier elimin... |
blob | commitdiff | raw | diff to current |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-02-09 |
ajreynol | Eager introduction of eqc, lemma cache for ground fmf... |
blob | commitdiff | raw | diff to current |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs. |
blob | commitdiff | raw | diff to current |
| 2015-12-16 |
ajreynol | Work on purification for quantifiers, minor updates. |
blob | commitdiff | raw | diff to current |
| 2015-11-12 |
ajreynol | Minor fixes and improvements to purify quant, relationa... |
blob | commitdiff | raw | diff to current |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checkin... |
blob | commitdiff | raw | diff to current |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes... |
blob | commitdiff | raw | diff to current |
| 2015-11-05 |
Tim King | Merging the google branch back into master. |
blob | commitdiff | raw | diff to current |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
blob | commitdiff | raw | diff to current |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended... |
blob | commitdiff | raw | diff to current |
| 2015-09-10 |
ajreynol | Fix bug 670. Minor. |
blob | commitdiff | raw | diff to current |
| 2015-09-06 |
ajreynol | Improve quantifiers rewriter, minor refactoring. |
blob | commitdiff | raw | diff to current |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for... |
blob | commitdiff | raw | diff to current |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-07-05 |
ajreynol | Add options --partial-triggers, --elim-taut-quant,... |
blob | commitdiff | raw | diff to current |
| 2015-07-01 |
ajreynol | Add options --qcf-all-conflict, --ite-dtt-split-quant... |
blob | commitdiff | raw | diff to current |
| 2015-02-22 |
ajreynol | New trigger options. --inst-no-entail on by default... |
blob | commitdiff | raw | diff to current |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-01-27 |
ajreynol | Always miniscope nested quantifiers. Disable miniscopi... |
blob | commitdiff | raw | diff to current |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewrite... |
blob | commitdiff | raw | diff to current |
| 2014-11-11 |
Kshitij Bansal | Merge pull request #64 from mdeters/theorysets-hashset... |
blob | commitdiff | raw | diff to current |
| 2014-11-10 |
Tianyi Liang | Merge pull request #63 from mdeters/theorystrings-hashs... |
blob | commitdiff | raw | diff to current |
| 2014-11-10 |
ajreynol | Do not eliminate variables only occurring in patterns... |
blob | commitdiff | raw | diff to current |
| 2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
blob | commitdiff | raw | diff to current |
| 2014-07-01 |
Morgan Deters | Update copyrights. |
blob | commitdiff | raw | diff to current |
| 2014-05-08 |
Andrew Reynolds | Fixes to quantifiers rewriter to prevent miniscoping... |
blob | commitdiff | raw | diff to current |
| 2014-05-02 |
Andrew Reynolds | Add option --dt-stc-ind for strengthening skolemization... |
blob | commitdiff | raw | diff to current |
| 2014-04-01 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriter... |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-19 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-18 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-17 |
Kshitij Bansal | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-10 |
Andrew Reynolds | Add new method --quant-cf for finding conflicts eagerly... |
blob | commitdiff | raw | diff to current |
| 2013-12-03 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-11-27 |
Andrew Reynolds | Bug fix for E-matching select terms, minor fix for... |
blob | commitdiff | raw | diff to current |
| 2013-05-03 |
Tim King | Merging branch 'soiquickexplain'. |
blob | commitdiff | raw | diff to current |
| 2013-05-03 |
Tim King | Merge branch 'fcexplanations' |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | fixed merge conflicts |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
Andrew Reynolds | Add option in quantifiers for clause splitting |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
| 2013-03-30 |
Andrew Reynolds | do simple ite rewriting within quantifiers |
blob | commitdiff | raw | diff to current |
| 2013-03-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-14 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-13 |
lianah | post failed attempts at getting the incremental solver... |
blob | commitdiff | raw | diff to current |
| 2013-03-06 |
Andrew Reynolds | fixed two bugs for the new E-matching implementation... |
blob | commitdiff | raw | diff to current |
| 2012-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code revie... |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history