summaryrefslogtreecommitdiff
path: root/src/expr/proof_rule.h
AgeCommit message (Expand)Author
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-21(proof-new) Minor documentation sync (#6592)Andrew Reynolds
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Expand arith's farkas lemma rule as a macro (#6577)Alex Ozdemir
2021-05-06[proof-new] Updating documentation for Subs/Rw ids (#6502)Haniel Barbosa
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-23BV: Add proof logging for bit-blasting. (#6373)Aina Niemetz
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-09[proof-new] Optimizing sat proof (#6324)Haniel Barbosa
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-11arith proof rules shuffle & add ARITH_SUM_UB (#6118)Alex Ozdemir
2021-03-10[proof-new] Clarifying doc (#6108)Haniel Barbosa
2021-03-10Improve arithmetic proofs (#6106)Gereon Kremer
2021-03-10(proof-new) Replace witness form by original form in the internal proof calcu...Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
2021-02-22(proof-new) Add proofs for exponential functions (#5956)Gereon Kremer
2021-02-22(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)Gereon Kremer
2020-12-21Add proof for pi bound lemma (#5709)Gereon Kremer
2020-12-21Add proof for sine shift lemmas. (#5710)Gereon Kremer
2020-12-18(proof-new) Add proof for tangent plane lemmas (#5700)Gereon Kremer
2020-12-07[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)Haniel Barbosa
2020-12-07Add support for BV proofs with the simple bitblasting solver. (#5603)Mathias Preiner
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-11-30(proof-new) Proofs for regular expression elimination (#5361)Andrew Reynolds
2020-10-26(proof-new) Add datatypes proof checker (#5340)Andrew Reynolds
2020-10-20(proof-new) Fixes for proofs in rewriter (#5307)Andrew Reynolds
2020-10-19[proof-new] Fixing resolution proof checker (#5262)Haniel Barbosa
2020-10-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-18(proof-new) Implementation of trust substitution (#5276)Andrew Reynolds
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
2020-10-08(proof-new) Fixes and improvements for smt proof postprocessor (#5197)Andrew Reynolds
2020-09-28Minor fixes to quantifiers proofs (#5151)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-08-18(proof-new) Theory preprocessor proof producing (#4807)Andrew Reynolds
2020-08-15(proof-new) Add the strings proof checker (#4858)Andrew Reynolds
2020-08-12(proof-new) Improve robustness of CONG rule (#4882)Andrew Reynolds
2020-08-12(proof-new) Improve interfaces to proof generators (#4803)Andrew Reynolds
2020-08-12(proof-new) Witness form proof generator (#4782)Andrew Reynolds
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback