projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b994f33) | patch
Add utilities for flattening nodes (#7961)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 31 Jan 2022 21:49:21 +0000 (13:49 -0800)
committerGitHub <noreply@github.com>
Mon, 31 Jan 2022 21:49:21 +0000 (21:49 +0000)
commitac2a185f2895095f2c8e1ddb52aa33c40ab07e2e
treedf5c81c248c0be8d594764975c83088e72c04d2ctree
parentb994f336a7db6180427014721d673519ee6febf3commit | diff
Add utilities for flattening nodes (#7961)

This PR adds new utilities for flattening nodes and checking whether they can be flattened. They replace the custom implementation we used in the arithmetic rewriter.
src/expr/CMakeLists.txt diff | blob | history
src/expr/algorithm/flatten.h [new file with mode: 0644] blob
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/unit/node/CMakeLists.txt diff | blob | history
test/unit/node/node_algorithms_black.cpp [new file with mode: 0644] blob