projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a5d7d89) | patch
Refactor post rewriter for addition (#7931)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 13 Jan 2022 00:55:46 +0000 (16:55 -0800)
committerGitHub <noreply@github.com>
Thu, 13 Jan 2022 00:55:46 +0000 (00:55 +0000)
commite233e778d8b7beb6783e566e0c1659df792b93ba
treeb9af67f05ad94a6dd3abc81b10f72ada8f282412tree
parenta5d7d89b2e26491987d674471e9eb1924e3ea3decommit | diff
Refactor post rewriter for addition (#7931)

This makes the post rewriter for addition aware of real algebraic numbers. Also, it tries a bit harder to avoid the normal_form utilities if only constants are present.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_arith_rewriter_black.cpp [new file with mode: 0644] blob