projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a02a794) | patch
(proof-new) Simplifications to arithmetic operator elimination and preprocessing...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 3 Mar 2021 17:25:02 +0000 (11:25 -0600)
committerGitHub <noreply@github.com>
Wed, 3 Mar 2021 17:25:02 +0000 (17:25 +0000)
commit8144381611d2c3dcdcf56bcd343690abe98f9d5e
tree482138ba397be43ec8619a0cf7fe90e823dcf650tree
parenta02a794c383ae2381e1210f53174cefb8d94e615commit | diff
(proof-new) Simplifications to arithmetic operator elimination and preprocessing (#6040)

Due to refactoring in theory preprocessor, which does fixed point preprocessing on created lemmas, several things can be simplified in arithmetic operator elimination.

This is required for further simplification to witness forms in the internal proof calculus.
src/theory/arith/operator_elim.cpp diff | blob | history
src/theory/arith/operator_elim.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history