projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8fcb59d) | patch
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 11 Feb 2021 19:00:18 +0000 (20:00 +0100)
committerGitHub <noreply@github.com>
Thu, 11 Feb 2021 19:00:18 +0000 (20:00 +0100)
commitf5486884229348516ac26300273e4f5458a74208
tree8e48bd833c3e55b247adca891ec2081fc9077528tree
parent8fcb59d072b09bfaf8f56334182d425274842461commit | diff
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)

This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
21 files changed:
src/theory/arith/arith_lemma.h diff | blob | history
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/bags/infer_info.cpp diff | blob | history
src/theory/bags/infer_info.h diff | blob | history
src/theory/bags/inference_generator.cpp diff | blob | history
src/theory/datatypes/infer_proof_cons.cpp diff | blob | history
src/theory/datatypes/inference.cpp diff | blob | history
src/theory/datatypes/inference.h diff | blob | history
src/theory/inference_manager_buffered.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/core_solver.h diff | blob | history
src/theory/strings/infer_info.cpp diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
src/theory/strings/infer_proof_cons.cpp diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/solver_state.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory_inference.cpp diff | blob | history
src/theory/theory_inference.h diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history