diff --git a/README.md b/README.md index 502b32147..e0821ac79 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 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 [3]: #building-z3-using-cmake 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 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() 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') 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; } } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 703e4489e..f80ff09f4 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,20 @@ namespace smt { } virtual void pop_core(unsigned n) { + 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); } @@ -274,6 +289,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); }