projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b32209) | patch
Add utilities to rewrite atoms for the arithmetic rewriter (#8014)
authorGereon Kremer <gkremer@cs.stanford.edu>
Fri, 25 Feb 2022 21:22:36 +0000 (22:22 +0100)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 21:22:36 +0000 (21:22 +0000)
commit0c8319a7ffe36f407f2b541bbd0a99f31b7add81
treeb2c6506df005be52b118558b5efc7698bfd7e4cdtree
parent5b32209ea2dd947c4cea384b2166e1de401cb929commit | diff
Add utilities to rewrite atoms for the arithmetic rewriter (#8014)

This PR adds utilities to rewrite atoms in the arithmetic rewriter. They retain compatibility with the current normal_form utility, but make the process more transparent so that changing the normal form in the future should be simpler.
src/CMakeLists.txt diff | blob | history
src/theory/arith/rewriter/addition.cpp diff | blob | history
src/theory/arith/rewriter/rewrite_atom.cpp [new file with mode: 0644] blob
src/theory/arith/rewriter/rewrite_atom.h [new file with mode: 0644] blob