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

[cvc5.git] / src / expr / proof_rule.cpp

2021-03-10	Andrew Reynolds	(proof-new) Replace witness form by original form in...	blob \| commitdiff \| raw
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-02-23	Gereon Kremer	Add proof for mult sign lemma (#5966)	blob \| commitdiff \| raw \| diff to current
2021-02-23	Gereon Kremer	Add proof for monomial bounds check (#5965)	blob \| commitdiff \| raw \| diff to current
2021-02-23	Gereon Kremer	(proof-new) Add proof generator for CAD solver (#5964)	blob \| commitdiff \| raw \| diff to current
2021-02-23	Gereon Kremer	Add trans secant proofs. (#5957)	blob \| commitdiff \| raw \| diff to current
2021-02-22	Gereon Kremer	(proof-new) Add proofs for exponential functions (...	blob \| commitdiff \| raw \| diff to current
2021-02-22	Gereon Kremer	(proof-new) Add proofs for sine lemmas in the transcend...	blob \| commitdiff \| raw \| diff to current
2021-02-02	Andrew Reynolds	(proof-new) Miscellaneous fixes and regressions (#5841)	blob \| commitdiff \| raw \| diff to current
2020-12-21	Gereon Kremer	Add proof for pi bound lemma (#5709)	blob \| commitdiff \| raw \| diff to current
2020-12-21	Gereon Kremer	Add proof for sine shift lemmas. (#5710)	blob \| commitdiff \| raw \| diff to current
2020-12-18	Gereon Kremer	(proof-new) Add proof for tangent plane lemmas (#5700)	blob \| commitdiff \| raw \| diff to current
2020-12-08	Mathias Preiner	Add support for BV proofs with the simple bitblasting...	blob \| commitdiff \| raw \| diff to current
2020-12-02	Andrew Reynolds	(proof-new) Proofs for expand definitions (#5562)	blob \| commitdiff \| raw \| diff to current
2020-10-26	Andrew Reynolds	(proof-new) Add datatypes proof checker (#5340)	blob \| commitdiff \| raw \| diff to current
2020-10-18	Andrew Reynolds	(proof-new) Implementation of trust substitution (...	blob \| commitdiff \| raw \| diff to current
2020-10-13	Andrew Reynolds	(proof-new) New rules for Booleans (#5243)	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-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-21	Andrew Reynolds	(proof-new) Add the arrays proof checker (#5047)	blob \| commitdiff \| raw \| diff to current
2020-09-16	Haniel Barbosa	[proof-new] Resolution rules and checkers (#5070)	blob \| commitdiff \| raw \| diff to current
2020-09-02	Andrew Reynolds	(proof-new) Updates to builtin proof checker (#4962)	blob \| commitdiff \| raw \| diff to current
2020-09-02	Andrew Reynolds	(proof-new) Add proof support in TheoryUF (#5002)	blob \| commitdiff \| raw \| diff to current
2020-08-18	Andrew Reynolds	(proof-new) Theory preprocessor proof producing (#4807)	blob \| commitdiff \| raw \| diff to current
2020-08-15	Andrew Reynolds	(proof-new) Add the strings proof checker (#4858)	blob \| commitdiff \| raw \| diff to current
2020-08-12	Andrew Reynolds	(proof-new) Improve interfaces to proof generators...	blob \| commitdiff \| raw \| diff to current
2020-08-12	Andrew Reynolds	(proof-new) Witness form proof generator (#4782)	blob \| commitdiff \| raw \| diff to current
2020-07-27	Andrew Reynolds	(proof-new) Proof production for term formula removal...	blob \| commitdiff \| raw \| diff to current
2020-07-17	Andrew Reynolds	(proof-new) Updates to strings core solver (#4642)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andrew Reynolds	(proof-new) Skeleton proof support in the Rewriter...	blob \| commitdiff \| raw \| diff to current
2020-07-13	Andrew Reynolds	(proof-new) SMT Preprocess proof generator (#4708)	blob \| commitdiff \| raw \| diff to current
2020-06-28	Alex Ozdemir	Proof Rules and Checker for Arithmetic (#4665)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-16	Andrew Reynolds	(proof-new) Add quantifiers proof checker (#4593)	blob \| commitdiff \| raw \| diff to current
2020-06-03	Haniel Barbosa	(proof-new) Adding rules and proof checker for EUF...	blob \| commitdiff \| raw \| diff to current
2020-06-03	Haniel Barbosa	(proof-new) Adding rules and proof checker for Boolean...	blob \| commitdiff \| raw \| diff to current
2020-06-03	Andrew Reynolds	(proof-new) Add builtin proof checker (#4537)	blob \| commitdiff \| raw \| diff to current
2020-04-20	Andrew Reynolds	Add SCOPE proof rule (#4332)	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Add ProofNode data structure (#4311)	blob \| commitdiff \| raw \| diff to current

RSS Atom