# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4

PortSystem          1.0
PortGroup           github 1.0
PortGroup           cmake 1.1
PortGroup           compiler_blacklist_versions 1.0
PortGroup           legacysupport 1.1

name                z3
categories          math science
maintainers         {landonf @landonf} openmaintainer
description         Z3 Theorem Prover
long_description    High performance SMT solver from Microsoft Research.

# FStar-qualified Z3 release?
if {${subport} eq "${name}-fstar"} {
    github.setup        Z3Prover z3 4.8.5 Z3-
    revision            5
    checksums           rmd160  cb3509b35dc3a428019950df2e2f94c555a7ee94 \
                        sha256  4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
                        size    4177051
} else {
    github.setup        Z3Prover z3 4.13.3 z3-
    revision            0
    checksums           rmd160  89b77de5ad59d633efe90151119540620840baf3 \
                        sha256  f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0 \
                        size    5583533
    github.tarball_from archive
}

platforms           darwin freebsd
license             MIT

github.tarball_from archive

if {[vercmp ${version} "4.8.9"] >= 0} {
    patchfiles-append   libz3-static.diff
} else {
    patchfiles-append   libz3-static-4.8.5.diff
}

worksrcdir          ${name}-${github.tag_prefix}${version}

cmake.build_type    Release
cmake.generator     Ninja

# Build requires -std=gnu++17
compiler.cxx_standard   2017

# Don't overide z3's default optimization flags
configure.optflags

destroot.target     install

# +polly requires a supported compiler (>= macports-clang-12).
#
# Note that the +polly variant does blacklist unsupported compilers, but if
# this results in all compilers being blacklisted (as is the case on 10.6, where
# macports-clang-12 is not available), a non-polly-enabled compiler fallback
# will be selected, and the build will break.
proc z3.polly_supported_compiler {compiler} {
        if {![regexp {macports-clang-(.*)} ${compiler} -> llvm_ver]} {
            return 0
        }

        if {[vercmp ${llvm_ver} "12"] >= 0} {
            return 1
        }

        return 0
}

proc z3.polly_compiler_available {} {
    global compiler.fallback

    foreach compiler ${compiler.fallback} {
        if {[z3.polly_supported_compiler ${compiler}]} {
            return 1
        }
    }

    return 0
}

# Common variants
variant debug description {Enable the debug build configuration} {
    cmake.build_type    Debug
}

# Options not shared with our language-binding subports
if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {

    set py_ver              3.12
    set py_ver_nodot        [string map {. {}} ${py_ver}]

    depends_build-append    port:python${py_ver_nodot} \
                            port:bash

    patchfiles-append       build-z3-qprofdiff.diff

    # z3 4.8.11 and later use std::variant<>, which is broken on macOS <= 10.12;
    # use macports' libc++ instead
    if {[vercmp ${version} "4.8.11"] >= 0 && ${os.platform} eq "darwin" && ${os.major} <= 16} {
        legacysupport.use_mp_libcxx                 yes
    }

    configure.args-append   -DPYTHON_EXECUTABLE=${prefix}/bin/python${py_ver}

    if {[vercmp ${version} "4.8.7"] >= 0} {
        configure.args-append   -DZ3_ENABLE_EXAMPLE_TARGETS=ON
    } else {
        configure.args-append   -DENABLE_EXAMPLE_TARGETS=ON
    }

    if {[vercmp ${version} "4.8.7"] >= 0} {
        configure.args-append   -DZ3_SINGLE_THREADED=ON
    } elseif {[vercmp ${version} "4.8.6"] >= 0} {
        configure.args-append   -DSINGLE_THREADED=ON
    } else {
        configure.args-append   -DUSE_OPENMP=OFF
    }

    # Optimal (hopefully) default variants selected based on benchmark results.
    # Benchmark configurations:
    #
    # darwin {
    #   ver     {4.8.5}
    #   cc      {macports-clang-8.0}
    #   cpu     {Intel Core i7-7700K @ 4.20GHz (4 cores/8 threads)}
    #   os      {macOS 10.14.6 (18G95)}
    # }
    # freebsd {
    #   ver     {4.8.5}
    #   cc      {macports-clang-8.0}
    #   cpu     {Dual Intel Xeon E5-2680 v4 @ 2.40GHz (2 x 14 cores/28 threads)}
    #   os      {FreeBSD 12.0-RELEASE-p9}
    # }
    #

    # +polly requires a supported compiler (>= macports-clang-12).
    if {[z3.polly_compiler_available]} {
        default_variants-append +polly +polly_late +polly_vector
    }

    # Unsupported prior to 4.8.6
    if {[vercmp ${version} "4.8.6"] >= 0} {
        default_variants-append +threads
    }

    # LTO is broken on <= macOS 10.6:
    #   'unknown scope for symbol ... in bitcode file'
    if {(${os.platform} ne "darwin" || ${os.major} > 10) && ![variant_isset debug]} {
        default_variants-append +lto
    }

    # TODO: We currently only have profiling data for z3-fstar; we should
    # investigate bechmark suites we could use to produce general-purpose
    # profiling data for the main z3 port.
    if {${subport} eq "${name}-fstar" && ![variant_isset profile]} {
        default_variants-append +pgo
    }

    variant lto conflicts debug description {Enable link-time (interprocedural) optimization} {
        configure.args-append           -DCMAKE_INTERPROCEDURAL_OPTIMIZATION=ON \
                                        -DCMAKE_POLICY_DEFAULT_CMP0069=NEW

        # Require clang (LTO may work with GCC, but is untested)
        compiler.blacklist-append       {*gcc*} cc

        # I don't believe -flto was supported by clang until Xcode 9
        platform darwin {
            compiler.blacklist-append   {clang < 900}
        }

        # TODO: Is this still required in 13.x+?
        platform freebsd {
           compiler.blacklist-append    clang
        }
    }

    variant gmp description {Use GNU GMP library for arbitrary precision arithmetic} {
        depends_lib-append          port:gmp
        if {[vercmp ${version} "4.8.7"] >= 0} {
            configure.args-append       -DZ3_USE_LIB_GMP=ON
        } else {
            configure.args-append       -DUSE_LIB_GMP=ON
        }
    }

    variant native description {Generate code optimized for this machine's CPU. The resulting binaries may not run on other processors} {
        configure.optflags-append   -march=native
    }

    variant profile description {Generate instrumented code that may be used for profile-guided optimization} {
        # Default to /dev/null, requiring that users explicitly set LLVM_PROFILE_FILE.
        # See also: https://clang.llvm.org/docs/UsersManual.html#profiling-with-instrumentation
        configure.optflags-append   -fprofile-instr-generate=/dev/null

        # Require clang
        compiler.blacklist-append   {*gcc*} cc

        notes-append "
        ${name} has been built with profiling instrumentation enabled; note\
        that this will introduce non-negligible runtime overhead.

        To generate profile data, specify an output path by setting the\
        LLVM_PROFILE_FILE environment variable before executing z3.
        "
    }

    if {[vercmp ${version} "4.8.6"] >= 0}  {
        variant threads description {Enable thread-safe build} {
            if {[vercmp ${version} "4.8.7"] >= 0} {
                configure.args-delete       -DZ3_SINGLE_THREADED=ON
                configure.args-append       -DZ3_SINGLE_THREADED=OFF
            } else {
                configure.args-delete       -DSINGLE_THREADED=ON
                configure.args-append       -DSINGLE_THREADED=OFF
            }
        }
    }

    variant polly conflicts debug description {Perform loop and data-locality optimization using LLVM's Polly optimizer} {
        # We need llvm built with polly support; this available by default as of our llvm-12 port,
        # so make that our minimum version.
        compiler.blacklist-append   {cc} \
                                    {clang} \
                                    {macports-clang-[0-9].*} \
                                    {macports-clang-10} \
                                    {macports-clang-11} \
                                    {*gcc*}
        # Currently seems to have problems with macports clang-19 so blacklist that as well
        # https://trac.macports.org/ticket/70852
        # macports-clang-18 is then used instead which is OK
        compiler.blacklist-append {macports-clang-19}

        configure.optflags-append   -O3 -mllvm -polly
    }

    variant polly_late requires polly description {Perform LLVM Polly optimization later in the LLVM optimization pass pipline} {
        # See https://polly.llvm.org/docs/Architecture.html#polly-in-the-llvm-pass-pipeline
        configure.optflags-append   -mllvm -polly-position=before-vectorizer
    }

    variant polly_two_level_tiling requires polly description {Enable second-level loop tiling using LLVM's Polly optimizer} {
        configure.optflags-append   -mllvm -polly-2nd-level-tiling
    }

    variant polly_vector requires polly description {Enable automatic vector code generation using LLVM's Polly optimizer} {
        configure.optflags-append   -mllvm -polly-vectorizer=stripmine
    }

    variant polly_parallel requires polly description {Enable automatic generation of OpenMP code for parallel loops using LLVM's Polly optimizer} {
        configure.optflags-append   -mllvm -polly-parallel

        # Generated OpenMP code requires libomp/libgomp
        # LLVM uses libomp
        depends_lib-append          port:libomp
        configure.ldflags-append    -L${prefix}/lib/libomp \
                                    -lomp
    }

    pre-configure {
        # Verify that a polly-supporting compiler was actually selected
        if {[variant_isset polly] && ![z3.polly_supported_compiler ${configure.compiler}]} {
            ui_error "${name} @${version}: +polly requires macports-clang-12 or later"
            return -code error "incompatible compiler selected"
        }

        #
        # If we enable +lto in combination with a variant (e.g. +polly) that
        # selects MacPorts' clang compiler, CMake fails to locate the llvm-ar and llvm-ranlib
        # binaries required for -flto.
        #
        # TODO: Investigate fixing this in upstream cmake, and/or in the cmake PortGroup
        #
        if {[variant_isset lto] && [regexp {macports-clang-(.*)} ${configure.compiler} -> llvm_ver]} {
            foreach lang {C CXX} {
                foreach tool {ar ranlib} {
                    set var     CMAKE_${lang}_COMPILER_[string toupper ${tool}]
                    set path    ${prefix}/bin/llvm-${tool}-mp-${llvm_ver}
                    configure.args-append -D${var}=${path}
                }
            }
        }
    }

    test.run    yes
    test.target test-z3
    post-test {
        # This actually executes the unit tests
        system -W ${test.dir} {./test-z3 /a}
    }
}

# F*-qualified z3 release; may trail behind the current z3 release.
subport ${name}-fstar {
    # Should be updated
    description             F*-qualified release of the Z3 Theorem Prover
    long_description        Private version of the Z3 theorem prover for use by (and qualified to work with) F*.
    cmake.install_prefix    ${prefix}/libexec/${subport}

    depends_build-append    port:py${py_ver_nodot}-setuptools

    destroot {
        xinstall -d -m 755 "${destroot}${cmake.install_prefix}/bin"
        xinstall -m 755 "${cmake.build_dir}/z3" "${destroot}${cmake.install_prefix}/bin/z3"
        ln -sf "${cmake.install_prefix}/bin/z3" "${destroot}${prefix}/bin/z3-fstar"
    }

    variant pgo conflicts profile description {Enable profile-guided optimization} {
        # Requires clang
        compiler.blacklist-append   {*gcc*}

        # We currently only provide profiling data for z3-fstar; this profile is
        # generated from a verification run over Project Everest subprojects, which
        # should be strongly representative of F*'s use of z3.
        #
        # To regenerate the profile, install z3-fstar with +profile -pgo, and then:
        #   ${filespath}/z3-fstar.profdata-generate.sh \
        #       -l llvm-profdata-mp-<llvm-version> \
        #       -z ${prefix}/bin/z3-fstar \
        #       -o ${filespath}/z3-fstar.profdata.tar.xz \
        #       -j <njobs> \
        #       <everest-src>
        configure.optflags-append   -fprofile-instr-use=${workpath}/${subport}.profdata
        depends_extract-append      bin:xz:xz
        post-extract {
            set tar [findBinary tar ${portutil::autoconf::tar_command}]
            set xz [findBinary xz ${portutil::autoconf::xz_path}]
            system "${xz} -cd ${filespath}/${subport}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -"
        }
    }
}

set pyversions {38 39 310 311 312}

# Create a top-level Python binding metaport
subport py-${name} {
    PortGroup   python 1.0
    PortGroup   stub   1.0

    supported_archs     noarch
    platforms           any
    categories-append   python

    description         Python bindings for the Z3 theorem prover
    long_description    Python bindings for the Z3 SMT solver library from Microsoft Research.

    python.default_version [lindex ${pyversions} end]
    depends_lib         port:${name} \
                        port:py${python.version}-${name}

    # Feb 2023 - master base/github PG default to yes which errors
    if {[exists extract.rename]} {
        extract.rename no
    }
}

# Create Python subports for each supported Python version
foreach v ${pyversions} {
    subport py${v}-${name} {
        PortGroup  python 1.0

        python.version          ${v}

        supported_archs         noarch
        platforms               {darwin any}
        categories-append       python

        description             Python ${python.branch} bindings for the Z3 theorem prover
        long_description        Python ${python.branch} bindings for the Z3 SMT solver library from Microsoft Research.

        # needs pkg_resources at runtime
        depends_lib-append      port:${name} \
                                port:python${v} \
                                port:py${v}-setuptools

        use_configure           yes
        configure.args-append   -DPython3_EXECUTABLE=${python.bin} \
                                -DZ3_BUILD_PYTHON_BINDINGS=ON \
                                -DZ3_INSTALL_PYTHON_BINDINGS=ON

        # Avoid rebuilding libz3
        post-patch {
            reinplace -E {s|^[[:blank:]]*DEPENDS[[:blank:]]+libz3|DEPENDS |g} \
                src/api/python/CMakeLists.txt
        }

        post-destroot {
            # The python module looks for libz3 in its package path
            ln -sf "${prefix}/lib/libz3.dylib" "${destroot}${python.pkgd}/z3/"
        }

        build.target            src/api/python/all
        destroot.cmd            ${build.cmd}
        destroot.target         src/api/python/install
    }
}

# Java bindings
subport ${name}-java {
    PortGroup  java 1.0

    java.version            1.8+
    java.fallback           openjdk11

    categories-append       java

    description             Java bindings for the Z3 theorem prover
    long_description        Java bindings for the Z3 SMT solver library from Microsoft Research.

    depends_lib-append      port:${name}

    patchfiles-append       java_libpath.diff

    configure.args-append   -DZ3_BUILD_JAVA_BINDINGS=ON \
                            -DZ3_INSTALL_JAVA_BINDINGS=ON \
                            -DZ3_JAVA_JNI_LIB_INSTALLDIR=${prefix}/lib/${name} \
                            -DZ3_JAVA_JAR_INSTALLDIR=${prefix}/share/java/${name}

    post-patch {
        # Avoid rebuilding libz3
        reinplace -E {s|(^[[:blank:]]*target_link_libraries[[:blank:]]*\([[:blank:]]*z3java[[:blank:]]*PRIVATE)[[:blank:]]*libz3(.*)|\1 z3 \2|g} \
            src/api/java/CMakeLists.txt

        # Fix up path to our JNI library
        reinplace "s|@PREFIX@|${prefix}|g" \
            scripts/update_api.py
    }

    post-destroot {
        ln -s "com.microsoft.z3.jar" "${destroot}${prefix}/share/java/${name}/z3.jar"
    }

    build.target            src/api/java/all
    destroot.cmd            ${build.cmd}
    destroot.target         src/api/java/install
}