git.libre-soc.org Git - cvc5.git/history - src/smt/proof_post

[cvc5.git] / src / smt / proof_post_processor.cpp

2021-05-20	Alex Ozdemir	Expand arith's farkas lemma rule as a macro (#6577)	blob \| commitdiff \| raw
2021-05-13	Mathias Preiner	Add std::hash overloads for Node, TNode and TypeNode...	blob \| commitdiff \| raw \| diff to current
2021-04-23	Andrew Reynolds	Add new substitution apply methods fixpoint, sequential...	blob \| commitdiff \| raw \| diff to current
2021-04-14	Gereon Kremer	Refactor / reimplement statistics (#6162)	blob \| commitdiff \| raw \| diff to current
2021-04-12	Aina Niemetz	Refactor and update copyright headers. (#6316)	blob \| commitdiff \| raw \| diff to current
2021-04-09	Haniel Barbosa	[proof-new] Optimizing sat proof (#6324)	blob \| commitdiff \| raw \| diff to current
2021-04-07	Haniel Barbosa	[proof-new] Fixing SMT post-processor's handling of...	blob \| commitdiff \| raw \| diff to current
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw \| diff to current
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-12	Andrew Reynolds	(proof-new) Miscellaneous sync to master (#6129)	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-03	Gereon Kremer	More cleanup of includes to reduce compilation times...	blob \| commitdiff \| raw \| diff to current
2021-02-22	Andrew Reynolds	(proof-new) Change proof-new option to proof (#5955)	blob \| commitdiff \| raw \| diff to current
2021-02-03	Haniel Barbosa	[proof-new] Fix MACRO_RESOLUTION expansion for singleto...	blob \| commitdiff \| raw \| diff to current
2021-02-02	Haniel Barbosa	[proof-new] Fix bug in expansion of MACRO_RESOLUTION...	blob \| commitdiff \| raw \| diff to current
2021-01-29	Andrew Reynolds	(proof-new) Distinguish pre vs post rewrites in term...	blob \| commitdiff \| raw \| diff to current
2021-01-22	Haniel Barbosa	[proof-new] Expanding MACRO_RESOLUTION in post-processi...	blob \| commitdiff \| raw \| diff to current
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-11-12	Andrew Reynolds	(proof-new) Improve printing and debugging for pedantic...	blob \| commitdiff \| raw \| diff to current
2020-10-21	Andrew Reynolds	(proof-new) Fixes for proofs in rewriter (#5307)	blob \| commitdiff \| raw \| diff to current
2020-10-20	Andrew Reynolds	(proof-new) Update add lazy step interface in LazyCDPro...	blob \| commitdiff \| raw \| diff to current
2020-10-18	Andrew Reynolds	(proof-new) More features for SMT proof post-processor...	blob \| commitdiff \| raw \| diff to current
2020-10-08	Andrew Reynolds	(proof-new) Fixes and improvements for smt proof postpr...	blob \| commitdiff \| raw \| diff to current
2020-09-29	Haniel Barbosa	[proof-new] Updates to proof node updater (#5156)	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-18	Andrew Reynolds	(proof-new) Updates to proof node updater algorithm...	blob \| commitdiff \| raw \| diff to current
2020-08-28	Andrew Reynolds	(proof-new) Add the SMT proof post processor (#4913)	blob \| commitdiff \| raw \| diff to current
2020-08-18	Andrew Reynolds	(proof-new) SMT proof postprocess callback (#4883)	blob \| commitdiff \| raw \| diff to current

RSS Atom