projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f66cbab) | patch
Eliminate arithmetic proof macros (#7226)
authorGereon Kremer <nafur42@gmail.com>
Wed, 22 Sep 2021 05:39:32 +0000 (22:39 -0700)
committerGitHub <noreply@github.com>
Wed, 22 Sep 2021 05:39:32 +0000 (05:39 +0000)
commitb849961a85b61a29b13f8f58aa8ed7fff3c902a4
treeba97a4ddfea0b8c9ffd5beb0d490aab8b81d033etree
parentf66cbabd6b67462ebbf9bbba5d3ccfb08b69ff25commit | diff
Eliminate arithmetic proof macros (#7226)

This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.
src/CMakeLists.txt diff | blob | history
src/theory/arith/callbacks.cpp diff | blob | history
src/theory/arith/callbacks.h diff | blob | history
src/theory/arith/constraint.cpp diff | blob | history
src/theory/arith/constraint.h diff | blob | history
src/theory/arith/linear_equality.cpp diff | blob | history
src/theory/arith/linear_equality.h diff | blob | history
src/theory/arith/proof_macros.h [deleted file] blob | history
src/theory/arith/simplex.cpp diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history