summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Expand)Author
2021-09-02Formatajreynol
2021-09-02Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-02Add missing Boolean rules to LFSC printerajreynol
2021-09-01Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
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-31Formatajreynol
2021-08-31Use more robust conversion for arithmetic trichotomyajreynol
2021-08-31Support arith trichotomy in LFSCajreynol
2021-08-31Formatajreynol
2021-08-31Add support concat unify in LFSCajreynol
2021-08-30Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-30Fix proof equality engine for "no-explain" premises (#7079)Andrew Reynolds
2021-08-26Fix LFSC for inst pattern listajreynol
2021-08-26Fixes from merge, refactorajreynol
2021-08-26Formatajreynol
2021-08-25Formatajreynol
2021-08-25Doc LFSC convertajreynol
2021-08-25Alpha equivalenceajreynol
2021-08-24Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
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-20Formatajreynol
2021-08-20Minorajreynol
2021-08-16Formatajreynol
2021-08-05Fix statsajreynol
2021-08-05Formatajreynol
2021-08-05Draft of annotation proof generator in theory inference managerajreynol
2021-08-05Preparing for annotation in theory inference manager, statisticsajreynol
2021-08-05Formatajreynol
2021-08-05Revisions to annotation proof generatorajreynol
2021-08-05Add draft of annotation proof generator utilityajreynol
2021-08-04Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-04Proper printing of proofs in the internal calculus (#6975)Andrew Reynolds
2021-08-04Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
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-04Formatajreynol
2021-08-04Docajreynol
2021-08-04Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-08-04Add containsAssumption proof utility (#6953)Andrew Reynolds
2021-08-04Make subproof merging robust to orderajreynol
2021-08-02Formatajreynol
2021-07-30Add proper conversion for bitblast term, proper printing for bitOf, update LF...ajreynol
2021-07-30Formatajreynol
2021-07-30Simplify smt2 printer, fix order issue in strings eager reduction, update LFS...ajreynol
2021-07-30Improveajreynol
2021-07-30Formatajreynol
2021-07-30Fix lfsc for bb termajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback