projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3fcaab) | patch
Decouple modules from TheoryArithPrivate (#5184)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 2 Oct 2020 14:06:02 +0000 (09:06 -0500)
committerGitHub <noreply@github.com>
Fri, 2 Oct 2020 14:06:02 +0000 (09:06 -0500)
commit3051fd4ea618348da9a0b856b7bb07fcda027839
treeff7870f6eb4eb875da499bcb285007fdc33a9a74tree
parentd3fcaabbafdfebe17aa20f656ff2d3922d0dcb96commit | diff
Decouple modules from TheoryArithPrivate (#5184)

This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.

This is in preparation for further refactoring of (lazy) arithmetic operator elimination.
src/CMakeLists.txt diff | blob | history
src/theory/arith/callbacks.h diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history
src/theory/arith/theory_arith_private_forward.h [deleted file] blob | history