Cleanup of inferences in arithmetic theory (#5927)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 19 Feb 2021 08:34:36 +0000 (09:34 +0100)
committerGitHub <noreply@github.com>
Fri, 19 Feb 2021 08:34:36 +0000 (09:34 +0100)
commitce58453982ddd53a5fc08d9db4c6c3f49b852838
treee77cb66ff4d5bca985524d3c2befd33d580916af
parent6ae21de6f85d9629018c1b6bf912ef39f3e169fb
Cleanup of inferences in arithmetic theory (#5927)

This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:

    remove the ArithLemma class and uses SimpleTheoryLemma instead
    only use NlLemma if we actually need it
    use proper InferenceIds everywhere
    remove unused code in the nonlinear extension
25 files changed:
src/CMakeLists.txt
src/theory/arith/arith_lemma.cpp [deleted file]
src/theory/arith/arith_lemma.h [deleted file]
src/theory/arith/arith_preprocess.cpp
src/theory/arith/inference_manager.cpp
src/theory/arith/inference_manager.h
src/theory/arith/nl/cad_solver.cpp
src/theory/arith/nl/ext/factoring_check.cpp
src/theory/arith/nl/ext/monomial_bounds_check.cpp
src/theory/arith/nl/ext/monomial_check.cpp
src/theory/arith/nl/ext/monomial_check.h
src/theory/arith/nl/ext/split_zero_check.cpp
src/theory/arith/nl/ext/tangent_plane_check.cpp
src/theory/arith/nl/iand_solver.cpp
src/theory/arith/nl/icp/icp_solver.cpp
src/theory/arith/nl/nl_lemma_utils.cpp
src/theory/arith/nl/nl_lemma_utils.h
src/theory/arith/nl/nl_model.cpp
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/nonlinear_extension.h
src/theory/arith/nl/transcendental/exponential_solver.cpp
src/theory/arith/nl/transcendental/sine_solver.cpp
src/theory/arith/nl/transcendental/transcendental_state.cpp
src/theory/inference_id.cpp
src/theory/inference_id.h