blob: 225776609305a0ed9daf640255353d393753d7d3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
cmake_minimum_required(VERSION 3.20)
project(atp_engine
VERSION 0.1.0
LANGUAGES CXX
)
# ─── C++ Standard ────────────────────────────────────────────────────────────
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
set(CMAKE_CXX_EXTENSIONS OFF)
# Export compile_commands.json for clang-tidy and IDE support
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
# ─── Compiler Warnings ──────────────────────────
set(ATP_PROJECT_WARNING_FLAGS
-Wall -Wextra -Wpedantic
-Wshadow -Wnon-virtual-dtor
-Wold-style-cast -Wcast-align -Wunused
-Woverloaded-virtual -Wconversion -Wsign-conversion
-Wnull-dereference -Wdouble-promotion
-Wformat=2 -Wimplicit-fallthrough
)
# ─── Sanitizers (Debug builds) ───────────────────────────────────────────────
option(ATP_ENABLE_SANITIZERS "Enable ASan + UBSan in Debug builds" ON)
if(ATP_ENABLE_SANITIZERS AND CMAKE_BUILD_TYPE STREQUAL "Debug")
add_compile_options(-fsanitize=address,undefined -fno-omit-frame-pointer)
add_link_options(-fsanitize=address,undefined)
endif()
# ─── clang-tidy Integration ─────────────────────────────────────────────────
option(ATP_ENABLE_CLANG_TIDY "Enable clang-tidy static analysis" OFF)
if(ATP_ENABLE_CLANG_TIDY)
find_program(CLANG_TIDY_EXE NAMES clang-tidy)
if(CLANG_TIDY_EXE)
message(STATUS "clang-tidy found: ${CLANG_TIDY_EXE}")
else()
message(WARNING "clang-tidy requested but not found")
endif()
endif()
# ─── clang-format Custom Target ─────────────────────────────────────────────
find_program(CLANG_FORMAT_EXE NAMES clang-format)
if(CLANG_FORMAT_EXE)
file(GLOB_RECURSE ALL_CXX_SOURCES
${PROJECT_SOURCE_DIR}/src/*.cc
${PROJECT_SOURCE_DIR}/include/*.h
${PROJECT_SOURCE_DIR}/tests/*.cc
)
add_custom_target(format
COMMAND ${CLANG_FORMAT_EXE} -i ${ALL_CXX_SOURCES}
COMMENT "Running clang-format on all source files"
VERBATIM
)
add_custom_target(format-check
COMMAND ${CLANG_FORMAT_EXE} --dry-run --Werror ${ALL_CXX_SOURCES}
COMMENT "Checking clang-format compliance"
VERBATIM
)
message(STATUS "clang-format found: ${CLANG_FORMAT_EXE}")
message(STATUS " Use 'cmake --build . --target format' to auto-format")
message(STATUS " Use 'cmake --build . --target format-check' to check format")
else()
message(WARNING "clang-format not found, format targets disabled")
endif()
# ─── Source Files ────────────────────────────────────────────────────────────
set(ATP_SOURCES
src/core/symbol_table.cc
src/core/term_bank.cc
src/core/clause_store.cc
src/normalize/clausifier.cc
src/infer/substitution.cc
src/infer/unification.cc
src/infer/resolution.cc
src/index/discrim_tree.cc
src/simplify/subsumption.cc
src/simplify/tautology.cc
src/search/prover.cc
src/proof/proof_trace.cc
src/rewrite/ordering.cc
src/rewrite/paramodulation.cc
src/strategy/problem_analyzer.cc
src/frontend/tptp_parser.cc
)
# ─── Core Library ────────────────────────────────────────────────────────────
add_library(atp_core STATIC ${ATP_SOURCES})
target_include_directories(atp_core PUBLIC
${PROJECT_SOURCE_DIR}/include
)
target_compile_options(atp_core PRIVATE ${ATP_PROJECT_WARNING_FLAGS})
if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE)
set_property(TARGET atp_core PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}")
endif()
# ─── Main Executable ────────────────────────────────────────────────────────
add_executable(atp src/main.cc)
target_link_libraries(atp PRIVATE atp_core)
target_compile_options(atp PRIVATE ${ATP_PROJECT_WARNING_FLAGS})
if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE)
set_property(TARGET atp PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}")
endif()
# ─── Tests ───────────────────────────────────────────────────────────────────
option(ATP_BUILD_TESTS "Build unit tests" ON)
if(ATP_BUILD_TESTS)
enable_testing()
add_subdirectory(tests)
endif()
|
