git.libre-soc.org Git - cvc5.git/history - src/proof/theory

[cvc5.git] / src / proof / theory_proof.cpp

2019-01-14	Alex Ozdemir	ClausalBitvectorProof (#2786)	blob \| commitdiff \| raw
2018-12-03	Alex Ozdemir	Bit vector proof superclass (#2599)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andres Noetzli	Fix warnings in proof code (#1850)	blob \| commitdiff \| raw \| diff to current
2018-04-25	yoni206	Refactor array-proofs and uf-proofs (#1655)	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Tim King	Adding garbage collection for Proof objects. (#1294)	blob \| commitdiff \| raw \| diff to current
2017-10-26	Tim King	Removing throw specifiers from OutputChannel and subcla...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-31	guykatzz	A more informative error message when a theory is not...	blob \| commitdiff \| raw \| diff to current
2017-03-17	guykatzz	better support for proof production when encountering...	blob \| commitdiff \| raw \| diff to current
2017-03-14	guykatzz	Merge pull request #133 from 4tXJ7f/fix_uninitialized	blob \| commitdiff \| raw \| diff to current
2017-03-14	Andres Notzli	fix uninitialized variable	blob \| commitdiff \| raw \| diff to current
2017-03-14	Clark Barrett	Merge pull request #132 from 4tXJ7f/fix_mingw64	blob \| commitdiff \| raw \| diff to current
2017-03-09	guykatzz	better proof support for bools and formulas	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-08-12	guykatzz	Merge pull request #90 from 4tXJ7f/fewer_preproc_holes	blob \| commitdiff \| raw \| diff to current
2016-08-12	Andres Notzli	Add support for fewer preprocessing holes	blob \| commitdiff \| raw \| diff to current
2016-08-09	guykatzz	Merge pull request #89 from 4tXJ7f/fix_proof_spaces	blob \| commitdiff \| raw \| diff to current
2016-08-09	Andres Notzli	Fix missing/redundant spaces in proofs	blob \| commitdiff \| raw \| diff to current
2016-07-27	guykatzz	Merge pull request #86 from 4tXJ7f/fix_warnings	blob \| commitdiff \| raw \| diff to current
2016-07-27	Andres Notzli	Fix warnings in src/proof	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Bug fix	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Propagate the usage of proof let maps into constant...	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Bug fix	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Use letification for the aliasing declarations as well...	blob \| commitdiff \| raw \| diff to current
2016-07-06	Guy	A few proof bugs fixed	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-07-01	Guy	When proving a lemma, ignore literals that don't belong...	blob \| commitdiff \| raw \| diff to current
2016-07-01	Guy	Handle bitvector lemmas where a literal gets rewritten...	blob \| commitdiff \| raw \| diff to current
2016-06-30	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-30	Guy	Support for the letification of chained AND and OR...	blob \| commitdiff \| raw \| diff to current
2016-06-23	Clark Barrett	Fixed some warnings, fixed bug in cdhashmap that was...	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-20	Guy	Addressed a bug that occurs when proof production is...	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-08	Guy	Support for printing a global let map in LFSC proofs.	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	Guy	Better infrastructure for proving constant disequality.	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Revert "Merging proof branch"	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merging proof branch	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-03-23	guykatzz	Merge pull request #82 from CVC4/master_for_merge	blob \| commitdiff \| raw \| diff to current
2016-03-23	Guy	squash-merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-02-24	Tim King	Unifying the definitions of ClauseId to a single source...	blob \| commitdiff \| raw \| diff to current
2016-02-01	Tim King	Adding a destructor to ProofOutputChannel.	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2016-01-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current
2015-03-10	ajreynol	CNF proofs. Infrastructure for preprocessing proofs...	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-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-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-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-09	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-08	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-02	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2013-12-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2013-12-26	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-12-24	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2013-12-24	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2013-12-23	Morgan Deters	Proof-checking code; fixups of segfaults and missing...	blob \| commitdiff \| raw \| diff to current
2013-11-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-11-06	lianah	fixed proof regression script and added a new uf test...	blob \| commitdiff \| raw \| diff to current
2013-11-04	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-09	lianah	cleaned up proof code	blob \| commitdiff \| raw \| diff to current
2013-10-09	lianah	fixed uf proof bug: now storing deleted theory lemmas	blob \| commitdiff \| raw \| diff to current
2013-10-08	lianah	added currying for uf proofs; still needs debugging	blob \| commitdiff \| raw \| diff to current
2013-10-08	lianah	fixed uf proof with holes bugs	blob \| commitdiff \| raw \| diff to current
2013-10-08	Liana Hadarean	first draft implementation of uf proofs with holes	blob \| commitdiff \| raw \| diff to current

RSS Atom