wehub-resource-sync
94 lines
3.4 KiB
CMake
94 lines
3.4 KiB
CMake
# Licensed to the Apache Software Foundation (ASF) under one
|
|
# or more contributor license agreements. See the NOTICE file
|
|
# distributed with this work for additional information
|
|
# regarding copyright ownership. The ASF licenses this file
|
|
# to you under the Apache License, Version 2.0 (the
|
|
# "License"); you may not use this file except in compliance
|
|
# with the License. You may obtain a copy of the License at
|
|
#
|
|
# http://www.apache.org/licenses/LICENSE-2.0
|
|
#
|
|
# Unless required by applicable law or agreed to in writing,
|
|
# software distributed under the License is distributed on an
|
|
# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
|
|
# KIND, either express or implied. See the License for the
|
|
# specific language governing permissions and limitations
|
|
# under the License.
|
|
|
|
# src/arith/z3_prover.cc is always part of COMPILER_SRCS (picked up by the
|
|
# src/arith/*.cc glob). It compiles a conservative stub by default and switches
|
|
# to the real Z3 implementation only when the TVM_USE_Z3 macro is defined below.
|
|
if(${USE_Z3} MATCHES ${IS_FALSE_PATTERN})
|
|
return()
|
|
endif()
|
|
|
|
set(TVM_Z3_REQUIRED TRUE)
|
|
if("${USE_Z3}" MATCHES "^[Aa][Uu][Tt][Oo]$")
|
|
set(TVM_Z3_REQUIRED FALSE)
|
|
endif()
|
|
|
|
# Default lookup: the PIC static Z3 library shipped by the PyPI `z3-static`
|
|
# package (headers + libz3.a + Z3 CMake package files). Linking it statically
|
|
# keeps libtvm free of a runtime libz3 dependency. Users can override the
|
|
# lookup by setting Z3_DIR/CMAKE_PREFIX_PATH to any Z3 installation (e.g. a
|
|
# shared system Z3).
|
|
if(NOT Z3_DIR)
|
|
find_package(Python3 COMPONENTS Interpreter QUIET)
|
|
if(Python3_EXECUTABLE)
|
|
execute_process(
|
|
COMMAND
|
|
"${Python3_EXECUTABLE}" -m z3_static.config --cmake-dir
|
|
OUTPUT_VARIABLE Z3_STATIC_CMAKE_DIR
|
|
OUTPUT_STRIP_TRAILING_WHITESPACE
|
|
ERROR_QUIET
|
|
RESULT_VARIABLE Z3_STATIC_RESULT
|
|
)
|
|
if(Z3_STATIC_RESULT EQUAL 0 AND EXISTS "${Z3_STATIC_CMAKE_DIR}")
|
|
set(Z3_DIR "${Z3_STATIC_CMAKE_DIR}")
|
|
endif()
|
|
endif()
|
|
endif()
|
|
|
|
find_package(Z3 CONFIG QUIET)
|
|
if(NOT Z3_FOUND AND NOT TARGET z3::libz3 AND NOT TARGET Z3::libz3)
|
|
find_package(Z3 QUIET)
|
|
endif()
|
|
|
|
if(TARGET z3::libz3 OR TARGET Z3::libz3)
|
|
if(TARGET z3::libz3)
|
|
set(Z3_TARGET z3::libz3)
|
|
else()
|
|
set(Z3_TARGET Z3::libz3)
|
|
endif()
|
|
get_target_property(Z3_TARGET_INCLUDE_DIRS ${Z3_TARGET} INTERFACE_INCLUDE_DIRECTORIES)
|
|
if(Z3_TARGET_INCLUDE_DIRS)
|
|
include_directories(SYSTEM ${Z3_TARGET_INCLUDE_DIRS})
|
|
endif()
|
|
list(APPEND TVM_LINKER_LIBS ${Z3_TARGET})
|
|
elseif(Z3_FOUND OR (Z3_INCLUDE_DIR AND Z3_LIBRARY))
|
|
if(NOT Z3_INCLUDE_DIR AND Z3_CXX_INCLUDE_DIRS)
|
|
set(Z3_INCLUDE_DIR ${Z3_CXX_INCLUDE_DIRS})
|
|
endif()
|
|
if(NOT Z3_LIBRARY AND Z3_LIBRARIES)
|
|
set(Z3_LIBRARY ${Z3_LIBRARIES})
|
|
endif()
|
|
if(NOT Z3_INCLUDE_DIR OR NOT Z3_LIBRARY)
|
|
message(FATAL_ERROR "USE_Z3 is ON, but Z3 include directory or library was not found.")
|
|
endif()
|
|
include_directories(SYSTEM ${Z3_INCLUDE_DIR})
|
|
list(APPEND TVM_LINKER_LIBS ${Z3_LIBRARY})
|
|
else()
|
|
if(TVM_Z3_REQUIRED)
|
|
message(FATAL_ERROR
|
|
"USE_Z3 is ON, but Z3 was not found. Install the static Z3 development "
|
|
"package with `pip install 'z3-static>=4.16.0.post1'`, or point "
|
|
"Z3_DIR/CMAKE_PREFIX_PATH at a Z3 installation.")
|
|
endif()
|
|
message(STATUS "Build without Z3 SMT solver support")
|
|
return()
|
|
endif()
|
|
|
|
# Enable the real Z3 implementation inside the single src/arith/z3_prover.cc file.
|
|
add_compile_definitions(TVM_USE_Z3)
|
|
message(STATUS "Build with Z3 SMT solver support")
|