projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f051883) | patch
Refactor rewriting of arithmetic addition (#8180)
authorGereon Kremer <gkremer@cs.stanford.edu>
Mon, 28 Feb 2022 15:22:48 +0000 (16:22 +0100)
committerGitHub <noreply@github.com>
Mon, 28 Feb 2022 15:22:48 +0000 (09:22 -0600)
commit77966f11fad2979a843722ba1bbc22dab2104ff1
tree0759fda979cf2e7a3898e0db9e36f717b8cc1a40tree
parentf051883afa31d9dbe14a5d1ae1c9700cffded3b1commit | diff
Refactor rewriting of arithmetic addition (#8180)

This PR uses the new addition utilities to refactor rewriting of arithmetic addition. This properly handles real algebraic numbers now, eliminating a few more edge cases where the previous solution might allow for non-idempotent rewrites.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/rewriter/addition.cpp diff | blob | history
src/theory/arith/rewriter/node_utils.cpp diff | blob | history