# -*- 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           boost 1.0

boost.depends_type  build

name                cvc4
version             1.4
revision            3

# Drop on next update:
if {${os.platform} eq "darwin" && ${os.major} < 10} {
    incr revision
}

categories          math devel
maintainers         nomaintainer
license             BSD
description         Automated theorem prover for SMT problems
long_description    CVC4 is a tool for determining the satisfiability of a first order formula \
                    modulo a first order theory (or a combination of such theories). It is \
                    the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, \
                    CVC3) but does not directly incorporate code from any previous version. \
                    \
                    CVC4 is intended to be an open and extensible SMT engine. It can be used \
                    as a stand-alone tool or as a library. It has been designed to increase \
                    the performance and reduce the memory overhead of its predecessors.
homepage            http://cvc4.cs.nyu.edu
master_sites        ${homepage}/builds/src/
checksums           rmd160  726f673afe0417bccdde9a2f038da5f642958d15 \
                    sha256  76fe4ff9eb9ad7d65589efb47d41aae95f3191bd0d0c3940698a7cb2df3f7024 \
                    size    6957278

depends_build-append \
                    bin:bash:bash \
                    path:bin/doxygen:doxygen \
                    path:bin/awk:gawk \
                    port:wget
depends_lib         port:gmp

configure.args      --bsd \
                    --disable-doxygen-pdf \
                    --enable-doxygen-dot \
                    --enable-shared \
                    --enable-static \
                    --with-antlr-dir="${worksrcpath}/antlr-3.4" \
                    --with-build=production \
                    --with-compat \
                    --with-gmp \
                    ANTLR="${worksrcpath}/antlr-3.4/bin/antlr3"

# TODO: added for safety, may not be required, try dropping on next update.
use_parallel_build  no

# --enable-language-bindings=c,java
# --with-portfolio
test.run            yes

variant debug description "Build a debug copy" {
    configure.args-replace \
                    --with-build=production --with-build=debug
}

variant java description "Build Java language bindings" {
    # TODO: java variant is completely untested at the moment.
    depends_build-append \
                    port:openjdk8 \
                    port:swig-java \
                    port:swig-tcl
    configure.args-append \
                    --enable-language-bindings=java \
                    JAVA_CPPFLAGS=-I${prefix}/Library/Java/JavaVirtualMachines/openjdk8/Contents/Home/include
}

pre-configure {
    system "MACHINE_TYPE=`${worksrcpath}/config/config.guess | cut -f1 -d-` ANTLR_CONFIGURE_ARGS=--disable-abiflags ${worksrcpath}/contrib/get-antlr-3.4"
}

post-build {
    system "make -C \"${worksrcpath}\" doc"
}

destroot {
    # strip binaries and libraries
    system "make -C \"${worksrcpath}\" install-strip DESTDIR=\"${destroot}\""
}

post-destroot {
    file mkdir "${destroot}${prefix}/share/doc/${name}/doxygen"
    file copy "${worksrcpath}/doc/doxygen/html" \
          "${destroot}${prefix}/share/doc/${name}/doxygen/html"
    system "make -C \"${worksrcpath}\" install-examples DESTDIR=\"${destroot}\""
}

livecheck.type          regex
livecheck.url           ${master_sites}
livecheck.regex         cvc4-(\[0-9.\]+)\\.tar\\.gz
