Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 11 Feb 2021 20:25:50 +0000 (21:25 +0100)
committerGitHub <noreply@github.com>
Thu, 11 Feb 2021 20:25:50 +0000 (21:25 +0100)
commite8333750e5932ab5ce9a8a491b53aef4ffa4b0aa
treea6de942fd32afb4dcb67d33884cdff7252c6f14f
parentf5486884229348516ac26300273e4f5458a74208
Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)

This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.
22 files changed:
src/theory/arith/arith_preprocess.cpp
src/theory/arrays/inference_manager.cpp
src/theory/bags/infer_info.cpp
src/theory/bv/bitblast/lazy_bitblaster.cpp
src/theory/bv/bv_solver_bitblast.cpp
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_solver_lazy.h
src/theory/bv/bv_solver_simple.cpp
src/theory/bv/bv_subtheory_core.cpp
src/theory/datatypes/inference_manager.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/sep/theory_sep.cpp
src/theory/sets/inference_manager.cpp
src/theory/sets/term_registry.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/strings/inference_manager.cpp
src/theory/theory_inference.cpp
src/theory/theory_inference_manager.cpp
src/theory/theory_inference_manager.h
src/theory/uf/cardinality_extension.cpp
src/theory/uf/ho_extension.cpp
src/theory/uf/theory_uf.cpp