add Z3 package (#5564)

* add Z3 package

* z3: don't assume python is installed

* [z3] attempt to fix build failure due to path truncation
patch already upstreamed

* [z3] add support for static build

* [z3] Fail preemptively on UWP

ports/z3/CONTROL

@@ -0,0 +1,3 @@
+Source: z3
+Version: 4.8.4
+Description: An SMT solver

ports/z3/LICENSE

@@ -0,0 +1,10 @@
+Z3
+Copyright (c) Microsoft Corporation
+All rights reserved. 
+MIT License
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

ports/z3/fix_cmake_long_dir.patch

@@ -0,0 +1,61 @@
+diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake
+index 8ab6e045d..ac6d1ec06 100644
+--- a/cmake/z3_add_component.cmake
++++ b/cmake/z3_add_component.cmake
+@@ -262,18 +262,20 @@ macro(z3_add_install_tactic_rule)
+       GLOBAL
+       PROPERTY Z3_${dependency}_TACTIC_HEADERS
+     )
+-    list(APPEND _tactic_header_files ${_component_tactic_header_files})
++    list(APPEND _tactic_header_files "${_component_tactic_header_files}")
+   endforeach()
+   unset(_component_tactic_header_files)
+ 
++  string(REPLACE ";" "\n" _tactic_header_files "${_tactic_header_files}")
++  file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files})
+   add_custom_command(OUTPUT "install_tactic.cpp"
+     COMMAND "${PYTHON_EXECUTABLE}"
+     "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+     "${CMAKE_CURRENT_BINARY_DIR}"
+-    ${_tactic_header_files}
++    "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
+     DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+             ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+-            ${_tactic_header_files}
++            "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
+     COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
+     ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+     VERBATIM
+diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py
+index a152eff14..b82e71354 100755
+--- a/scripts/mk_install_tactic_cpp.py
++++ b/scripts/mk_install_tactic_cpp.py
+@@ -14,19 +14,22 @@ def main(args):
+     logging.basicConfig(level=logging.INFO)
+     parser = argparse.ArgumentParser(description=__doc__)
+     parser.add_argument("destination_dir", help="destination directory")
+-    parser.add_argument("header_files", nargs="+",
+-                        help="One or more header files to parse")
++    parser.add_argument("deps", help="file with header file names to parse")
+     pargs = parser.parse_args(args)
+ 
+     if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
+         return 1
+ 
+-    if not mk_genfile_common.check_files_exist(pargs.header_files):
++    if not mk_genfile_common.check_files_exist([pargs.deps]):
+         return 1
+ 
+-    h_files_full_path = []
+-    for header_file in pargs.header_files:
+-        h_files_full_path.append(os.path.abspath(header_file))
++    with open(pargs.deps, 'r') as f:
++        lines = f.read().split('\n')
++        h_files_full_path = [os.path.abspath(header_file)
++                                for header_file in lines if header_file]
++
++    if not mk_genfile_common.check_files_exist(h_files_full_path):
++        return 1
+ 
+     output = mk_genfile_common.mk_install_tactic_cpp_internal(
+         h_files_full_path,

ports/z3/portfile.cmake

@@ -0,0 +1,63 @@
+if (VCPKG_TARGET_ARCHITECTURE STREQUAL "arm64")
+  message(FATAL_ERROR "Z3 doesn't currently support ARM64")
+endif()
+
+if (VCPKG_CMAKE_SYSTEM_NAME STREQUAL "WindowsStore")
+  message(FATAL_ERROR "Z3 doesn't currently support UWP")
+endif()
+
+include(vcpkg_common_functions)
+
+vcpkg_find_acquire_program(PYTHON2)
+get_filename_component(PYTHON2_DIR "${PYTHON2}" DIRECTORY)
+vcpkg_add_to_path("${PYTHON2_DIR}")
+
+vcpkg_from_github(
+  OUT_SOURCE_PATH SOURCE_PATH
+  REPO Z3Prover/z3
+  REF z3-4.8.4
+  SHA512 4660ba6ab33a6345b2e8396c332d4afcfc73eda66ceb2595a39f152df4d62a9ea0f349b0f9212389ba84ecba6bdae6ad9b62b376ba44dc4d9c74f80d7a818bf4
+  HEAD_REF master
+  PATCHES fix_cmake_long_dir.patch
+)
+
+if (VCPKG_LIBRARY_LINKAGE STREQUAL "static")
+  set(BUILD_STATIC "-DBUILD_LIBZ3_SHARED=OFF")
+endif()
+
+vcpkg_configure_cmake(
+  SOURCE_PATH ${SOURCE_PATH}
+  PREFER_NINJA
+  OPTIONS
+    ${BUILD_STATIC}
+)
+
+vcpkg_build_cmake()
+
+
+function(install_z3 SHORT_BUILDTYPE DEBUG_DIR)
+  set(LIBS ".so" ".lib" ".dylib" ".a")
+  set(DLLS ".dll" ".pdb")
+  file(GLOB FILES ${CURRENT_BUILDTREES_DIR}/${TARGET_TRIPLET}-${SHORT_BUILDTYPE}/libz3.*)
+
+  foreach (FILE in ${FILES})
+    get_filename_component(FILEXT ${FILE} EXT)
+    if ("${FILEXT}" IN_LIST LIBS)
+      file(INSTALL ${FILE} DESTINATION ${CURRENT_PACKAGES_DIR}${DEBUG_DIR}/lib)
+    elseif ("${FILEXT}" IN_LIST DLLS)
+      file(INSTALL ${FILE} DESTINATION ${CURRENT_PACKAGES_DIR}${DEBUG_DIR}/bin)
+    endif()
+  endforeach()
+endfunction()
+
+if (NOT DEFINED VCPKG_BUILD_TYPE OR VCPKG_BUILD_TYPE STREQUAL "release")
+  install_z3("dbg" "/debug")
+endif()
+if (NOT DEFINED VCPKG_BUILD_TYPE OR VCPKG_BUILD_TYPE STREQUAL "debug")
+  install_z3("rel" "")
+endif()
+
+file(GLOB HEADERS ${SOURCE_PATH}/src/api/z3*.h)
+file(INSTALL ${HEADERS} DESTINATION ${CURRENT_PACKAGES_DIR}/include)
+
+file(INSTALL ${SOURCE_PATH}/LICENSE.txt DESTINATION ${CURRENT_PACKAGES_DIR}/share/z3 RENAME copyright)