1############################################
2# Copyright (c) 2012 Microsoft Corporation
3#
4# Auxiliary scripts for generating Makefiles
5# and Visual Studio project files.
6#
7# Author: Leonardo de Moura (leonardo)
8############################################
9import io
10import sys
11import os
12import re
13import getopt
14import shutil
15from mk_exception import *
16import mk_genfile_common
17from fnmatch import fnmatch
18import distutils.sysconfig
19import compileall
20import subprocess
21
22def getenv(name, default):
23    try:
24        return os.environ[name].strip(' "\'')
25    except:
26        return default
27
28CXX=getenv("CXX", None)
29CC=getenv("CC", None)
30CPPFLAGS=getenv("CPPFLAGS", "")
31CXXFLAGS=getenv("CXXFLAGS", "")
32AR=getenv("AR", "ar")
33EXAMP_DEBUG_FLAG=''
34LDFLAGS=getenv("LDFLAGS", "")
35JNI_HOME=getenv("JNI_HOME", None)
36OCAMLC=getenv("OCAMLC", "ocamlc")
37OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
38OCAML_LIB=getenv("OCAML_LIB", None)
39OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
40DOTNET="dotnet"
41# Standard install directories relative to PREFIX
42INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
43INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
44INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
45INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig'))
46
47CXX_COMPILERS=['g++', 'clang++']
48C_COMPILERS=['gcc', 'clang']
49JAVAC=None
50JAR=None
51PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
52BUILD_DIR='build'
53REV_BUILD_DIR='..'
54SRC_DIR='src'
55EXAMPLE_DIR='examples'
56# Required Components
57Z3_DLL_COMPONENT='api_dll'
58PATTERN_COMPONENT='pattern'
59UTIL_COMPONENT='util'
60API_COMPONENT='api'
61DOTNET_COMPONENT='dotnet'
62DOTNET_CORE_COMPONENT='dotnet'
63JAVA_COMPONENT='java'
64ML_COMPONENT='ml'
65CPP_COMPONENT='cpp'
66PYTHON_COMPONENT='python'
67#####################
68IS_WINDOWS=False
69IS_LINUX=False
70IS_HURD=False
71IS_OSX=False
72IS_DRAGONFLY=False
73IS_NETBSD=False
74IS_OPENBSD=False
75IS_SUNOS=False
76IS_CYGWIN=False
77IS_CYGWIN_MINGW=False
78IS_MSYS2=False
79VERBOSE=True
80DEBUG_MODE=False
81SHOW_CPPS = True
82VS_X64 = False
83VS_ARM = False
84LINUX_X64 = True
85ONLY_MAKEFILES = False
86Z3PY_SRC_DIR=None
87Z3JS_SRC_DIR=None
88VS_PROJ = False
89TRACE = False
90PYTHON_ENABLED=False
91DOTNET_CORE_ENABLED=False
92DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
93JAVA_ENABLED=False
94ML_ENABLED=False
95JS_ENABLED=False
96PYTHON_INSTALL_ENABLED=False
97STATIC_LIB=False
98STATIC_BIN=False
99VER_MAJOR=None
100VER_MINOR=None
101VER_BUILD=None
102VER_TWEAK=None
103PREFIX=sys.prefix
104GMP=False
105VS_PAR=False
106VS_PAR_NUM=8
107GPROF=False
108GIT_HASH=False
109GIT_DESCRIBE=False
110SLOW_OPTIMIZE=False
111LOG_SYNC=False
112SINGLE_THREADED=False
113GUARD_CF=False
114ALWAYS_DYNAMIC_BASE=False
115
116FPMATH="Default"
117FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
118
119
120def check_output(cmd):
121    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
122    if out != None:
123        enc = sys.stdout.encoding
124        if enc != None: return out.decode(enc).rstrip('\r\n')
125        else: return out.rstrip('\r\n')
126    else:
127        return ""
128
129def git_hash():
130    try:
131        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
132        r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
133    except:
134        raise MKException("Failed to retrieve git hash")
135    ls = r.split(' ')
136    if len(ls) != 2:
137        raise MKException("Unexpected git output " + r)
138    return ls[0]
139
140def is_windows():
141    return IS_WINDOWS
142
143def is_linux():
144    return IS_LINUX
145
146def is_hurd():
147    return IS_HURD
148
149def is_dragonfly():
150    return IS_DRAGONFLY
151
152def is_netbsd():
153    return IS_NETBSD
154
155def is_openbsd():
156    return IS_OPENBSD
157
158def is_sunos():
159    return IS_SUNOS
160
161def is_osx():
162    return IS_OSX
163
164def is_cygwin():
165    return IS_CYGWIN
166
167def is_cygwin_mingw():
168    return IS_CYGWIN_MINGW
169
170def is_msys2():
171    return IS_MSYS2
172
173def norm_path(p):
174    return os.path.expanduser(os.path.normpath(p))
175
176def which(program):
177    import os
178    def is_exe(fpath):
179        return os.path.isfile(fpath) and os.access(fpath, os.X_OK)
180
181    fpath, fname = os.path.split(program)
182    if fpath:
183        if is_exe(program):
184            return program
185    else:
186        for path in getenv("PATH", "").split(os.pathsep):
187            exe_file = os.path.join(path, program)
188            if is_exe(exe_file):
189                return exe_file
190    return None
191
192class TempFile:
193    def __init__(self, name):
194        try:
195            self.name  = name
196            self.fname = open(name, 'w')
197        except:
198            raise MKException("Failed to create temporary file '%s'" % self.name)
199
200    def add(self, s):
201        self.fname.write(s)
202
203    def commit(self):
204        self.fname.close()
205
206    def __del__(self):
207        self.fname.close()
208        try:
209            os.remove(self.name)
210        except:
211            pass
212
213def exec_cmd(cmd):
214    if isinstance(cmd, str):
215        cmd = cmd.split(' ')
216    new_cmd = []
217    first = True
218    for e in cmd:
219        if first:
220            first = False
221            new_cmd.append(e)
222        else:
223            if e != "":
224                se = e.split(' ')
225                if len(se) > 1:
226                    for e2 in se:
227                        if e2 != "":
228                            new_cmd.append(e2)
229                else:
230                    new_cmd.append(e)
231    cmd = new_cmd
232    null = open(os.devnull, 'wb')
233    try:
234        return subprocess.call(cmd, stdout=null, stderr=null)
235    except:
236        # Failed to create process
237        return 1
238    finally:
239        null.close()
240
241# rm -f fname
242def rmf(fname):
243    if os.path.exists(fname):
244        os.remove(fname)
245
246def exec_compiler_cmd(cmd):
247    r = exec_cmd(cmd)
248    if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
249        rmf('a.exe')
250    else:
251        rmf('a.out')
252    return r
253
254def test_cxx_compiler(cc):
255    if is_verbose():
256        print("Testing %s..." % cc)
257    t = TempFile('tst.cpp')
258    t.add('#include<iostream>\nint main() { return 0; }\n')
259    t.commit()
260    return exec_compiler_cmd([cc, CPPFLAGS, CXXFLAGS, 'tst.cpp', LDFLAGS]) == 0
261
262def test_c_compiler(cc):
263    if is_verbose():
264        print("Testing %s..." % cc)
265    t = TempFile('tst.c')
266    t.add('#include<stdio.h>\nint main() { return 0; }\n')
267    t.commit()
268    return exec_compiler_cmd([cc, CPPFLAGS, 'tst.c', LDFLAGS]) == 0
269
270def test_gmp(cc):
271    if is_verbose():
272        print("Testing GMP...")
273    t = TempFile('tstgmp.cpp')
274    t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
275    t.commit()
276    return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
277
278
279
280def test_fpmath(cc):
281    global FPMATH_FLAGS
282    if is_verbose():
283        print("Testing floating point support...")
284    t = TempFile('tstsse.cpp')
285    t.add('int main() { return 42; }\n')
286    t.commit()
287    # -Werror is needed because some versions of clang warn about unrecognized
288    # -m flags.
289    if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
290        FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
291        return "SSE2-GCC"
292    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
293        FPMATH_FLAGS="-msse -msse2"
294        return "SSE2-CLANG"
295    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
296        FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
297        return "ARM-VFP"
298    else:
299        FPMATH_FLAGS=""
300        return "UNKNOWN"
301
302
303def find_jni_h(path):
304    for root, dirs, files in os.walk(path):
305        for f in files:
306            if f == 'jni.h':
307                return root
308    return False
309
310def check_java():
311    global JNI_HOME
312    global JAVAC
313    global JAR
314
315    JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.
316
317    if is_verbose():
318        print("Finding javac ...")
319
320    if JDK_HOME is not None:
321        if IS_WINDOWS:
322            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe')
323        else:
324            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac')
325
326        if not os.path.exists(JAVAC):
327            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))
328    else:
329        # Search for javac in the path.
330        ind = 'javac'
331        if IS_WINDOWS:
332            ind = ind + '.exe'
333        paths = os.getenv('PATH', None)
334        if paths:
335            spaths = paths.split(os.pathsep)
336            for i in range(0, len(spaths)):
337                cmb = os.path.join(spaths[i], ind)
338                if os.path.exists(cmb):
339                    JAVAC = cmb
340                    break
341
342    if JAVAC is None:
343        raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.')
344
345    if is_verbose():
346        print("Finding jar ...")
347
348    if IS_WINDOWS:
349        JAR = os.path.join(os.path.dirname(JAVAC), 'jar.exe')
350    else:
351        JAR = os.path.join(os.path.dirname(JAVAC), 'jar')
352
353    if not os.path.exists(JAR):
354        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))
355
356    if is_verbose():
357        print("Testing %s..." % JAVAC)
358
359    t = TempFile('Hello.java')
360    t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
361    t.commit()
362
363    oo = TempFile('output')
364    eo = TempFile('errout')
365    try:
366        subprocess.call([JAVAC, 'Hello.java', '-verbose', '-source', '1.8', '-target', '1.8' ], stdout=oo.fname, stderr=eo.fname)
367        oo.commit()
368        eo.commit()
369    except:
370        raise MKException('Found, but failed to run Java compiler at %s' % (JAVAC))
371
372    os.remove('Hello.class')
373
374    if is_verbose():
375        print("Finding jni.h...")
376
377    if JNI_HOME is not None:
378        if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
379            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))
380    else:
381        # Search for jni.h in the library directories...
382        t = open('errout', 'r')
383        open_pat = re.compile("\[search path for class files: (.*)\]")
384        cdirs = []
385        for line in t:
386            m = open_pat.match(line)
387            if m:
388                libdirs = m.group(1).split(',')
389                for libdir in libdirs:
390                    q = os.path.dirname(libdir)
391                    if cdirs.count(q) == 0 and len(q) > 0:
392                        cdirs.append(q)
393        t.close()
394
395        # ... plus some heuristic ones.
396        extra_dirs = []
397
398        # For the libraries, even the JDK usually uses a JRE that comes with it. To find the
399        # headers we have to go a little bit higher up.
400        for dir in cdirs:
401            extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))
402
403        if IS_OSX: # Apparently Apple knows best where to put stuff...
404            extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')
405
406        cdirs[len(cdirs):] = extra_dirs
407
408        for dir in cdirs:
409            q = find_jni_h(dir)
410            if q is not False:
411                JNI_HOME = q
412
413        if JNI_HOME is None:
414            raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
415
416def test_csc_compiler(c):
417    t = TempFile('hello.cs')
418    t.add('public class hello { public static void Main() {} }')
419    t.commit()
420    if is_verbose():
421        print ('Testing %s...' % c)
422    r = exec_cmd([c, 'hello.cs'])
423    try:
424        rmf('hello.cs')
425        rmf('hello.exe')
426    except:
427        pass
428    return r == 0
429
430def check_dotnet_core():
431    if not IS_WINDOWS:
432        return
433    r = exec_cmd([DOTNET, '--help'])
434    if r != 0:
435        raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities')
436
437def check_ml():
438    t = TempFile('hello.ml')
439    t.add('print_string "Hello world!\n";;')
440    t.commit()
441    if is_verbose():
442        print ('Testing %s...' % OCAMLC)
443    r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
444    if r != 0:
445        raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
446    if is_verbose():
447        print ('Testing %s...' % OCAMLOPT)
448    r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
449    if r != 0:
450        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.')
451    try:
452        rmf('hello.cmi')
453        rmf('hello.cmo')
454        rmf('hello.cmx')
455        rmf('a.out')
456        rmf('hello.o')
457    except:
458        pass
459    find_ml_lib()
460    find_ocaml_find()
461
462def find_ocaml_find():
463    global OCAMLFIND
464    if is_verbose():
465        print ("Testing %s..." % OCAMLFIND)
466    r = exec_cmd([OCAMLFIND, 'printconf'])
467    if r != 0:
468        OCAMLFIND = ''
469
470def find_ml_lib():
471    global OCAML_LIB
472    if is_verbose():
473        print ('Finding OCAML_LIB...')
474    t = TempFile('output')
475    null = open(os.devnull, 'wb')
476    try:
477        subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
478        t.commit()
479    except:
480        raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
481    finally:
482        null.close()
483
484    t = open('output', 'r')
485    for line in t:
486        OCAML_LIB = line[:-1]
487    if is_verbose():
488        print ('OCAML_LIB=%s' % OCAML_LIB)
489    t.close()
490    rmf('output')
491    return
492
493def is64():
494    global LINUX_X64
495    if is_sunos() and sys.version_info.major < 3:
496        return LINUX_X64
497    else:
498        return LINUX_X64 and sys.maxsize >= 2**32
499
500def check_ar():
501    if is_verbose():
502        print("Testing ar...")
503    if which(AR) is None:
504        raise MKException('%s (archive tool) was not found' % AR)
505
506def find_cxx_compiler():
507    global CXX, CXX_COMPILERS
508    if CXX is not None:
509        if test_cxx_compiler(CXX):
510            return CXX
511    for cxx in CXX_COMPILERS:
512        if test_cxx_compiler(cxx):
513            CXX = cxx
514            return CXX
515    raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
516
517def find_c_compiler():
518    global CC, C_COMPILERS
519    if CC is not None:
520        if test_c_compiler(CC):
521            return CC
522    for c in C_COMPILERS:
523        if test_c_compiler(c):
524            CC = c
525            return CC
526    raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
527
528def set_version(major, minor, build, revision):
529    global VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK, GIT_DESCRIBE
530    VER_MAJOR = major
531    VER_MINOR = minor
532    VER_BUILD = build
533    VER_TWEAK = revision
534    if GIT_DESCRIBE:
535        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
536        VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
537
538def get_version():
539    return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
540
541def get_version_string(n):
542    if n == 3:
543        return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD)
544    return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_TWEAK)
545
546def build_static_lib():
547    return STATIC_LIB
548
549def build_static_bin():
550    return STATIC_BIN
551
552def is_cr_lf(fname):
553    # Check whether text files use cr/lf
554    f = open(fname, 'r')
555    line = f.readline()
556    f.close()
557    sz = len(line)
558    return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n'
559
560# dos2unix in python
561#    cr/lf --> lf
562def dos2unix(fname):
563    if is_cr_lf(fname):
564        fin  = open(fname, 'r')
565        fname_new = '%s.new' % fname
566        fout = open(fname_new, 'w')
567        for line in fin:
568            line = line.rstrip('\r\n')
569            fout.write(line)
570            fout.write('\n')
571        fin.close()
572        fout.close()
573        shutil.move(fname_new, fname)
574        if is_verbose():
575            print("dos2unix '%s'" % fname)
576
577def dos2unix_tree():
578    for root, dirs, files in os.walk('src'):
579        for f in files:
580            dos2unix(os.path.join(root, f))
581
582
583def check_eol():
584    if not IS_WINDOWS:
585        # Linux/OSX/BSD check if the end-of-line is cr/lf
586        if is_cr_lf('LICENSE.txt'):
587            if is_verbose():
588                print("Fixing end of line...")
589            dos2unix_tree()
590
591if os.name == 'nt':
592    IS_WINDOWS=True
593    # Visual Studio already displays the files being compiled
594    SHOW_CPPS=False
595elif os.name == 'posix':
596    if os.uname()[0] == 'Darwin':
597        IS_OSX=True
598    elif os.uname()[0] == 'Linux':
599        IS_LINUX=True
600    elif os.uname()[0] == 'GNU':
601        IS_HURD=True
602    elif os.uname()[0] == 'DragonFly':
603        IS_DRAGONFLY=True
604    elif os.uname()[0] == 'NetBSD':
605        IS_NETBSD=True
606    elif os.uname()[0] == 'OpenBSD':
607        IS_OPENBSD=True
608    elif os.uname()[0] == 'SunOS':
609        IS_SUNOS=True
610    elif os.uname()[0][:6] == 'CYGWIN':
611        IS_CYGWIN=True
612        if (CC != None and "mingw" in CC):
613            IS_CYGWIN_MINGW=True
614    elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
615        IS_MSYS2=True
616        if os.uname()[4] == 'x86_64':
617            LINUX_X64=True
618        else:
619            LINUX_X64=False
620
621
622def display_help(exit_code):
623    print("mk_make.py: Z3 Makefile generator\n")
624    print("This script generates the Makefile for the Z3 theorem prover.")
625    print("It must be executed from the Z3 root directory.")
626    print("\nOptions:")
627    print("  -h, --help                    display this message.")
628    print("  -s, --silent                  do not print verbose messages.")
629    if not IS_WINDOWS:
630        print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
631    else:
632        print("  --parallel=num                use cl option /MP with 'num' parallel processes")
633    print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
634    print("  -b <subdir>, --build=<subdir>  subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
635    print("  --githash=hash                include the given hash in the binaries.")
636    print("  --git-describe                include the output of 'git describe' in the version information.")
637    print("  -d, --debug                   compile Z3 in debug mode.")
638    print("  -t, --trace                   enable tracing in release mode.")
639    if IS_WINDOWS:
640        print("  --guardcf                     enable Control Flow Guard runtime checks.")
641        print("  -x, --x64                     create 64 binary when using Visual Studio.")
642    else:
643        print("  --x86                         force 32-bit x86 build on x64 systems.")
644    print("  -m, --makefiles               generate only makefiles.")
645    if IS_WINDOWS:
646        print("  -v, --vsproj                  generate Visual Studio Project Files.")
647        print("  --optimize                    generate optimized code during linking.")
648    print("  --dotnet                      generate .NET platform bindings.")
649    print("  --dotnet-key=<file>           sign the .NET assembly using the private key in <file>.")
650    print("  --java                        generate Java bindings.")
651    print("  --ml                          generate OCaml bindings.")
652    print("  --js                          generate JScript bindings.")
653    print("  --python                      generate Python bindings.")
654    print("  --staticlib                   build Z3 static library.")
655    print("  --staticbin                   build a statically linked Z3 binary.")
656    if not IS_WINDOWS:
657        print("  -g, --gmp                     use GMP.")
658        print("  --gprof                       enable gprof")
659    print("  --log-sync                    synchronize access to API log files to enable multi-thread API logging.")
660    print("  --single-threaded             non-thread-safe build")
661    print("")
662    print("Some influential environment variables:")
663    if not IS_WINDOWS:
664        print("  CXX        C++ compiler")
665        print("  CC         C compiler")
666        print("  LDFLAGS    Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
667        print("  CPPFLAGS   Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
668        print("  CXXFLAGS   C++ compiler flags")
669    print("  JDK_HOME   JDK installation directory (only relevant if -j or --java option is provided)")
670    print("  JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)")
671    print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
672    print("  OCAMLFIND  Ocaml find tool (only relevant with --ml)")
673    print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
674    print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
675    print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
676    print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
677    print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
678    print("  Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
679    exit(exit_code)
680
681# Parse configuration option for mk_make script
682def parse_options():
683    global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
684    global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
685    global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
686    global GUARD_CF, ALWAYS_DYNAMIC_BASE
687    try:
688        options, remainder = getopt.gnu_getopt(sys.argv[1:],
689                                               'b:df:sxhmcvtnp:gj',
690                                               ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
691                                                'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
692                                                'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
693    except:
694        print("ERROR: Invalid command line option")
695        display_help(1)
696
697    for opt, arg in options:
698        print('opt = %s, arg = %s' % (opt, arg))
699        if opt in ('-b', '--build'):
700            if arg == 'src':
701                raise MKException('The src directory should not be used to host the Makefile')
702            set_build_dir(arg)
703        elif opt in ('-s', '--silent'):
704            VERBOSE = False
705        elif opt in ('-d', '--debug'):
706            DEBUG_MODE = True
707        elif opt in ('-x', '--x64'):
708            if not IS_WINDOWS:
709                raise MKException('x64 compilation mode can only be specified when using Visual Studio')
710            VS_X64 = True
711        elif opt in ('--x86'):
712            LINUX_X64=False
713        elif opt in ('-h', '--help'):
714            display_help(0)
715        elif opt in ('-m', '--makefiles'):
716            ONLY_MAKEFILES = True
717        elif opt in ('-c', '--showcpp'):
718            SHOW_CPPS = True
719        elif opt in ('-v', '--vsproj'):
720            VS_PROJ = True
721        elif opt in ('-t', '--trace'):
722            TRACE = True
723        elif opt in ('--dotnet',):
724            DOTNET_CORE_ENABLED = True
725        elif opt in ('--dotnet-key'):
726            DOTNET_KEY_FILE = arg
727        elif opt in ('--staticlib'):
728            STATIC_LIB = True
729        elif opt in ('--staticbin'):
730            STATIC_BIN = True
731        elif opt in ('--optimize'):
732            SLOW_OPTIMIZE = True
733        elif not IS_WINDOWS and opt in ('-p', '--prefix'):
734            PREFIX = arg
735        elif opt in ('--pypkgdir'):
736            PYTHON_PACKAGE_DIR = arg
737        elif IS_WINDOWS and opt == '--parallel':
738            VS_PAR = True
739            VS_PAR_NUM = int(arg)
740        elif opt in ('-g', '--gmp'):
741            GMP = True
742        elif opt in ('-j', '--java'):
743            JAVA_ENABLED = True
744        elif opt == '--gprof':
745            GPROF = True
746        elif opt == '--githash':
747            GIT_HASH=arg
748        elif opt == '--git-describe':
749            GIT_DESCRIBE = True
750        elif opt in ('', '--ml'):
751            ML_ENABLED = True
752        elif opt == "--js":
753            JS_ENABLED = True
754        elif opt in ('', '--log-sync'):
755            LOG_SYNC = True
756        elif opt == '--single-threaded':
757            SINGLE_THREADED = True
758        elif opt in ('--python'):
759            PYTHON_ENABLED = True
760            PYTHON_INSTALL_ENABLED = True
761        elif opt == '--guardcf':
762            GUARD_CF = True
763            ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE
764        else:
765            print("ERROR: Invalid command line option '%s'" % opt)
766            display_help(1)
767
768
769# Return a list containing a file names included using '#include' in
770# the given C/C++ file named fname.
771def extract_c_includes(fname):
772    result = []
773    # We look for well behaved #include directives
774    std_inc_pat     = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
775    system_inc_pat  = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
776    # We should generate and error for any occurrence of #include that does not match the previous pattern.
777    non_std_inc_pat = re.compile(".*#include.*")
778
779    f = io.open(fname, encoding='utf-8', mode='r')
780    linenum = 1
781    for line in f:
782        m1 = std_inc_pat.match(line)
783        if m1:
784            root_file_name = m1.group(1)
785            slash_pos =  root_file_name.rfind('/')
786            if slash_pos >= 0  and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src"
787                # print(root_file_name)
788                root_file_name = root_file_name[slash_pos+1:]
789            result.append(root_file_name)
790        elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
791            raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
792        linenum = linenum + 1
793    f.close()
794    return result
795
796
797# Given a path dir1/subdir2/subdir3 returns ../../..
798def reverse_path(p):
799    # Filter out empty components (e.g. will have one if path ends in a slash)
800    l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
801    n = len(l)
802    r = '..'
803    for i in range(1, n):
804        r = os.path.join(r, '..')
805    return r
806
807def mk_dir(d):
808    if not os.path.exists(d):
809        os.makedirs(d)
810
811def set_build_dir(d):
812    global BUILD_DIR, REV_BUILD_DIR
813    BUILD_DIR = norm_path(d)
814    REV_BUILD_DIR = reverse_path(d)
815
816def set_z3js_dir(p):
817    global SRC_DIR, Z3JS_SRC_DIR
818    p = norm_path(p)
819    full = os.path.join(SRC_DIR, p)
820    if not os.path.exists(full):
821        raise MKException("Python bindings directory '%s' does not exist" % full)
822    Z3JS_SRC_DIR = full
823    if VERBOSE:
824        print("Js bindings directory was detected.")
825
826def set_z3py_dir(p):
827    global SRC_DIR, Z3PY_SRC_DIR
828    p = norm_path(p)
829    full = os.path.join(SRC_DIR, p)
830    if not os.path.exists(full):
831        raise MKException("Python bindings directory '%s' does not exist" % full)
832    Z3PY_SRC_DIR = full
833    if VERBOSE:
834        print("Python bindings directory was detected.")
835
836_UNIQ_ID = 0
837
838def mk_fresh_name(prefix):
839    global _UNIQ_ID
840    r = '%s_%s' % (prefix, _UNIQ_ID)
841    _UNIQ_ID = _UNIQ_ID + 1
842    return r
843
844_Id = 0
845_Components = []
846_ComponentNames = set()
847_Name2Component = {}
848_Processed_Headers = set()
849
850# Return the Component object named name
851def get_component(name):
852    return _Name2Component[name]
853
854def get_components():
855    return _Components
856
857# Return the directory where the python bindings are located.
858def get_z3py_dir():
859    return Z3PY_SRC_DIR
860
861# Return directory where the js bindings are located
862def get_z3js_dir():
863    return Z3JS_SRC_DIR
864
865# Return true if in verbose mode
866def is_verbose():
867    return VERBOSE
868
869def is_java_enabled():
870    return JAVA_ENABLED
871
872def is_ml_enabled():
873    return ML_ENABLED
874
875def is_js_enabled():
876    return JS_ENABLED
877
878def is_dotnet_core_enabled():
879    return DOTNET_CORE_ENABLED
880
881def is_python_enabled():
882    return PYTHON_ENABLED
883
884def is_python_install_enabled():
885    return PYTHON_INSTALL_ENABLED
886
887def is_compiler(given, expected):
888    """
889    Return True if the 'given' compiler is the expected one.
890    >>> is_compiler('g++', 'g++')
891    True
892    >>> is_compiler('/home/g++', 'g++')
893    True
894    >>> is_compiler(os.path.join('home', 'g++'), 'g++')
895    True
896    >>> is_compiler('clang++', 'g++')
897    False
898    >>> is_compiler(os.path.join('home', 'clang++'), 'clang++')
899    True
900    """
901    if given == expected:
902        return True
903    if len(expected) < len(given):
904        return given[len(given) - len(expected) - 1] == os.sep and given[len(given) - len(expected):] == expected
905    return False
906
907def is_CXX_gpp():
908    return is_compiler(CXX, 'g++')
909
910def is_clang_in_gpp_form(cc):
911    str = check_output([cc, '--version'])
912    try:
913       version_string = str.encode('utf-8')
914    except:
915       version_string = str
916    clang = 'clang'.encode('utf-8')
917    return version_string.find(clang) != -1
918
919def is_CXX_clangpp():
920    if is_compiler(CXX, 'g++'):
921        return is_clang_in_gpp_form(CXX)
922    return is_compiler(CXX, 'clang++')
923
924def get_files_with_ext(path, ext):
925    return filter(lambda f: f.endswith(ext), os.listdir(path))
926
927def get_cpp_files(path):
928    return get_files_with_ext(path,'.cpp')
929
930def get_c_files(path):
931    return get_files_with_ext(path,'.c')
932
933def get_cs_files(path):
934    return get_files_with_ext(path,'.cs')
935
936def get_java_files(path):
937    return get_files_with_ext(path,'.java')
938
939def get_ml_files(path):
940    return get_files_with_ext(path,'.ml')
941
942def find_all_deps(name, deps):
943    new_deps = []
944    for dep in deps:
945        if dep in _ComponentNames:
946            if not (dep in new_deps):
947                new_deps.append(dep)
948            for dep_dep in get_component(dep).deps:
949                if not (dep_dep in new_deps):
950                    new_deps.append(dep_dep)
951        else:
952            raise MKException("Unknown component '%s' at '%s'." % (dep, name))
953    return new_deps
954
955class Component:
956    def __init__(self, name, path, deps):
957        global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
958        if name in _ComponentNames:
959            raise MKException("Component '%s' was already defined." % name)
960        if path is None:
961            path = name
962        self.name = name
963        path = norm_path(path)
964        self.path = path
965        self.deps = find_all_deps(name, deps)
966        self.build_dir = path
967        self.src_dir   = os.path.join(SRC_DIR, path)
968        self.to_src_dir = os.path.join(REV_BUILD_DIR, self.src_dir)
969
970    def get_link_name(self):
971        return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
972
973
974    # Find fname in the include paths for the given component.
975    # ownerfile is only used for creating error messages.
976    # That is, we were looking for fname when processing ownerfile
977    def find_file(self, fname, ownerfile):
978        full_fname = os.path.join(self.src_dir, fname)
979        if os.path.exists(full_fname):
980            return self
981        for dep in self.deps:
982            c_dep = get_component(dep)
983            full_fname = os.path.join(c_dep.src_dir, fname)
984            if os.path.exists(full_fname):
985                return c_dep
986        raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name))
987
988    # Display all dependencies of file basename located in the given component directory.
989    # The result is displayed at out
990    def add_cpp_h_deps(self, out, basename):
991        includes = extract_c_includes(os.path.join(self.src_dir, basename))
992        out.write(os.path.join(self.to_src_dir, basename))
993        for include in includes:
994            owner = self.find_file(include, basename)
995            out.write(' %s.node' % os.path.join(owner.build_dir, include))
996
997    # Add a rule for each #include directive in the file basename located at the current component.
998    def add_rule_for_each_include(self, out, basename):
999        fullname = os.path.join(self.src_dir, basename)
1000        includes = extract_c_includes(fullname)
1001        for include in includes:
1002            owner = self.find_file(include, fullname)
1003            owner.add_h_rule(out, include)
1004
1005    # Display a Makefile rule for an include file located in the given component directory.
1006    # 'include' is something of the form: ast.h, polynomial.h
1007    # The rule displayed at out is of the form
1008    #     ast/ast_pp.h.node : ../src/util/ast_pp.h util/util.h.node ast/ast.h.node
1009    #       @echo "done" > ast/ast_pp.h.node
1010    def add_h_rule(self, out, include):
1011        include_src_path   = os.path.join(self.to_src_dir, include)
1012        if include_src_path in _Processed_Headers:
1013            return
1014        _Processed_Headers.add(include_src_path)
1015        self.add_rule_for_each_include(out, include)
1016        include_node = '%s.node' % os.path.join(self.build_dir, include)
1017        out.write('%s: ' % include_node)
1018        self.add_cpp_h_deps(out, include)
1019        out.write('\n')
1020        out.write('\t@echo done > %s\n' % include_node)
1021
1022    def add_cpp_rules(self, out, include_defs, cppfile):
1023        self.add_rule_for_each_include(out, cppfile)
1024        objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1025        srcfile = os.path.join(self.to_src_dir, cppfile)
1026        out.write('%s: ' % objfile)
1027        self.add_cpp_h_deps(out, cppfile)
1028        out.write('\n')
1029        if SHOW_CPPS:
1030            out.write('\t@echo %s\n' % os.path.join(self.src_dir, cppfile))
1031        out.write('\t@$(CXX) $(CXXFLAGS) $(%s) $(CXX_OUT_FLAG)%s %s\n' % (include_defs, objfile, srcfile))
1032
1033    def mk_makefile(self, out):
1034        include_defs = mk_fresh_name('includes')
1035        out.write('%s =' % include_defs)
1036        for dep in self.deps:
1037            out.write(' -I%s' % get_component(dep).to_src_dir)
1038        out.write(' -I%s' % os.path.join(REV_BUILD_DIR,"src"))
1039        out.write('\n')
1040        mk_dir(os.path.join(BUILD_DIR, self.build_dir))
1041        if VS_PAR and IS_WINDOWS:
1042            cppfiles = list(get_cpp_files(self.src_dir))
1043            dependencies = set()
1044            for cppfile in cppfiles:
1045                dependencies.add(os.path.join(self.to_src_dir, cppfile))
1046                self.add_rule_for_each_include(out, cppfile)
1047                includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
1048                for include in includes:
1049                    owner = self.find_file(include, cppfile)
1050                    dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
1051            for cppfile in cppfiles:
1052                out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
1053            out.write(': ')
1054            for dep in dependencies:
1055                out.write(dep)
1056                out.write(' ')
1057            out.write('\n')
1058            out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
1059            for cppfile in cppfiles:
1060                out.write(' ')
1061                out.write(os.path.join(self.to_src_dir, cppfile))
1062            out.write('\n')
1063            out.write('\tmove *.obj %s\n' % self.build_dir)
1064        else:
1065            for cppfile in get_cpp_files(self.src_dir):
1066                self.add_cpp_rules(out, include_defs, cppfile)
1067
1068    # Return true if the component should be included in the all: rule
1069    def main_component(self):
1070        return False
1071
1072    # Return true if the component contains an AssemblyInfo.cs file that needs to be updated.
1073    def has_assembly_info(self):
1074        return False
1075
1076    # Return true if the component needs builder to generate an install_tactics.cpp file
1077    def require_install_tactics(self):
1078        return False
1079
1080    # Return true if the component needs a def file
1081    def require_def_file(self):
1082        return False
1083
1084    # Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
1085    def require_mem_initializer(self):
1086        return False
1087
1088    def mk_install_deps(self, out):
1089        return
1090
1091    def mk_install(self, out):
1092        return
1093
1094    def mk_uninstall(self, out):
1095        return
1096
1097    def is_example(self):
1098        return False
1099
1100    # Invoked when creating a (windows) distribution package using components at build_path, and
1101    # storing them at dist_path
1102    def mk_win_dist(self, build_path, dist_path):
1103        return
1104
1105    def mk_unix_dist(self, build_path, dist_path):
1106        return
1107
1108    # Used to print warnings or errors after mk_make.py is done, so that they
1109    # are not quite as easy to miss.
1110    def final_info(self):
1111        pass
1112
1113class LibComponent(Component):
1114    def __init__(self, name, path, deps, includes2install):
1115        Component.__init__(self, name, path, deps)
1116        self.includes2install = includes2install
1117
1118    def mk_makefile(self, out):
1119        Component.mk_makefile(self, out)
1120        # generate rule for lib
1121        objs = []
1122        for cppfile in get_cpp_files(self.src_dir):
1123            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1124            objs.append(objfile)
1125
1126        libfile = '%s$(LIB_EXT)' % os.path.join(self.build_dir, self.name)
1127        out.write('%s:' % libfile)
1128        for obj in objs:
1129            out.write(' ')
1130            out.write(obj)
1131        out.write('\n')
1132        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
1133        for obj in objs:
1134            out.write(' ')
1135            out.write(obj)
1136        out.write('\n')
1137        out.write('%s: %s\n\n' % (self.name, libfile))
1138
1139    def mk_install_deps(self, out):
1140        return
1141
1142    def mk_install(self, out):
1143        for include in self.includes2install:
1144            MakeRuleCmd.install_files(
1145                out,
1146                os.path.join(self.to_src_dir, include),
1147                os.path.join(INSTALL_INCLUDE_DIR, include)
1148            )
1149
1150    def mk_uninstall(self, out):
1151        for include in self.includes2install:
1152            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include))
1153
1154    def mk_win_dist(self, build_path, dist_path):
1155        mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR))
1156        for include in self.includes2install:
1157            shutil.copy(os.path.join(self.src_dir, include),
1158                        os.path.join(dist_path, INSTALL_INCLUDE_DIR, include))
1159
1160    def mk_unix_dist(self, build_path, dist_path):
1161        self.mk_win_dist(build_path, dist_path)
1162
1163# "Library" containing only .h files. This is just a placeholder for includes files to be installed.
1164class HLibComponent(LibComponent):
1165    def __init__(self, name, path, includes2install):
1166        LibComponent.__init__(self, name, path, [], includes2install)
1167
1168    def mk_makefile(self, out):
1169        return
1170
1171# Auxiliary function for sort_components
1172def comp_components(c1, c2):
1173    id1 = get_component(c1).id
1174    id2 = get_component(c2).id
1175    return id2 - id1
1176
1177# Sort components based on (reverse) definition time
1178def sort_components(cnames):
1179    return sorted(cnames, key=lambda c: get_component(c).id, reverse=True)
1180
1181class ExeComponent(Component):
1182    def __init__(self, name, exe_name, path, deps, install):
1183        Component.__init__(self, name, path, deps)
1184        if exe_name is None:
1185            exe_name = name
1186        self.exe_name = exe_name
1187        self.install = install
1188
1189    def mk_makefile(self, out):
1190        Component.mk_makefile(self, out)
1191        # generate rule for exe
1192
1193        exefile = '%s$(EXE_EXT)' % self.exe_name
1194        out.write('%s:' % exefile)
1195        deps = sort_components(self.deps)
1196        objs = []
1197        for cppfile in get_cpp_files(self.src_dir):
1198            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1199            objs.append(objfile)
1200        for obj in objs:
1201            out.write(' ')
1202            out.write(obj)
1203        for dep in deps:
1204            c_dep = get_component(dep)
1205            out.write(' ' + c_dep.get_link_name())
1206        out.write('\n')
1207        extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else ''
1208        out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile))
1209        for obj in objs:
1210            out.write(' ')
1211            out.write(obj)
1212        for dep in deps:
1213            c_dep = get_component(dep)
1214            out.write(' ' + c_dep.get_link_name())
1215        out.write(' $(LINK_EXTRA_FLAGS)\n')
1216        out.write('%s: %s\n\n' % (self.name, exefile))
1217
1218    def require_install_tactics(self):
1219        return ('tactic' in self.deps) and ('cmd_context' in self.deps)
1220
1221    def require_mem_initializer(self):
1222        return True
1223
1224    # All executables (to be installed) are included in the all: rule
1225    def main_component(self):
1226        return self.install
1227
1228    def mk_install_deps(self, out):
1229        if self.install:
1230            exefile = '%s$(EXE_EXT)' % self.exe_name
1231            out.write('%s' % exefile)
1232
1233    def mk_install(self, out):
1234        if self.install:
1235            exefile = '%s$(EXE_EXT)' % self.exe_name
1236            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile))
1237
1238    def mk_uninstall(self, out):
1239        if self.install:
1240            exefile = '%s$(EXE_EXT)' % self.exe_name
1241            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile))
1242
1243    def mk_win_dist(self, build_path, dist_path):
1244        if self.install:
1245            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1246            shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name),
1247                        '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
1248
1249    def mk_unix_dist(self, build_path, dist_path):
1250        if self.install:
1251            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1252            shutil.copy(os.path.join(build_path, self.exe_name),
1253                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
1254
1255
1256class ExtraExeComponent(ExeComponent):
1257    def __init__(self, name, exe_name, path, deps, install):
1258        ExeComponent.__init__(self, name, exe_name, path, deps, install)
1259
1260    def main_component(self):
1261        return False
1262
1263    def require_mem_initializer(self):
1264        return False
1265
1266def get_so_ext():
1267    sysname = os.uname()[0]
1268    if sysname == 'Darwin':
1269        return 'dylib'
1270    elif sysname == 'Linux' or sysname == 'GNU' or sysname == 'DragonFly' or sysname == 'NetBSD' or sysname == 'OpenBSD':
1271        return 'so'
1272    elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
1273        return 'dll'
1274    else:
1275        assert(False)
1276        return 'dll'
1277
1278class DLLComponent(Component):
1279    def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None):
1280        Component.__init__(self, name, path, deps)
1281        if dll_name is None:
1282            dll_name = name
1283        self.dll_name = dll_name
1284        self.export_files = export_files
1285        self.reexports = reexports
1286        self.install = install
1287        self.static = static
1288        self.staging_link = staging_link    # link a copy of the shared object into this directory on build
1289
1290    def get_link_name(self):
1291        if self.static:
1292            return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
1293        else:
1294            return self.name + '$(SO_EXT)'
1295
1296    def dll_file(self):
1297        """
1298            Return file name of component suitable for use in a Makefile
1299        """
1300        return '%s$(SO_EXT)' % self.dll_name
1301
1302    def install_path(self):
1303        """
1304            Return install location of component (relative to prefix)
1305            suitable for use in a Makefile
1306        """
1307        return os.path.join(INSTALL_LIB_DIR, self.dll_file())
1308
1309    def mk_makefile(self, out):
1310        Component.mk_makefile(self, out)
1311        # generate rule for (SO_EXT)
1312        out.write('%s:' % self.dll_file())
1313        deps = sort_components(self.deps)
1314        objs = []
1315        for cppfile in get_cpp_files(self.src_dir):
1316            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1317            objs.append(objfile)
1318        # Explicitly include obj files of reexport. This fixes problems with exported symbols on Linux and OSX.
1319        for reexport in self.reexports:
1320            reexport = get_component(reexport)
1321            for cppfile in get_cpp_files(reexport.src_dir):
1322                objfile = '%s$(OBJ_EXT)' % os.path.join(reexport.build_dir, os.path.splitext(cppfile)[0])
1323                objs.append(objfile)
1324        for obj in objs:
1325            out.write(' ')
1326            out.write(obj)
1327        for dep in deps:
1328            if dep not in self.reexports:
1329                c_dep = get_component(dep)
1330                out.write(' ' + c_dep.get_link_name())
1331        out.write('\n')
1332        out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file())
1333        for obj in objs:
1334            out.write(' ')
1335            out.write(obj)
1336        for dep in deps:
1337            if dep not in self.reexports:
1338                c_dep = get_component(dep)
1339                out.write(' ' + c_dep.get_link_name())
1340        out.write(' $(SLINK_EXTRA_FLAGS)')
1341        if IS_WINDOWS:
1342            out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name))
1343        if self.staging_link:
1344            if IS_WINDOWS:
1345                out.write('\n\tcopy %s %s' % (self.dll_file(), self.staging_link))
1346            elif IS_OSX:
1347                out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link))
1348            else:
1349                out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link))
1350        out.write('\n')
1351        if self.static:
1352            if IS_WINDOWS:
1353                libfile = '%s-static$(LIB_EXT)' % self.dll_name
1354            else:
1355                libfile = '%s$(LIB_EXT)' % self.dll_name
1356            self.mk_static(out, libfile)
1357            out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile))
1358        else:
1359            out.write('%s: %s\n\n' % (self.name, self.dll_file()))
1360
1361    def mk_static(self, out, libfile):
1362        # generate rule for lib
1363        objs = []
1364        for cppfile in get_cpp_files(self.src_dir):
1365            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1366            objs.append(objfile)
1367        # we have to "reexport" all object files
1368        for dep in self.deps:
1369            dep = get_component(dep)
1370            for cppfile in get_cpp_files(dep.src_dir):
1371                objfile = '%s$(OBJ_EXT)' % os.path.join(dep.build_dir, os.path.splitext(cppfile)[0])
1372                objs.append(objfile)
1373        out.write('%s:' % libfile)
1374        for obj in objs:
1375            out.write(' ')
1376            out.write(obj)
1377        out.write('\n')
1378        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
1379        for obj in objs:
1380            out.write(' ')
1381            out.write(obj)
1382        out.write('\n')
1383
1384    def main_component(self):
1385        return self.install
1386
1387    def require_install_tactics(self):
1388        return ('tactic' in self.deps) and ('cmd_context' in self.deps)
1389
1390    def require_mem_initializer(self):
1391        return True
1392
1393    def require_def_file(self):
1394        return IS_WINDOWS and self.export_files
1395
1396    def mk_install_deps(self, out):
1397        out.write('%s$(SO_EXT)' % self.dll_name)
1398        if self.static:
1399            out.write(' %s$(LIB_EXT)' % self.dll_name)
1400
1401    def mk_install(self, out):
1402        if self.install:
1403            MakeRuleCmd.install_files(out, self.dll_file(), self.install_path())
1404            if self.static:
1405                libfile = '%s$(LIB_EXT)' % self.dll_name
1406                MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile))
1407
1408    def mk_uninstall(self, out):
1409        MakeRuleCmd.remove_installed_files(out, self.install_path())
1410        libfile = '%s$(LIB_EXT)' % self.dll_name
1411        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
1412
1413    def mk_win_dist(self, build_path, dist_path):
1414        if self.install:
1415            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1416            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1417                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1418            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1419                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1420            shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
1421                        '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1422
1423    def mk_unix_dist(self, build_path, dist_path):
1424        if self.install:
1425            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1426            so = get_so_ext()
1427            shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
1428                        '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
1429            shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
1430                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1431
1432class JsComponent(Component):
1433    def __init__(self):
1434         Component.__init__(self, "js", None, [])
1435
1436    def main_component(self):
1437        return False
1438
1439    def mk_win_dist(self, build_path, dist_path):
1440        return
1441
1442    def mk_unix_dist(self, build_path, dist_path):
1443        return
1444
1445    def mk_makefile(self, out):
1446        return
1447
1448class PythonComponent(Component):
1449    def __init__(self, name, libz3Component):
1450        assert isinstance(libz3Component, DLLComponent)
1451        global PYTHON_ENABLED
1452        Component.__init__(self, name, None, [])
1453        self.libz3Component = libz3Component
1454
1455    def main_component(self):
1456        return False
1457
1458    def mk_win_dist(self, build_path, dist_path):
1459        if not is_python_enabled():
1460            return
1461
1462        src = os.path.join(build_path, 'python', 'z3')
1463        dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
1464        if os.path.exists(dst):
1465            shutil.rmtree(dst)
1466        shutil.copytree(src, dst)
1467
1468    def mk_unix_dist(self, build_path, dist_path):
1469        self.mk_win_dist(build_path, dist_path)
1470
1471    def mk_makefile(self, out):
1472        return
1473
1474class PythonInstallComponent(Component):
1475    def __init__(self, name, libz3Component):
1476        assert isinstance(libz3Component, DLLComponent)
1477        global PYTHON_INSTALL_ENABLED
1478        Component.__init__(self, name, None, [])
1479        self.pythonPkgDir = None
1480        self.in_prefix_install = True
1481        self.libz3Component = libz3Component
1482
1483        if not PYTHON_INSTALL_ENABLED:
1484            return
1485
1486        if IS_WINDOWS:
1487            # Installing under Windows doesn't make sense as the install prefix is used
1488            # but that doesn't make sense under Windows
1489            # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix,
1490            # i.e., something along the lines of C:\Python\... At the moment we are not
1491            # sure whether we would want to install libz3.dll into that directory though.
1492            PYTHON_INSTALL_ENABLED = False
1493            return
1494        else:
1495            PYTHON_INSTALL_ENABLED = True
1496
1497        if IS_WINDOWS or IS_OSX:
1498            # Use full path that is possibly outside of install prefix
1499            self.in_prefix_install = PYTHON_PACKAGE_DIR.startswith(PREFIX)
1500            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
1501        else:
1502            # Use path inside the prefix (should be the normal case on Linux)
1503            # CMW: Also normal on *BSD?
1504            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
1505                raise MKException(('The python package directory ({}) must live ' +
1506                    'under the install prefix ({}) to install the python bindings.' +
1507                    'Use --pypkgdir and --prefix to set the python package directory ' +
1508                    'and install prefix respectively. Note that the python package ' +
1509                    'directory does not need to exist and will be created if ' +
1510                    'necessary during install.').format(
1511                        PYTHON_PACKAGE_DIR,
1512                        PREFIX))
1513            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
1514            self.in_prefix_install = True
1515
1516        if self.in_prefix_install:
1517            assert not os.path.isabs(self.pythonPkgDir)
1518
1519    def final_info(self):
1520        if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED:
1521            print("Warning: The detected Python package directory (%s) is not "
1522                  "in the installation prefix (%s). This can lead to a broken "
1523                  "Python API installation. Use --pypkgdir= to change the "
1524                  "Python package directory." % (PYTHON_PACKAGE_DIR, PREFIX))
1525
1526    def main_component(self):
1527        return False
1528
1529    def mk_install(self, out):
1530        if not is_python_install_enabled():
1531            return
1532        MakeRuleCmd.make_install_directory(out,
1533                                           os.path.join(self.pythonPkgDir, 'z3'),
1534                                           in_prefix=self.in_prefix_install)
1535        MakeRuleCmd.make_install_directory(out,
1536                                           os.path.join(self.pythonPkgDir, 'z3', 'lib'),
1537                                           in_prefix=self.in_prefix_install)
1538
1539        # Sym-link or copy libz3 into python package directory
1540        if IS_WINDOWS or IS_OSX:
1541            MakeRuleCmd.install_files(out,
1542                                      self.libz3Component.dll_file(),
1543                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
1544                                                   self.libz3Component.dll_file()),
1545                                      in_prefix=self.in_prefix_install
1546                                     )
1547        else:
1548            # Create symbolic link to save space.
1549            # It's important that this symbolic link be relative (rather
1550            # than absolute) so that the install is relocatable (needed for
1551            # staged installs that use DESTDIR).
1552            MakeRuleCmd.create_relative_symbolic_link(out,
1553                                                      self.libz3Component.install_path(),
1554                                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
1555                                                                   self.libz3Component.dll_file()
1556                                                                  ),
1557                                                     )
1558
1559        MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'),
1560                                  os.path.join(self.pythonPkgDir, 'z3'),
1561                                  in_prefix=self.in_prefix_install)
1562        if sys.version >= "3":
1563            pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__')
1564            MakeRuleCmd.make_install_directory(out,
1565                                               pythonPycacheDir,
1566                                               in_prefix=self.in_prefix_install)
1567            MakeRuleCmd.install_files(out,
1568                                      os.path.join('python', 'z3', '__pycache__', '*.pyc'),
1569                                      pythonPycacheDir,
1570                                      in_prefix=self.in_prefix_install)
1571        else:
1572            MakeRuleCmd.install_files(out,
1573                                      os.path.join('python', 'z3', '*.pyc'),
1574                                      os.path.join(self.pythonPkgDir,'z3'),
1575                                      in_prefix=self.in_prefix_install)
1576
1577        if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
1578            out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
1579
1580    def mk_uninstall(self, out):
1581        if not is_python_install_enabled():
1582            return
1583        MakeRuleCmd.remove_installed_files(out,
1584                                           os.path.join(self.pythonPkgDir,
1585                                                        self.libz3Component.dll_file()),
1586                                           in_prefix=self.in_prefix_install
1587                                          )
1588        MakeRuleCmd.remove_installed_files(out,
1589                                           os.path.join(self.pythonPkgDir, 'z3', '*.py'),
1590                                           in_prefix=self.in_prefix_install)
1591        MakeRuleCmd.remove_installed_files(out,
1592                                           os.path.join(self.pythonPkgDir, 'z3', '*.pyc'),
1593                                           in_prefix=self.in_prefix_install)
1594        MakeRuleCmd.remove_installed_files(out,
1595                                           os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
1596                                           in_prefix=self.in_prefix_install
1597                                          )
1598        MakeRuleCmd.remove_installed_files(out,
1599                                           os.path.join(self.pythonPkgDir, 'z3', 'lib',
1600                                                        self.libz3Component.dll_file()))
1601
1602    def mk_makefile(self, out):
1603        return
1604
1605def set_key_file(self):
1606    global DOTNET_KEY_FILE
1607    # We need to give the assembly a strong name so that it
1608    # can be installed into the GAC with ``make install``
1609    if not DOTNET_KEY_FILE is None:
1610       self.key_file = DOTNET_KEY_FILE
1611
1612    if not self.key_file is None:
1613       if os.path.isfile(self.key_file):
1614           self.key_file = os.path.abspath(self.key_file)
1615       elif os.path.isfile(os.path.join(self.src_dir, self.key_file)):
1616           self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file))
1617       else:
1618           print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
1619           self.key_file = None
1620
1621
1622# build for dotnet core
1623class DotNetDLLComponent(Component):
1624    def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file):
1625        Component.__init__(self, name, path, deps)
1626        if dll_name is None:
1627            dll_name = name
1628        if assembly_info_dir is None:
1629            assembly_info_dir = "."
1630        self.dll_name          = dll_name
1631        self.assembly_info_dir = assembly_info_dir
1632        self.key_file = default_key_file
1633
1634
1635    def mk_makefile(self, out):
1636        if not is_dotnet_core_enabled():
1637            return
1638        cs_fp_files = []
1639        for cs_file in get_cs_files(self.src_dir):
1640            cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
1641        if self.assembly_info_dir != '.':
1642            for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
1643                cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
1644        dllfile = '%s.dll' % self.dll_name
1645        out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
1646        for cs_file in cs_fp_files:
1647            out.write(' ')
1648            out.write(cs_file)
1649        out.write('\n')
1650
1651        set_key_file(self)
1652        key = ""
1653        if not self.key_file is None:
1654            key = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
1655            key += "\n<SignAssembly>true</SignAssembly>"
1656
1657        version = get_version_string(3)
1658
1659        core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
1660
1661  <PropertyGroup>
1662    <TargetFramework>netstandard1.4</TargetFramework>
1663    <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
1664    <DebugType>portable</DebugType>
1665    <AssemblyName>Microsoft.Z3</AssemblyName>
1666    <OutputType>Library</OutputType>
1667    <PackageId>Microsoft.Z3</PackageId>
1668    <GenerateDocumentationFile>true</GenerateDocumentationFile>
1669    <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
1670    <Version>%s</Version>
1671    <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
1672    <Authors>Microsoft</Authors>
1673    <Company>Microsoft</Company>
1674    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
1675    <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
1676    <Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
1677    <PackageTags>smt constraint solver theorem prover</PackageTags>
1678    %s
1679  </PropertyGroup>
1680
1681  <ItemGroup>
1682    <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
1683  </ItemGroup>
1684
1685</Project>""" % (version, key, self.to_src_dir)
1686
1687        mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
1688        csproj = os.path.join('dotnet', 'z3.csproj')
1689        with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
1690            ous.write(core_csproj_str)
1691
1692        dotnetCmdLine = [DOTNET, "build", csproj]
1693
1694        dotnetCmdLine.extend(['-c'])
1695        if DEBUG_MODE:
1696            dotnetCmdLine.extend(['Debug'])
1697        else:
1698            dotnetCmdLine.extend(['Release'])
1699
1700        path = os.path.join(os.path.abspath(BUILD_DIR), ".")
1701        dotnetCmdLine.extend(['-o', path])
1702
1703        MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
1704        out.write('\n')
1705        out.write('%s: %s\n\n' % (self.name, dllfile))
1706
1707    def main_component(self):
1708        return is_dotnet_core_enabled()
1709
1710    def has_assembly_info(self):
1711        # TBD: is this required for dotnet core given that version numbers are in z3.csproj file?
1712        return False
1713
1714
1715    def mk_win_dist(self, build_path, dist_path):
1716        if is_dotnet_core_enabled():
1717            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1718            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1719                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1720            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1721                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1722            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
1723                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1724            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
1725                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1726            if DEBUG_MODE:
1727                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1728                            '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1729
1730    def mk_unix_dist(self, build_path, dist_path):
1731        if is_dotnet_core_enabled():
1732            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1733            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1734                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1735            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
1736                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1737            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
1738                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1739
1740    def mk_install_deps(self, out):
1741        pass
1742
1743    def mk_install(self, out):
1744        pass
1745
1746    def mk_uninstall(self, out):
1747        pass
1748
1749class JavaDLLComponent(Component):
1750    def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
1751        Component.__init__(self, name, path, deps)
1752        if dll_name is None:
1753            dll_name = name
1754        self.dll_name     = dll_name
1755        self.package_name = package_name
1756        self.manifest_file = manifest_file
1757        self.install = not is_windows()
1758
1759    def mk_makefile(self, out):
1760        global JAVAC
1761        global JAR
1762
1763        if is_java_enabled():
1764            mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
1765            dllfile = '%s$(SO_EXT)' % self.dll_name
1766            out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
1767            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)
1768            if IS_OSX:
1769                t = t.replace('PLATFORM', 'darwin')
1770            elif is_linux():
1771                t = t.replace('PLATFORM', 'linux')
1772            elif is_hurd():
1773                t = t.replace('PLATFORM', 'hurd')
1774            elif IS_DRAGONFLY:
1775                t = t.replace('PLATFORM', 'dragonfly')
1776            elif IS_NETBSD:
1777                t = t.replace('PLATFORM', 'netbsd')
1778            elif IS_OPENBSD:
1779                t = t.replace('PLATFORM', 'openbsd')
1780            elif IS_SUNOS:
1781                t = t.replace('PLATFORM', 'SunOS')
1782            elif IS_CYGWIN:
1783                t = t.replace('PLATFORM', 'cygwin')
1784            elif IS_MSYS2:
1785                t = t.replace('PLATFORM', 'win32')
1786            else:
1787                t = t.replace('PLATFORM', 'win32')
1788            out.write(t)
1789            if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
1790                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
1791                          os.path.join('api', 'java', 'Native'))
1792            else:
1793                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
1794                          os.path.join('api', 'java', 'Native'))
1795            out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
1796            deps = ''
1797            for jfile in get_java_files(self.src_dir):
1798                deps += ('%s ' % os.path.join(self.to_src_dir, jfile))
1799            for jfile in get_java_files(os.path.join(self.src_dir, "enumerations")):
1800                deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile)
1801            out.write(deps)
1802            out.write('\n')
1803            #if IS_WINDOWS:
1804            JAVAC = '"%s"' % JAVAC
1805            JAR = '"%s"' % JAR
1806            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')))
1807            out.write(t)
1808            t = ('\t%s -source 1.8 -target 1.8 -cp %s %s.java -d %s\n' % (JAVAC,
1809                                                  os.path.join('api', 'java', 'classes'),
1810                                                  os.path.join(self.to_src_dir, '*'),
1811                                                  os.path.join('api', 'java', 'classes')))
1812            out.write(t)
1813            out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
1814                                                         os.path.join(self.to_src_dir, 'manifest'),
1815                                                         os.path.join('api', 'java', 'classes')))
1816            out.write('java: %s.jar\n\n' % self.package_name)
1817
1818    def main_component(self):
1819        return is_java_enabled()
1820
1821    def mk_win_dist(self, build_path, dist_path):
1822        if JAVA_ENABLED:
1823            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1824            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
1825                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
1826            shutil.copy(os.path.join(build_path, 'libz3java.dll'),
1827                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll'))
1828            shutil.copy(os.path.join(build_path, 'libz3java.lib'),
1829                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib'))
1830
1831    def mk_unix_dist(self, build_path, dist_path):
1832        if JAVA_ENABLED:
1833            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1834            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
1835                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
1836            so = get_so_ext()
1837            shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
1838                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
1839
1840    def mk_install(self, out):
1841        if is_java_enabled() and self.install:
1842            dllfile = '%s$(SO_EXT)' % self.dll_name
1843            MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile))
1844            jarfile = '{}.jar'.format(self.package_name)
1845            MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile))
1846
1847    def mk_uninstall(self, out):
1848        if is_java_enabled() and self.install:
1849            dllfile = '%s$(SO_EXT)' % self.dll_name
1850            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
1851            jarfile = '{}.jar'.format(self.package_name)
1852            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))
1853
1854class MLComponent(Component):
1855
1856    def __init__(self, name, lib_name, path, deps):
1857        Component.__init__(self, name, path, deps)
1858        if lib_name is None:
1859            lib_name = name
1860        self.lib_name = lib_name
1861        self.modules = ["z3enums", "z3native", "z3"]  # dependencies in this order!
1862        self.stubs = "z3native_stubs"
1863        self.sub_dir = os.path.join('api', 'ml')
1864
1865        self.destdir = ""
1866        self.ldconf = ""
1867        # Calling _init_ocamlfind_paths() is postponed to later because
1868        # OCAMLFIND hasn't been checked yet.
1869
1870    def _install_bindings(self):
1871        # FIXME: Depending on global state is gross.  We can't pre-compute this
1872        # in the constructor because we haven't tested for ocamlfind yet
1873        return OCAMLFIND != ''
1874
1875    def _init_ocamlfind_paths(self):
1876        """
1877            Initialises self.destdir and self.ldconf
1878            Do not call this from the MLComponent constructor because OCAMLFIND
1879            has not been checked at that point
1880        """
1881        if self.destdir != "" and self.ldconf != "":
1882            # Initialisation already done
1883            return
1884        # Use Ocamlfind to get the default destdir and ldconf path
1885        self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir'])
1886        if self.destdir == "":
1887            raise MKException('Failed to get OCaml destdir')
1888
1889        if not os.path.isdir(self.destdir):
1890            raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir))
1891
1892        self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf'])
1893        if self.ldconf == "":
1894            raise MKException('Failed to get OCaml ldconf path')
1895
1896    def final_info(self):
1897        if not self._install_bindings():
1898            print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed")
1899
1900    def mk_makefile(self, out):
1901        if is_ml_enabled():
1902            CP_CMD = 'cp'
1903            if IS_WINDOWS:
1904                CP_CMD='copy'
1905
1906            OCAML_FLAGS = ''
1907            if DEBUG_MODE:
1908                OCAML_FLAGS += '-g'
1909
1910            if OCAMLFIND:
1911                OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package zarith' + ' ' + OCAML_FLAGS
1912                OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package zarith' + ' ' + OCAML_FLAGS
1913            else:
1914                OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
1915                OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
1916
1917            src_dir = self.to_src_dir
1918            mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
1919            api_src = get_component(API_COMPONENT).to_src_dir
1920            # remove /GL and -std=c++11; the ocaml tools don't like them.
1921            if IS_WINDOWS:
1922                out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n')
1923            else:
1924                out.write('CXXFLAGS_OCAML=$(subst -std=c++11,,$(CXXFLAGS))\n')
1925
1926            substitutions = { 'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) }
1927
1928            configure_file(os.path.join(self.src_dir, 'META.in'),
1929                           os.path.join(BUILD_DIR, self.sub_dir, 'META'),
1930                           substitutions)
1931
1932            stubsc = os.path.join(src_dir, self.stubs + '.c')
1933            stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
1934            base_dll_name = get_component(Z3_DLL_COMPONENT).dll_name
1935            if STATIC_LIB:
1936                z3link = 'z3-static'
1937                z3linkdep = base_dll_name + '-static$(LIB_EXT)'
1938                out.write('%s: %s\n' % (z3linkdep, base_dll_name + '$(LIB_EXT)'))
1939                out.write('\tcp $< $@\n')
1940            else:
1941                z3link = 'z3'
1942                z3linkdep = base_dll_name + '$(SO_EXT)'
1943            out.write('%s: %s %s\n' % (stubso, stubsc, z3linkdep))
1944            out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
1945                      (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))
1946
1947            cmos = ''
1948            for m in self.modules:
1949                ml = os.path.join(src_dir, m + '.ml')
1950                cmo = os.path.join(self.sub_dir, m + '.cmo')
1951                existing_mli = os.path.join(src_dir, m + '.mli')
1952                mli = os.path.join(self.sub_dir, m + '.mli')
1953                cmi = os.path.join(self.sub_dir, m + '.cmi')
1954                out.write('%s: %s %s\n' % (cmo, ml, cmos))
1955                if (os.path.exists(existing_mli[3:])):
1956                    out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
1957                else:
1958                    out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli))
1959                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
1960                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml))
1961                cmos = cmos + cmo + ' '
1962
1963            cmxs = ''
1964            for m in self.modules:
1965                ff = os.path.join(src_dir, m + '.ml')
1966                ft = os.path.join(self.sub_dir, m + '.cmx')
1967                out.write('%s: %s %s %s\n' % (ft, ff, cmos, cmxs))
1968                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
1969                cmxs = cmxs + ' ' + ft
1970
1971
1972            OCAMLMKLIB = 'ocamlmklib'
1973
1974            LIBZ3 = '-l' + z3link + ' -lstdc++'
1975            if is_cygwin() and not(is_cygwin_mingw()):
1976                LIBZ3 = z3linkdep
1977
1978            LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))
1979
1980            if DEBUG_MODE and not(is_cygwin()):
1981                # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
1982                OCAMLMKLIB += ' -g'
1983
1984            z3mls = os.path.join(self.sub_dir, 'z3ml')
1985
1986            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))
1987            out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
1988            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))
1989            out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
1990            out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
1991            out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
1992
1993            out.write('\n')
1994            out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
1995            out.write('\n')
1996
1997            if IS_WINDOWS:
1998                out.write('ocamlfind_install: ')
1999                self.mk_install_deps(out)
2000                out.write('\n')
2001                self.mk_install(out)
2002                out.write('\n')
2003                out.write('ocamlfind_uninstall:\n')
2004                self.mk_uninstall(out)
2005                out.write('\n')
2006
2007    def mk_install_deps(self, out):
2008        if is_ml_enabled() and self._install_bindings():
2009            out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
2010            out.write(os.path.join(self.sub_dir, 'META '))
2011            out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
2012            out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
2013            out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))
2014
2015    def mk_install(self, out):
2016        if is_ml_enabled() and self._install_bindings():
2017            self._init_ocamlfind_paths()
2018            in_prefix = self.destdir.startswith(PREFIX)
2019            maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX)
2020            # Note that when doing a staged install with DESTDIR that modifying
2021            # OCaml's ``ld.conf`` may fail. Therefore packagers will need to
2022            # make their packages modify it manually at package install time
2023            # as opposed to ``make install`` time.
2024            MakeRuleCmd.make_install_directory(out,
2025                                               maybe_stripped_destdir,
2026                                               in_prefix=in_prefix)
2027            out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format(
2028                ldconf=self.ldconf,
2029                ocamlfind=OCAMLFIND,
2030                ocaml_destdir=self.destdir,
2031                metafile=os.path.join(self.sub_dir, 'META')))
2032
2033            for m in self.modules:
2034                mli = os.path.join(self.src_dir, m) + '.mli'
2035                if os.path.exists(mli):
2036                    out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
2037                else:
2038                    out.write(' ' + os.path.join(self.sub_dir, m) + '.mli')
2039                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
2040                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx')
2041            out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
2042            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
2043            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma'))))
2044            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa'))))
2045            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs'))))
2046            out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
2047            if is_windows() or is_cygwin_mingw():
2048                out.write('.dll')
2049            else:
2050                out.write('.so') # .so also on OSX!
2051            out.write('\n')
2052
2053    def mk_uninstall(self, out):
2054        if is_ml_enabled() and self._install_bindings():
2055            self._init_ocamlfind_paths()
2056            out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format(
2057                ldconf=self.ldconf,
2058                ocamlfind=OCAMLFIND,
2059                ocaml_destdir=self.destdir))
2060
2061    def main_component(self):
2062        return is_ml_enabled()
2063
2064class ExampleComponent(Component):
2065    def __init__(self, name, path):
2066        Component.__init__(self, name, path, [])
2067        self.ex_dir   = os.path.join(EXAMPLE_DIR, self.path)
2068        self.to_ex_dir = os.path.join(REV_BUILD_DIR, self.ex_dir)
2069
2070    def is_example(self):
2071        return True
2072
2073class CppExampleComponent(ExampleComponent):
2074    def __init__(self, name, path):
2075        ExampleComponent.__init__(self, name, path)
2076
2077    def compiler(self):
2078        return "$(CXX)"
2079
2080    def src_files(self):
2081        return get_cpp_files(self.ex_dir)
2082
2083    def mk_makefile(self, out):
2084        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
2085        dll = '%s$(SO_EXT)' % dll_name
2086
2087        objfiles = ''
2088        for cppfile in self.src_files():
2089            objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')])
2090            objfiles = objfiles + ('%s ' % objfile)
2091            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile)));
2092            out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
2093            # Add include dir components
2094            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
2095            out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
2096            out.write(' %s' % os.path.join(self.to_ex_dir, cppfile))
2097            out.write('\n')
2098
2099        exefile = '%s$(EXE_EXT)' % self.name
2100        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
2101        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
2102        if IS_WINDOWS:
2103            out.write('%s.lib' % dll_name)
2104        else:
2105            out.write(dll)
2106        out.write(' $(LINK_EXTRA_FLAGS)\n')
2107        out.write('_ex_%s: %s\n\n' % (self.name, exefile))
2108
2109class CExampleComponent(CppExampleComponent):
2110    def __init__(self, name, path):
2111        CppExampleComponent.__init__(self, name, path)
2112
2113    def compiler(self):
2114        return "$(CC)"
2115
2116    def src_files(self):
2117        return get_c_files(self.ex_dir)
2118
2119    def mk_makefile(self, out):
2120        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
2121        dll = '%s$(SO_EXT)' % dll_name
2122
2123        objfiles = ''
2124        for cfile in self.src_files():
2125            objfile = '%s$(OBJ_EXT)' % (cfile[:cfile.rfind('.')])
2126            objfiles = objfiles + ('%s ' % objfile)
2127            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cfile)));
2128            out.write('\t%s $(CFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(C_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
2129            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
2130            out.write(' %s' % os.path.join(self.to_ex_dir, cfile))
2131            out.write('\n')
2132
2133        exefile = '%s$(EXE_EXT)' % self.name
2134        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
2135        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
2136        if IS_WINDOWS:
2137            out.write('%s.lib' % dll_name)
2138        else:
2139            out.write(dll)
2140        out.write(' $(LINK_EXTRA_FLAGS)\n')
2141        out.write('_ex_%s: %s\n\n' % (self.name, exefile))
2142
2143class DotNetExampleComponent(ExampleComponent):
2144    def __init__(self, name, path):
2145        ExampleComponent.__init__(self, name, path)
2146
2147    def is_example(self):
2148        return is_dotnet_core_enabled()
2149
2150    def mk_makefile(self, out):
2151        if is_dotnet_core_enabled():
2152            proj_name = 'dotnet_example.csproj'
2153            out.write('_ex_%s:' % self.name)
2154            for csfile in get_cs_files(self.ex_dir):
2155                out.write(' ')
2156                out.write(os.path.join(self.to_ex_dir, csfile))
2157
2158            mk_dir(os.path.join(BUILD_DIR, 'dotnet_example'))
2159            csproj = os.path.join('dotnet_example', proj_name)
2160            if VS_X64:
2161                platform = 'x64'
2162            elif VS_ARM:
2163                platform = 'ARM'
2164            else:
2165                platform = 'x86'
2166
2167            dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk">
2168  <PropertyGroup>
2169    <OutputType>Exe</OutputType>
2170    <TargetFramework>netcoreapp2.0</TargetFramework>
2171    <PlatformTarget>%s</PlatformTarget>
2172  </PropertyGroup>
2173  <ItemGroup>
2174    <Compile Include="..\%s/*.cs" />
2175    <Reference Include="Microsoft.Z3">
2176      <HintPath>..\Microsoft.Z3.dll</HintPath>
2177    </Reference>
2178  </ItemGroup>
2179</Project>""" % (platform, self.to_ex_dir)
2180
2181            with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
2182                ous.write(dotnet_proj_str)
2183
2184            out.write('\n')
2185            dotnetCmdLine = [DOTNET, "build", csproj]
2186            dotnetCmdLine.extend(['-c'])
2187            if DEBUG_MODE:
2188                dotnetCmdLine.extend(['Debug'])
2189            else:
2190                dotnetCmdLine.extend(['Release'])
2191            MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
2192            out.write('\n')
2193
2194class JavaExampleComponent(ExampleComponent):
2195    def __init__(self, name, path):
2196        ExampleComponent.__init__(self, name, path)
2197
2198    def is_example(self):
2199        return JAVA_ENABLED
2200
2201    def mk_makefile(self, out):
2202        if JAVA_ENABLED:
2203            pkg = get_component(JAVA_COMPONENT).package_name + '.jar'
2204            out.write('JavaExample.class: %s' % (pkg))
2205            deps = ''
2206            for jfile in get_java_files(self.ex_dir):
2207                out.write(' %s' % os.path.join(self.to_ex_dir, jfile))
2208            if IS_WINDOWS:
2209                deps = deps.replace('/', '\\')
2210            out.write('%s\n' % deps)
2211            out.write('\t%s -cp %s ' % (JAVAC, pkg))
2212            win_ex_dir = self.to_ex_dir
2213            for javafile in get_java_files(self.ex_dir):
2214                out.write(' ')
2215                out.write(os.path.join(win_ex_dir, javafile))
2216            out.write(' -d .\n')
2217            out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
2218
2219class MLExampleComponent(ExampleComponent):
2220    def __init__(self, name, path):
2221        ExampleComponent.__init__(self, name, path)
2222
2223    def is_example(self):
2224        return ML_ENABLED
2225
2226    def mk_makefile(self, out):
2227        if ML_ENABLED:
2228            out.write('ml_example.byte: api/ml/z3ml.cma')
2229            for mlfile in get_ml_files(self.ex_dir):
2230                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
2231            out.write('\n')
2232            out.write('\tocamlfind %s ' % OCAMLC)
2233            if DEBUG_MODE:
2234                out.write('-g ')
2235            out.write('-custom -o ml_example.byte -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cma')
2236            for mlfile in get_ml_files(self.ex_dir):
2237                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
2238            out.write('\n')
2239            out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa')
2240            for mlfile in get_ml_files(self.ex_dir):
2241                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
2242            out.write('\n')
2243            out.write('\tocamlfind %s ' % OCAMLOPT)
2244            if DEBUG_MODE:
2245                out.write('-g ')
2246            out.write('-o ml_example$(EXE_EXT) -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cmxa')
2247            for mlfile in get_ml_files(self.ex_dir):
2248                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
2249            out.write('\n')
2250            out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
2251
2252class PythonExampleComponent(ExampleComponent):
2253    def __init__(self, name, path):
2254        ExampleComponent.__init__(self, name, path)
2255
2256    # Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked.
2257    # We don't need to include them in the :examples rule
2258    def mk_makefile(self, out):
2259        full = os.path.join(EXAMPLE_DIR, self.path)
2260        for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
2261            shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py))
2262            if is_verbose():
2263                print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python')))
2264        out.write('_ex_%s: \n\n' % self.name)
2265
2266    def mk_win_dist(self, build_path, dist_path):
2267        full = os.path.join(EXAMPLE_DIR, self.path)
2268        py = 'example.py'
2269        shutil.copyfile(os.path.join(full, py),
2270                        os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))
2271
2272    def mk_unix_dist(self, build_path, dist_path):
2273        self.mk_win_dist(build_path, dist_path)
2274
2275
2276def reg_component(name, c):
2277    global _Id, _Components, _ComponentNames, _Name2Component
2278    c.id = _Id
2279    _Id = _Id + 1
2280    _Components.append(c)
2281    _ComponentNames.add(name)
2282    _Name2Component[name] = c
2283    if VERBOSE:
2284        print("New component: '%s'" % name)
2285
2286def add_lib(name, deps=[], path=None, includes2install=[]):
2287    c = LibComponent(name, path, deps, includes2install)
2288    reg_component(name, c)
2289
2290def add_clib(name, deps=[], path=None, includes2install=[]):
2291    c = CLibComponent(name, path, deps, includes2install)
2292    reg_component(name, c)
2293
2294def add_hlib(name, path=None, includes2install=[]):
2295    c = HLibComponent(name, path, includes2install)
2296    reg_component(name, c)
2297
2298def add_exe(name, deps=[], path=None, exe_name=None, install=True):
2299    c = ExeComponent(name, exe_name, path, deps, install)
2300    reg_component(name, c)
2301
2302def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
2303    c = ExtraExeComponent(name, exe_name, path, deps, install)
2304    reg_component(name, c)
2305
2306def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None):
2307    c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link)
2308    reg_component(name, c)
2309    return c
2310
2311def add_dot_net_core_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None):
2312    c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
2313    reg_component(name, c)
2314
2315def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None):
2316    c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
2317    reg_component(name, c)
2318
2319def add_python(libz3Component):
2320    name = 'python'
2321    reg_component(name, PythonComponent(name, libz3Component))
2322
2323def add_js():
2324    reg_component('js', JsComponent())
2325
2326def add_python_install(libz3Component):
2327    name = 'python_install'
2328    reg_component(name, PythonInstallComponent(name, libz3Component))
2329
2330def add_ml_lib(name, deps=[], path=None, lib_name=None):
2331    c = MLComponent(name, lib_name, path, deps)
2332    reg_component(name, c)
2333
2334def add_cpp_example(name, path=None):
2335    c = CppExampleComponent(name, path)
2336    reg_component(name, c)
2337
2338def add_c_example(name, path=None):
2339    c = CExampleComponent(name, path)
2340    reg_component(name, c)
2341
2342def add_dotnet_example(name, path=None):
2343    c = DotNetExampleComponent(name, path)
2344    reg_component(name, c)
2345
2346def add_java_example(name, path=None):
2347    c = JavaExampleComponent(name, path)
2348    reg_component(name, c)
2349
2350def add_ml_example(name, path=None):
2351    c = MLExampleComponent(name, path)
2352    reg_component(name, c)
2353
2354def add_z3py_example(name, path=None):
2355    c = PythonExampleComponent(name, path)
2356    reg_component(name, c)
2357
2358def mk_config():
2359    if ONLY_MAKEFILES:
2360        return
2361    config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
2362    global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED
2363    if IS_WINDOWS:
2364        config.write(
2365            'CC=cl\n'
2366            'CXX=cl\n'
2367            'CXX_OUT_FLAG=/Fo\n'
2368            'C_OUT_FLAG=/Fo\n'
2369            'OBJ_EXT=.obj\n'
2370            'LIB_EXT=.lib\n'
2371            'AR=lib\n'
2372            'AR_OUTFLAG=/OUT:\n'
2373            'EXE_EXT=.exe\n'
2374            'LINK=cl\n'
2375            'LINK_OUT_FLAG=/Fe\n'
2376            'SO_EXT=.dll\n'
2377            'SLINK=cl\n'
2378            'SLINK_OUT_FLAG=/Fe\n'
2379            'OS_DEFINES=/D _WINDOWS\n')
2380        extra_opt = ''
2381        link_extra_opt = ''
2382        if LOG_SYNC:
2383            extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt
2384        if SINGLE_THREADED:
2385            extra_opt = '%s /DSINGLE_THREAD' % extra_opt
2386        if GIT_HASH:
2387            extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
2388        if GUARD_CF:
2389            extra_opt = ' %s /guard:cf' % extra_opt
2390            link_extra_opt = ' %s /GUARD:CF' % link_extra_opt
2391        if STATIC_BIN:
2392            static_opt = '/MT'
2393        else:
2394            static_opt = '/MD'
2395        maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO'
2396        if DEBUG_MODE:
2397            static_opt = static_opt + 'd'
2398            config.write(
2399                'AR_FLAGS=/nologo\n'
2400                'LINK_FLAGS=/nologo %s\n'
2401                'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
2402            if VS_X64:
2403                config.write(
2404                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd %s %s\n' % (extra_opt, static_opt))
2405                config.write(
2406                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2407                    'SLINK_EXTRA_FLAGS=/link /DEBUG /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))
2408            elif VS_ARM:
2409                print("ARM on VS is unsupported")
2410                exit(1)
2411            else:
2412                config.write(
2413                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd /arch:SSE2 %s %s\n' % (extra_opt, static_opt))
2414                config.write(
2415                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2416                    'SLINK_EXTRA_FLAGS=/link /DEBUG /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))
2417        else:
2418            # Windows Release mode
2419            LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
2420            GL = ' /GL' if SLOW_OPTIMIZE else ''
2421            config.write(
2422                'AR_FLAGS=/nologo %s\n'
2423                'LINK_FLAGS=/nologo %s\n'
2424                'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt))
2425            if TRACE:
2426                extra_opt = '%s /D _TRACE ' % extra_opt
2427            if VS_X64:
2428                config.write(
2429                    'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /Gd /GF /Gy /TP %s %s\n' % (GL, extra_opt, static_opt))
2430                config.write(
2431                    'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
2432                    'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
2433            elif VS_ARM:
2434                print("ARM on VS is unsupported")
2435                exit(1)
2436            else:
2437                config.write(
2438                    'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /Gd /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
2439                config.write(
2440                    'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2441                    'SLINK_EXTRA_FLAGS=/link%s /DEBUG /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))
2442
2443        config.write('CFLAGS=$(CXXFLAGS)\n')
2444
2445        # End of Windows VS config.mk
2446        if is_verbose():
2447            print('64-bit:         %s' % is64())
2448            if is_java_enabled():
2449                print('JNI Bindings:   %s' % JNI_HOME)
2450                print('Java Compiler:  %s' % JAVAC)
2451            if is_ml_enabled():
2452                print('OCaml Compiler: %s' % OCAMLC)
2453                print('OCaml Find tool: %s' % OCAMLFIND)
2454                print('OCaml Native:   %s' % OCAMLOPT)
2455                print('OCaml Library:  %s' % OCAML_LIB)
2456    else:
2457        OS_DEFINES = ""
2458        ARITH = "internal"
2459        check_ar()
2460        CXX = find_cxx_compiler()
2461        CC  = find_c_compiler()
2462        SLIBEXTRAFLAGS = ''
2463#       SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
2464        EXE_EXT = ''
2465        LIB_EXT = '.a'
2466        if GPROF:
2467            CXXFLAGS = '%s -pg' % CXXFLAGS
2468            LDFLAGS  = '%s -pg' % LDFLAGS
2469        if GMP:
2470            test_gmp(CXX)
2471            ARITH = "gmp"
2472            CPPFLAGS = '%s -D_MP_GMP' % CPPFLAGS
2473            LDFLAGS  = '%s -lgmp' % LDFLAGS
2474            SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
2475        else:
2476            CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
2477        if GIT_HASH:
2478            CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
2479        CXXFLAGS = '%s -std=c++11' % CXXFLAGS
2480        CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
2481        FPMATH = test_fpmath(CXX)
2482        CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
2483        if LOG_SYNC:
2484            CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
2485        if SINGLE_THREADED:
2486            CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS
2487        if DEBUG_MODE:
2488            CXXFLAGS     = '%s -g -Wall' % CXXFLAGS
2489            EXAMP_DEBUG_FLAG = '-g'
2490            CPPFLAGS     = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
2491        else:
2492            CXXFLAGS     = '%s -O3' % CXXFLAGS
2493            if GPROF:
2494                CXXFLAGS     += '-fomit-frame-pointer'
2495            CPPFLAGS     = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
2496        if is_CXX_clangpp():
2497            CXXFLAGS   = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
2498        sysname, _, _, _, machine = os.uname()
2499        if sysname == 'Darwin':
2500            SO_EXT         = '.dylib'
2501            SLIBFLAGS      = '-dynamiclib'
2502        elif sysname == 'Linux':
2503            CXXFLAGS       = '%s -D_LINUX_' % CXXFLAGS
2504            OS_DEFINES     = '-D_LINUX_'
2505            SO_EXT         = '.so'
2506            SLIBFLAGS      = '-shared'
2507            SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
2508        elif sysname == 'GNU':
2509            CXXFLAGS       = '%s -D_HURD_' % CXXFLAGS
2510            OS_DEFINES     = '-D_HURD_'
2511            SO_EXT         = '.so'
2512            SLIBFLAGS      = '-shared'
2513        elif sysname == 'DragonFly':
2514            CXXFLAGS       = '%s -D_DRAGONFLY_' % CXXFLAGS
2515            OS_DEFINES     = '-D_DRAGONFLY_'
2516            SO_EXT         = '.so'
2517            SLIBFLAGS      = '-shared'
2518        elif sysname == 'NetBSD':
2519            CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
2520            OS_DEFINES     = '-D_NETBSD_'
2521            SO_EXT         = '.so'
2522            SLIBFLAGS      = '-shared'
2523        elif sysname == 'OpenBSD':
2524            CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
2525            OS_DEFINES     = '-D_OPENBSD_'
2526            SO_EXT         = '.so'
2527            SLIBFLAGS      = '-shared'
2528        elif sysname  == 'SunOS':
2529            CXXFLAGS       = '%s -D_SUNOS_' % CXXFLAGS
2530            OS_DEFINES     = '-D_SUNOS_'
2531            SO_EXT         = '.so'
2532            SLIBFLAGS      = '-shared'
2533            SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
2534        elif sysname.startswith('CYGWIN'):
2535            CXXFLAGS       = '%s -D_CYGWIN' % CXXFLAGS
2536            OS_DEFINES     = '-D_CYGWIN'
2537            SO_EXT         = '.dll'
2538            SLIBFLAGS      = '-shared'
2539        elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
2540            CXXFLAGS       = '%s -D_MINGW' % CXXFLAGS
2541            OS_DEFINES     = '-D_MINGW'
2542            SO_EXT         = '.dll'
2543            SLIBFLAGS      = '-shared'
2544            EXE_EXT        = '.exe'
2545            LIB_EXT        = '.lib'
2546        else:
2547            raise MKException('Unsupported platform: %s' % sysname)
2548        if is64():
2549            if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
2550                CXXFLAGS     = '%s -fPIC' % CXXFLAGS
2551            if sysname == 'Linux':
2552                CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
2553        elif not LINUX_X64:
2554            CXXFLAGS     = '%s -m32' % CXXFLAGS
2555            LDFLAGS      = '%s -m32' % LDFLAGS
2556            SLIBFLAGS    = '%s -m32' % SLIBFLAGS
2557        if TRACE or DEBUG_MODE:
2558            CPPFLAGS     = '%s -D_TRACE' % CPPFLAGS
2559        if is_cygwin_mingw():
2560            # when cross-compiling with MinGW, we need to statically link its standard libraries
2561            # and to make it create an import library.
2562            SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS
2563            LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
2564        if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
2565            CXXFLAGS = '%s -fpic' % CXXFLAGS
2566
2567        config.write('PREFIX=%s\n' % PREFIX)
2568        config.write('CC=%s\n' % CC)
2569        config.write('CXX=%s\n' % CXX)
2570        config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
2571        config.write('CFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS.replace('-std=c++11', '')))
2572        config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
2573        config.write('CXX_OUT_FLAG=-o \n')
2574        config.write('C_OUT_FLAG=-o \n')
2575        config.write('OBJ_EXT=.o\n')
2576        config.write('LIB_EXT=%s\n' % LIB_EXT)
2577        config.write('AR=%s\n' % AR)
2578        config.write('AR_FLAGS=rcs\n')
2579        config.write('AR_OUTFLAG=\n')
2580        config.write('EXE_EXT=%s\n' % EXE_EXT)
2581        config.write('LINK=%s\n' % CXX)
2582        config.write('LINK_FLAGS=\n')
2583        config.write('LINK_OUT_FLAG=-o \n')
2584        if is_linux() and (build_static_lib() or build_static_bin()):
2585            config.write('LINK_EXTRA_FLAGS=-Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive %s\n' % LDFLAGS)
2586        else:
2587            config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
2588        config.write('SO_EXT=%s\n' % SO_EXT)
2589        config.write('SLINK=%s\n' % CXX)
2590        config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
2591        config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
2592        config.write('SLINK_OUT_FLAG=-o \n')
2593        config.write('OS_DEFINES=%s\n' % OS_DEFINES)
2594        if is_verbose():
2595            print('Host platform:  %s' % sysname)
2596            print('C++ Compiler:   %s' % CXX)
2597            print('C Compiler  :   %s' % CC)
2598            if is_cygwin_mingw():
2599                print('MinGW32 cross:  %s' % (is_cygwin_mingw()))
2600            print('Archive Tool:   %s' % AR)
2601            print('Arithmetic:     %s' % ARITH)
2602            print('Prefix:         %s' % PREFIX)
2603            print('64-bit:         %s' % is64())
2604            print('FP math:        %s' % FPMATH)
2605            print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
2606            if GPROF:
2607                print('gprof:          enabled')
2608            print('Python version: %s' % distutils.sysconfig.get_python_version())
2609            if is_java_enabled():
2610                print('JNI Bindings:   %s' % JNI_HOME)
2611                print('Java Compiler:  %s' % JAVAC)
2612            if is_ml_enabled():
2613                print('OCaml Compiler: %s' % OCAMLC)
2614                print('OCaml Find tool: %s' % OCAMLFIND)
2615                print('OCaml Native:   %s' % OCAMLOPT)
2616                print('OCaml Library:  %s' % OCAML_LIB)
2617            if is_dotnet_core_enabled():
2618                print('C# Compiler:    %s' % DOTNET)
2619
2620    config.close()
2621
2622def mk_install(out):
2623    out.write('install: ')
2624    for c in get_components():
2625        c.mk_install_deps(out)
2626        out.write(' ')
2627    out.write('\n')
2628    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
2629    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
2630    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
2631    for c in get_components():
2632        c.mk_install(out)
2633    out.write('\t@echo Z3 was successfully installed.\n')
2634    out.write('\n')
2635
2636def mk_uninstall(out):
2637    out.write('uninstall:\n')
2638    for c in get_components():
2639        c.mk_uninstall(out)
2640    out.write('\t@echo Z3 was successfully uninstalled.\n')
2641    out.write('\n')
2642
2643# Generate the Z3 makefile
2644def mk_makefile():
2645    mk_dir(BUILD_DIR)
2646    mk_config()
2647    if VERBOSE:
2648        print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile'))
2649    out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w')
2650    out.write('# Automatically generated file.\n')
2651    out.write('include config.mk\n')
2652    # Generate :all rule
2653    out.write('all:')
2654    for c in get_components():
2655        if c.main_component():
2656            out.write(' %s' % c.name)
2657    out.write('\n\t@echo Z3 was successfully built.\n')
2658    out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python'))
2659    pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
2660    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))
2661    if not IS_WINDOWS:
2662        out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
2663        out.write('\t@echo "    sudo make install"\n\n')
2664        # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
2665        # out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
2666    # Generate :examples rule
2667    out.write('examples:')
2668    for c in get_components():
2669        if c.is_example():
2670            out.write(' _ex_%s' % c.name)
2671    out.write('\n\t@echo Z3 examples were successfully built.\n')
2672    # Generate components
2673    for c in get_components():
2674        c.mk_makefile(out)
2675    # Generate install/uninstall rules if not WINDOWS
2676    if not IS_WINDOWS:
2677        mk_install(out)
2678        mk_uninstall(out)
2679    for c in get_components():
2680        c.final_info()
2681    out.close()
2682    # Finalize
2683    if VERBOSE:
2684        print("Makefile was successfully generated.")
2685        if DEBUG_MODE:
2686            print("  compilation mode: Debug")
2687        else:
2688            print("  compilation mode: Release")
2689        if IS_WINDOWS:
2690            if VS_X64:
2691                print("  platform: x64\n")
2692                print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
2693            elif VS_ARM:
2694                print("  platform: ARM\n")
2695                print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
2696            else:
2697                print("  platform: x86")
2698                print("To build Z3, open a [Visual Studio Command Prompt], then")
2699            print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR))
2700            print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
2701        else:
2702            print("Type 'cd %s; make' to build Z3" % BUILD_DIR)
2703
2704# Generate automatically generated source code
2705def mk_auto_src():
2706    if not ONLY_MAKEFILES:
2707        exec_pyg_scripts()
2708        mk_pat_db()
2709        mk_all_install_tactic_cpps()
2710        mk_all_mem_initializer_cpps()
2711        mk_all_gparams_register_modules()
2712
2713
2714def _execfile(file, globals=globals(), locals=locals()):
2715    if sys.version < "2.7":
2716        execfile(file, globals, locals)
2717    else:
2718        with open(file, "r") as fh:
2719            exec(fh.read()+"\n", globals, locals)
2720
2721# Execute python auxiliary scripts that generate extra code for Z3.
2722def exec_pyg_scripts():
2723    for root, dirs, files in os.walk('src'):
2724        for f in files:
2725            if f.endswith('.pyg'):
2726                script = os.path.join(root, f)
2727                generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root)
2728                if is_verbose():
2729                    print("Generated '{}'".format(generated_file))
2730
2731# TODO: delete after src/ast/pattern/expr_pattern_match
2732# database.smt ==> database.h
2733def mk_pat_db():
2734    c = get_component(PATTERN_COMPONENT)
2735    fin  = os.path.join(c.src_dir, 'database.smt2')
2736    fout = os.path.join(c.src_dir, 'database.h')
2737    mk_genfile_common.mk_pat_db_internal(fin, fout)
2738    if VERBOSE:
2739        print("Generated '{}'".format(fout))
2740
2741# Update version numbers
2742def update_version():
2743    major = VER_MAJOR
2744    minor = VER_MINOR
2745    build = VER_BUILD
2746    revision = VER_TWEAK
2747    if major is None or minor is None or build is None or revision is None:
2748        raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
2749    if not ONLY_MAKEFILES:
2750        mk_version_dot_h(major, minor, build, revision)
2751        mk_all_assembly_infos(major, minor, build, revision)
2752        mk_def_files()
2753
2754def get_full_version_string(major, minor, build, revision):
2755    global GIT_HASH, GIT_DESCRIBE
2756    res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
2757    if GIT_HASH:
2758        res += " " + GIT_HASH
2759    if GIT_DESCRIBE:
2760        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
2761        res += " " + branch + " " + check_output(['git', 'describe'])
2762    return '"' + res + '"'
2763
2764# Update files with the version number
2765def mk_version_dot_h(major, minor, build, revision):
2766    c = get_component(UTIL_COMPONENT)
2767    version_template = os.path.join(c.src_dir, 'z3_version.h.in')
2768    version_header_output = os.path.join(c.src_dir, 'z3_version.h')
2769    # Note the substitution names are what is used by the CMake
2770    # builds system. If you change these you should change them
2771    # in the CMake build too
2772    configure_file(version_template, version_header_output,
2773        { 'Z3_VERSION_MAJOR': str(major),
2774          'Z3_VERSION_MINOR': str(minor),
2775          'Z3_VERSION_PATCH': str(build),
2776          'Z3_VERSION_TWEAK': str(revision),
2777          'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision)
2778        }
2779    )
2780    if VERBOSE:
2781        print("Generated '%s'" % version_header_output)
2782
2783# Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template
2784def mk_all_assembly_infos(major, minor, build, revision):
2785    for c in get_components():
2786        if c.has_assembly_info():
2787            c.make_assembly_info(major, minor, build, revision)
2788
2789def get_header_files_for_components(component_src_dirs):
2790    assert isinstance(component_src_dirs, list)
2791    h_files_full_path = []
2792    for component_src_dir in sorted(component_src_dirs):
2793        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
2794        h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
2795        h_files_full_path.extend(h_files)
2796    return h_files_full_path
2797
2798def mk_install_tactic_cpp(cnames, path):
2799    component_src_dirs = []
2800    for cname in cnames:
2801        print("Component %s" % cname)
2802        c = get_component(cname)
2803        component_src_dirs.append(c.src_dir)
2804    h_files_full_path = get_header_files_for_components(component_src_dirs)
2805    generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(h_files_full_path, path)
2806    if VERBOSE:
2807        print("Generated '{}'".format(generated_file))
2808
2809def mk_all_install_tactic_cpps():
2810    if not ONLY_MAKEFILES:
2811        for c in get_components():
2812            if c.require_install_tactics():
2813                cnames = []
2814                cnames.extend(c.deps)
2815                cnames.append(c.name)
2816                mk_install_tactic_cpp(cnames, c.src_dir)
2817
2818def mk_mem_initializer_cpp(cnames, path):
2819    component_src_dirs = []
2820    for cname in cnames:
2821        c = get_component(cname)
2822        component_src_dirs.append(c.src_dir)
2823    h_files_full_path = get_header_files_for_components(component_src_dirs)
2824    generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path)
2825    if VERBOSE:
2826        print("Generated '{}'".format(generated_file))
2827
2828def mk_all_mem_initializer_cpps():
2829    if not ONLY_MAKEFILES:
2830        for c in get_components():
2831            if c.require_mem_initializer():
2832                cnames = []
2833                cnames.extend(c.deps)
2834                cnames.append(c.name)
2835                mk_mem_initializer_cpp(cnames, c.src_dir)
2836
2837def mk_gparams_register_modules(cnames, path):
2838    component_src_dirs = []
2839    for cname in cnames:
2840        c = get_component(cname)
2841        component_src_dirs.append(c.src_dir)
2842    h_files_full_path = get_header_files_for_components(component_src_dirs)
2843    generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path)
2844    if VERBOSE:
2845        print("Generated '{}'".format(generated_file))
2846
2847def mk_all_gparams_register_modules():
2848    if not ONLY_MAKEFILES:
2849        for c in get_components():
2850            if c.require_mem_initializer():
2851                cnames = []
2852                cnames.extend(c.deps)
2853                cnames.append(c.name)
2854                mk_gparams_register_modules(cnames, c.src_dir)
2855
2856# Generate a .def based on the files at c.export_files slot.
2857def mk_def_file(c):
2858    defname = '%s.def' % os.path.join(c.src_dir, c.name)
2859    dll_name = c.dll_name
2860    export_header_files = []
2861    for dot_h in c.export_files:
2862        dot_h_c = c.find_file(dot_h, c.name)
2863        api = os.path.join(dot_h_c.src_dir, dot_h)
2864        export_header_files.append(api)
2865    mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files)
2866    if VERBOSE:
2867        print("Generated '%s'" % defname)
2868
2869def mk_def_files():
2870    if not ONLY_MAKEFILES:
2871        for c in get_components():
2872            if c.require_def_file():
2873                mk_def_file(c)
2874
2875def cp_z3py_to_build():
2876    mk_dir(BUILD_DIR)
2877    mk_dir(os.path.join(BUILD_DIR, 'python'))
2878    z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3')
2879    z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3')
2880
2881    # Erase existing .pyc files
2882    for root, dirs, files in os.walk(Z3PY_SRC_DIR):
2883        for f in files:
2884            if f.endswith('.pyc'):
2885                rmf(os.path.join(root, f))
2886    # Compile Z3Py files
2887    if compileall.compile_dir(z3py_src, force=1) != 1:
2888        raise MKException("failed to compile Z3Py sources")
2889    if is_verbose:
2890        print("Generated python bytecode")
2891    # Copy sources to build
2892    mk_dir(z3py_dest)
2893    for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)):
2894        shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py))
2895        if is_verbose():
2896            print("Copied '%s'" % py)
2897    # Python 2.x support
2898    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)):
2899        shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc))
2900        if is_verbose():
2901            print("Copied '%s'" % pyc)
2902    # Python 3.x support
2903    src_pycache = os.path.join(z3py_src, '__pycache__')
2904    target_pycache = os.path.join(z3py_dest, '__pycache__')
2905    if os.path.exists(src_pycache):
2906        for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)):
2907            mk_dir(target_pycache)
2908            shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
2909            if is_verbose():
2910                print("Copied '%s'" % pyc)
2911    # Copy z3test.py
2912    shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py'))
2913
2914def mk_bindings(api_files):
2915    if not ONLY_MAKEFILES:
2916        mk_z3consts_py(api_files)
2917        new_api_files = []
2918        api = get_component(API_COMPONENT)
2919        for api_file in api_files:
2920            api_file_path = api.find_file(api_file, api.name)
2921            new_api_files.append(os.path.join(api_file_path.src_dir, api_file))
2922        g = globals()
2923        g["API_FILES"] = new_api_files
2924        if is_java_enabled():
2925            check_java()
2926            mk_z3consts_java(api_files)
2927        # Generate some of the bindings and "api" module files
2928        import update_api
2929        dotnet_output_dir = None
2930        if is_dotnet_core_enabled():
2931          dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet')
2932          mk_dir(dotnet_output_dir)
2933        java_output_dir = None
2934        java_package_name = None
2935        if is_java_enabled():
2936          java_output_dir = get_component('java').src_dir
2937          java_package_name = get_component('java').package_name
2938        ml_output_dir = None
2939        if is_ml_enabled():
2940          ml_output_dir = get_component('ml').src_dir
2941        if is_js_enabled():
2942          set_z3js_dir("api/js")
2943          js_output_dir = get_component('js').src_dir
2944        # Get the update_api module to do the work for us
2945        update_api.generate_files(api_files=new_api_files,
2946          api_output_dir=get_component('api').src_dir,
2947          z3py_output_dir=get_z3py_dir(),
2948          dotnet_output_dir=dotnet_output_dir,
2949          java_output_dir=java_output_dir,
2950          java_package_name=java_package_name,
2951          js_output_dir=get_z3js_dir(),
2952          ml_output_dir=ml_output_dir,
2953          ml_src_dir=ml_output_dir
2954        )
2955        cp_z3py_to_build()
2956        if is_ml_enabled():
2957            check_ml()
2958            mk_z3consts_ml(api_files)
2959        if  is_dotnet_core_enabled():
2960            check_dotnet_core()
2961            mk_z3consts_dotnet(api_files, dotnet_output_dir)
2962
2963# Extract enumeration types from API files, and add python definitions.
2964def mk_z3consts_py(api_files):
2965    if Z3PY_SRC_DIR is None:
2966        raise MKException("You must invoke set_z3py_dir(path):")
2967    full_path_api_files = []
2968    api_dll = get_component(Z3_DLL_COMPONENT)
2969    for api_file in api_files:
2970        api_file_c = api_dll.find_file(api_file, api_dll.name)
2971        api_file   = os.path.join(api_file_c.src_dir, api_file)
2972        full_path_api_files.append(api_file)
2973    generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
2974    if VERBOSE:
2975        print("Generated '{}".format(generated_file))
2976
2977# Extract enumeration types from z3_api.h, and add .Net definitions
2978def mk_z3consts_dotnet(api_files, output_dir):
2979    dotnet = get_component(DOTNET_COMPONENT)
2980    if not dotnet:
2981       dotnet = get_component(DOTNET_CORE_COMPONENT)
2982    full_path_api_files = []
2983    for api_file in api_files:
2984        api_file_c = dotnet.find_file(api_file, dotnet.name)
2985        api_file   = os.path.join(api_file_c.src_dir, api_file)
2986        full_path_api_files.append(api_file)
2987    generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir)
2988    if VERBOSE:
2989        print("Generated '{}".format(generated_file))
2990
2991# Extract enumeration types from z3_api.h, and add Java definitions
2992def mk_z3consts_java(api_files):
2993    java = get_component(JAVA_COMPONENT)
2994    full_path_api_files = []
2995    for api_file in api_files:
2996        api_file_c = java.find_file(api_file, java.name)
2997        api_file   = os.path.join(api_file_c.src_dir, api_file)
2998        full_path_api_files.append(api_file)
2999    generated_files = mk_genfile_common.mk_z3consts_java_internal(
3000        full_path_api_files,
3001        java.package_name,
3002        java.src_dir)
3003    if VERBOSE:
3004        for generated_file in generated_files:
3005            print("Generated '{}'".format(generated_file))
3006
3007# Extract enumeration types from z3_api.h, and add ML definitions
3008def mk_z3consts_ml(api_files):
3009    ml = get_component(ML_COMPONENT)
3010    full_path_api_files = []
3011    for api_file in api_files:
3012        api_file_c = ml.find_file(api_file, ml.name)
3013        api_file   = os.path.join(api_file_c.src_dir, api_file)
3014        full_path_api_files.append(api_file)
3015    generated_file = mk_genfile_common.mk_z3consts_ml_internal(
3016        full_path_api_files,
3017        ml.src_dir)
3018    if VERBOSE:
3019        print ('Generated "%s"' % generated_file)
3020
3021def mk_gui_str(id):
3022    return '4D2F40D8-E5F9-473B-B548-%012d' % id
3023
3024def get_platform_toolset_str():
3025    default = 'v110';
3026    vstr = check_output(['msbuild', '/ver'])
3027    lines = vstr.split('\n')
3028    lline = lines[-1]
3029    tokens = lline.split('.')
3030    if len(tokens) < 2:
3031        return default
3032    else:
3033        if tokens[0] == "15":
3034            # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
3035            return "v141"
3036        else:
3037            return 'v' + tokens[0] + tokens[1]
3038
3039def mk_vs_proj_property_groups(f, name, target_ext, type):
3040    f.write('  <ItemGroup Label="ProjectConfigurations">\n')
3041    f.write('    <ProjectConfiguration Include="Debug|Win32">\n')
3042    f.write('      <Configuration>Debug</Configuration>\n')
3043    f.write('      <Platform>Win32</Platform>\n')
3044    f.write('    </ProjectConfiguration>\n')
3045    f.write('    <ProjectConfiguration Include="Release|Win32">\n')
3046    f.write('      <Configuration>Release</Configuration>\n')
3047    f.write('      <Platform>Win32</Platform>\n')
3048    f.write('    </ProjectConfiguration>\n')
3049    f.write('  </ItemGroup>\n')
3050    f.write('  <PropertyGroup Label="Globals">\n')
3051    f.write('    <ProjectGuid>{%s}</ProjectGuid>\n' % mk_gui_str(0))
3052    f.write('    <ProjectName>%s</ProjectName>\n' % name)
3053    f.write('    <Keyword>Win32Proj</Keyword>\n')
3054    f.write('    <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
3055    f.write('  </PropertyGroup>\n')
3056    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
3057    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
3058    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
3059    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
3060    f.write('    <UseOfMfc>false</UseOfMfc>\n')
3061    f.write('  </PropertyGroup>\n')
3062    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n')
3063    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
3064    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
3065    f.write('    <UseOfMfc>false</UseOfMfc>\n')
3066    f.write('  </PropertyGroup>\n')
3067    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
3068    f.write('  <ImportGroup Label="ExtensionSettings" />\n')
3069    f.write('   <ImportGroup Label="PropertySheets">\n')
3070    f.write('    <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
3071    f.write('  <PropertyGroup Label="UserMacros" />\n')
3072    f.write('  <PropertyGroup>\n')
3073    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
3074    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
3075    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
3076    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
3077    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
3078    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
3079    f.write('  </PropertyGroup>\n')
3080    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3081    f.write('        <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
3082    f.write('  </PropertyGroup>\n')
3083    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3084    f.write('    <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
3085    f.write('  </PropertyGroup>\n')
3086
3087
3088def mk_vs_proj_cl_compile(f, name, components, debug):
3089    f.write('    <ClCompile>\n')
3090    f.write('      <Optimization>Disabled</Optimization>\n')
3091    if debug:
3092        f.write('      <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
3093    else:
3094        f.write('      <PreprocessorDefinitions>WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
3095    if VS_PAR:
3096        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
3097        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
3098    else:
3099        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
3100    f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
3101    f.write('      <WarningLevel>Level3</WarningLevel>\n')
3102    if debug:
3103        f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
3104    else:
3105        f.write('      <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')
3106    f.write('      <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
3107    f.write('      <AdditionalIncludeDirectories>')
3108    deps = find_all_deps(name, components)
3109    first = True
3110    for dep in deps:
3111        if first:
3112            first = False
3113        else:
3114            f.write(';')
3115        f.write(get_component(dep).to_src_dir)
3116    f.write(';%s\n' % os.path.join(REV_BUILD_DIR, SRC_DIR))
3117    f.write('</AdditionalIncludeDirectories>\n')
3118    f.write('    </ClCompile>\n')
3119
3120def mk_vs_proj_dep_groups(f, name, components):
3121    f.write('  <ItemGroup>\n')
3122    deps = find_all_deps(name, components)
3123    for dep in deps:
3124        dep = get_component(dep)
3125        for cpp in filter(lambda f: f.endswith('.cpp'), os.listdir(dep.src_dir)):
3126            f.write('    <ClCompile Include="%s" />\n' % os.path.join(dep.to_src_dir, cpp))
3127    f.write('  </ItemGroup>\n')
3128
3129def mk_vs_proj_link_exe(f, name, debug):
3130    f.write('    <Link>\n')
3131    f.write('      <OutputFile>$(OutDir)%s.exe</OutputFile>\n' % name)
3132    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
3133    f.write('      <SubSystem>Console</SubSystem>\n')
3134    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
3135    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
3136    f.write('      <DataExecutionPrevention/>\n')
3137    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
3138    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
3139    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')
3140    f.write('    </Link>\n')
3141
3142def mk_vs_proj(name, components):
3143    if not VS_PROJ:
3144        return
3145    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
3146    modes=['Debug', 'Release']
3147    PLATFORMS=['Win32']
3148    f = open(proj_name, 'w')
3149    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
3150    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
3151    mk_vs_proj_property_groups(f, name, 'exe', 'Application')
3152    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3153    mk_vs_proj_cl_compile(f, name, components, debug=True)
3154    mk_vs_proj_link_exe(f, name, debug=True)
3155    f.write('  </ItemDefinitionGroup>\n')
3156    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3157    mk_vs_proj_cl_compile(f, name, components, debug=False)
3158    mk_vs_proj_link_exe(f, name, debug=False)
3159    f.write('  </ItemDefinitionGroup>\n')
3160    mk_vs_proj_dep_groups(f, name, components)
3161    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
3162    f.write('  <ImportGroup Label="ExtensionTargets">\n')
3163    f.write('  </ImportGroup>\n')
3164    f.write('</Project>\n')
3165    f.close()
3166    if is_verbose():
3167        print("Generated '%s'" % proj_name)
3168
3169def mk_vs_proj_link_dll(f, name, debug):
3170    f.write('    <Link>\n')
3171    f.write('      <OutputFile>$(OutDir)%s.dll</OutputFile>\n' % name)
3172    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
3173    f.write('      <SubSystem>Console</SubSystem>\n')
3174    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
3175    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
3176    f.write('      <DataExecutionPrevention/>\n')
3177    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
3178    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
3179    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')
3180    f.write('      <ModuleDefinitionFile>%s</ModuleDefinitionFile>' % os.path.join(get_component('api_dll').to_src_dir, 'api_dll.def'))
3181    f.write('    </Link>\n')
3182
3183def mk_vs_proj_dll(name, components):
3184    if not VS_PROJ:
3185        return
3186    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
3187    modes=['Debug', 'Release']
3188    PLATFORMS=['Win32']
3189    f = open(proj_name, 'w')
3190    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
3191    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
3192    mk_vs_proj_property_groups(f, name, 'dll', 'DynamicLibrary')
3193    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3194    mk_vs_proj_cl_compile(f, name, components, debug=True)
3195    mk_vs_proj_link_dll(f, name, debug=True)
3196    f.write('  </ItemDefinitionGroup>\n')
3197    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3198    mk_vs_proj_cl_compile(f, name, components, debug=False)
3199    mk_vs_proj_link_dll(f, name, debug=False)
3200    f.write('  </ItemDefinitionGroup>\n')
3201    mk_vs_proj_dep_groups(f, name, components)
3202    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
3203    f.write('  <ImportGroup Label="ExtensionTargets">\n')
3204    f.write('  </ImportGroup>\n')
3205    f.write('</Project>\n')
3206    f.close()
3207    if is_verbose():
3208        print("Generated '%s'" % proj_name)
3209
3210def mk_win_dist(build_path, dist_path):
3211    for c in get_components():
3212        c.mk_win_dist(build_path, dist_path)
3213
3214def mk_unix_dist(build_path, dist_path):
3215    for c in get_components():
3216        c.mk_unix_dist(build_path, dist_path)
3217    # Add Z3Py to bin directory
3218    for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
3219        shutil.copy(os.path.join(build_path, pyc),
3220                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
3221
3222class MakeRuleCmd(object):
3223    """
3224        These class methods provide a convenient way to emit frequently
3225        needed commands used in Makefile rules
3226        Note that several of the method are meant for use during ``make
3227        install`` and ``make uninstall``.  These methods correctly use
3228        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable
3229        to writing commands manually which can be error prone.
3230    """
3231    @classmethod
3232    def install_root(cls):
3233        """
3234            Returns a string that will expand to the
3235            install location when used in a makefile rule.
3236        """
3237        # Note: DESTDIR is to support staged installs
3238        return "$(DESTDIR)$(PREFIX)/"
3239
3240    @classmethod
3241    def _is_str(cls, obj):
3242        if sys.version_info.major > 2:
3243            # Python 3 or newer. Strings are always unicode and of type str
3244            return isinstance(obj, str)
3245        else:
3246            # Python 2. Has byte-string and unicode representation, allow both
3247            return isinstance(obj, str) or isinstance(obj, unicode)
3248
3249    @classmethod
3250    def _install_root(cls, path, in_prefix, out, is_install=True):
3251        if not in_prefix:
3252            # The Python bindings on OSX are sometimes not installed inside the prefix.
3253            install_root = "$(DESTDIR)"
3254            action_string = 'install' if is_install else 'uninstall'
3255            cls.write_cmd(out, 'echo "WARNING: {}ing files/directories ({}) that are not in the install prefix ($(PREFIX))."'.format(
3256                    action_string, path))
3257            #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
3258            #        action_string, 'to' if is_install else 'from', path, PREFIX))
3259        else:
3260            # assert not os.path.isabs(path)
3261            install_root = cls.install_root()
3262        return install_root
3263
3264    @classmethod
3265    def install_files(cls, out, src_pattern, dest, in_prefix=True):
3266        assert len(dest) > 0
3267        assert cls._is_str(src_pattern)
3268        assert not ' ' in src_pattern
3269        assert cls._is_str(dest)
3270        assert not ' ' in dest
3271        assert not os.path.isabs(src_pattern)
3272        install_root = cls._install_root(dest, in_prefix, out)
3273
3274        cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
3275            src_pattern=src_pattern,
3276            install_root=install_root,
3277            dest=dest))
3278
3279    @classmethod
3280    def remove_installed_files(cls, out, pattern, in_prefix=True):
3281        assert len(pattern) > 0
3282        assert cls._is_str(pattern)
3283        assert not ' ' in pattern
3284        install_root = cls._install_root(pattern, in_prefix, out, is_install=False)
3285
3286        cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
3287            install_root=install_root,
3288            pattern=pattern))
3289
3290    @classmethod
3291    def make_install_directory(cls, out, dir, in_prefix=True):
3292        assert len(dir) > 0
3293        assert cls._is_str(dir)
3294        assert not ' ' in dir
3295        install_root = cls._install_root(dir, in_prefix, out)
3296
3297        if is_windows():
3298            cls.write_cmd(out, "IF NOT EXIST {dir} (mkdir {dir})".format(
3299                install_root=install_root,
3300                dir=dir))
3301        else:
3302            cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
3303                install_root=install_root,
3304                dir=dir))
3305
3306    @classmethod
3307    def _is_path_prefix_of(cls, temp_path, target_as_abs):
3308        """
3309            Returns True iff ``temp_path`` is a path prefix
3310            of ``target_as_abs``
3311        """
3312        assert cls._is_str(temp_path)
3313        assert cls._is_str(target_as_abs)
3314        assert len(temp_path) > 0
3315        assert len(target_as_abs) > 0
3316        assert os.path.isabs(temp_path)
3317        assert os.path.isabs(target_as_abs)
3318
3319        # Need to stick extra slash in front otherwise we might think that
3320        # ``/lib`` is a prefix of ``/lib64``.  Of course if ``temp_path ==
3321        # '/'`` then we shouldn't else we would check if ``//`` (rather than
3322        # ``/``) is a prefix of ``/lib64``, which would fail.
3323        if len(temp_path) > 1:
3324            temp_path += os.sep
3325        return target_as_abs.startswith(temp_path)
3326
3327    @classmethod
3328    def create_relative_symbolic_link(cls, out, target, link_name):
3329        assert cls._is_str(target)
3330        assert cls._is_str(link_name)
3331        assert len(target) > 0
3332        assert len(link_name) > 0
3333        assert not os.path.isabs(target)
3334        assert not os.path.isabs(link_name)
3335
3336        # We can't test to see if link_name is a file or directory
3337        # because it may not exist yet. Instead follow the convention
3338        # that if there is a leading slash target is a directory otherwise
3339        # it's a file
3340        if link_name[-1] != '/':
3341            # link_name is a file
3342            temp_path = os.path.dirname(link_name)
3343        else:
3344            # link_name is a directory
3345            temp_path = link_name[:-1]
3346        temp_path = '/' + temp_path
3347        relative_path = ""
3348        targetAsAbs = '/' + target
3349        assert os.path.isabs(targetAsAbs)
3350        assert os.path.isabs(temp_path)
3351        # Keep walking up the directory tree until temp_path
3352        # is a prefix of targetAsAbs
3353        while not cls._is_path_prefix_of(temp_path, targetAsAbs):
3354            assert temp_path != '/'
3355            temp_path = os.path.dirname(temp_path)
3356            relative_path += '../'
3357
3358        # Now get the path from the common prefix directory to the target
3359        target_from_prefix = targetAsAbs[len(temp_path):]
3360        relative_path += target_from_prefix
3361        # Remove any double slashes
3362        relative_path = relative_path.replace('//','/')
3363        cls.create_symbolic_link(out, relative_path, link_name)
3364
3365    @classmethod
3366    def create_symbolic_link(cls, out, target, link_name):
3367        assert cls._is_str(target)
3368        assert cls._is_str(link_name)
3369        assert not os.path.isabs(target)
3370
3371        cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
3372            target=target,
3373            install_root=cls.install_root(),
3374            link_name=link_name))
3375
3376    # TODO: Refactor all of the build system to emit commands using this
3377    # helper to simplify code. This will also let us replace ``@`` with
3378    # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
3379    # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
3380    # would be very helpful for debugging.
3381    @classmethod
3382    def write_cmd(cls, out, line):
3383        out.write("\t@{}\n".format(line))
3384
3385def strip_path_prefix(path, prefix):
3386    if path.startswith(prefix):
3387        stripped_path = path[len(prefix):]
3388        stripped_path.replace('//','/')
3389        if stripped_path[0] == '/':
3390            stripped_path = stripped_path[1:]
3391        assert not os.path.isabs(stripped_path)
3392        return stripped_path
3393    else:
3394        return path
3395
3396def configure_file(template_file_path, output_file_path, substitutions):
3397    """
3398        Read a template file ``template_file_path``, perform substitutions
3399        found in the ``substitutions`` dictionary and write the result to
3400        the output file ``output_file_path``.
3401        The template file should contain zero or more template strings of the
3402        form ``@NAME@``.
3403        The substitutions dictionary maps old strings (without the ``@``
3404        symbols) to their replacements.
3405    """
3406    assert isinstance(template_file_path, str)
3407    assert isinstance(output_file_path, str)
3408    assert isinstance(substitutions, dict)
3409    assert len(template_file_path) > 0
3410    assert len(output_file_path) > 0
3411    print("Generating {} from {}".format(output_file_path, template_file_path))
3412
3413    if not os.path.exists(template_file_path):
3414        raise MKException('Could not find template file "{}"'.format(template_file_path))
3415
3416    # Read whole template file into string
3417    template_string = None
3418    with open(template_file_path, 'r') as f:
3419        template_string = f.read()
3420
3421    # Do replacements
3422    for (old_string, replacement) in substitutions.items():
3423        template_string = template_string.replace('@{}@'.format(old_string), replacement)
3424
3425    # Write the string to the file
3426    with open(output_file_path, 'w') as f:
3427        f.write(template_string)
3428
3429if __name__ == '__main__':
3430    import doctest
3431    doctest.testmod()
3432