projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9f8d593) | patch
[proofs] Alethe: Translate of Arithmetic rules (#7613)
authorLachnitt <lachnitt@stanford.edu>
Wed, 10 Nov 2021 12:54:09 +0000 (04:54 -0800)
committerGitHub <noreply@github.com>
Wed, 10 Nov 2021 12:54:09 +0000 (12:54 +0000)
commite57c53e8a3c518a00cf52f199d14fbec94bdaca8
tree936cdb22fa772ece50d477d1d39891aeffc83c99tree
parent9f8d59391ecf0272db184624e4e44ee13241c6bdcommit | diff
[proofs] Alethe: Translate of Arithmetic rules (#7613)

Implementation of the translation of MACRO_ARITH_SCALE_SUM_UB, INT_TIGHT_UB and INT_TIGHT_LB into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
src/proof/alethe/alethe_post_processor.cpp diff | blob | history