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

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

2020-10-28	Andrew Reynolds	Remove more uses of Expr (#5357)	blob \| commitdiff \| raw
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-06-19	Haniel Barbosa	Generalize atom collection in old proof code (#4626)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andres Noetzli	Fix issues with unsat cores and reset-assertions (...	blob \| commitdiff \| raw \| diff to current
2020-03-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-11-19	Alex Ozdemir	Add a few comments to ProofManager (#3477)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-07-02	Alex Ozdemir	Optimize DRAT optimization: clause matching (#3074)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2019-03-16	Alex Ozdemir	Enable CryptoMiniSat-backed BV proofs (#2847)	blob \| commitdiff \| raw \| diff to current
2019-03-13	Andres Noetzli	Add statistics for proof gen./checking time, size ...	blob \| commitdiff \| raw \| diff to current
2018-12-07	Alex Ozdemir	Enable BV proofs when using an eager bitblaster (#2733)	blob \| commitdiff \| raw \| diff to current
2018-12-03	Alex Ozdemir	Bit vector proof superclass (#2599)	blob \| commitdiff \| raw \| diff to current
2018-09-25	yoni206	carefully printing trusted assertions in proofs (#2505)	blob \| commitdiff \| raw \| diff to current
2018-08-27	Andres Noetzli	Resolution proof: separate printing from proof (#1964)	blob \| commitdiff \| raw \| diff to current
2018-07-13	Andres Noetzli	Properly clean up assertion stack in CnfProof (#2147)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	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-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-04	guykatzz	skolemization manager may be called also when just...	blob \| commitdiff \| raw \| diff to current
2017-03-23	guykatzz	support incremental unsat cores	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	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
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-06	guykatzz	Added an option that allow empty dependencies when...	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-03	Guy	Fixed an issue where arrays proofs would sometimes...	blob \| commitdiff \| raw \| diff to current
2016-08-03	barrettcw	Merge pull request #87 from 4tXJ7f/fix_oob_access	blob \| commitdiff \| raw \| diff to current
2016-07-28	Guy	The "aggressive" optimizer for lemma L now returns...	blob \| commitdiff \| raw \| diff to current
2016-07-28	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-28	Guy	Bug fix involving negated lemmas	blob \| commitdiff \| raw \| diff to current
2016-07-27	Guy	Proper handling of IFF lemmas in the unsat core.	blob \| commitdiff \| raw \| diff to current
2016-07-27	Guy	Added an option for a more aggressive weakest implicant...	blob \| commitdiff \| raw \| diff to current
2016-07-27	Guy	If we can't find a weaker implicant, fail gracefully...	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	Guy	Bug fix:	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	Guy	Letification of BV constants	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Added functionality to retrieve a lemma's "weakest...	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-20	Guy	Bug fix	blob \| commitdiff \| raw \| diff to current
2016-07-20	Guy	Allow a caller to query whether an unsat core is availa...	blob \| commitdiff \| raw \| diff to current
2016-07-15	Guy	Moved the assertion to a better spot	blob \| commitdiff \| raw \| diff to current
2016-07-15	Guy	The ProofManager now allows theory solvers to get their...	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-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-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-20	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-20	Guy	Fixed a bug where the proofManager's init() call was...	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-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-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-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-06-01	ajreynol	When proof enabled, disable uf sym break. Add regression.	blob \| commitdiff \| raw \| diff to current
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-23	Clark Barrett	Merge branch 'master' into google	blob \| commitdiff \| raw \| diff to current
2015-04-23	Liana Hadarean	Added option for --check-unsat-cores and various core...	blob \| commitdiff \| raw \| diff to current
2015-03-16	Liana Hadarean	Fixed proof unitialized memory and minor memory leaks.	blob \| commitdiff \| raw \| diff to current
2015-03-10	ajreynol	CNF proofs. Infrastructure for preprocessing proofs...	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
next

RSS Atom