projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e2b1154) | patch
Refactor abs rewriting (#7935)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 20 Jan 2022 18:29:25 +0000 (10:29 -0800)
committerGitHub <noreply@github.com>
Thu, 20 Jan 2022 18:29:25 +0000 (18:29 +0000)
commitf68764d01a070be71dda42e5e26483b2cfb1281a
tree018c9789eb144c697a42bb6ae9740670166e2096tree
parente2b1154c3e9a82e2a69e98a7ff7aadf73f9009dfcommit | diff
Refactor abs rewriting (#7935)

This PR refactors rewriting for ABS to also support real algebraic number. We also generalize the ABS operator to real arguments in general, instead of integer arguments.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/kinds diff | blob | history
test/unit/theory/theory_arith_rewriter_black.cpp diff | blob | history