projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f039c2a) | patch
Refactor multiplication in arithmetic rewriter (#7965)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 23 Feb 2022 14:57:53 +0000 (15:57 +0100)
committerGitHub <noreply@github.com>
Wed, 23 Feb 2022 14:57:53 +0000 (14:57 +0000)
commit281bda09e88c568d151464559e00e4ea73c7192f
tree96eb0c5f124b07557b501cffa8f84fb37e7cc2fctree
parentf039c2a0eaf7ce44af9e8b8df64960cf0c409478commit | diff
Refactor multiplication in arithmetic rewriter (#7965)

This PR refactors the rewriting of multiplication. Most importantly, we explicitly deal with distributivity of addition and multiplication explicitly using the new utilities.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/rewriter/addition.h diff | blob | history
src/theory/arith/rewriter/ordering.h diff | blob | history