summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Expand)Author
2021-10-25[proofs] Alethe: Translate SPLIT rule (#7399)Lachnitt
2021-10-22Fix out-of-sync pruning in CDCAC proofs (#7470)Gereon Kremer
2021-10-22[proofs] Alethe: Translate FACTORING rule (#7398)Lachnitt
2021-10-22[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)Lachnitt
2021-10-20Eliminate last static calls to rewriter from smt layer (#7355)Andrew Reynolds
2021-10-20[proofs] Alethe: Documentation on Translation (#7394)Lachnitt
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-07Finish the LFSC printer (#7285)Andrew Reynolds
2021-10-01Add the LFSC printer (#7158)Andrew Reynolds
2021-09-23[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)Lachnitt
2021-09-23[proofs] Alethe: Translate THEORY_REWRITE (#7236)Lachnitt
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
2021-09-23[proofs] Alethe: Translate SCOPE rule (#7224)Lachnitt
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
2021-09-21[Proofs] Alethe: Translate ASSUME rule (#7213)Lachnitt
2021-09-21[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)Lachnitt
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
2021-09-20Add the LFSC proof post-processor (#7134)Andrew Reynolds
2021-09-17[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)Lachnitt
2021-09-17[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)Lachnitt
2021-09-15[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)Lachnitt
2021-09-15[proof] Added printer for proof rule names (#7185)Lachnitt
2021-09-15[proof] Alethe proof rules (#7180)Lachnitt
2021-09-08Add Lfsc print channel utilities (#7123)Andrew Reynolds
2021-09-08Improve pre-skolemization, move quantifiers preprocess to own file (#7153)Andrew Reynolds
2021-09-08Add LFSC side condition conversion utility for list variables (#7131)Andrew Reynolds
2021-09-08Use rewriteViaMethod instead of accessing builtin proof checker (#7146)Andrew Reynolds
2021-09-02Add LFSC node converter (#6944)Andrew Reynolds
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-01Fix issues with cyclic proofs due to double SYMM applications (#7083)Andrew Reynolds
2021-09-01Lazy proof reconstruction for strings theory solver (#7096)Andrew Reynolds
2021-08-30Fix proof equality engine for "no-explain" premises (#7079)Andrew Reynolds
2021-08-24Uniform treatment of trusted theory inferences in proofs (#7044)Andrew Reynolds
2021-08-24Miscellaneous changes from proof-new (#7042)Andrew Reynolds
2021-08-04Proper printing of proofs in the internal calculus (#6975)Andrew Reynolds
2021-08-04Fix policy for merging subproofs (#6981)Andrew Reynolds
2021-08-04[proof] [dot] Fix comments on dot printer (#6983)Diego Della Rocca de Camargos
2021-08-04Add containsAssumption proof utility (#6953)Andrew Reynolds
2021-07-27proof: Add eqrange expansion rule. (#6936)Mathias Preiner
2021-07-27Track instantiation reasons in proofs (#6935)Andrew Reynolds
2021-07-27Add basic LFSC utilities (#6879)Andrew Reynolds
2021-07-27Add print expression utility (#6880)Andrew Reynolds
2021-07-27Add proof letify utility (#6881)Andrew Reynolds
2021-07-26Enable default equality proofs for sets (#6931)Andrew Reynolds
2021-07-22Preparation for carry the rewrite rule database in the proof checker (#6915)Andrew Reynolds
2021-07-15Distinguish quantifiers preprocess as its own proof rule (#6897)Andrew Reynolds
2021-07-13bv: Simplify BV_BITBLAST_* proof rules. (#6871)Mathias Preiner
2021-07-08[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)Haniel Barbosa
2021-06-30Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)Andrew Reynolds
2021-06-28[proof] [dot] Make dot printer stateful (#6799)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback