projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ffbdd1b) | patch
Refactor rewriteMinus (#7932)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 12 Jan 2022 22:19:31 +0000 (14:19 -0800)
committerGitHub <noreply@github.com>
Wed, 12 Jan 2022 22:19:31 +0000 (22:19 +0000)
commitd603925de77bc465fe6bfe5097e848224337acf9
treed632a93173b4e2ea8d6dec0cf2c39b7688d2cf30tree
parentffbdd1b3c3352fa342683facb44ca3e916844ac7commit | diff
Refactor rewriteMinus (#7932)

Refactors rewriteMinus to be generally simpler and explicitly rely on rewriting addition.
Note that rewriteMinus would almost never be called in post rewrite anyway, as it would rewrite to addition in pre rewrite.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history