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

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

2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw
2020-02-27	Andres Noetzli	Fix -Wshadow warnings in common headers (#3826)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Alex Ozdemir	expectedType in proof-printing code (#3665)	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-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	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-01-14	Alex Ozdemir	ClausalBitvectorProof (#2786)	blob \| commitdiff \| raw \| diff to current
2018-12-17	Aina Niemetz	New C++ API: Add tests for term object. (#2755)	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-08-27	Andres Noetzli	Resolution proof: separate printing from proof (#1964)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-04-25	yoni206	Refactor array-proofs and uf-proofs (#1655)	blob \| commitdiff \| raw \| diff to current
2018-04-02	Mathias Preiner	Reorganize bitblaster code. (#1695)	blob \| commitdiff \| raw \| diff to current
2017-11-16	Tim King	Initializes BitVectorProof::d_isAssumptionConflict...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-03-23	guykatzz	support incremental unsat cores	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	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-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	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	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-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-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	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-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-03	Guy	A better mechanism for handling BV terms with aliases...	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Fixed a magical bug that only appears when compiling...	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Fix	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-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current

RSS Atom