projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b3f05d5) | patch
Merge InferenceIds into one enum (#5892)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 11 Feb 2021 14:55:31 +0000 (15:55 +0100)
committerGitHub <noreply@github.com>
Thu, 11 Feb 2021 14:55:31 +0000 (15:55 +0100)
commit1d0492104a200f6fa5cc7a1cee539436ee26ea99
treea66ff6b0bc869f1e84dceb03ddbcc7910e23c77ctree
parentb3f05d5c25facaf0c34ee79faed060bda3f61a8dcommit | diff
Merge InferenceIds into one enum (#5892)

This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
43 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/arith/arith_lemma.h diff | blob | history
src/theory/arith/inference_id.cpp [deleted file] blob | history
src/theory/arith/inference_id.h [deleted file] blob | history
src/theory/arith/inference_manager.h diff | blob | history
src/theory/arith/nl/cad_solver.cpp diff | blob | history
src/theory/arith/nl/ext/factoring_check.cpp diff | blob | history
src/theory/arith/nl/ext/monomial_bounds_check.cpp diff | blob | history
src/theory/arith/nl/ext/monomial_check.cpp diff | blob | history
src/theory/arith/nl/ext/split_zero_check.cpp diff | blob | history
src/theory/arith/nl/ext/tangent_plane_check.cpp diff | blob | history
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/stats.h diff | blob | history
src/theory/arith/nl/transcendental/exponential_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.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/infer_proof_cons.h diff | blob | history
src/theory/datatypes/inference.cpp diff | blob | history
src/theory/datatypes/inference.h diff | blob | history
src/theory/datatypes/inference_manager.cpp diff | blob | history
src/theory/datatypes/inference_manager.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/inference_id.cpp [new file with mode: 0644] blob
src/theory/inference_id.h [new file with mode: 0644] blob
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/extf_solver.cpp 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/infer_proof_cons.h diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/inference_manager.h diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
src/theory/strings/sequences_stats.h diff | blob | history
src/theory/strings/solver_state.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history