scripts/mk_util.py

############################################
# Copyright (c) 2012 Microsoft Corporation
#
# Auxiliary scripts for generating Makefiles
# and Visual Studio project files.
#
# Author: Leonardo de Moura (leonardo)
############################################
import io
import sys
import os
import re
import getopt
import shutil
from mk_exception import *
import mk_genfile_common
from fnmatch import fnmatch
import sysconfig
import compileall
import subprocess

def getenv(name, default):
    try:
        return os.environ[name].strip(' "\'')
    except:
        return default

CXX=getenv("CXX", None)
CC=getenv("CC", None)
CPPFLAGS=getenv("CPPFLAGS", "")
CXXFLAGS=getenv("CXXFLAGS", "")
AR=getenv("AR", "ar")
EXAMP_DEBUG_FLAG=''
LDFLAGS=getenv("LDFLAGS", "")
JNI_HOME=getenv("JNI_HOME", None)
OCAMLC=getenv("OCAMLC", "ocamlc")
OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
OCAML_LIB=getenv("OCAML_LIB", None)
OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
DOTNET="dotnet"
# Standard install directories relative to PREFIX
INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig'))

CXX_COMPILERS=['g++', 'clang++']
C_COMPILERS=['gcc', 'clang']
JAVAC=None
JAR=None
PYTHON_PACKAGE_DIR=sysconfig.get_path('purelib')
BUILD_DIR='build'
REV_BUILD_DIR='..'
SRC_DIR='src'
EXAMPLE_DIR='examples'
# Required Components
Z3_DLL_COMPONENT='api_dll'
PATTERN_COMPONENT='pattern'
UTIL_COMPONENT='util'
API_COMPONENT='api'
DOTNET_COMPONENT='dotnet'
DOTNET_CORE_COMPONENT='dotnet'
JAVA_COMPONENT='java'
ML_COMPONENT='ml'
CPP_COMPONENT='cpp'
PYTHON_COMPONENT='python'
#####################
IS_WINDOWS=False
IS_LINUX=False
IS_HURD=False
IS_OSX=False
IS_ARCH_ARM64=False
IS_FREEBSD=False
IS_NETBSD=False
IS_OPENBSD=False
IS_SUNOS=False
IS_CYGWIN=False
IS_CYGWIN_MINGW=False
IS_MSYS2=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
VS_X64 = False
VS_ARM = False
LINUX_X64 = True
ONLY_MAKEFILES = False
Z3PY_SRC_DIR=None
Z3JS_SRC_DIR=None
VS_PROJ = False
TRACE = False
PYTHON_ENABLED=False
DOTNET_CORE_ENABLED=False
DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
ASSEMBLY_VERSION=getenv("Z2_ASSEMBLY_VERSION", None)
JAVA_ENABLED=False
ML_ENABLED=False
PYTHON_INSTALL_ENABLED=False
STATIC_LIB=False
STATIC_BIN=False
VER_MAJOR=None
VER_MINOR=None
VER_BUILD=None
VER_TWEAK=None
PREFIX=sys.prefix
GMP=False
VS_PAR=False
VS_PAR_NUM=8
GPROF=False
GIT_HASH=False
GIT_DESCRIBE=False
SLOW_OPTIMIZE=False
LOG_SYNC=False
SINGLE_THREADED=False
GUARD_CF=False
ALWAYS_DYNAMIC_BASE=False

FPMATH="Default"
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
FPMATH_ENABLED=getenv("FPMATH_ENABLED", "True")


def check_output(cmd):
    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
    if out != None:
        enc = sys.getdefaultencoding()
        if enc != None: return out.decode(enc).rstrip('\r\n')
        else: return out.rstrip('\r\n')
    else:
        return ""

def git_hash():
    try:
        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
        r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
    except:
        raise MKException("Failed to retrieve git hash")
    ls = r.split(' ')
    if len(ls) != 2:
        raise MKException("Unexpected git output " + r)
    return ls[0]

def is_windows():
    return IS_WINDOWS

def is_linux():
    return IS_LINUX

def is_hurd():
    return IS_HURD

def is_freebsd():
    return IS_FREEBSD

def is_netbsd():
    return IS_NETBSD

def is_openbsd():
    return IS_OPENBSD

def is_sunos():
    return IS_SUNOS

def is_osx():
    return IS_OSX

def is_cygwin():
    return IS_CYGWIN

def is_cygwin_mingw():
    return IS_CYGWIN_MINGW

def is_msys2():
    return IS_MSYS2

def norm_path(p):
    return os.path.expanduser(os.path.normpath(p))

def which(program):
    import os
    def is_exe(fpath):
        return os.path.isfile(fpath) and os.access(fpath, os.X_OK)

    fpath, fname = os.path.split(program)
    if fpath:
        if is_exe(program):
            return program
    else:
        for path in getenv("PATH", "").split(os.pathsep):
            exe_file = os.path.join(path, program)
            if is_exe(exe_file):
                return exe_file
    return None

class TempFile:
    def __init__(self, name):
        try:
            self.name  = name
            self.fname = open(name, 'w')
        except:
            raise MKException("Failed to create temporary file '%s'" % self.name)

    def add(self, s):
        self.fname.write(s)

    def commit(self):
        self.fname.close()

    def __del__(self):
        self.fname.close()
        try:
            os.remove(self.name)
        except:
            pass

def exec_cmd(cmd):
    if isinstance(cmd, str):
        cmd = cmd.split(' ')
    new_cmd = []
    first = True
    for e in cmd:
        if first:
            first = False
            new_cmd.append(e)
        else:
            if e != "":
                se = e.split(' ')
                if len(se) > 1:
                    for e2 in se:
                        if e2 != "":
                            new_cmd.append(e2)
                else:
                    new_cmd.append(e)
    cmd = new_cmd
    null = open(os.devnull, 'wb')
    try:
        return subprocess.call(cmd, stdout=null, stderr=null)
    except:
        # Failed to create process
        return 1
    finally:
        null.close()

# rm -f fname
def rmf(fname):
    if os.path.exists(fname):
        os.remove(fname)

def exec_compiler_cmd(cmd):
    r = exec_cmd(cmd)
    # Windows
    rmf('a.exe')
    # Unix
    rmf('a.out')
    # Emscripten
    rmf('a.wasm')
    rmf('a.worker.js')
    return r

def test_cxx_compiler(cc):
    if is_verbose():
        print("Testing %s..." % cc)
    t = TempFile('tst.cpp')
    t.add('#include<iostream>\nint main() { return 0; }\n')
    t.commit()
    return exec_compiler_cmd([cc, CPPFLAGS, CXXFLAGS, 'tst.cpp', LDFLAGS]) == 0

def test_c_compiler(cc):
    if is_verbose():
        print("Testing %s..." % cc)
    t = TempFile('tst.c')
    t.add('#include<stdio.h>\nint main() { return 0; }\n')
    t.commit()
    return exec_compiler_cmd([cc, CPPFLAGS, 'tst.c', LDFLAGS]) == 0

def test_gmp(cc):
    if is_verbose():
        print("Testing GMP...")
    t = TempFile('tstgmp.cpp')
    t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
    t.commit()
    return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0


def test_fpmath(cc):
    global FPMATH_FLAGS, IS_ARCH_ARM64, IS_OSX
    if FPMATH_ENABLED == "False":
        FPMATH_FLAGS=""
        return "Disabled"
    if IS_ARCH_ARM64 and IS_OSX:
        FPMATH_FLAGS = ""
        return "Disabled-ARM64"
    if is_verbose():
        print("Testing floating point support...")
    t = TempFile('tstsse.cpp')
    t.add('int main() { return 42; }\n')
    t.commit()
    # -Werror is needed because some versions of clang warn about unrecognized
    # -m flags.
    # TODO(ritave): Safari doesn't allow SIMD WebAssembly extension, add a flag to build script
    if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2 -msimd128']) == 0:
        FPMATH_FLAGS='-msse -msse2 -msimd128'
        return 'SSE2-EMSCRIPTEN'
    if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
        FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
        return "SSE2-GCC"
    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
        FPMATH_FLAGS="-msse -msse2"
        return "SSE2-CLANG"
    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
        FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
        return "ARM-VFP"
    else:
        FPMATH_FLAGS=""
        return "UNKNOWN"


def find_jni_h(path):
    for root, dirs, files in os.walk(path):
        for f in files:
            if f == 'jni.h':
                return root
    return False

def check_java():
    global JNI_HOME
    global JAVAC
    global JAR

    JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.

    if is_verbose():
        print("Finding javac ...")

    if JDK_HOME is not None:
        if IS_WINDOWS:
            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe')
        else:
            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac')

        if not os.path.exists(JAVAC):
            raise MKException("Failed to detect javac at '%s/bin'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME))
    else:
        # Search for javac in the path.
        ind = 'javac'
        if IS_WINDOWS:
            ind = ind + '.exe'
        paths = os.getenv('PATH', None)
        if paths:
            spaths = paths.split(os.pathsep)
            for i in range(0, len(spaths)):
                cmb = os.path.join(spaths[i], ind)
                if os.path.exists(cmb):
                    JAVAC = cmb
                    break

    if JAVAC is None:
        raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.')

    if is_verbose():
        print("Finding jar ...")

    if IS_WINDOWS:
        JAR = os.path.join(os.path.dirname(JAVAC), 'jar.exe')
    else:
        JAR = os.path.join(os.path.dirname(JAVAC), 'jar')

    if not os.path.exists(JAR):
        raise MKException("Failed to detect jar at '%s'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME))

    if is_verbose():
        print("Testing %s..." % JAVAC)

    t = TempFile('Hello.java')
    t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
    t.commit()

    oo = TempFile('output')
    eo = TempFile('errout')
    try:
        subprocess.call([JAVAC, 'Hello.java', '-verbose', '-source', '1.8', '-target', '1.8' ], stdout=oo.fname, stderr=eo.fname)
        oo.commit()
        eo.commit()
    except:
        raise MKException('Found, but failed to run Java compiler at %s' % (JAVAC))

    os.remove('Hello.class')

    if is_verbose():
        print("Finding jni.h...")

    if JNI_HOME is not None:
        if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
            raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME))
    else:
        # Search for jni.h in the library directories...
        t = open('errout', 'r')
        open_pat = re.compile(r"\[search path for class files: (.*)\]")
        cdirs = []
        for line in t:
            m = open_pat.match(line)
            if m:
                libdirs = m.group(1).split(',')
                for libdir in libdirs:
                    q = os.path.dirname(libdir)
                    if cdirs.count(q) == 0 and len(q) > 0:
                        cdirs.append(q)
        t.close()

        # ... plus some heuristic ones.
        extra_dirs = []

        # For the libraries, even the JDK usually uses a JRE that comes with it. To find the
        # headers we have to go a little bit higher up.
        for dir in cdirs:
            extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))

        if IS_OSX: # Apparently Apple knows best where to put stuff...
            extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')

        cdirs[len(cdirs):] = extra_dirs

        for dir in cdirs:
            q = find_jni_h(dir)
            if q is not False:
                JNI_HOME = q

        if JNI_HOME is None:
            raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")

def test_csc_compiler(c):
    t = TempFile('hello.cs')
    t.add('public class hello { public static void Main() {} }')
    t.commit()
    if is_verbose():
        print ('Testing %s...' % c)
    r = exec_cmd([c, 'hello.cs'])
    try:
        rmf('hello.cs')
        rmf('hello.exe')
    except:
        pass
    return r == 0

def check_dotnet_core():
    if not IS_WINDOWS:
        return
    r = exec_cmd([DOTNET, '--help'])
    if r != 0:
        raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities')

def check_ml():
    t = TempFile('hello.ml')
    t.add('print_string "Hello world!\n";;')
    t.commit()
    if is_verbose():
        print ('Testing %s...' % OCAMLC)
    r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
    if r != 0:
        raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
    if is_verbose():
        print ('Testing %s...' % OCAMLOPT)
    r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
    if r != 0:
        raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
    try:
        rmf('hello.cmi')
        rmf('hello.cmo')
        rmf('hello.cmx')
        rmf('a.out')
        rmf('hello.o')
    except:
        pass
    find_ml_lib()
    find_ocaml_find()

def find_ocaml_find():
    global OCAMLFIND
    if is_verbose():
        print ("Testing %s..." % OCAMLFIND)
    r = exec_cmd([OCAMLFIND, 'printconf'])
    if r != 0:
        OCAMLFIND = ''

def find_ml_lib():
    global OCAML_LIB
    if is_verbose():
        print ('Finding OCAML_LIB...')
    t = TempFile('output')
    null = open(os.devnull, 'wb')
    try:
        subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
        t.commit()
    except:
        raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
    finally:
        null.close()

    t = open('output', 'r')
    for line in t:
        OCAML_LIB = line[:-1]
    if is_verbose():
        print ('OCAML_LIB=%s' % OCAML_LIB)
    t.close()
    rmf('output')
    return

def is64():
    global LINUX_X64
    if is_sunos() and sys.version_info.major < 3:
        return LINUX_X64
    else:
        return LINUX_X64 and sys.maxsize >= 2**32

def check_ar():
    if is_verbose():
        print("Testing ar...")
    if which(AR) is None:
        raise MKException('%s (archive tool) was not found' % AR)

def find_cxx_compiler():
    global CXX, CXX_COMPILERS
    if CXX is not None:
        if test_cxx_compiler(CXX):
            return CXX
    for cxx in CXX_COMPILERS:
        if test_cxx_compiler(cxx):
            CXX = cxx
            return CXX
    raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')

def find_c_compiler():
    global CC, C_COMPILERS
    if CC is not None:
        if test_c_compiler(CC):
            return CC
    for c in C_COMPILERS:
        if test_c_compiler(c):
            CC = c
            return CC
    raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')

def set_version(major, minor, build, revision):
    global ASSEMBLY_VERSION, VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK, GIT_DESCRIBE

    # We need to give the assembly a build specific version
    # global version overrides local default expression
    if ASSEMBLY_VERSION is not None:
        versionSplits = ASSEMBLY_VERSION.split('.')
        if len(versionSplits) > 3:
            VER_MAJOR = versionSplits[0]
            VER_MINOR = versionSplits[1]
            VER_BUILD = versionSplits[2]
            VER_TWEAK = versionSplits[3]
            print("Set Assembly Version (BUILD):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
            return

    # use parameters to set up version if not provided by script args            
    VER_MAJOR = major
    VER_MINOR = minor
    VER_BUILD = build
    VER_TWEAK = revision

    # update VER_TWEAK base on github     
    if GIT_DESCRIBE:
        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
        VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
    
    print("Set Assembly Version (DEFAULT):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
    
def get_version():
    return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)

def get_version_string(n):
    if n == 3:
        return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD)
    return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_TWEAK)

def build_static_lib():
    return STATIC_LIB

def build_static_bin():
    return STATIC_BIN

def is_cr_lf(fname):
    # Check whether text files use cr/lf
    f = open(fname, 'r')
    line = f.readline()
    f.close()
    sz = len(line)
    return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n'

# dos2unix in python
#    cr/lf --> lf
def dos2unix(fname):
    if is_cr_lf(fname):
        fin  = open(fname, 'r')
        fname_new = '%s.new' % fname
        fout = open(fname_new, 'w')
        for line in fin:
            line = line.rstrip('\r\n')
            fout.write(line)
            fout.write('\n')
        fin.close()
        fout.close()
        shutil.move(fname_new, fname)
        if is_verbose():
            print("dos2unix '%s'" % fname)

def dos2unix_tree():
    for root, dirs, files in os.walk('src'):
        for f in files:
            dos2unix(os.path.join(root, f))


def check_eol():
    if not IS_WINDOWS:
        # Linux/OSX/BSD check if the end-of-line is cr/lf
        if is_cr_lf('LICENSE.txt'):
            if is_verbose():
                print("Fixing end of line...")
            dos2unix_tree()

if os.name == 'nt':
    IS_WINDOWS=True
    # Visual Studio already displays the files being compiled
    SHOW_CPPS=False
elif os.name == 'posix':
    if os.uname()[0] == 'Darwin':
        IS_OSX=True
    elif os.uname()[0] == 'Linux':
        IS_LINUX=True
    elif os.uname()[0] == 'GNU':
        IS_HURD=True
    elif os.uname()[0] == 'FreeBSD':
        IS_FREEBSD=True
    elif os.uname()[0] == 'NetBSD':
        IS_NETBSD=True
    elif os.uname()[0] == 'OpenBSD':
        IS_OPENBSD=True
    elif os.uname()[0] == 'SunOS':
        IS_SUNOS=True
    elif os.uname()[0][:6] == 'CYGWIN':
        IS_CYGWIN=True
        if (CC != None and "mingw" in CC):
            IS_CYGWIN_MINGW=True
    elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
        IS_MSYS2=True
        if os.uname()[4] == 'x86_64':
            LINUX_X64=True
        else:
            LINUX_X64=False


if os.name == 'posix' and os.uname()[4] == 'arm64':
    IS_ARCH_ARM64 = True


def display_help(exit_code):
    print("mk_make.py: Z3 Makefile generator\n")
    print("This script generates the Makefile for the Z3 theorem prover.")
    print("It must be executed from the Z3 root directory.")
    print("\nOptions:")
    print("  -h, --help                    display this message.")
    print("  -s, --silent                  do not print verbose messages.")
    if not IS_WINDOWS:
        print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
    else:
        print("  --parallel=num                use cl option /MP with 'num' parallel processes")
    print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
    print("  -b <subdir>, --build=<subdir>  subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
    print("  --githash=hash                include the given hash in the binaries.")
    print("  --git-describe                include the output of 'git describe' in the version information.")
    print("  -d, --debug                   compile Z3 in debug mode.")
    print("  -t, --trace                   enable tracing in release mode.")
    if IS_WINDOWS:
        print("  --guardcf                     enable Control Flow Guard runtime checks.")
        print("  -x, --x64                     create 64 binary when using Visual Studio.")
    else:
        print("  --x86                         force 32-bit x86 build on x64 systems.")
    print("  --arm64=<bool>                    forcearm64 bit build  on/off (supported for Darwin).")
    print("  -m, --makefiles               generate only makefiles.")
    if IS_WINDOWS:
        print("  -v, --vsproj                  generate Visual Studio Project Files.")
        print("  --optimize                    generate optimized code during linking.")
    print("  --dotnet                      generate .NET platform bindings.")
    print("  --dotnet-key=<file>           sign the .NET assembly using the private key in <file>.")
    print("  --assembly-version=<x.x.x.x>  provide version number for build")
    print("  --java                        generate Java bindings.")
    print("  --ml                          generate OCaml bindings.")
    print("  --js                          generate JScript bindings.")
    print("  --python                      generate Python bindings.")
    print("  --staticlib                   build Z3 static library.")
    print("  --staticbin                   build a statically linked Z3 binary.")
    if not IS_WINDOWS:
        print("  -g, --gmp                     use GMP.")
        print("  --gprof                       enable gprof")
    print("  --log-sync                    synchronize access to API log files to enable multi-thread API logging.")
    print("  --single-threaded             non-thread-safe build")
    print("")
    print("Some influential environment variables:")
    if not IS_WINDOWS:
        print("  CXX        C++ compiler")
        print("  CC         C compiler")
        print("  LDFLAGS    Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
        print("  CPPFLAGS   Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
        print("  CXXFLAGS   C++ compiler flags")
    print("  JDK_HOME   JDK installation directory (only relevant if -j or --java option is provided)")
    print("  JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)")
    print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
    print("  OCAMLFIND  Ocaml find tool (only relevant with --ml)")
    print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
    print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
    print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
    print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
    print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
    print("  Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
    exit(exit_code)

# Parse configuration option for mk_make script
def parse_options():
    global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
    global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
    global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
    global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64
    try:
        options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                               'b:df:sxa:hmcvtnp:gj',
                                               ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
                                                'trace', 'dotnet', 'dotnet-key=', 'assembly-version=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
                                                'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
    except:
        print("ERROR: Invalid command line option")
        display_help(1)

    for opt, arg in options:
        print('opt = %s, arg = %s' % (opt, arg))
        if opt in ('-b', '--build'):
            if arg == 'src':
                raise MKException('The src directory should not be used to host the Makefile')
            set_build_dir(arg)
        elif opt in ('-s', '--silent'):
            VERBOSE = False
        elif opt in ('-d', '--debug'):
            DEBUG_MODE = True
        elif opt in ('-x', '--x64'):
            if not IS_WINDOWS:
                raise MKException('x64 compilation mode can only be specified when using Visual Studio')
            VS_X64 = True
        elif opt in ('--x86'):
            LINUX_X64=False
        elif opt in ('--arm64'):
            IS_ARCH_ARM64 = arg in ('true','on','True','TRUE')
        elif opt in ('-h', '--help'):
            display_help(0)
        elif opt in ('-m', '--makefiles'):
            ONLY_MAKEFILES = True
        elif opt in ('-c', '--showcpp'):
            SHOW_CPPS = True
        elif opt in ('-v', '--vsproj'):
            VS_PROJ = True
        elif opt in ('-t', '--trace'):
            TRACE = True
        elif opt in ('--dotnet',):
            DOTNET_CORE_ENABLED = True
        elif opt in ('--dotnet-key'):
            DOTNET_KEY_FILE = arg
        elif opt in ('--assembly-version'):
            ASSEMBLY_VERSION = arg
        elif opt in ('--staticlib'):
            STATIC_LIB = True
        elif opt in ('--staticbin'):
            STATIC_BIN = True
        elif opt in ('--optimize'):
            SLOW_OPTIMIZE = True
        elif not IS_WINDOWS and opt in ('-p', '--prefix'):
            PREFIX = arg
        elif opt in ('--pypkgdir'):
            PYTHON_PACKAGE_DIR = arg
        elif IS_WINDOWS and opt == '--parallel':
            VS_PAR = True
            VS_PAR_NUM = int(arg)
        elif opt in ('-g', '--gmp'):
            GMP = True
        elif opt in ('-j', '--java'):
            JAVA_ENABLED = True
        elif opt == '--gprof':
            GPROF = True
        elif opt == '--githash':
            GIT_HASH=arg
        elif opt == '--git-describe':
            GIT_DESCRIBE = True
        elif opt in ('', '--ml'):
            ML_ENABLED = True
        elif opt in ('', '--log-sync'):
            LOG_SYNC = True
        elif opt == '--single-threaded':
            SINGLE_THREADED = True
        elif opt in ('--python'):
            PYTHON_ENABLED = True
            PYTHON_INSTALL_ENABLED = True
        elif opt == '--guardcf':
            GUARD_CF = True
            ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE
        else:
            print("ERROR: Invalid command line option '%s'" % opt)
            display_help(1)


# Return a list containing a file names included using '#include' in
# the given C/C++ file named fname.
def extract_c_includes(fname):
    result = {}
    # We look for well behaved #include directives
    std_inc_pat     = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
    system_inc_pat  = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*")
    # We should generate and error for any occurrence of #include that does not match the previous pattern.
    non_std_inc_pat = re.compile(".*#include.*")

    f = io.open(fname, encoding='utf-8', mode='r')
    linenum = 1
    for line in f:
        m1 = std_inc_pat.match(line)
        if m1:
            root_file_name = m1.group(1)
            slash_pos =  root_file_name.rfind('/')
            if slash_pos >= 0  and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src"
                # print(root_file_name)
                root_file_name = root_file_name[slash_pos+1:]
            result[root_file_name] = m1.group(1)
        elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
            raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
        linenum = linenum + 1
    f.close()
    return result


# Given a path dir1/subdir2/subdir3 returns ../../..
def reverse_path(p):
    # Filter out empty components (e.g. will have one if path ends in a slash)
    l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
    n = len(l)
    r = '..'
    for i in range(1, n):
        r = os.path.join(r, '..')
    return r

def mk_dir(d):
    if not os.path.exists(d):
        os.makedirs(d)

def set_build_dir(d):
    global BUILD_DIR, REV_BUILD_DIR
    BUILD_DIR = norm_path(d)
    REV_BUILD_DIR = reverse_path(d)

def set_z3py_dir(p):
    global SRC_DIR, Z3PY_SRC_DIR
    p = norm_path(p)
    full = os.path.join(SRC_DIR, p)
    if not os.path.exists(full):
        raise MKException("Python bindings directory '%s' does not exist" % full)
    Z3PY_SRC_DIR = full
    if VERBOSE:
        print("Python bindings directory was detected.")

_UNIQ_ID = 0

def mk_fresh_name(prefix):
    global _UNIQ_ID
    r = '%s_%s' % (prefix, _UNIQ_ID)
    _UNIQ_ID = _UNIQ_ID + 1
    return r

_Id = 0
_Components = []
_ComponentNames = set()
_Name2Component = {}
_Processed_Headers = set()

# Return the Component object named name
def get_component(name):
    return _Name2Component[name]

def get_components():
    return _Components

# Return the directory where the python bindings are located.
def get_z3py_dir():
    return Z3PY_SRC_DIR


# Return true if in verbose mode
def is_verbose():
    return VERBOSE

def is_java_enabled():
    return JAVA_ENABLED

def is_ml_enabled():
    return ML_ENABLED

def is_dotnet_core_enabled():
    return DOTNET_CORE_ENABLED

def is_python_enabled():
    return PYTHON_ENABLED

def is_python_install_enabled():
    return PYTHON_INSTALL_ENABLED

def is_compiler(given, expected):
    """
    Return True if the 'given' compiler is the expected one.
    >>> is_compiler('g++', 'g++')
    True
    >>> is_compiler('/home/g++', 'g++')
    True
    >>> is_compiler(os.path.join('home', 'g++'), 'g++')
    True
    >>> is_compiler('clang++', 'g++')
    False
    >>> is_compiler(os.path.join('home', 'clang++'), 'clang++')
    True
    """
    if given == expected:
        return True
    if len(expected) < len(given):
        return given[len(given) - len(expected) - 1] == os.sep and given[len(given) - len(expected):] == expected
    return False

def is_CXX_gpp():
    return is_compiler(CXX, 'g++')

def is_clang_in_gpp_form(cc):
    str = check_output([cc, '--version'])
    try:
       version_string = str.encode('utf-8')
    except:
       version_string = str
    clang = 'clang'.encode('utf-8')
    return version_string.find(clang) != -1

def is_CXX_clangpp():
    if is_compiler(CXX, 'g++'):
        return is_clang_in_gpp_form(CXX)
    return is_compiler(CXX, 'clang++')

def get_files_with_ext(path, ext):
    return filter(lambda f: f.endswith(ext), os.listdir(path))

def get_cpp_files(path):
    return get_files_with_ext(path,'.cpp')

def get_c_files(path):
    return get_files_with_ext(path,'.c')

def get_cs_files(path):
    return get_files_with_ext(path,'.cs')

def get_java_files(path):
    return get_files_with_ext(path,'.java')

def get_ml_files(path):
    return get_files_with_ext(path,'.ml')

def find_all_deps(name, deps):
    new_deps = []
    for dep in deps:
        if dep in _ComponentNames:
            if not (dep in new_deps):
                new_deps.append(dep)
            for dep_dep in get_component(dep).deps:
                if not (dep_dep in new_deps):
                    new_deps.append(dep_dep)
        else:
            raise MKException("Unknown component '%s' at '%s'." % (dep, name))
    return new_deps

class Component:
    def __init__(self, name, path, deps):
        global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
        if name in _ComponentNames:
            raise MKException("Component '%s' was already defined." % name)
        if path is None:
            path = name
        self.name = name
        path = norm_path(path)
        self.path = path
        self.deps = find_all_deps(name, deps)
        self.build_dir = path
        self.src_dir   = os.path.join(SRC_DIR, path)
        self.to_src_dir = os.path.join(REV_BUILD_DIR, self.src_dir)

    def get_link_name(self):
        return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'


    # Find fname in the include paths for the given component.
    # ownerfile is only used for creating error messages.
    # That is, we were looking for fname when processing ownerfile
    def find_file(self, fname, ownerfile, orig_include=None):
        full_fname = os.path.join(self.src_dir, fname)

        # Store all our possible locations
        possibilities = set()

        # If the our file exists in the current directory, then we store it
        if os.path.exists(full_fname):

            # We cannot return here, as we might have files with the same
            # basename, but different include paths
            possibilities.add(self)

        for dep in self.deps:
            c_dep = get_component(dep)
            full_fname = os.path.join(c_dep.src_dir, fname)
            if os.path.exists(full_fname):
                possibilities.add(c_dep)

        if possibilities:

            # We have ambiguity
            if len(possibilities) > 1:

                # We expect orig_path to be non-None here, so we can disambiguate
                assert orig_include is not None

                # Get the original directory name
                orig_dir = os.path.dirname(orig_include)

                # Iterate through all of the possibilities
                for possibility in possibilities:

                    path = possibility.path.replace("\\","/")
                    # If we match the suffix of the path ...
                    if path.endswith(orig_dir):

                        # ... use our new match
                        return possibility

            # This means we didn't make an exact match ...
            #
            # We return any one possibility, just to ensure we don't break Z3's
            # builds
            return possibilities.pop()

        raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name))

    # Display all dependencies of file basename located in the given component directory.
    # The result is displayed at out
    def add_cpp_h_deps(self, out, basename):
        includes = extract_c_includes(os.path.join(self.src_dir, basename))
        out.write(os.path.join(self.to_src_dir, basename))
        for include, orig_include in includes.items():
            owner = self.find_file(include, basename, orig_include)
            out.write(' %s.node' % os.path.join(owner.build_dir, include))

    # Add a rule for each #include directive in the file basename located at the current component.
    def add_rule_for_each_include(self, out, basename):
        fullname = os.path.join(self.src_dir, basename)
        includes = extract_c_includes(fullname)
        for include, orig_include in includes.items():
            owner = self.find_file(include, fullname, orig_include)
            owner.add_h_rule(out, include)

    # Display a Makefile rule for an include file located in the given component directory.
    # 'include' is something of the form: ast.h, polynomial.h
    # The rule displayed at out is of the form
    #     ast/ast_pp.h.node : ../src/util/ast_pp.h util/util.h.node ast/ast.h.node
    #       @echo "done" > ast/ast_pp.h.node
    def add_h_rule(self, out, include):
        include_src_path   = os.path.join(self.to_src_dir, include)
        if include_src_path in _Processed_Headers:
            return
        _Processed_Headers.add(include_src_path)
        self.add_rule_for_each_include(out, include)
        include_node = '%s.node' % os.path.join(self.build_dir, include)
        out.write('%s: ' % include_node)
        self.add_cpp_h_deps(out, include)
        out.write('\n')
        out.write('\t@echo done > %s\n' % include_node)

    def add_cpp_rules(self, out, include_defs, cppfile):
        self.add_rule_for_each_include(out, cppfile)
        objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
        srcfile = os.path.join(self.to_src_dir, cppfile)
        out.write('%s: ' % objfile)
        self.add_cpp_h_deps(out, cppfile)
        out.write('\n')
        if SHOW_CPPS:
            out.write('\t@echo %s\n' % os.path.join(self.src_dir, cppfile))
        out.write('\t@$(CXX) $(CXXFLAGS) $(%s) $(CXX_OUT_FLAG)%s %s\n' % (include_defs, objfile, srcfile))

    def mk_makefile(self, out):
        include_defs = mk_fresh_name('includes')
        out.write('%s =' % include_defs)
        for dep in self.deps:
            out.write(' -I%s' % get_component(dep).to_src_dir)
        out.write(' -I%s' % os.path.join(REV_BUILD_DIR,"src"))
        out.write('\n')
        mk_dir(os.path.join(BUILD_DIR, self.build_dir))
        if VS_PAR and IS_WINDOWS:
            cppfiles = list(get_cpp_files(self.src_dir))
            dependencies = set()
            for cppfile in cppfiles:
                dependencies.add(os.path.join(self.to_src_dir, cppfile))
                self.add_rule_for_each_include(out, cppfile)
                includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
                for include, orig_include in includes.items():
                    owner = self.find_file(include, cppfile, orig_include)
                    dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
            for cppfile in cppfiles:
                out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
            out.write(': ')
            for dep in dependencies:
                out.write(dep)
                out.write(' ')
            out.write('\n')
            out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
            for cppfile in cppfiles:
                out.write(' ')
                out.write(os.path.join(self.to_src_dir, cppfile))
            out.write('\n')
            out.write('\tmove *.obj %s\n' % self.build_dir)
        else:
            for cppfile in get_cpp_files(self.src_dir):
                self.add_cpp_rules(out, include_defs, cppfile)

    # Return true if the component should be included in the all: rule
    def main_component(self):
        return False

    # Return true if the component contains an AssemblyInfo.cs file that needs to be updated.
    def has_assembly_info(self):
        return False

    # Return true if the component needs builder to generate an install_tactics.cpp file
    def require_install_tactics(self):
        return False

    # Return true if the component needs a def file
    def require_def_file(self):
        return False

    # Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
    def require_mem_initializer(self):
        return False

    def mk_install_deps(self, out):
        return

    def mk_install(self, out):
        return

    def mk_uninstall(self, out):
        return

    def is_example(self):
        return False

    # Invoked when creating a (windows) distribution package using components at build_path, and
    # storing them at dist_path
    def mk_win_dist(self, build_path, dist_path):
        return

    def mk_unix_dist(self, build_path, dist_path):
        return

    # Used to print warnings or errors after mk_make.py is done, so that they
    # are not quite as easy to miss.
    def final_info(self):
        pass

class LibComponent(Component):
    def __init__(self, name, path, deps, includes2install):
        Component.__init__(self, name, path, deps)
        self.includes2install = includes2install

    def mk_makefile(self, out):
        Component.mk_makefile(self, out)
        # generate rule for lib
        objs = []
        for cppfile in get_cpp_files(self.src_dir):
            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
            objs.append(objfile)

        libfile = '%s$(LIB_EXT)' % os.path.join(self.build_dir, self.name)
        out.write('%s:' % libfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        out.write('\n')
        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        out.write('\n')
        out.write('%s: %s\n\n' % (self.name, libfile))

    def mk_install_deps(self, out):
        return

    def mk_install(self, out):
        for include in self.includes2install:
            MakeRuleCmd.install_files(
                out,
                os.path.join(self.to_src_dir, include),
                os.path.join(INSTALL_INCLUDE_DIR, include)
            )

    def mk_uninstall(self, out):
        for include in self.includes2install:
            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include))

    def mk_win_dist(self, build_path, dist_path):
        mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR))
        for include in self.includes2install:
            shutil.copy(os.path.join(self.src_dir, include),
                        os.path.join(dist_path, INSTALL_INCLUDE_DIR, include))

    def mk_unix_dist(self, build_path, dist_path):
        self.mk_win_dist(build_path, dist_path)

# "Library" containing only .h files. This is just a placeholder for includes files to be installed.
class HLibComponent(LibComponent):
    def __init__(self, name, path, includes2install):
        LibComponent.__init__(self, name, path, [], includes2install)

    def mk_makefile(self, out):
        return

# Auxiliary function for sort_components
def comp_components(c1, c2):
    id1 = get_component(c1).id
    id2 = get_component(c2).id
    return id2 - id1

# Sort components based on (reverse) definition time
def sort_components(cnames):
    return sorted(cnames, key=lambda c: get_component(c).id, reverse=True)

class ExeComponent(Component):
    def __init__(self, name, exe_name, path, deps, install):
        Component.__init__(self, name, path, deps)
        if exe_name is None:
            exe_name = name
        self.exe_name = exe_name
        self.install = install

    def mk_makefile(self, out):
        Component.mk_makefile(self, out)
        # generate rule for exe

        exefile = '%s$(EXE_EXT)' % self.exe_name
        out.write('%s:' % exefile)
        deps = sort_components(self.deps)
        objs = []
        for cppfile in get_cpp_files(self.src_dir):
            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
            objs.append(objfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        for dep in deps:
            c_dep = get_component(dep)
            out.write(' ' + c_dep.get_link_name())
        out.write('\n')
        extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else ''
        out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile))
        for obj in objs:
            out.write(' ')
            out.write(obj)
        for dep in deps:
            c_dep = get_component(dep)
            out.write(' ' + c_dep.get_link_name())
        out.write(' $(LINK_EXTRA_FLAGS)\n')
        out.write('%s: %s\n\n' % (self.name, exefile))

    def require_install_tactics(self):
        return ('tactic' in self.deps) and ('cmd_context' in self.deps)

    def require_mem_initializer(self):
        return True

    # All executables (to be installed) are included in the all: rule
    def main_component(self):
        return self.install

    def mk_install_deps(self, out):
        if self.install:
            exefile = '%s$(EXE_EXT)' % self.exe_name
            out.write('%s' % exefile)

    def mk_install(self, out):
        if self.install:
            exefile = '%s$(EXE_EXT)' % self.exe_name
            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile))

    def mk_uninstall(self, out):
        if self.install:
            exefile = '%s$(EXE_EXT)' % self.exe_name
            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile))

    def mk_win_dist(self, build_path, dist_path):
        if self.install:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name),
                        '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))

    def mk_unix_dist(self, build_path, dist_path):
        if self.install:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy(os.path.join(build_path, self.exe_name),
                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))


class ExtraExeComponent(ExeComponent):
    def __init__(self, name, exe_name, path, deps, install):
        ExeComponent.__init__(self, name, exe_name, path, deps, install)

    def main_component(self):
        return False

    def require_mem_initializer(self):
        return False

def get_so_ext():
    sysname = os.uname()[0]
    if sysname == 'Darwin':
        return 'dylib'
    elif sysname == 'Linux' or sysname == 'GNU' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
        return 'so'
    elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
        return 'dll'
    else:
        assert(False)
        return 'dll'

class DLLComponent(Component):
    def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None):
        Component.__init__(self, name, path, deps)
        if dll_name is None:
            dll_name = name
        self.dll_name = dll_name
        self.export_files = export_files
        self.reexports = reexports
        self.install = install
        self.static = static
        self.staging_link = staging_link    # link a copy of the shared object into this directory on build

    def get_link_name(self):
        if self.static:
            return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
        else:
            return self.name + '$(SO_EXT)'

    def dll_file(self):
        """
            Return file name of component suitable for use in a Makefile
        """
        return '%s$(SO_EXT)' % self.dll_name

    def install_path(self):
        """
            Return install location of component (relative to prefix)
            suitable for use in a Makefile
        """
        return os.path.join(INSTALL_LIB_DIR, self.dll_file())

    def mk_makefile(self, out):
        Component.mk_makefile(self, out)
        # generate rule for (SO_EXT)
        out.write('%s:' % self.dll_file())
        deps = sort_components(self.deps)
        objs = []
        for cppfile in get_cpp_files(self.src_dir):
            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
            objs.append(objfile)
        # Explicitly include obj files of reexport. This fixes problems with exported symbols on Linux and OSX.
        for reexport in self.reexports:
            reexport = get_component(reexport)
            for cppfile in get_cpp_files(reexport.src_dir):
                objfile = '%s$(OBJ_EXT)' % os.path.join(reexport.build_dir, os.path.splitext(cppfile)[0])
                objs.append(objfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        for dep in deps:
            if dep not in self.reexports:
                c_dep = get_component(dep)
                out.write(' ' + c_dep.get_link_name())
        out.write('\n')
        out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file())
        for obj in objs:
            out.write(' ')
            out.write(obj)
        for dep in deps:
            if dep not in self.reexports:
                c_dep = get_component(dep)
                out.write(' ' + c_dep.get_link_name())
        out.write(' $(SLINK_EXTRA_FLAGS)')
        if IS_WINDOWS:
            out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name))
        if self.staging_link:
            if IS_WINDOWS:
                out.write('\n\tcopy %s %s' % (self.dll_file(), self.staging_link))
            elif IS_OSX:
                out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link))
            else:
                out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link))
        out.write('\n')
        if self.static:
            if IS_WINDOWS:
                libfile = '%s-static$(LIB_EXT)' % self.dll_name
            else:
                libfile = '%s$(LIB_EXT)' % self.dll_name
            self.mk_static(out, libfile)
            out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile))
        else:
            out.write('%s: %s\n\n' % (self.name, self.dll_file()))

    def mk_static(self, out, libfile):
        # generate rule for lib
        objs = []
        for cppfile in get_cpp_files(self.src_dir):
            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
            objs.append(objfile)
        # we have to "reexport" all object files
        for dep in self.deps:
            dep = get_component(dep)
            for cppfile in get_cpp_files(dep.src_dir):
                objfile = '%s$(OBJ_EXT)' % os.path.join(dep.build_dir, os.path.splitext(cppfile)[0])
                objs.append(objfile)
        out.write('%s:' % libfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        out.write('\n')
        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
        for obj in objs:
            out.write(' ')
            out.write(obj)
        out.write('\n')

    def main_component(self):
        return self.install

    def require_install_tactics(self):
        return ('tactic' in self.deps) and ('cmd_context' in self.deps)

    def require_mem_initializer(self):
        return True

    def require_def_file(self):
        return IS_WINDOWS and self.export_files

    def mk_install_deps(self, out):
        out.write('%s$(SO_EXT)' % self.dll_name)
        if self.static:
            out.write(' %s$(LIB_EXT)' % self.dll_name)

    def mk_install(self, out):
        if self.install:
            MakeRuleCmd.install_files(out, self.dll_file(), self.install_path())
            if self.static:
                libfile = '%s$(LIB_EXT)' % self.dll_name
                MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile))

    def mk_uninstall(self, out):
        MakeRuleCmd.remove_installed_files(out, self.install_path())
        libfile = '%s$(LIB_EXT)' % self.dll_name
        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))

    def mk_win_dist(self, build_path, dist_path):
        if self.install:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
                        '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))

    def mk_unix_dist(self, build_path, dist_path):
        if self.install:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            so = get_so_ext()
            shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
                        '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
            shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))

class JsComponent(Component):
    def __init__(self):
         Component.__init__(self, "js", None, [])

    def main_component(self):
        return False

    def mk_win_dist(self, build_path, dist_path):
        return

    def mk_unix_dist(self, build_path, dist_path):
        return

    def mk_makefile(self, out):
        return

class PythonComponent(Component):
    def __init__(self, name, libz3Component):
        assert isinstance(libz3Component, DLLComponent)
        global PYTHON_ENABLED
        Component.__init__(self, name, None, [])
        self.libz3Component = libz3Component

    def main_component(self):
        return False

    def mk_win_dist(self, build_path, dist_path):
        if not is_python_enabled():
            return

        src = os.path.join(build_path, 'python', 'z3')
        dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
        if os.path.exists(dst):
            shutil.rmtree(dst)
        shutil.copytree(src, dst)

    def mk_unix_dist(self, build_path, dist_path):
        self.mk_win_dist(build_path, dist_path)

    def mk_makefile(self, out):
        return

class PythonInstallComponent(Component):
    def __init__(self, name, libz3Component):
        assert isinstance(libz3Component, DLLComponent)
        global PYTHON_INSTALL_ENABLED
        Component.__init__(self, name, None, [])
        self.pythonPkgDir = None
        self.in_prefix_install = True
        self.libz3Component = libz3Component

        if not PYTHON_INSTALL_ENABLED:
            return

        if IS_WINDOWS:
            # Installing under Windows doesn't make sense as the install prefix is used
            # but that doesn't make sense under Windows
            # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix,
            # i.e., something along the lines of C:\Python\... At the moment we are not
            # sure whether we would want to install libz3.dll into that directory though.
            PYTHON_INSTALL_ENABLED = False
            return
        else:
            PYTHON_INSTALL_ENABLED = True

        if IS_WINDOWS or IS_OSX:
            # Use full path that is possibly outside of install prefix
            self.in_prefix_install = PYTHON_PACKAGE_DIR.startswith(PREFIX)
            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
        else:
            # Use path inside the prefix (should be the normal case on Linux)
            # CMW: Also normal on *BSD?
            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
                raise MKException(('The python package directory ({}) must live ' +
                    'under the install prefix ({}) to install the python bindings.' +
                    'Use --pypkgdir and --prefix to set the python package directory ' +
                    'and install prefix respectively. Note that the python package ' +
                    'directory does not need to exist and will be created if ' +
                    'necessary during install.').format(
                        PYTHON_PACKAGE_DIR,
                        PREFIX))
            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
            self.in_prefix_install = True

        if self.in_prefix_install:
            assert not os.path.isabs(self.pythonPkgDir)

    def final_info(self):
        if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED:
            print("Warning: The detected Python package directory (%s) is not "
                  "in the installation prefix (%s). This can lead to a broken "
                  "Python API installation. Use --pypkgdir= to change the "
                  "Python package directory." % (PYTHON_PACKAGE_DIR, PREFIX))

    def main_component(self):
        return False

    def mk_install(self, out):
        if not is_python_install_enabled():
            return
        MakeRuleCmd.make_install_directory(out,
                                           os.path.join(self.pythonPkgDir, 'z3'),
                                           in_prefix=self.in_prefix_install)
        MakeRuleCmd.make_install_directory(out,
                                           os.path.join(self.pythonPkgDir, 'z3', 'lib'),
                                           in_prefix=self.in_prefix_install)

        # Sym-link or copy libz3 into python package directory
        if IS_WINDOWS or IS_OSX:
            MakeRuleCmd.install_files(out,
                                      self.libz3Component.dll_file(),
                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
                                                   self.libz3Component.dll_file()),
                                      in_prefix=self.in_prefix_install
                                     )
        else:
            # Create symbolic link to save space.
            # It's important that this symbolic link be relative (rather
            # than absolute) so that the install is relocatable (needed for
            # staged installs that use DESTDIR).
            MakeRuleCmd.create_relative_symbolic_link(out,
                                                      self.libz3Component.install_path(),
                                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
                                                                   self.libz3Component.dll_file()
                                                                  ),
                                                     )

        MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'),
                                  os.path.join(self.pythonPkgDir, 'z3'),
                                  in_prefix=self.in_prefix_install)
        if sys.version >= "3":
            pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__')
            MakeRuleCmd.make_install_directory(out,
                                               pythonPycacheDir,
                                               in_prefix=self.in_prefix_install)
            MakeRuleCmd.install_files(out,
                                      os.path.join('python', 'z3', '__pycache__', '*.pyc'),
                                      pythonPycacheDir,
                                      in_prefix=self.in_prefix_install)
        else:
            MakeRuleCmd.install_files(out,
                                      os.path.join('python', 'z3', '*.pyc'),
                                      os.path.join(self.pythonPkgDir,'z3'),
                                      in_prefix=self.in_prefix_install)

        if PYTHON_PACKAGE_DIR != sysconfig.get_path('purelib'):
            out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)

    def mk_uninstall(self, out):
        if not is_python_install_enabled():
            return
        MakeRuleCmd.remove_installed_files(out,
                                           os.path.join(self.pythonPkgDir,
                                                        self.libz3Component.dll_file()),
                                           in_prefix=self.in_prefix_install
                                          )
        MakeRuleCmd.remove_installed_files(out,
                                           os.path.join(self.pythonPkgDir, 'z3', '*.py'),
                                           in_prefix=self.in_prefix_install)
        MakeRuleCmd.remove_installed_files(out,
                                           os.path.join(self.pythonPkgDir, 'z3', '*.pyc'),
                                           in_prefix=self.in_prefix_install)
        MakeRuleCmd.remove_installed_files(out,
                                           os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
                                           in_prefix=self.in_prefix_install
                                          )
        MakeRuleCmd.remove_installed_files(out,
                                           os.path.join(self.pythonPkgDir, 'z3', 'lib',
                                                        self.libz3Component.dll_file()))

    def mk_makefile(self, out):
        return

def set_key_file(self):
    global DOTNET_KEY_FILE
    # We need to give the assembly a strong name so that it
    # can be installed into the GAC with ``make install``
    if not DOTNET_KEY_FILE is None:
       self.key_file = DOTNET_KEY_FILE

    if not self.key_file is None:
       if os.path.isfile(self.key_file):
           self.key_file = os.path.abspath(self.key_file)
       elif os.path.isfile(os.path.join(self.src_dir, self.key_file)):
           self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file))
       else:
           print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
           self.key_file = None


# build for dotnet core
class DotNetDLLComponent(Component):
    def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file):
        Component.__init__(self, name, path, deps)
        if dll_name is None:
            dll_name = name
        if assembly_info_dir is None:
            assembly_info_dir = "."
        self.dll_name          = dll_name
        self.assembly_info_dir = assembly_info_dir
        self.key_file = default_key_file


    def mk_makefile(self, out):
        if not is_dotnet_core_enabled():
            return
        cs_fp_files = []
        for cs_file in get_cs_files(self.src_dir):
            cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
        if self.assembly_info_dir != '.':
            for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
                cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
        dllfile = '%s.dll' % self.dll_name
        out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
        for cs_file in cs_fp_files:
            out.write(' ')
            out.write(cs_file)
        out.write('\n')

        set_key_file(self)
        key = ""
        if not self.key_file is None:
            key = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
            key += "\n<SignAssembly>true</SignAssembly>"

        version = get_version_string(4)

        print("Version output to csproj:", version)

        core_csproj_str = r"""<Project Sdk="Microsoft.NET.Sdk">

  <PropertyGroup>
    <TargetFramework>netstandard1.4</TargetFramework>
    <LangVersion>8.0</LangVersion>
    <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
    <DebugType>full</DebugType>
    <AssemblyName>Microsoft.Z3</AssemblyName>
    <OutputType>Library</OutputType>
    <PackageId>Microsoft.Z3</PackageId>
    <GenerateDocumentationFile>true</GenerateDocumentationFile>
    <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
    <Version>%s</Version>
    <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
    <Authors>Microsoft</Authors>
    <Company>Microsoft</Company>
    <PackageReadmeFile>README.md</PackageReadmeFile>
    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
    <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
    <Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
    <PackageTags>smt constraint solver theorem prover</PackageTags>
    %s
  </PropertyGroup>

  <ItemGroup>
    <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
    <None Include="..\%s\README.md" Pack="true" PackagePath="/"/>
  </ItemGroup>

</Project>""" % (version, key, self.to_src_dir, self.to_src_dir)

        mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
        csproj = os.path.join('dotnet', 'z3.csproj')
        with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
            ous.write(core_csproj_str)

        dotnetCmdLine = [DOTNET, "build", csproj]

        dotnetCmdLine.extend(['-c'])
        if DEBUG_MODE:
            dotnetCmdLine.extend(['Debug'])
        else:
            dotnetCmdLine.extend(['Release'])

        path = os.path.join(os.path.abspath(BUILD_DIR), ".")
        dotnetCmdLine.extend(['-o', "\"%s\"" % path])

        MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
        out.write('\n')
        out.write('%s: %s\n\n' % (self.name, dllfile))

    def main_component(self):
        return is_dotnet_core_enabled()

    def has_assembly_info(self):
        # TBD: is this required for dotnet core given that version numbers are in z3.csproj file?
        return False


    def mk_win_dist(self, build_path, dist_path):
        if is_dotnet_core_enabled():
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            if DEBUG_MODE:
                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
                            '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))

    def mk_unix_dist(self, build_path, dist_path):
        if is_dotnet_core_enabled():
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))

    def mk_install_deps(self, out):
        pass

    def mk_install(self, out):
        pass

    def mk_uninstall(self, out):
        pass

class JavaDLLComponent(Component):
    def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
        Component.__init__(self, name, path, deps)
        if dll_name is None:
            dll_name = name
        self.dll_name     = dll_name
        self.package_name = package_name
        self.manifest_file = manifest_file
        self.install = not is_windows()

    def mk_makefile(self, out):
        global JAVAC
        global JAR

        if is_java_enabled():
            mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
            dllfile = '%s$(SO_EXT)' % self.dll_name
            out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
            t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s" -I"%s/PLATFORM" -I%s %s/Native.cpp\n' % (JNI_HOME, JNI_HOME, get_component('api').to_src_dir, self.to_src_dir)
            if IS_OSX:
                t = t.replace('PLATFORM', 'darwin')
            elif is_linux():
                t = t.replace('PLATFORM', 'linux')
            elif is_hurd():
                t = t.replace('PLATFORM', 'hurd')
            elif IS_FREEBSD:
                t = t.replace('PLATFORM', 'freebsd')
            elif IS_NETBSD:
                t = t.replace('PLATFORM', 'netbsd')
            elif IS_OPENBSD:
                t = t.replace('PLATFORM', 'openbsd')
            elif IS_SUNOS:
                t = t.replace('PLATFORM', 'SunOS')
            elif IS_CYGWIN:
                t = t.replace('PLATFORM', 'cygwin')
            elif IS_MSYS2:
                t = t.replace('PLATFORM', 'win32')
            else:
                t = t.replace('PLATFORM', 'win32')
            out.write(t)
            if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
                          os.path.join('api', 'java', 'Native'))
            elif IS_OSX and IS_ARCH_ARM64:
                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
                          os.path.join('api', 'java', 'Native'))                
            else:
                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
                          os.path.join('api', 'java', 'Native'))
            out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
            deps = ''
            for jfile in get_java_files(self.src_dir):
                deps += ('%s ' % os.path.join(self.to_src_dir, jfile))
            for jfile in get_java_files(os.path.join(self.src_dir, "enumerations")):
                deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile)
            out.write(deps)
            out.write('\n')
            #if IS_WINDOWS:
            JAVAC = '"%s"' % JAVAC
            JAR = '"%s"' % JAR
            t = ('\t%s -source 1.8 -target 1.8 %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
            out.write(t)
            t = ('\t%s -source 1.8 -target 1.8 -cp %s %s.java -d %s\n' % (JAVAC,
                                                  os.path.join('api', 'java', 'classes'),
                                                  os.path.join(self.to_src_dir, '*'),
                                                  os.path.join('api', 'java', 'classes')))
            out.write(t)
            out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
                                                         os.path.join(self.to_src_dir, 'manifest'),
                                                         os.path.join('api', 'java', 'classes')))
            out.write('java: %s.jar\n\n' % self.package_name)

    def main_component(self):
        return is_java_enabled()

    def mk_win_dist(self, build_path, dist_path):
        if JAVA_ENABLED:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
            shutil.copy(os.path.join(build_path, 'libz3java.dll'),
                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll'))
            shutil.copy(os.path.join(build_path, 'libz3java.lib'),
                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib'))

    def mk_unix_dist(self, build_path, dist_path):
        if JAVA_ENABLED:
            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
            so = get_so_ext()
            shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))

    def mk_install(self, out):
        if is_java_enabled() and self.install:
            dllfile = '%s$(SO_EXT)' % self.dll_name
            MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile))
            jarfile = '{}.jar'.format(self.package_name)
            MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile))

    def mk_uninstall(self, out):
        if is_java_enabled() and self.install:
            dllfile = '%s$(SO_EXT)' % self.dll_name
            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
            jarfile = '{}.jar'.format(self.package_name)
            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))

class MLComponent(Component):

    def __init__(self, name, lib_name, path, deps):
        Component.__init__(self, name, path, deps)
        if lib_name is None:
            lib_name = name
        self.lib_name = lib_name
        self.modules = ["z3enums", "z3native", "z3"]  # dependencies in this order!
        self.stubs = "z3native_stubs"
        self.sub_dir = os.path.join('api', 'ml')

        self.destdir = ""
        self.ldconf = ""
        # Calling _init_ocamlfind_paths() is postponed to later because
        # OCAMLFIND hasn't been checked yet.

    def _install_bindings(self):
        # FIXME: Depending on global state is gross.  We can't pre-compute this
        # in the constructor because we haven't tested for ocamlfind yet
        return OCAMLFIND != ''

    def _init_ocamlfind_paths(self):
        """
            Initialises self.destdir and self.ldconf
            Do not call this from the MLComponent constructor because OCAMLFIND
            has not been checked at that point
        """
        if self.destdir != "" and self.ldconf != "":
            # Initialisation already done
            return
        # Use Ocamlfind to get the default destdir and ldconf path
        self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir'])
        if self.destdir == "":
            raise MKException('Failed to get OCaml destdir')

        if not os.path.isdir(self.destdir):
            raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir))

        self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf'])
        if self.ldconf == "":
            raise MKException('Failed to get OCaml ldconf path')

    def final_info(self):
        if not self._install_bindings():
            print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed")

    def mk_makefile(self, out):
        if is_ml_enabled():
            CP_CMD = 'cp'
            if IS_WINDOWS:
                CP_CMD='copy'

            OCAML_FLAGS = ''
            if DEBUG_MODE:
                OCAML_FLAGS += '-g'

            if OCAMLFIND:
                OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package zarith' + ' ' + OCAML_FLAGS
                OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package zarith' + ' ' + OCAML_FLAGS
            else:
                OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
                OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS

            src_dir = self.to_src_dir
            mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
            api_src = get_component(API_COMPONENT).to_src_dir
            # remove /GL and -std=c++17; the ocaml tools don't like them.
            if IS_WINDOWS:
                out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n')
            else:
                out.write('CXXFLAGS_OCAML=$(subst -std=c++17,,$(CXXFLAGS))\n')

            substitutions = { 'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) }

            configure_file(os.path.join(self.src_dir, 'META.in'),
                           os.path.join(BUILD_DIR, self.sub_dir, 'META'),
                           substitutions)

            stubsc = os.path.join(src_dir, self.stubs + '.c')
            stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
            base_dll_name = get_component(Z3_DLL_COMPONENT).dll_name
            if STATIC_LIB:
                z3link = 'z3-static'
                z3linkdep = base_dll_name + '-static$(LIB_EXT)'
                out.write('%s: %s\n' % (z3linkdep, base_dll_name + '$(LIB_EXT)'))
                out.write('\tcp $< $@\n')
            else:
                z3link = 'z3'
                z3linkdep = base_dll_name + '$(SO_EXT)'
            out.write('%s: %s %s\n' % (stubso, stubsc, z3linkdep))
            out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
                      (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))

            cmos = ''
            for m in self.modules:
                ml = os.path.join(src_dir, m + '.ml')
                cmo = os.path.join(self.sub_dir, m + '.cmo')
                existing_mli = os.path.join(src_dir, m + '.mli')
                mli = os.path.join(self.sub_dir, m + '.mli')
                cmi = os.path.join(self.sub_dir, m + '.cmi')
                out.write('%s: %s %s\n' % (cmo, ml, cmos))
                if (os.path.exists(existing_mli[3:])):
                    out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
                else:
                    out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli))
                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml))
                cmos = cmos + cmo + ' '

            cmxs = ''
            for m in self.modules:
                ff = os.path.join(src_dir, m + '.ml')
                ft = os.path.join(self.sub_dir, m + '.cmx')
                out.write('%s: %s %s %s\n' % (ft, ff, cmos, cmxs))
                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
                cmxs = cmxs + ' ' + ft


            OCAMLMKLIB = 'ocamlmklib'

            LIBZ3 = '-l' + z3link + ' -lstdc++'
            if is_cygwin() and not(is_cygwin_mingw()):
                LIBZ3 = z3linkdep

            LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))

            stubs_install_path = '$$(%s printconf destdir)/stublibs' % OCAMLFIND
            if not STATIC_LIB:
                loadpath = '-ccopt -L' + stubs_install_path
                dllpath = '-dllpath ' + stubs_install_path
                LIBZ3 = LIBZ3 + ' ' + loadpath + ' ' + dllpath

            if DEBUG_MODE and not(is_cygwin()):
                # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
                OCAMLMKLIB += ' -g'

            z3mls = os.path.join(self.sub_dir, 'z3ml')

            LIBZ3ML = ''
            if STATIC_LIB:
                LIBZ3ML = '-oc ' + os.path.join(self.sub_dir, 'z3ml-static')

            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))
            out.write('\t%s -o %s %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, LIBZ3ML, self.sub_dir, stubso, cmos, LIBZ3))
            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))
            out.write('\t%s -o %s %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, LIBZ3ML, self.sub_dir, stubso, cmxs, LIBZ3))
            out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
            out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))

            out.write('\n')
            out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
            if IS_OSX:
                out.write('\tinstall_name_tool -id %s/libz3.dylib libz3.dylib\n' % (stubs_install_path))
                out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path))
            out.write('\n')

            if IS_WINDOWS:
                out.write('ocamlfind_install: ')
                self.mk_install_deps(out)
                out.write('\n')
                self.mk_install(out)
                out.write('\n')
                out.write('ocamlfind_uninstall:\n')
                self.mk_uninstall(out)
                out.write('\n')

    # The following three functions may be out of date.
    def mk_install_deps(self, out):
        if is_ml_enabled() and self._install_bindings():
            out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
            out.write(os.path.join(self.sub_dir, 'META '))
            out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
            out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
            out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))

    def mk_install(self, out):
        if is_ml_enabled() and self._install_bindings():
            self._init_ocamlfind_paths()
            in_prefix = self.destdir.startswith(PREFIX)
            maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX)
            # Note that when doing a staged install with DESTDIR that modifying
            # OCaml's ``ld.conf`` may fail. Therefore packagers will need to
            # make their packages modify it manually at package install time
            # as opposed to ``make install`` time.
            MakeRuleCmd.make_install_directory(out,
                                               maybe_stripped_destdir,
                                               in_prefix=in_prefix)
            out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format(
                ldconf=self.ldconf,
                ocamlfind=OCAMLFIND,
                ocaml_destdir=self.destdir,
                metafile=os.path.join(self.sub_dir, 'META')))

            for m in self.modules:
                mli = os.path.join(self.src_dir, m) + '.mli'
                if os.path.exists(mli):
                    out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
                else:
                    out.write(' ' + os.path.join(self.sub_dir, m) + '.mli')
                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx')
            out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma'))))
            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa'))))
            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs'))))
            out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
            if is_windows() or is_cygwin_mingw() or is_msys2():
                out.write('.dll')
            else:
                out.write('.so') # .so also on OSX!
            out.write('\n')

    def mk_uninstall(self, out):
        if is_ml_enabled() and self._install_bindings():
            self._init_ocamlfind_paths()
            out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format(
                ldconf=self.ldconf,
                ocamlfind=OCAMLFIND,
                ocaml_destdir=self.destdir))

    def main_component(self):
        return is_ml_enabled()

class ExampleComponent(Component):
    def __init__(self, name, path):
        Component.__init__(self, name, path, [])
        self.ex_dir   = os.path.join(EXAMPLE_DIR, self.path)
        self.to_ex_dir = os.path.join(REV_BUILD_DIR, self.ex_dir)

    def is_example(self):
        return True

class CppExampleComponent(ExampleComponent):
    def __init__(self, name, path):
        ExampleComponent.__init__(self, name, path)

    def compiler(self):
        return "$(CXX)"

    def src_files(self):
        return get_cpp_files(self.ex_dir)

    def mk_makefile(self, out):
        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
        dll = '%s$(SO_EXT)' % dll_name

        objfiles = ''
        for cppfile in self.src_files():
            objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')])
            objfiles = objfiles + ('%s ' % objfile)
            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile)));
            out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
            # Add include dir components
            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
            out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
            out.write(' %s' % os.path.join(self.to_ex_dir, cppfile))
            out.write('\n')

        exefile = '%s$(EXE_EXT)' % self.name
        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
        if IS_WINDOWS:
            out.write('%s.lib' % dll_name)
        else:
            out.write(dll)
        out.write(' $(LINK_EXTRA_FLAGS)\n')
        out.write('_ex_%s: %s\n\n' % (self.name, exefile))

class CExampleComponent(CppExampleComponent):
    def __init__(self, name, path):
        CppExampleComponent.__init__(self, name, path)

    def compiler(self):
        return "$(CC)"

    def src_files(self):
        return get_c_files(self.ex_dir)

    def mk_makefile(self, out):
        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
        dll = '%s$(SO_EXT)' % dll_name

        objfiles = ''
        for cfile in self.src_files():
            objfile = '%s$(OBJ_EXT)' % (cfile[:cfile.rfind('.')])
            objfiles = objfiles + ('%s ' % objfile)
            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cfile)));
            out.write('\t%s $(CFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(C_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
            out.write(' %s' % os.path.join(self.to_ex_dir, cfile))
            out.write('\n')

        exefile = '%s$(EXE_EXT)' % self.name
        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
        if IS_WINDOWS:
            out.write('%s.lib' % dll_name)
        else:
            out.write(dll)
        out.write(' $(LINK_EXTRA_FLAGS)\n')
        out.write('_ex_%s: %s\n\n' % (self.name, exefile))

class DotNetExampleComponent(ExampleComponent):
    def __init__(self, name, path):
        ExampleComponent.__init__(self, name, path)

    def is_example(self):
        return is_dotnet_core_enabled()

    def mk_makefile(self, out):
        if is_dotnet_core_enabled():
            proj_name = 'dotnet_example.csproj'
            out.write('_ex_%s:' % self.name)
            for csfile in get_cs_files(self.ex_dir):
                out.write(' ')
                out.write(os.path.join(self.to_ex_dir, csfile))

            mk_dir(os.path.join(BUILD_DIR, 'dotnet_example'))
            csproj = os.path.join('dotnet_example', proj_name)
            if VS_X64:
                platform = 'x64'
            elif VS_ARM:
                platform = 'ARM'
            else:
                platform = 'x86'

            dotnet_proj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
  <PropertyGroup>
    <OutputType>Exe</OutputType>
    <TargetFramework>netcoreapp2.0</TargetFramework>
    <PlatformTarget>%s</PlatformTarget>
  </PropertyGroup>
  <ItemGroup>
    <Compile Include="..\%s/*.cs" />
    <Reference Include="Microsoft.Z3">
      <HintPath>..\Microsoft.Z3.dll</HintPath>
    </Reference>
  </ItemGroup>
</Project>""" % (platform, self.to_ex_dir)

            with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
                ous.write(dotnet_proj_str)

            out.write('\n')
            dotnetCmdLine = [DOTNET, "build", csproj]
            dotnetCmdLine.extend(['-c'])
            if DEBUG_MODE:
                dotnetCmdLine.extend(['Debug'])
            else:
                dotnetCmdLine.extend(['Release'])
            MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
            out.write('\n')

class JavaExampleComponent(ExampleComponent):
    def __init__(self, name, path):
        ExampleComponent.__init__(self, name, path)

    def is_example(self):
        return JAVA_ENABLED

    def mk_makefile(self, out):
        if JAVA_ENABLED:
            pkg = get_component(JAVA_COMPONENT).package_name + '.jar'
            out.write('JavaExample.class: %s' % (pkg))
            deps = ''
            for jfile in get_java_files(self.ex_dir):
                out.write(' %s' % os.path.join(self.to_ex_dir, jfile))
            if IS_WINDOWS:
                deps = deps.replace('/', '\\')
            out.write('%s\n' % deps)
            out.write('\t%s -cp %s ' % (JAVAC, pkg))
            win_ex_dir = self.to_ex_dir
            for javafile in get_java_files(self.ex_dir):
                out.write(' ')
                out.write(os.path.join(win_ex_dir, javafile))
            out.write(' -d .\n')
            out.write('_ex_%s: JavaExample.class\n\n' % (self.name))

class MLExampleComponent(ExampleComponent):
    def __init__(self, name, path):
        ExampleComponent.__init__(self, name, path)

    def is_example(self):
        return ML_ENABLED

    def mk_makefile(self, out):
        if ML_ENABLED:
            out.write('ml_example.byte: api/ml/z3ml.cma')
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
            out.write('\n')
            out.write('\tocamlfind %s ' % OCAMLC)
            if DEBUG_MODE:
                out.write('-g ')
            out.write('-custom -o ml_example.byte -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cma')
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
            out.write('\n')
            out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa')
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
            out.write('\n')
            out.write('\tocamlfind %s ' % OCAMLOPT)
            if DEBUG_MODE:
                out.write('-g ')
            out.write('-o ml_example$(EXE_EXT) -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cmxa')
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
            out.write('\n')
            out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)

        debug_opt = '-g ' if DEBUG_MODE else ''

        if STATIC_LIB:
            opam_z3_opts = '-thread -package z3-static -linkpkg'
            ml_post_install_tests = [
                (OCAMLC,              'ml_example_static.byte'),
                (OCAMLC + ' -custom', 'ml_example_static_custom.byte'),
                (OCAMLOPT,            'ml_example_static$(EXE_EXT)')
            ]
        else:
            opam_z3_opts = '-thread -package z3 -linkpkg'
            ml_post_install_tests = [
                (OCAMLC,              'ml_example_shared.byte'),
                (OCAMLC + ' -custom', 'ml_example_shared_custom.byte'),
                (OCAMLOPT,            'ml_example_shared$(EXE_EXT)')
            ]

        for ocaml_compiler, testname in ml_post_install_tests:
            out.write(testname + ':')
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
            out.write('\n')
            out.write('\tocamlfind %s -o %s %s %s ' % (ocaml_compiler, debug_opt, testname, opam_z3_opts))
            for mlfile in get_ml_files(self.ex_dir):
                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
            out.write('\n')

        if STATIC_LIB:
            out.write('_ex_ml_example_post_install: ml_example_static.byte ml_example_static_custom.byte ml_example_static$(EXE_EXT)\n')
        else:
            out.write('_ex_ml_example_post_install: ml_example_shared.byte ml_example_shared_custom.byte ml_example_shared$(EXE_EXT)\n')

        out.write('\n')


class PythonExampleComponent(ExampleComponent):
    def __init__(self, name, path):
        ExampleComponent.__init__(self, name, path)

    # Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked.
    # We don't need to include them in the :examples rule
    def mk_makefile(self, out):
        full = os.path.join(EXAMPLE_DIR, self.path)
        for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
            shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py))
            if is_verbose():
                print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python')))
        out.write('_ex_%s: \n\n' % self.name)

    def mk_win_dist(self, build_path, dist_path):
        full = os.path.join(EXAMPLE_DIR, self.path)
        py = 'example.py'
        shutil.copyfile(os.path.join(full, py),
                        os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))

    def mk_unix_dist(self, build_path, dist_path):
        self.mk_win_dist(build_path, dist_path)


def reg_component(name, c):
    global _Id, _Components, _ComponentNames, _Name2Component
    c.id = _Id
    _Id = _Id + 1
    _Components.append(c)
    _ComponentNames.add(name)
    _Name2Component[name] = c
    if VERBOSE:
        print("New component: '%s'" % name)

def add_lib(name, deps=[], path=None, includes2install=[]):
    c = LibComponent(name, path, deps, includes2install)
    reg_component(name, c)

def add_clib(name, deps=[], path=None, includes2install=[]):
    c = CLibComponent(name, path, deps, includes2install)
    reg_component(name, c)

def add_hlib(name, path=None, includes2install=[]):
    c = HLibComponent(name, path, includes2install)
    reg_component(name, c)

def add_exe(name, deps=[], path=None, exe_name=None, install=True):
    c = ExeComponent(name, exe_name, path, deps, install)
    reg_component(name, c)

def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
    c = ExtraExeComponent(name, exe_name, path, deps, install)
    reg_component(name, c)

def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None):
    c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link)
    reg_component(name, c)
    return c

def add_dot_net_core_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None):
    c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
    reg_component(name, c)

def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None):
    c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
    reg_component(name, c)

def add_python(libz3Component):
    name = 'python'
    reg_component(name, PythonComponent(name, libz3Component))

def add_js():
    reg_component('js', JsComponent())

def add_python_install(libz3Component):
    name = 'python_install'
    reg_component(name, PythonInstallComponent(name, libz3Component))

def add_ml_lib(name, deps=[], path=None, lib_name=None):
    c = MLComponent(name, lib_name, path, deps)
    reg_component(name, c)

def add_cpp_example(name, path=None):
    c = CppExampleComponent(name, path)
    reg_component(name, c)

def add_c_example(name, path=None):
    c = CExampleComponent(name, path)
    reg_component(name, c)

def add_dotnet_example(name, path=None):
    c = DotNetExampleComponent(name, path)
    reg_component(name, c)

def add_java_example(name, path=None):
    c = JavaExampleComponent(name, path)
    reg_component(name, c)

def add_ml_example(name, path=None):
    c = MLExampleComponent(name, path)
    reg_component(name, c)

def add_z3py_example(name, path=None):
    c = PythonExampleComponent(name, path)
    reg_component(name, c)

def mk_config():
    if ONLY_MAKEFILES:
        return
    config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
    global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64
    if IS_WINDOWS:
        CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++17'
        config.write(
            'CC=cl\n'
            'CXX=cl\n'
            'CXX_OUT_FLAG=/Fo\n'
            'C_OUT_FLAG=/Fo\n'
            'OBJ_EXT=.obj\n'
            'LIB_EXT=.lib\n'
            'AR=lib\n'
            'AR_OUTFLAG=/OUT:\n'
            'EXE_EXT=.exe\n'
            'LINK=cl\n'
            'LINK_OUT_FLAG=/Fe\n'
            'SO_EXT=.dll\n'
            'SLINK=cl\n'
            'SLINK_OUT_FLAG=/Fe\n'
            'OS_DEFINES=/D _WINDOWS\n')
        extra_opt = ''
        link_extra_opt = ''
        if LOG_SYNC:
            extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt
        if SINGLE_THREADED:
            extra_opt = '%s /DSINGLE_THREAD' % extra_opt
        if GIT_HASH:
            extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
        if GUARD_CF:
            extra_opt = ' %s /guard:cf' % extra_opt
            link_extra_opt = ' %s /GUARD:CF' % link_extra_opt
        if STATIC_BIN:
            static_opt = '/MT'
        else:
            static_opt = '/MD'
        maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO'
        if DEBUG_MODE:
            static_opt = static_opt + 'd'
            config.write(
                'AR_FLAGS=/nologo\n'
                'LINK_FLAGS=/nologo %s\n'
                'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
            if VS_X64:
                config.write(
                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                config.write(
                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
            elif VS_ARM:
                print("ARM on VS is unsupported")
                exit(1)
            else:
                config.write(
                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                config.write(
                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
        else:
            # Windows Release mode
            LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
            GL = ' /GL' if SLOW_OPTIMIZE else ''
            config.write(
                'AR_FLAGS=/nologo %s\n'
                'LINK_FLAGS=/nologo %s\n'
                'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt))
            if TRACE:
                extra_opt = '%s /D _TRACE ' % extra_opt
            if VS_X64:
                config.write(
                    'CXXFLAGS=/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                config.write(
                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
            elif VS_ARM:
                print("ARM on VS is unsupported")
                exit(1)
            else:
                config.write(
                    'CXXFLAGS=/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                config.write(
                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))

        config.write('CFLAGS=$(CXXFLAGS)\n')

        # End of Windows VS config.mk
        if is_verbose():
            print('64-bit:         %s' % is64())
            if is_java_enabled():
                print('JNI Bindings:   %s' % JNI_HOME)
                print('Java Compiler:  %s' % JAVAC)
            if is_ml_enabled():
                print('OCaml Compiler: %s' % OCAMLC)
                print('OCaml Find tool: %s' % OCAMLFIND)
                print('OCaml Native:   %s' % OCAMLOPT)
                print('OCaml Library:  %s' % OCAML_LIB)
    else:
        OS_DEFINES = ""
        ARITH = "internal"
        check_ar()
        CXX = find_cxx_compiler()
        CC  = find_c_compiler()
        SLIBEXTRAFLAGS = ''
#       SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
        EXE_EXT = ''
        LIB_EXT = '.a'
        if GPROF:
            CXXFLAGS = '%s -pg' % CXXFLAGS
            LDFLAGS  = '%s -pg' % LDFLAGS
        if GMP:
            test_gmp(CXX)
            ARITH = "gmp"
            CPPFLAGS = '%s -D_MP_GMP' % CPPFLAGS
            LDFLAGS  = '%s -lgmp' % LDFLAGS
            SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
        else:
            CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
        if GIT_HASH:
            CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
        CXXFLAGS = '%s -std=c++17' % CXXFLAGS
        CXXFLAGS = '%s -fvisibility=hidden -fvisibility-inlines-hidden -c' % CXXFLAGS
        FPMATH = test_fpmath(CXX)
        CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
        if LOG_SYNC:
            CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
        if SINGLE_THREADED:
            CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS
        if DEBUG_MODE:
            CXXFLAGS     = '%s -g -Wall' % CXXFLAGS
            EXAMP_DEBUG_FLAG = '-g'
            CPPFLAGS     = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
        else:
            CXXFLAGS     = '%s -O3' % CXXFLAGS
            if GPROF:
                CXXFLAGS     += '-fomit-frame-pointer'
            CPPFLAGS     = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
        if is_CXX_clangpp():
            CXXFLAGS   = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
        sysname, _, _, _, machine = os.uname()
        if sysname == 'Darwin':
            SO_EXT         = '.dylib'
            SLIBFLAGS      = '-dynamiclib'
        elif sysname == 'Linux':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
            SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
        elif sysname == 'GNU':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
        elif sysname == 'FreeBSD':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
            SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
        elif sysname == 'NetBSD':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
        elif sysname == 'OpenBSD':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
        elif sysname  == 'SunOS':
            SO_EXT         = '.so'
            SLIBFLAGS      = '-shared'
            SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
        elif sysname.startswith('CYGWIN'):
            SO_EXT         = '.dll'
            SLIBFLAGS      = '-shared'
        elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
            SO_EXT         = '.dll'
            SLIBFLAGS      = '-shared'
            EXE_EXT        = '.exe'
            LIB_EXT        = '.lib'
        else:
            raise MKException('Unsupported platform: %s' % sysname)
        if is64():
            if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
                CXXFLAGS     = '%s -fPIC' % CXXFLAGS
        elif not LINUX_X64:
            CXXFLAGS     = '%s -m32' % CXXFLAGS
            LDFLAGS      = '%s -m32' % LDFLAGS
            SLIBFLAGS    = '%s -m32' % SLIBFLAGS
        if TRACE or DEBUG_MODE:
            CPPFLAGS     = '%s -D_TRACE' % CPPFLAGS
        if is_cygwin_mingw() or is_msys2():
            # when cross-compiling with MinGW, we need to statically link its standard libraries
            # and to make it create an import library.
            SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS
            LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
        if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
            CXXFLAGS = '%s -fpic' % CXXFLAGS
        if IS_ARCH_ARM64 and IS_OSX:
            print("Setting arm64")
            CXXFLAGS = '%s -arch arm64' % CXXFLAGS
            LDFLAGS = '%s -arch arm64' % LDFLAGS
            SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS

        config.write('PREFIX=%s\n' % PREFIX)
        config.write('CC=%s\n' % CC)
        config.write('CXX=%s\n' % CXX)
        config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
        config.write('CFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS.replace('-std=c++17', '')))
        config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
        config.write('CXX_OUT_FLAG=-o \n')
        config.write('C_OUT_FLAG=-o \n')
        config.write('OBJ_EXT=.o\n')
        config.write('LIB_EXT=%s\n' % LIB_EXT)
        config.write('AR=%s\n' % AR)
        config.write('AR_FLAGS=rcs\n')
        config.write('AR_OUTFLAG=\n')
        config.write('EXE_EXT=%s\n' % EXE_EXT)
        config.write('LINK=%s\n' % CXX)
        config.write('LINK_FLAGS=\n')
        config.write('LINK_OUT_FLAG=-o \n')
        if is_linux() and (build_static_lib() or build_static_bin()):
            config.write('LINK_EXTRA_FLAGS=-Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive %s\n' % LDFLAGS)
        else:
            config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
        config.write('SO_EXT=%s\n' % SO_EXT)
        config.write('SLINK=%s\n' % CXX)
        config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
        config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
        config.write('SLINK_OUT_FLAG=-o \n')
        config.write('OS_DEFINES=%s\n' % OS_DEFINES)
        if is_verbose():
            print('Host platform:  %s' % sysname)
            print('C++ Compiler:   %s' % CXX)
            print('C Compiler  :   %s' % CC)
            if is_cygwin_mingw():
                print('MinGW32 cross:  %s' % (is_cygwin_mingw()))
            print('Archive Tool:   %s' % AR)
            print('Arithmetic:     %s' % ARITH)
            print('Prefix:         %s' % PREFIX)
            print('64-bit:         %s' % is64())
            print('FP math:        %s' % FPMATH)
            print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
            if GPROF:
                print('gprof:          enabled')
            print('Python version: %s' % sysconfig.get_python_version())
            if is_java_enabled():
                print('JNI Bindings:   %s' % JNI_HOME)
                print('Java Compiler:  %s' % JAVAC)
            if is_ml_enabled():
                print('OCaml Compiler: %s' % OCAMLC)
                print('OCaml Find tool: %s' % OCAMLFIND)
                print('OCaml Native:   %s' % OCAMLOPT)
                print('OCaml Library:  %s' % OCAML_LIB)
            if is_dotnet_core_enabled():
                print('C# Compiler:    %s' % DOTNET)

    config.close()

def mk_install(out):
    out.write('install: ')
    for c in get_components():
        c.mk_install_deps(out)
        out.write(' ')
    out.write('\n')
    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
    for c in get_components():
        c.mk_install(out)
    out.write('\t@echo Z3 was successfully installed.\n')
    out.write('\n')

def mk_uninstall(out):
    out.write('uninstall:\n')
    for c in get_components():
        c.mk_uninstall(out)
    out.write('\t@echo Z3 was successfully uninstalled.\n')
    out.write('\n')

# Generate the Z3 makefile
def mk_makefile():
    mk_dir(BUILD_DIR)
    mk_config()
    if VERBOSE:
        print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile'))
    out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w')
    out.write('# Automatically generated file.\n')
    out.write('include config.mk\n')
    # Generate :all rule
    out.write('all:')
    for c in get_components():
        if c.main_component():
            out.write(' %s' % c.name)
    out.write('\n\t@echo Z3 was successfully built.\n')
    out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python'))
    pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable and the \'%s\' directory is added to the %s environment variable.\"\n" % (os.path.join(BUILD_DIR, 'python'), BUILD_DIR, pathvar))
    if not IS_WINDOWS:
        out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
        out.write('\t@echo "    sudo make install"\n\n')
        # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
        # out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
    # Generate :examples rule
    out.write('examples:')
    for c in get_components():
        if c.is_example():
            out.write(' _ex_%s' % c.name)
    out.write('\n\t@echo Z3 examples were successfully built.\n')
    # Generate components
    for c in get_components():
        c.mk_makefile(out)
    # Generate install/uninstall rules if not WINDOWS
    if not IS_WINDOWS:
        mk_install(out)
        mk_uninstall(out)
    for c in get_components():
        c.final_info()
    out.close()
    # Finalize
    if VERBOSE:
        print("Makefile was successfully generated.")
        if DEBUG_MODE:
            print("  compilation mode: Debug")
        else:
            print("  compilation mode: Release")
        if IS_WINDOWS:
            if VS_X64:
                print("  platform: x64\n")
                print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
            elif VS_ARM:
                print("  platform: ARM\n")
                print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
            else:
                print("  platform: x86")
                print("To build Z3, open a [Visual Studio Command Prompt], then")
            print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR))
            print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
        else:
            print("Type 'cd %s; make' to build Z3" % BUILD_DIR)

# Generate automatically generated source code
def mk_auto_src():
    if not ONLY_MAKEFILES:
        exec_pyg_scripts()
        mk_pat_db()
        mk_all_install_tactic_cpps()
        mk_all_mem_initializer_cpps()
        mk_all_gparams_register_modules()


def _execfile(file, globals=globals(), locals=locals()):
    if sys.version < "2.7":
        execfile(file, globals, locals)
    else:
        with open(file, "r") as fh:
            exec(fh.read()+"\n", globals, locals)

# Execute python auxiliary scripts that generate extra code for Z3.
def exec_pyg_scripts():
    for root, dirs, files in os.walk('src'):
        for f in files:
            if f.endswith('.pyg'):
                script = os.path.join(root, f)
                generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root)
                if is_verbose():
                    print("Generated '{}'".format(generated_file))

# TODO: delete after src/ast/pattern/expr_pattern_match
# database.smt ==> database.h
def mk_pat_db():
    c = get_component(PATTERN_COMPONENT)
    fin  = os.path.join(c.src_dir, 'database.smt2')
    fout = os.path.join(c.src_dir, 'database.h')
    mk_genfile_common.mk_pat_db_internal(fin, fout)
    if VERBOSE:
        print("Generated '{}'".format(fout))

# Update version numbers
def update_version():
    major = VER_MAJOR
    minor = VER_MINOR
    build = VER_BUILD
    revision = VER_TWEAK

    print("UpdateVersion:", get_full_version_string(major, minor, build, revision))
    
    if major is None or minor is None or build is None or revision is None:
        raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
    if not ONLY_MAKEFILES:
        mk_version_dot_h(major, minor, build, revision)
        mk_all_assembly_infos(major, minor, build, revision)
        mk_def_files()

def get_full_version_string(major, minor, build, revision):
    global GIT_HASH, GIT_DESCRIBE
    res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
    if GIT_HASH:
        res += " " + GIT_HASH
    if GIT_DESCRIBE:
        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
        res += " " + branch + " " + check_output(['git', 'describe'])
    return '"' + res + '"'

# Update files with the version number
def mk_version_dot_h(major, minor, build, revision):
    c = get_component(UTIL_COMPONENT)
    version_template = os.path.join(c.src_dir, 'z3_version.h.in')
    version_header_output = os.path.join(c.src_dir, 'z3_version.h')
    # Note the substitution names are what is used by the CMake
    # builds system. If you change these you should change them
    # in the CMake build too
    configure_file(version_template, version_header_output,
        { 'Z3_VERSION_MAJOR': str(major),
          'Z3_VERSION_MINOR': str(minor),
          'Z3_VERSION_PATCH': str(build),
          'Z3_VERSION_TWEAK': str(revision),
          'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision)
        }
    )
    if VERBOSE:
        print("Generated '%s'" % version_header_output)

# Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template
def mk_all_assembly_infos(major, minor, build, revision):
    for c in get_components():
        if c.has_assembly_info():
            c.make_assembly_info(major, minor, build, revision)

def get_header_files_for_components(component_src_dirs):
    assert isinstance(component_src_dirs, list)
    h_files_full_path = []
    for component_src_dir in sorted(component_src_dirs):
        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
        h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
        h_files_full_path.extend(h_files)
    return h_files_full_path

def mk_install_tactic_cpp(cnames, path):
    component_src_dirs = []
    for cname in cnames:
        print("Component %s" % cname)
        c = get_component(cname)
        component_src_dirs.append(c.src_dir)
    h_files_full_path = get_header_files_for_components(component_src_dirs)
    generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(h_files_full_path, path)
    if VERBOSE:
        print("Generated '{}'".format(generated_file))

def mk_all_install_tactic_cpps():
    if not ONLY_MAKEFILES:
        for c in get_components():
            if c.require_install_tactics():
                cnames = []
                cnames.extend(c.deps)
                cnames.append(c.name)
                mk_install_tactic_cpp(cnames, c.src_dir)

def mk_mem_initializer_cpp(cnames, path):
    component_src_dirs = []
    for cname in cnames:
        c = get_component(cname)
        component_src_dirs.append(c.src_dir)
    h_files_full_path = get_header_files_for_components(component_src_dirs)
    generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path)
    if VERBOSE:
        print("Generated '{}'".format(generated_file))

def mk_all_mem_initializer_cpps():
    if not ONLY_MAKEFILES:
        for c in get_components():
            if c.require_mem_initializer():
                cnames = []
                cnames.extend(c.deps)
                cnames.append(c.name)
                mk_mem_initializer_cpp(cnames, c.src_dir)

def mk_gparams_register_modules(cnames, path):
    component_src_dirs = []
    for cname in cnames:
        c = get_component(cname)
        component_src_dirs.append(c.src_dir)
    h_files_full_path = get_header_files_for_components(component_src_dirs)
    generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path)
    if VERBOSE:
        print("Generated '{}'".format(generated_file))

def mk_all_gparams_register_modules():
    if not ONLY_MAKEFILES:
        for c in get_components():
            if c.require_mem_initializer():
                cnames = []
                cnames.extend(c.deps)
                cnames.append(c.name)
                mk_gparams_register_modules(cnames, c.src_dir)

# Generate a .def based on the files at c.export_files slot.
def mk_def_file(c):
    defname = '%s.def' % os.path.join(c.src_dir, c.name)
    dll_name = c.dll_name
    export_header_files = []
    for dot_h in c.export_files:
        dot_h_c = c.find_file(dot_h, c.name)
        api = os.path.join(dot_h_c.src_dir, dot_h)
        export_header_files.append(api)
    mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files)
    if VERBOSE:
        print("Generated '%s'" % defname)

def mk_def_files():
    if not ONLY_MAKEFILES:
        for c in get_components():
            if c.require_def_file():
                mk_def_file(c)

def cp_z3py_to_build():
    mk_dir(BUILD_DIR)
    mk_dir(os.path.join(BUILD_DIR, 'python'))
    z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3')
    z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3')

    # Erase existing .pyc files
    for root, dirs, files in os.walk(Z3PY_SRC_DIR):
        for f in files:
            if f.endswith('.pyc'):
                rmf(os.path.join(root, f))
    # We do not want a second copy of the compiled files in the system-wide cache,
    # so we disable it temporarily. This is an issue with recent versions of MacOS
    # where XCode's Python has a cache, but the build scripts don't have access to
    # it (e.g. during OPAM package installation).
    have_cache = hasattr(sys, 'pycache_prefix') and sys.pycache_prefix is not None
    if have_cache:
        pycache_prefix_before = sys.pycache_prefix
        sys.pycache_prefix = None
    # Compile Z3Py files
    if compileall.compile_dir(z3py_src, force=1) != 1:
        raise MKException("failed to compile Z3Py sources")
    if have_cache:
        sys.pycache_prefix = pycache_prefix_before
    if is_verbose:
        print("Generated python bytecode")
    # Copy sources to build
    mk_dir(z3py_dest)
    for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)):
        shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py))
        if is_verbose():
            print("Copied '%s'" % py)
    # Python 2.x support
    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)):
        shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc))
        if is_verbose():
            print("Copied '%s'" % pyc)
    # Python 3.x support
    src_pycache = os.path.join(z3py_src, '__pycache__')
    target_pycache = os.path.join(z3py_dest, '__pycache__')
    if os.path.exists(src_pycache):
        for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)):
            mk_dir(target_pycache)
            shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
            if is_verbose():
                print("Copied '%s'" % pyc)
    # Copy z3test.py
    shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py'))

def mk_bindings(api_files):
    if not ONLY_MAKEFILES:
        mk_z3consts_py(api_files)
        new_api_files = []
        api = get_component(API_COMPONENT)
        for api_file in api_files:
            api_file_path = api.find_file(api_file, api.name)
            new_api_files.append(os.path.join(api_file_path.src_dir, api_file))
        g = globals()
        g["API_FILES"] = new_api_files
        if is_java_enabled():
            check_java()
            mk_z3consts_java(api_files)
        # Generate some of the bindings and "api" module files
        import update_api
        dotnet_output_dir = None
        if is_dotnet_core_enabled():
          dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet')
          mk_dir(dotnet_output_dir)
        java_input_dir = None
        java_output_dir = None
        java_package_name = None
        if is_java_enabled():
          java_output_dir = get_component('java').src_dir
          java_input_dir = get_component('java').src_dir
          java_package_name = get_component('java').package_name
        ml_output_dir = None
        if is_ml_enabled():
          ml_output_dir = get_component('ml').src_dir
        # Get the update_api module to do the work for us
        update_api.VERBOSE = is_verbose()
        update_api.generate_files(api_files=new_api_files,
          api_output_dir=get_component('api').src_dir,
          z3py_output_dir=get_z3py_dir(),
          dotnet_output_dir=dotnet_output_dir,
          java_input_dir=java_input_dir,
          java_output_dir=java_output_dir,                                  
          java_package_name=java_package_name,
          ml_output_dir=ml_output_dir,
          ml_src_dir=ml_output_dir
        )
        cp_z3py_to_build()
        if is_ml_enabled():
            check_ml()
            mk_z3consts_ml(api_files)
        if  is_dotnet_core_enabled():
            check_dotnet_core()
            mk_z3consts_dotnet(api_files, dotnet_output_dir)

# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):
    if Z3PY_SRC_DIR is None:
        raise MKException("You must invoke set_z3py_dir(path):")
    full_path_api_files = []
    api_dll = get_component(Z3_DLL_COMPONENT)
    for api_file in api_files:
        api_file_c = api_dll.find_file(api_file, api_dll.name)
        api_file   = os.path.join(api_file_c.src_dir, api_file)
        full_path_api_files.append(api_file)
    generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
    if VERBOSE:
        print("Generated '{}".format(generated_file))

# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files, output_dir):
    dotnet = get_component(DOTNET_COMPONENT)
    if not dotnet:
       dotnet = get_component(DOTNET_CORE_COMPONENT)
    full_path_api_files = []
    for api_file in api_files:
        api_file_c = dotnet.find_file(api_file, dotnet.name)
        api_file   = os.path.join(api_file_c.src_dir, api_file)
        full_path_api_files.append(api_file)
    generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir)
    if VERBOSE:
        print("Generated '{}".format(generated_file))

# Extract enumeration types from z3_api.h, and add Java definitions
def mk_z3consts_java(api_files):
    java = get_component(JAVA_COMPONENT)
    full_path_api_files = []
    for api_file in api_files:
        api_file_c = java.find_file(api_file, java.name)
        api_file   = os.path.join(api_file_c.src_dir, api_file)
        full_path_api_files.append(api_file)
    generated_files = mk_genfile_common.mk_z3consts_java_internal(
        full_path_api_files,
        java.package_name,
        java.src_dir)
    if VERBOSE:
        for generated_file in generated_files:
            print("Generated '{}'".format(generated_file))

# Extract enumeration types from z3_api.h, and add ML definitions
def mk_z3consts_ml(api_files):
    ml = get_component(ML_COMPONENT)
    full_path_api_files = []
    for api_file in api_files:
        api_file_c = ml.find_file(api_file, ml.name)
        api_file   = os.path.join(api_file_c.src_dir, api_file)
        full_path_api_files.append(api_file)
    generated_file = mk_genfile_common.mk_z3consts_ml_internal(
        full_path_api_files,
        ml.src_dir)
    if VERBOSE:
        print ('Generated "%s"' % generated_file)

def mk_gui_str(id):
    return '4D2F40D8-E5F9-473B-B548-%012d' % id

def get_platform_toolset_str():
    default = 'v110';
    vstr = check_output(['msbuild', '/ver'])
    lines = vstr.split('\n')
    lline = lines[-1]
    tokens = lline.split('.')
    if len(tokens) < 2:
        return default
    else:
        if tokens[0] == "15":
            # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
            return "v141"
        else:
            return 'v' + tokens[0] + tokens[1]

def mk_vs_proj_property_groups(f, name, target_ext, type):
    f.write('  <ItemGroup Label="ProjectConfigurations">\n')
    f.write('    <ProjectConfiguration Include="Debug|Win32">\n')
    f.write('      <Configuration>Debug</Configuration>\n')
    f.write('      <Platform>Win32</Platform>\n')
    f.write('    </ProjectConfiguration>\n')
    f.write('    <ProjectConfiguration Include="Release|Win32">\n')
    f.write('      <Configuration>Release</Configuration>\n')
    f.write('      <Platform>Win32</Platform>\n')
    f.write('    </ProjectConfiguration>\n')
    f.write('  </ItemGroup>\n')
    f.write('  <PropertyGroup Label="Globals">\n')
    f.write('    <ProjectGuid>{%s}</ProjectGuid>\n' % mk_gui_str(0))
    f.write('    <ProjectName>%s</ProjectName>\n' % name)
    f.write('    <Keyword>Win32Proj</Keyword>\n')
    f.write('    <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
    f.write('  </PropertyGroup>\n')
    f.write('  <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.Default.props" />\n')
    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
    f.write('    <UseOfMfc>false</UseOfMfc>\n')
    f.write('  </PropertyGroup>\n')
    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n')
    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
    f.write('    <UseOfMfc>false</UseOfMfc>\n')
    f.write('  </PropertyGroup>\n')
    f.write('  <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.props" />\n')
    f.write('  <ImportGroup Label="ExtensionSettings" />\n')
    f.write('   <ImportGroup Label="PropertySheets">\n')
    f.write('    <Import Project="$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
    f.write('  <PropertyGroup Label="UserMacros" />\n')
    f.write('  <PropertyGroup>\n')
    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
    f.write('  </PropertyGroup>\n')
    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
    f.write('        <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
    f.write('  </PropertyGroup>\n')
    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
    f.write('    <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
    f.write('  </PropertyGroup>\n')


def mk_vs_proj_cl_compile(f, name, components, debug):
    f.write('    <ClCompile>\n')
    f.write('      <Optimization>Disabled</Optimization>\n')
    if debug:
        f.write('      <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
    else:
        f.write('      <PreprocessorDefinitions>WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
    if VS_PAR:
        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
    else:
        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
    f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
    f.write('      <WarningLevel>Level3</WarningLevel>\n')
    if debug:
        f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
    else:
        f.write('      <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')
    f.write('      <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
    f.write('      <AdditionalIncludeDirectories>')
    deps = find_all_deps(name, components)
    first = True
    for dep in deps:
        if first:
            first = False
        else:
            f.write(';')
        f.write(get_component(dep).to_src_dir)
    f.write(';%s\n' % os.path.join(REV_BUILD_DIR, SRC_DIR))
    f.write('</AdditionalIncludeDirectories>\n')
    f.write('    </ClCompile>\n')

def mk_vs_proj_dep_groups(f, name, components):
    f.write('  <ItemGroup>\n')
    deps = find_all_deps(name, components)
    for dep in deps:
        dep = get_component(dep)
        for cpp in filter(lambda f: f.endswith('.cpp'), os.listdir(dep.src_dir)):
            f.write('    <ClCompile Include="%s" />\n' % os.path.join(dep.to_src_dir, cpp))
    f.write('  </ItemGroup>\n')

def mk_vs_proj_link_exe(f, name, debug):
    f.write('    <Link>\n')
    f.write('      <OutputFile>$(OutDir)%s.exe</OutputFile>\n' % name)
    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
    f.write('      <SubSystem>Console</SubSystem>\n')
    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
    f.write('      <DataExecutionPrevention/>\n')
    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
    f.write('      <AdditionalDependencies>psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)</AdditionalDependencies>\n')
    f.write('    </Link>\n')

def mk_vs_proj(name, components):
    if not VS_PROJ:
        return
    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
    modes=['Debug', 'Release']
    PLATFORMS=['Win32']
    f = open(proj_name, 'w')
    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
    mk_vs_proj_property_groups(f, name, 'exe', 'Application')
    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
    mk_vs_proj_cl_compile(f, name, components, debug=True)
    mk_vs_proj_link_exe(f, name, debug=True)
    f.write('  </ItemDefinitionGroup>\n')
    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
    mk_vs_proj_cl_compile(f, name, components, debug=False)
    mk_vs_proj_link_exe(f, name, debug=False)
    f.write('  </ItemDefinitionGroup>\n')
    mk_vs_proj_dep_groups(f, name, components)
    f.write('  <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
    f.write('  <ImportGroup Label="ExtensionTargets">\n')
    f.write('  </ImportGroup>\n')
    f.write('</Project>\n')
    f.close()
    if is_verbose():
        print("Generated '%s'" % proj_name)

def mk_vs_proj_link_dll(f, name, debug):
    f.write('    <Link>\n')
    f.write('      <OutputFile>$(OutDir)%s.dll</OutputFile>\n' % name)
    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
    f.write('      <SubSystem>Console</SubSystem>\n')
    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
    f.write('      <DataExecutionPrevention/>\n')
    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
    f.write('      <AdditionalDependencies>psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)</AdditionalDependencies>\n')
    f.write('      <ModuleDefinitionFile>%s</ModuleDefinitionFile>' % os.path.join(get_component('api_dll').to_src_dir, 'api_dll.def'))
    f.write('    </Link>\n')

def mk_vs_proj_dll(name, components):
    if not VS_PROJ:
        return
    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
    modes=['Debug', 'Release']
    PLATFORMS=['Win32']
    f = open(proj_name, 'w')
    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
    mk_vs_proj_property_groups(f, name, 'dll', 'DynamicLibrary')
    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
    mk_vs_proj_cl_compile(f, name, components, debug=True)
    mk_vs_proj_link_dll(f, name, debug=True)
    f.write('  </ItemDefinitionGroup>\n')
    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
    mk_vs_proj_cl_compile(f, name, components, debug=False)
    mk_vs_proj_link_dll(f, name, debug=False)
    f.write('  </ItemDefinitionGroup>\n')
    mk_vs_proj_dep_groups(f, name, components)
    f.write('  <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
    f.write('  <ImportGroup Label="ExtensionTargets">\n')
    f.write('  </ImportGroup>\n')
    f.write('</Project>\n')
    f.close()
    if is_verbose():
        print("Generated '%s'" % proj_name)

def mk_win_dist(build_path, dist_path):
    for c in get_components():
        c.mk_win_dist(build_path, dist_path)

def mk_unix_dist(build_path, dist_path):
    for c in get_components():
        c.mk_unix_dist(build_path, dist_path)
    # Add Z3Py to bin directory
    for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
        shutil.copy(os.path.join(build_path, pyc),
                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))

class MakeRuleCmd(object):
    """
        These class methods provide a convenient way to emit frequently
        needed commands used in Makefile rules
        Note that several of the method are meant for use during ``make
        install`` and ``make uninstall``.  These methods correctly use
        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable
        to writing commands manually which can be error prone.
    """
    @classmethod
    def install_root(cls):
        """
            Returns a string that will expand to the
            install location when used in a makefile rule.
        """
        # Note: DESTDIR is to support staged installs
        return "$(DESTDIR)$(PREFIX)/"

    @classmethod
    def _is_str(cls, obj):
        if sys.version_info.major > 2:
            # Python 3 or newer. Strings are always unicode and of type str
            return isinstance(obj, str)
        else:
            # Python 2. Has byte-string and unicode representation, allow both
            return isinstance(obj, str) or isinstance(obj, unicode)

    @classmethod
    def _install_root(cls, path, in_prefix, out, is_install=True):
        if not in_prefix:
            # The Python bindings on OSX are sometimes not installed inside the prefix.
            install_root = "$(DESTDIR)"
            action_string = 'install' if is_install else 'uninstall'
            cls.write_cmd(out, 'echo "WARNING: {}ing files/directories ({}) that are not in the install prefix ($(PREFIX))."'.format(
                    action_string, path))
            #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
            #        action_string, 'to' if is_install else 'from', path, PREFIX))
        else:
            # assert not os.path.isabs(path)
            install_root = cls.install_root()
        return install_root

    @classmethod
    def install_files(cls, out, src_pattern, dest, in_prefix=True):
        assert len(dest) > 0
        assert cls._is_str(src_pattern)
        assert not ' ' in src_pattern
        assert cls._is_str(dest)
        assert not ' ' in dest
        assert not os.path.isabs(src_pattern)
        install_root = cls._install_root(dest, in_prefix, out)

        cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
            src_pattern=src_pattern,
            install_root=install_root,
            dest=dest))

    @classmethod
    def remove_installed_files(cls, out, pattern, in_prefix=True):
        assert len(pattern) > 0
        assert cls._is_str(pattern)
        assert not ' ' in pattern
        install_root = cls._install_root(pattern, in_prefix, out, is_install=False)

        cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
            install_root=install_root,
            pattern=pattern))

    @classmethod
    def make_install_directory(cls, out, dir, in_prefix=True):
        assert len(dir) > 0
        assert cls._is_str(dir)
        assert not ' ' in dir
        install_root = cls._install_root(dir, in_prefix, out)

        if is_windows():
            cls.write_cmd(out, "IF NOT EXIST {dir} (mkdir {dir})".format(
                install_root=install_root,
                dir=dir))
        else:
            cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
                install_root=install_root,
                dir=dir))

    @classmethod
    def _is_path_prefix_of(cls, temp_path, target_as_abs):
        """
            Returns True iff ``temp_path`` is a path prefix
            of ``target_as_abs``
        """
        assert cls._is_str(temp_path)
        assert cls._is_str(target_as_abs)
        assert len(temp_path) > 0
        assert len(target_as_abs) > 0
        assert os.path.isabs(temp_path)
        assert os.path.isabs(target_as_abs)

        # Need to stick extra slash in front otherwise we might think that
        # ``/lib`` is a prefix of ``/lib64``.  Of course if ``temp_path ==
        # '/'`` then we shouldn't else we would check if ``//`` (rather than
        # ``/``) is a prefix of ``/lib64``, which would fail.
        if len(temp_path) > 1:
            temp_path += os.sep
        return target_as_abs.startswith(temp_path)

    @classmethod
    def create_relative_symbolic_link(cls, out, target, link_name):
        assert cls._is_str(target)
        assert cls._is_str(link_name)
        assert len(target) > 0
        assert len(link_name) > 0
        assert not os.path.isabs(target)
        assert not os.path.isabs(link_name)

        # We can't test to see if link_name is a file or directory
        # because it may not exist yet. Instead follow the convention
        # that if there is a leading slash target is a directory otherwise
        # it's a file
        if link_name[-1] != '/':
            # link_name is a file
            temp_path = os.path.dirname(link_name)
        else:
            # link_name is a directory
            temp_path = link_name[:-1]
        temp_path = '/' + temp_path
        relative_path = ""
        targetAsAbs = '/' + target
        assert os.path.isabs(targetAsAbs)
        assert os.path.isabs(temp_path)
        # Keep walking up the directory tree until temp_path
        # is a prefix of targetAsAbs
        while not cls._is_path_prefix_of(temp_path, targetAsAbs):
            assert temp_path != '/'
            temp_path = os.path.dirname(temp_path)
            relative_path += '../'

        # Now get the path from the common prefix directory to the target
        target_from_prefix = targetAsAbs[len(temp_path):]
        relative_path += target_from_prefix
        # Remove any double slashes
        relative_path = relative_path.replace('//','/')
        cls.create_symbolic_link(out, relative_path, link_name)

    @classmethod
    def create_symbolic_link(cls, out, target, link_name):
        assert cls._is_str(target)
        assert cls._is_str(link_name)
        assert not os.path.isabs(target)

        cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
            target=target,
            install_root=cls.install_root(),
            link_name=link_name))

    # TODO: Refactor all of the build system to emit commands using this
    # helper to simplify code. This will also let us replace ``@`` with
    # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
    # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
    # would be very helpful for debugging.
    @classmethod
    def write_cmd(cls, out, line):
        out.write("\t@{}\n".format(line))

def strip_path_prefix(path, prefix):
    if path.startswith(prefix):
        stripped_path = path[len(prefix):]
        stripped_path.replace('//','/')
        if stripped_path[0] == '/':
            stripped_path = stripped_path[1:]
        assert not os.path.isabs(stripped_path)
        return stripped_path
    else:
        return path

def configure_file(template_file_path, output_file_path, substitutions):
    """
        Read a template file ``template_file_path``, perform substitutions
        found in the ``substitutions`` dictionary and write the result to
        the output file ``output_file_path``.
        The template file should contain zero or more template strings of the
        form ``@NAME@``.
        The substitutions dictionary maps old strings (without the ``@``
        symbols) to their replacements.
    """
    assert isinstance(template_file_path, str)
    assert isinstance(output_file_path, str)
    assert isinstance(substitutions, dict)
    assert len(template_file_path) > 0
    assert len(output_file_path) > 0
    print("Generating {} from {}".format(output_file_path, template_file_path))

    if not os.path.exists(template_file_path):
        raise MKException('Could not find template file "{}"'.format(template_file_path))

    # Read whole template file into string
    template_string = None
    with open(template_file_path, 'r') as f:
        template_string = f.read()

    # Do replacements
    for (old_string, replacement) in substitutions.items():
        template_string = template_string.replace('@{}@'.format(old_string), replacement)

    # Write the string to the file
    with open(output_file_path, 'w') as f:
        f.write(template_string)

if __name__ == '__main__':
    import doctest
    doctest.testmod()