diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-10-10 18:52:46 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-10 18:52:46 -0700 |
| commit | 91acac585b0b2bc5a3fab4466d887cfbafa35f77 (patch) | |
| tree | 0cb007ff0fb13c6d80675675e6375a9b5bab1be0 /src/CMakeLists.txt | |
| parent | 9c39dca48e7f0bff035cfff233c9d5224d9a0974 (diff) | |
Make order of theories explicit in the source code. (#3379)
Fixes #2517.
This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.
This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.
I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0a6dec216..a24a2e31a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -682,6 +682,8 @@ libcvc4_add_sources( theory/theory.h theory/theory_engine.cpp theory/theory_engine.h + theory/theory_id.cpp + theory/theory_id.h theory/theory_model.cpp theory/theory_model.h theory/theory_model_builder.cpp @@ -717,10 +719,6 @@ include_directories(include) include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# -# IMPORTANT: The order of the theories is important. It affects the order in -# which theory solvers are called/initialized internally. For example, strings -# depends on arith, quantifiers needs to come as the very last. -# See issue https://github.com/CVC4/CVC4/issues/2517 for more details. set(KINDS_FILES ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds @@ -928,6 +926,7 @@ install(FILES ${INCLUDE_INSTALL_DIR}/cvc4/smt_util) install(FILES theory/logic_info.h + theory/theory_id.h DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/theory) install(FILES |