projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add node utils for the arithmetic rewriter (#8012)
[cvc5.git] / src / proof /
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) tree | commitdiff
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) tree | commitdiff
2022-02-02 Andrew ReynoldsFix printing of re.loop as an operator in LFSC (#8029) tree | commitdiff
2022-02-02 Andrew ReynoldsAdd missing null terminators for regexp (#8027) tree | commitdiff
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique... tree | commitdiff
2022-01-10 Andrew ReynoldsFix internal type error when printing lambdas with... tree | commitdiff
2021-12-20 Andrew ReynoldsUpdates to LFSC signatures (#7840) tree | commitdiff
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-10 Haniel Barbosa[proofs] Make LazyCDProofChain extend CDProof (#7726) tree | commitdiff
2021-12-09 Andrew ReynoldsRemove a few static access to options in proof code... tree | commitdiff
2021-12-07 Gereon KremerRemove more static accesses to options (#7764) tree | commitdiff
2021-12-07 Andrew ReynoldsAdd proof annotation option (#7750) tree | commitdiff
2021-12-07 Lachnitt[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (... tree | commitdiff
2021-12-07 Lachnitt[proofs] Alethe: Fix Bug in Finalize (#7746) tree | commitdiff
2021-12-03 Lachnitt[proofs] Alethe: Implementation of Process Function... tree | commitdiff
2021-12-01 Haniel Barbosa[proofs] Add method to CDProof to obtain number of... tree | commitdiff
2021-12-01 Lachnitt[proofs] Alethe: Add finalize function to insert missin... tree | commitdiff
2021-12-01 LachnittAlethe: Add function that adds final steps to proof... tree | commitdiff
2021-11-30 LachnittAlethe: Further Printer Implementation (#7675) tree | commitdiff
2021-11-30 Lachnitt[proofs] Alethe: Implementation of Printer (#7674) tree | commitdiff
2021-11-30 Lachnitt[proofs] Alethe: Printer Specification (#7673) tree | commitdiff
2021-11-23 Gereon KremerPush output language inside the printing code (#7683) tree | commitdiff
2021-11-22 Gereon KremerRefactor IO stream manipulators (#7555) tree | commitdiff
2021-11-18 Lachnitt[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661) tree | commitdiff
2021-11-17 Andrew ReynoldsPreparations for eliminating arithmetic subtyping ... tree | commitdiff
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-12 Andrew Reynolds[proofs] Cancel SYMM in CDProof, throw an error for... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-10 Lachnitt[proofs] Alethe: Translate of Arithmetic rules (#7613) tree | commitdiff
2021-11-10 Lachnitt[proofs] Alethe: Translate INSTANTIATE rule (#7607) tree | commitdiff
2021-11-09 Lachnitt[proofs] Alethe: Translate Further Equality rules ... tree | commitdiff
2021-11-09 Lachnitt[proofs] Alethe: Translate Equality rules (#7605) tree | commitdiff
2021-11-09 Haniel Barbosa[proofs] Generalize trivial cycle detection in LazyCDPr... tree | commitdiff
2021-11-09 Lachnitt[proofs] Alethe: Translate REORDERING rule (#7533) tree | commitdiff
2021-11-08 Andrew ReynoldsAdd lambda lift utility (#7601) tree | commitdiff
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-08 Haniel Barbosa[proofs] Adding NoSubtype node converter to Alethe... tree | commitdiff
2021-11-08 Haniel Barbosa[proofs] Method to convert node representation of Aleth... tree | commitdiff
2021-11-06 Gereon KremerRemove `Notice()` in favor of new `verbose()` (#7588) tree | commitdiff
2021-11-05 Haniel Barbosa[proofs] Fix open sat proof (#7509) tree | commitdiff
2021-11-05 LachnittAlethe: Translate CNF rules (#7532) tree | commitdiff
2021-10-29 Andrew ReynoldsMinor cleanup of proof messages (#7494) tree | commitdiff
2021-10-29 Andrew ReynoldsAdd PfRule ARITH_POLY_NORM (#7501) tree | commitdiff
2021-10-29 Andrew ReynoldsImprovements for LFSC proof conversion (#7524) tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Modularize check for whether a clause is singl... tree | commitdiff
2021-10-26 Andrew ReynoldsDisable automatic symmetry in proofs of theory explanat... tree | commitdiff
2021-10-26 Lachnitt[proofs] Alethe: Translate Block of clause pattern... tree | commitdiff
2021-10-26 Lachnitt[proofs] Alethe: Translate AND_INTRO rule (#7405) tree | commitdiff
2021-10-26 Lachnitt[proofs] Alethe: Translate AND_ELIM rule (#7404) tree | commitdiff
2021-10-26 Lachnitt[proofs] Alethe: Translate CONTRA rule (#7403) tree | commitdiff
2021-10-26 Lachnitt[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402) tree | commitdiff
2021-10-25 Lachnitt[proofs] Alethe: Translate MODUS_PONENS rule (#7401) tree | commitdiff
2021-10-25 Lachnitt[proofs] Alethe: Translate EQ_RESOLVE rule (#7400) tree | commitdiff
2021-10-25 Lachnitt[proofs] Alethe: Translate SPLIT rule (#7399) tree | commitdiff
2021-10-22 Gereon KremerFix out-of-sync pruning in CDCAC proofs (#7470) tree | commitdiff
2021-10-22 Lachnitt[proofs] Alethe: Translate FACTORING rule (#7398) tree | commitdiff
2021-10-22 Lachnitt[proofs] Alethe: Translate CHAIN_RESOLUTION rule (... tree | commitdiff
2021-10-20 Andrew ReynoldsEliminate last static calls to rewriter from smt layer... tree | commitdiff
2021-10-20 Lachnitt[proofs] Alethe: Documentation on Translation (#7394) tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-07 Andrew ReynoldsFinish the LFSC printer (#7285) tree | commitdiff
2021-10-01 Andrew ReynoldsAdd the LFSC printer (#7158) tree | commitdiff
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
next