-
Notifications
You must be signed in to change notification settings - Fork 0
/
CMakeLists.txt
137 lines (92 loc) · 4.54 KB
/
CMakeLists.txt
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
cmake_minimum_required(VERSION 3.11.4)
project (lilotane)
set(CMAKE_CXX_STANDARD 17)
if(NOT IPASIRSOLVER)
set(IPASIRSOLVER "glucose4")
endif()
if(NOT IPASIRDIR)
set(IPASIRDIR "${CMAKE_CURRENT_SOURCE_DIR}/lib")
endif()
if(NOT SMT_SOLVER)
set(SMT_SOLVER "cvc5")
endif()
if(NOT SMT_DIR)
set(SMT_DIR "${CMAKE_CURRENT_SOURCE_DIR}/lib")
endif()
# Build-specific compile options
set(MY_DEFINITIONS IPASIRSOLVER=\"${IPASIRSOLVER}\")
if(CMAKE_BUILD_TYPE MATCHES DEBUG)
set(MY_DEFINITIONS ${MY_DEFINITIONS} LILOTANE_VERSION=\"dbg-${IPASIRSOLVER}\")
set(MY_DEBUG_OPTIONS "-rdynamic -g -ggdb")
else()
set(MY_DEFINITIONS ${MY_DEFINITIONS} LILOTANE_VERSION=\"rls-${IPASIRSOLVER}\")
set(MY_DEBUG_OPTIONS "-rdynamic -g -ggdb")
#set(BASE_COMPILEFLAGS -flto)
endif()
if(LILOTANE_USE_ASAN)
set(MY_DEBUG_OPTIONS "${MY_DEBUG_OPTIONS} -fno-omit-frame-pointer -fsanitize=address -static-libasan")
endif()
# Libraries and includes
link_directories(lib ${IPASIRDIR}/${IPASIRSOLVER} build)
set(BASE_LIBS ${MPI_CXX_LIBRARIES} ${MPI_CXX_LINK_FLAGS} m z pandaPIparser)
set(BASE_INCLUDES ${MPI_CXX_INCLUDE_PATH} src src/pandaPIparser/src)
if(EXISTS ${IPASIRDIR}/${IPASIRSOLVER}/LIBS)
message(STATUS "${IPASIRDIR}/${IPASIRSOLVER}/LIBS exists")
file(READ ${IPASIRDIR}/${IPASIRSOLVER}/LIBS SOLVERLIBS)
else()
message(STATUS "${IPASIRDIR}/${IPASIRSOLVER}/LIBS does not exist")
# Assume that dummy functions are required
set(SOLVERLIBS "-ldummyfuncs")
endif()
# Source files (without main.cpp)
set(BASE_SOURCES
src/algo/arg_iterator.cpp src/algo/domination_resolver.cpp src/algo/fact_analysis.cpp src/algo/instantiator.cpp src/algo/network_traversal.cpp src/algo/planner.cpp src/algo/plan_writer.cpp src/algo/retroactive_pruning.cpp
src/data/action.cpp src/data/htn_instance.cpp src/data/htn_op.cpp src/data/layer.cpp src/data/position.cpp src/data/reduction.cpp src/data/signature.cpp src/data/substitution.cpp
src/sat/binary_amo.cpp src/sat/encoding.cpp src/sat/literal_tree.cpp src/sat/plan_optimizer.cpp src/sat/variable_domain.cpp
src/util/log.cpp src/util/names.cpp src/util/params.cpp src/util/random.cpp src/util/signal_manager.cpp src/util/timer.cpp
)
# Base library for Lilotane (liblotane)
add_library(lotane STATIC ${BASE_SOURCES})
target_include_directories(lotane PRIVATE ${BASE_INCLUDES})
target_compile_options(lotane PRIVATE ${BASE_COMPILEFLAGS})
# Executable
add_executable(lilotane src/main.cpp)
target_include_directories(lilotane PRIVATE ${BASE_INCLUDES})
target_compile_options(lilotane PRIVATE ${BASE_COMPILEFLAGS})
target_compile_definitions(lilotane PRIVATE ${MY_DEFINITIONS})
#########################################################################################################################
### Add CVC5 library
target_include_directories(lotane PUBLIC "lib/cvc5/src/api/cpp/" "lib/cvc5/build/src/" "lib/cvc5/src/")
# link_directories("lib/cvc5/build/src/")
target_link_libraries(lotane PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/lib/cvc5/build/src/libcvc5.so")
### Add z3 library
target_include_directories(lotane PUBLIC "lib/z3/src/api/c++/" "lib/z3/src/api")
# link_directories("lib/z3/build/src/api/c++/")
target_link_libraries(lotane PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/lib/z3/build/libz3.so")
#########################################################################################################################
if("${SOLVERLIBS}" MATCHES ".*dummyfuncs.*")
# "dummyfuncs" library for unimplemented extra IPASIR functions
add_library(dummyfuncs
STATIC lib/dummyfuncs/dummyfuncs.cpp
)
endif()
if("${SOLVERLIBS}" MATCHES ".*[A-Za-z].*")
target_link_libraries(lilotane lotane ${BASE_LIBS} ipasir${IPASIRSOLVER} ${SOLVERLIBS})
else()
target_link_libraries(lilotane lotane ${BASE_LIBS} ipasir${IPASIRSOLVER})
endif()
# PandaPIparser
add_custom_target(parser cd ../src/ && bash fetch_and_build_parser.sh)
add_dependencies(lotane parser)
# Solver library
add_custom_target(solverlib cd .. && cd ${IPASIRDIR}/${IPASIRSOLVER}/ && [ ! -f fetch_and_build.sh ] || bash fetch_and_build.sh)
add_dependencies(lilotane solverlib)
# Global debug flags
add_definitions("${MY_DEBUG_OPTIONS}")
SET(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${MY_DEBUG_OPTIONS}")
enable_testing()
add_executable(test_arg_iterator src/test/test_arg_iterator.cpp)
target_include_directories(test_arg_iterator PRIVATE ${BASE_INCLUDES})
target_compile_options(test_arg_iterator PRIVATE ${BASE_COMPILEFLAGS})
target_link_libraries(test_arg_iterator ${BASE_LIBS} lotane)
add_test(NAME test_arg_iterator COMMAND test_arg_iterator)