Refactoring theory inference process (#5920)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 19 Feb 2021 15:26:36 +0000 (09:26 -0600)
committerGitHub <noreply@github.com>
Fri, 19 Feb 2021 15:26:36 +0000 (09:26 -0600)
commitc4822869beac8d4a0eac4b234e0662d3db49f995
treed34b86c54b0ac8de6df4734e1e76afa5f43d5efb
parent00479d03cdeac3e864a1930dddb16c71c5bf2ce9
Refactoring theory inference process (#5920)

This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
31 files changed:
src/theory/arith/arith_preprocess.cpp
src/theory/arith/nl/iand_solver.cpp
src/theory/arith/nl/nl_lemma_utils.cpp
src/theory/arith/nl/nl_lemma_utils.h
src/theory/arrays/inference_manager.cpp
src/theory/arrays/inference_manager.h
src/theory/bags/bag_solver.cpp
src/theory/bags/infer_info.cpp
src/theory/bags/infer_info.h
src/theory/bags/inference_generator.cpp
src/theory/bags/inference_generator.h
src/theory/bags/inference_manager.h
src/theory/bags/theory_bags.cpp
src/theory/datatypes/inference.cpp
src/theory/datatypes/inference.h
src/theory/datatypes/inference_manager.cpp
src/theory/datatypes/inference_manager.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/inference_manager_buffered.cpp
src/theory/inference_manager_buffered.h
src/theory/sets/term_registry.cpp
src/theory/strings/infer_info.cpp
src/theory/strings/infer_info.h
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h
src/theory/theory_inference.cpp
src/theory/theory_inference.h
src/theory/theory_inference_manager.cpp
src/theory/theory_inference_manager.h
src/theory/uf/cardinality_extension.cpp
src/theory/uf/theory_uf.cpp