projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Expand arith's farkas lemma rule as a macro (#6577)
[cvc5.git] / src / expr / proof_rule.h
2021-05-20 Alex OzdemirExpand arith's farkas lemma rule as a macro (#6577) blob | commitdiff | raw
2021-05-06 Haniel Barbosa[proof-new] Updating documentation for Subs/Rw ids... blob | commitdiff | raw | diff to current
2021-04-24 Mathias PreinerAdd assumption-based unsat cores. (#6427) blob | commitdiff | raw | diff to current
2021-04-23 Aina NiemetzBV: Add proof logging for bit-blasting. (#6373) blob | commitdiff | raw | diff to current
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) 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-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) blob | commitdiff | raw | diff to current
2021-03-10 Haniel Barbosa[proof-new] Clarifying doc (#6108) blob | commitdiff | raw | diff to current
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) blob | commitdiff | raw | diff to current
2021-03-10 Andrew Reynolds(proof-new) Replace witness form by original form in... blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966) blob | commitdiff | raw | diff to current
2021-02-23 Gereon KremerAdd 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 KremerAdd 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
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) blob | commitdiff | raw | diff to current
2020-12-21 Gereon KremerAdd 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 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating... blob | commitdiff | raw | diff to current
2020-12-08 Mathias PreinerAdd 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-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... 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-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) blob | commitdiff | raw | diff to current
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262) blob | commitdiff | raw | diff to current
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... 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-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate 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 robustness of CONG rule (#4882) 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-07-02 Andrew Reynolds(proof-new) Proof rule checkers run on skolem forms... blob | commitdiff | raw | diff to current
2020-06-28 Alex OzdemirProof Rules and Checker for Arithmetic (#4665) blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate 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 ReynoldsAdd SCOPE proof rule (#4332) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsAdd ProofNode data structure (#4311) blob | commitdiff | raw | diff to current