projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
remove stuff (#7258)
[cvc5.git] / src / proof /
2021-09-23 Lachnitt[proofs[ Alethe: Fix Order of Arguments of addAletheSte... tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Translate THEORY_REWRITE (#7236) tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Add Alethe Files to be Compiled ... tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Translate SCOPE rule (#7224) tree | commitdiff
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-21 Lachnitt[Proofs] Alethe: Translate ASSUME rule (#7213) tree | commitdiff
2021-09-21 Lachnitt[proofs] Alethe: Implementation of AletheProofPostproce... tree | commitdiff
2021-09-20 Haniel Barbosa[proofs] Alethe: adds a node converter tree | commitdiff
2021-09-20 Andrew ReynoldsAdd the LFSC proof post-processor (#7134) tree | commitdiff
2021-09-17 Lachnitt[proofs] Alethe: Added Proof Postprocessor to alethe_pr... tree | commitdiff
2021-09-17 Lachnitt[proofs] Alethe: Added Final Callback Function to aleth... tree | commitdiff
2021-09-15 Lachnitt[proofs] Alethe: Added Callback Function to alethe_proo... tree | commitdiff
2021-09-15 Lachnitt[proof] Added printer for proof rule names (#7185) tree | commitdiff
2021-09-15 Lachnitt[proof] Alethe proof rules (#7180) tree | commitdiff
2021-09-08 Andrew ReynoldsAdd Lfsc print channel utilities (#7123) tree | commitdiff
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... tree | commitdiff
2021-09-08 Andrew ReynoldsAdd LFSC side condition conversion utility for list... tree | commitdiff
2021-09-08 Andrew ReynoldsUse rewriteViaMethod instead of accessing builtin proof... tree | commitdiff
2021-09-02 Andrew ReynoldsAdd LFSC node converter (#6944) tree | commitdiff
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) tree | commitdiff
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic... tree | commitdiff
2021-09-01 Andrew ReynoldsLazy proof reconstruction for strings theory solver... tree | commitdiff
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... tree | commitdiff
2021-08-24 Andrew ReynoldsUniform treatment of trusted theory inferences in proof... tree | commitdiff
2021-08-24 Andrew ReynoldsMiscellaneous changes from proof-new (#7042) tree | commitdiff
2021-08-04 Andrew ReynoldsProper printing of proofs in the internal calculus... tree | commitdiff
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981) tree | commitdiff
2021-08-04 Diego Della Rocca... [proof] [dot] Fix comments on dot printer (#6983) tree | commitdiff
2021-08-04 Andrew ReynoldsAdd containsAssumption proof utility (#6953) tree | commitdiff
2021-07-27 Mathias Preinerproof: Add eqrange expansion rule. (#6936) tree | commitdiff
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935) tree | commitdiff
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879) tree | commitdiff
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880) tree | commitdiff
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881) tree | commitdiff
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931) tree | commitdiff
2021-07-22 Andrew ReynoldsPreparation for carry the rewrite rule database in... tree | commitdiff
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof... tree | commitdiff
2021-07-13 Mathias Preinerbv: Simplify BV_BITBLAST_* proof rules. (#6871) tree | commitdiff
2021-07-08 Haniel Barbosa[proof] [dot] Print let map (of terms in proof) as... tree | commitdiff
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces... tree | commitdiff
2021-06-28 Haniel Barbosa[proof] [dot] Make dot printer stateful (#6799) tree | commitdiff
2021-06-23 Haniel Barbosa[proofs] [dot] Adding a counter for subproofs (#6735) tree | commitdiff
2021-06-21 Haniel Barbosa[proof] Fix documentation of array rule (#6770) tree | commitdiff
2021-06-07 Andrew Reynolds(proof-new) Fix missing connection in trust substitutio... tree | commitdiff
2021-06-07 Andrew Reynolds(proof-new) Lazy proof chain debug names (#6680) tree | commitdiff
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-04-26 Diego Della Rocca... New design in DOT representation, nodes colored based... tree | commitdiff
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-14 Haniel Barbosa[proof-new] Miscellaneous improvements to dot printer... tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) tree | commitdiff
2021-03-14 Diego Della Rocca... [proof-new] Adding a dot printer for proof nodes (... tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-03 Andres NoetzliRemove SWIG bindings (#4683) tree | commitdiff
2020-06-19 Haniel BarbosaGeneralize atom collection in old proof code (#4626) tree | commitdiff
2020-06-18 Andres NoetzliImprove memory management in Java bindings (#4629) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) tree | commitdiff
2020-03-16 Alex OzdemirRemove AlwaysAssert(false) for hole. tree | commitdiff
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826) tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752) tree | commitdiff
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740) tree | commitdiff
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732) tree | commitdiff
2020-02-07 Alex OzdemirPropagate expected types through UF arguments (#3717) tree | commitdiff
2020-02-07 Alex OzdemirAdd `ArithProof::{printInteger,getLfscFunction}` (... tree | commitdiff
2020-02-01 Alex OzdemirHandle `expectedType` in TheoryProofEngine (#3691) tree | commitdiff
2020-01-30 Alex OzdemirexpectedType in proof-printing code (#3665) tree | commitdiff
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... tree | commitdiff
2019-11-19 Alex OzdemirAdd a few comments to ProofManager (#3477) tree | commitdiff
next