From 650ea7b9ccd25c1ec3e372baae944a9a0faa73ba Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 11 Jan 2017 18:40:11 +0000 Subject: [PATCH 1/9] Bugfix for smt.core.extend_patterns --- src/smt/smt_solver.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 703e4489e..c843c2f78 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -103,6 +103,7 @@ namespace smt { virtual void assert_expr(expr * t, expr * a) { solver_na2as::assert_expr(t, a); + SASSERT(!m_name2assertion.contains(a)); get_manager().inc_ref(t); m_name2assertion.insert(a, t); } @@ -112,6 +113,17 @@ namespace smt { } virtual void pop_core(unsigned n) { + unsigned lvl = m_scopes.size(); + SASSERT(n <= lvl); + unsigned new_lvl = lvl - n; + unsigned old_sz = m_scopes[new_lvl]; + for (unsigned i = m_assumptions.size() - 1; i >= old_sz; i--) { + expr * key = m_assumptions[i].get(); + SASSERT(m_name2assertion.contains(key)); + expr * value = m_name2assertion.find(key); + m.dec_ref(value); + m_name2assertion.erase(key); + } m_context.pop(n); } @@ -274,6 +286,7 @@ namespace smt { unsigned sz = core.size(); for (unsigned i = 0; i < sz; i++) { expr_ref name(core[i], m); + SASSERT(m_name2assertion.contains(name)); expr_ref assrtn(m_name2assertion.find(name), m); collect_pattern_func_decls(assrtn, pattern_fds); } From f7ebe1604671e75925b841b397f51c185db03544 Mon Sep 17 00:00:00 2001 From: Daniel Perelman Date: Wed, 11 Jan 2017 16:56:28 -0800 Subject: [PATCH 2/9] Omit '.dll' from library name for DllImport. --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index b8978ff21..031b39c75 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -365,7 +365,7 @@ def mk_dotnet(dotnet): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public class LIB\n') dotnet.write(' {\n') - dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' + dotnet.write(' const string Z3_DLL_NAME = \"libz3\";\n' ' \n') dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') From 3370adcdffd93e00a08ef6dbdf44a3562cb7a1bc Mon Sep 17 00:00:00 2001 From: Daniel Perelman Date: Wed, 11 Jan 2017 17:02:26 -0800 Subject: [PATCH 3/9] Mark void DummyContracts as Conditional to avoid compiling their arguments. --- src/api/dotnet/core/DummyContracts.cs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs index e0002e5be..49b498b1a 100644 --- a/src/api/dotnet/core/DummyContracts.cs +++ b/src/api/dotnet/core/DummyContracts.cs @@ -44,15 +44,21 @@ namespace System.Diagnostics.Contracts public static class Contract { + [Conditional("false")] public static void Ensures(bool b) { } + [Conditional("false")] public static void Requires(bool b) { } + [Conditional("false")] public static void Assume(bool b, string msg) { } + [Conditional("false")] public static void Assert(bool b) { } public static bool ForAll(bool b) { return true; } public static bool ForAll(Object c, Func p) { return true; } public static bool ForAll(int from, int to, Predicate p) { return true; } + [Conditional("false")] public static void Invariant(bool b) { } public static T[] Result() { return new T[1]; } + [Conditional("false")] public static void EndContractBlock() { } public static T ValueAtReturn(out T v) { T[] t = new T[1]; v = t[0]; return v; } } From 2458db30cf0329128db4c92e79909284892619f0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Jan 2017 12:49:26 +0000 Subject: [PATCH 4/9] Corner-case fix for smt::solver::pop_core --- src/smt/smt_solver.cpp | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c843c2f78..f80ff09f4 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -113,16 +113,19 @@ namespace smt { } virtual void pop_core(unsigned n) { - unsigned lvl = m_scopes.size(); - SASSERT(n <= lvl); - unsigned new_lvl = lvl - n; - unsigned old_sz = m_scopes[new_lvl]; - for (unsigned i = m_assumptions.size() - 1; i >= old_sz; i--) { - expr * key = m_assumptions[i].get(); - SASSERT(m_name2assertion.contains(key)); - expr * value = m_name2assertion.find(key); - m.dec_ref(value); - m_name2assertion.erase(key); + unsigned cur_sz = m_assumptions.size(); + if (n > 0 && cur_sz > 0) { + unsigned lvl = m_scopes.size(); + SASSERT(n <= lvl); + unsigned new_lvl = lvl - n; + unsigned old_sz = m_scopes[new_lvl]; + for (unsigned i = cur_sz - 1; i >= old_sz; i--) { + expr * key = m_assumptions[i].get(); + SASSERT(m_name2assertion.contains(key)); + expr * value = m_name2assertion.find(key); + m.dec_ref(value); + m_name2assertion.erase(key); + } } m_context.pop(n); } From 43eb6cc022308c0d027c4053348b202c4420c0c2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Jan 2017 20:43:53 +0000 Subject: [PATCH 5/9] CI trigger From 37916fe7e9b17ff296de10e942ce68e548582ce6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Jan 2017 21:33:11 +0000 Subject: [PATCH 6/9] Update README.md --- README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/README.md b/README.md index 502b32147..204fb371e 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,12 @@ Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. I See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. +## Build status + +| Windows | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | +| ------- | ---------- | ---------- | ---------- | --- | +![windows-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) + [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #building-z3-using-cmake From d8e4966a11887bc22d7b84e8da251500860bd174 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Jan 2017 14:18:37 +0000 Subject: [PATCH 7/9] Added win64 build badge --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 204fb371e..e0821ac79 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | -| ------- | ---------- | ---------- | ---------- | --- | -![windows-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) +| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | +| ----------- | ----------- | ---------- | ---------- | ---------- | --- | +![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang From b30f3a6dbd570988f9cce3d949036ed0562782a3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Jan 2017 14:56:25 +0000 Subject: [PATCH 8/9] Separated win32/64 builds --- scripts/mk_win_dist.py | 88 +++++++++++++++++++++++++++++------------- 1 file changed, 61 insertions(+), 27 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 92d89480f..9d3abaf2c 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -29,6 +29,9 @@ DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False PYTHON_ENABLED=True +X86ONLY=False +X64ONLY=False +MAKEJOBS=getenv("MAKEJOBS", 24) def set_verbose(flag): global VERBOSE @@ -63,11 +66,13 @@ def display_help(): print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") + print(" --x86-only x86 dist only.") + print(" --x64-only x64 dist only.") exit(0) # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -77,7 +82,9 @@ def parse_options(): 'nodotnet', 'dotnet-key=', 'githash', - 'nopython' + 'nopython', + 'x86-only', + 'x64-only' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -100,6 +107,10 @@ def parse_options(): JAVA_ENABLED = False elif opt == '--githash': GIT_HASH = True + elif opt == '--x86-only' and not X64ONLY: + X86ONLY = True + elif opt == '--x64-only' and not X86ONLY: + X64ONLY = True else: raise MKException("Invalid command line option '%s'" % opt) set_build_dir(path) @@ -111,7 +122,8 @@ def check_build_dir(path): # Create a build directory using mk_make.py def mk_build_dir(path, x64): if not check_build_dir(path) or FORCE_MK: - opts = ["python", os.path.join('scripts', 'mk_make.py'), "--parallel=24", "-b", path] + parallel = '--parallel=' + MAKEJOBS + opts = ["python", os.path.join('scripts', 'mk_make.py'), parallel, "-b", path] if DOTNET_ENABLED: opts.append('--dotnet') if not DOTNET_KEY_FILE is None: @@ -160,7 +172,7 @@ def exec_cmds(cmds): return res # Compile Z3 (if x64 == True, then it builds it in x64 mode). -def mk_z3_core(x64): +def mk_z3(x64): cmds = [] if x64: cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64') @@ -172,9 +184,9 @@ def mk_z3_core(x64): if exec_cmds(cmds) != 0: raise MKException("Failed to make z3, x64: %s" % x64) -def mk_z3(): - mk_z3_core(False) - mk_z3_core(True) +def mk_z3s(): + mk_z3(False) + mk_z3(True) def get_z3_name(x64): major, minor, build, revision = get_version() @@ -187,7 +199,7 @@ def get_z3_name(x64): else: return 'z3-%s.%s.%s-%s-win' % (major, minor, build, platform) -def mk_dist_dir_core(x64): +def mk_dist_dir(x64): if x64: platform = "x64" build_path = BUILD_X64_DIR @@ -204,14 +216,14 @@ def mk_dist_dir_core(x64): if is_verbose(): print("Generated %s distribution folder at '%s'" % (platform, dist_path)) -def mk_dist_dir(): - mk_dist_dir_core(False) - mk_dist_dir_core(True) +def mk_dist_dirs(): + mk_dist_dir(False) + mk_dist_dir(True) def get_dist_path(x64): return get_z3_name(x64) -def mk_zip_core(x64): +def mk_zip(x64): dist_path = get_dist_path(x64) old = os.getcwd() try: @@ -228,7 +240,7 @@ def mk_zip_core(x64): os.chdir(old) # Create a zip file for each platform -def mk_zip(): +def mk_zips(): mk_zip_core(False) mk_zip_core(True) @@ -238,7 +250,7 @@ VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'), re.compile('msvcr.*\.dll')] # Copy Visual Studio Runtime libraries -def cp_vs_runtime_core(x64): +def cp_vs_runtime(x64): if x64: platform = "x64" @@ -262,27 +274,49 @@ def cp_vs_runtime_core(x64): if is_verbose(): print("Copied '%s' to '%s'" % (f, bin_dist_path)) -def cp_vs_runtime(): - cp_vs_runtime_core(True) - cp_vs_runtime_core(False) +def cp_vs_runtimes(): + cp_vs_runtime(True) + cp_vs_runtime(False) -def cp_license(): - shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(True))) - shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(False))) +def cp_license(x64): + shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(x64))) + +def cp_licenses(): + cp_license(True) + cp_license(False) # Entry point def main(): if os.name != 'nt': raise MKException("This script is for Windows only") + parse_options() check_vc_cmd_prompt() - mk_build_dirs() - mk_z3() - init_project_def() - mk_dist_dir() - cp_license() - cp_vs_runtime() - mk_zip() + + if X86ONLY: + mk_build_dir(BUILD_X86_DIR, False) + mk_z3(False) + init_project_def() + mk_dist_dir(False) + cp_license(False) + cp_vs_runtime(False) + mk_zip(False) + elif X64ONLY: + mk_build_dir(BUILD_X64_DIR, True) + mk_z3(True) + init_project_def() + mk_dist_dir(True) + cp_license(True) + cp_vs_runtime(True) + mk_zip(True) + else: + mk_build_dirs() + mk_z3s() + init_project_def() + mk_dist_dirs() + cp_licenses() + cp_vs_runtime() + mk_zip() main() From 340ba7780e012b45b4c5ce3be6077495f3591db5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Jan 2017 18:57:10 +0000 Subject: [PATCH 9/9] Added MAKEJOBS env var to mk_unix_dist.py --- scripts/mk_unix_dist.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 527797e66..488bc4364 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -27,6 +27,7 @@ DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False PYTHON_ENABLED=True +MAKEJOBS=getenv("MAKEJOBS", '8') def set_verbose(flag): global VERBOSE @@ -139,7 +140,7 @@ class cd: def mk_z3(): with cd(BUILD_DIR): try: - return subprocess.call(['make', '-j', '8']) + return subprocess.call(['make', '-j', MAKEJOBS]) except: return 1