projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e456766) | patch
Add rewrites for div/mod in the arithmetic rewriter (#5352)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 28 Oct 2020 17:35:43 +0000 (12:35 -0500)
committerGitHub <noreply@github.com>
Wed, 28 Oct 2020 17:35:43 +0000 (12:35 -0500)
commitb0dd5a3adc67d72a08ca9d8d3de208840a1001a3
treedecbb9c5c6ee9f927e91f49ee505fdacb62e815etree
parente4567666de0c6fe19e11eeecfecaebca03920a40commit | diff
Add rewrites for div/mod in the arithmetic rewriter (#5352)

This adds some basic rewrites for integer div/mod in the rewriter.

This is in preparation for improved preprocessing and rewriting for NIA problems with heavy use of div/mod.
src/CMakeLists.txt diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/rewrites.cpp [new file with mode: 0644] blob
src/theory/arith/rewrites.h [new file with mode: 0644] blob