projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e01ae3a) | patch
Add arithmetic preprocess rewrite equality module (#6860)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Jul 2021 18:55:13 +0000 (13:55 -0500)
committerGitHub <noreply@github.com>
Mon, 12 Jul 2021 18:55:13 +0000 (18:55 +0000)
commitb35641f1a4ac8d70cf868b273971ee7c5e3b35f0
treee05ba328b28ed05a11756712a9303ac05cefdd1dtree
parente01ae3a87f4e1dc4b4511e8bd028d5c0838ccedccommit | diff
Add arithmetic preprocess rewrite equality module (#6860)

This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.

This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.
src/CMakeLists.txt diff | blob | history
src/theory/arith/pp_rewrite_eq.cpp [new file with mode: 0644] blob
src/theory/arith/pp_rewrite_eq.h [new file with mode: 0644] blob