From 6261a5c27bac07275178889052ae983e828a0811 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 4 May 2017 15:28:20 +0100 Subject: [PATCH 1/5] Fix bug in `mk_api_doc.py` where the Z3 python package path would be checked when building the Z3 python package documentation was disabled. --- doc/mk_api_doc.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 014a152b4..234dd670c 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -103,15 +103,17 @@ def parse_options(): TEMP_DIR = pargs.temp_dir OUTPUT_DIRECTORY = pargs.output_dir Z3PY_PACKAGE_PATH = pargs.z3py_package_path - if not os.path.exists(Z3PY_PACKAGE_PATH): - raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH)) - if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3': - raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH)) Z3PY_ENABLED = not pargs.no_z3py DOTNET_ENABLED = not pargs.no_dotnet JAVA_ENABLED = not pargs.no_java DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths JAVA_API_SEARCH_PATHS = pargs.java_search_paths + + if Z3PY_ENABLED: + if not os.path.exists(Z3PY_PACKAGE_PATH): + raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH)) + if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3': + raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH)) return def mk_dir(d): From 1db07f1189d6560316537ec4822d41e84f0a7105 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 4 May 2017 15:29:47 +0100 Subject: [PATCH 2/5] [CMake] Remove `BYPRODUCTS` declaration for `api_docs` target. This breaks the `clean` rule when using Ninja as the CMake generator. Unfortunately this means `clean` doesn't try to remove the generated documentation anymore when using Ninja. --- contrib/cmake/doc/CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/contrib/cmake/doc/CMakeLists.txt b/contrib/cmake/doc/CMakeLists.txt index 86e208ab1..2f8ee0dc5 100644 --- a/contrib/cmake/doc/CMakeLists.txt +++ b/contrib/cmake/doc/CMakeLists.txt @@ -67,7 +67,6 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG} ${JAVA_API_OPTIONS} DEPENDS ${DOC_EXTRA_DEPENDS} - BYPRODUCTS "${DOC_DEST_DIR}" COMMENT "Generating documentation" ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG} ) From 0ebce66c57e124ebcb4c3bb3d34fe9d35779341b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 5 May 2017 14:22:40 +0100 Subject: [PATCH 3/5] Fixed bug with .NET keyfile path containing spaces. Fixes #1003. --- scripts/mk_util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index f05250ae7..b0ac92a8d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1633,6 +1633,8 @@ class DotNetDLLComponent(Component): if not self.key_file is None: print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file)) + if (self.key_file.find(' ') != -1): + self.key_file = '"' + self.key_file + '"' cscCmdLine.append('/keyfile:{}'.format(self.key_file)) cscCmdLine.extend( ['/unsafe+', From 79dcf03a42a79f4f6fe09b60ff809be39dce38d8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 5 May 2017 15:01:10 +0100 Subject: [PATCH 4/5] Enabled C++11 in GCC and Clang --- scripts/mk_util.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b0ac92a8d..d1bbd6ca4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2421,6 +2421,7 @@ def mk_config(): FOCI2 = False if GIT_HASH: CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) + CXXFLAGS = '%s -std=c++11' % CXXFLAGS CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS FPMATH = test_fpmath(CXX) CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) @@ -2445,8 +2446,8 @@ def mk_config(): CXXFLAGS = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS sysname, _, _, _, machine = os.uname() if sysname == 'Darwin': - SO_EXT = '.dylib' - SLIBFLAGS = '-dynamiclib' + SO_EXT = '.dylib' + SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' From 7e1fae418a766532f99cea06a1c6021268661864 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 May 2017 10:59:47 -0400 Subject: [PATCH 5/5] fix #1005, disable expansion of regular expression range to union as it degrades performance significantly Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 1 + src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 11 +++++++---- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 85d2ba749..7aa9329d4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1434,6 +1434,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) */ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { + return BR_FAILED; TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); zstring str_lo, str_hi; if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 439adbdff..cdc1a3933 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -505,7 +505,7 @@ namespace smt { struct var_value_eq { theory_arith & m_th; var_value_eq(theory_arith & th):m_th(th) {} - bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int(v1) == m_th.is_int(v2); } + bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int_src(v1) == m_th.is_int_src(v2); } }; typedef int_hashtable var_value_table; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index de357c8d3..54b617152 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2201,16 +2201,19 @@ namespace smt { int num = get_num_vars(); for (theory_var v = 0; v < num; v++) { enode * n = get_enode(v); - TRACE("func_interp_bug", tout << "#" << n->get_owner_id() << " -> " << m_value[v] << "\n";); - if (!is_relevant_and_shared(n)) + TRACE("func_interp_bug", tout << mk_pp(n->get_owner(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";); + if (!is_relevant_and_shared(n)) { continue; + } theory_var other = null_theory_var; other = m_var_value_table.insert_if_not_there(v); - if (other == v) + if (other == v) { continue; + } enode * n2 = get_enode(other); - if (n->get_root() == n2->get_root()) + if (n->get_root() == n2->get_root()) { continue; + } TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";); m_assume_eq_candidates.push_back(std::make_pair(other, v)); result = true;