From 6bff15e12efbadeb553dcc80bf1b5f5e3bd33536 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 May 2018 10:38:46 -0700 Subject: [PATCH 1/6] fix #1609 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 ++++++++ src/smt/smt_solver.cpp | 11 +++++++---- src/solver/combined_solver.cpp | 4 +++- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 36283356d..3eaf20763 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9826,6 +9826,14 @@ def String(name, ctx=None): ctx = _get_ctx(ctx) return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) +def SubString(s, offset, length): + """Extract substring or subsequence starting at offset""" + return Extract(s, offset, length) + +def SubSeq(s, offset, length): + """Extract substring or subsequence starting at offset""" + return Extract(s, offset, length) + def Strings(names, ctx=None): """Return a tuple of String constants. """ ctx = _get_ctx(ctx) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d813f249a..a5f9e0c34 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -61,10 +61,13 @@ namespace smt { smt_solver * result = alloc(smt_solver, m, p, m_logic); smt::kernel::copy(m_context, result->m_context); - for (auto & kv : m_name2assertion) - result->m_name2assertion.insert(translator(kv.m_key), - translator(kv.m_value)); - + for (auto & kv : m_name2assertion) { + expr* val = translator(kv.m_value); + expr* t = translator(kv.m_key); + result->m_name2assertion.insert(t, val); + result->solver_na2as::assert_expr(val, t); + m.inc_ref(val); + } return result; } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 9d2d8aa46..6469ab065 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -59,7 +59,8 @@ private: ref m_solver2; // We delay sending assertions to solver 2 // This is relevant for big benchmarks that are meant to be solved - // by a non-incremental solver. + // by a non-incremental solver. ); + bool m_solver2_initialized; bool m_ignore_solver1; @@ -137,6 +138,7 @@ public: } solver* translate(ast_manager& m, params_ref const& p) override { + TRACE("solver", tout << "translate\n";); solver* s1 = m_solver1->translate(m, p); solver* s2 = m_solver2->translate(m, p); combined_solver* r = alloc(combined_solver, s1, s2, p); From c279fd9f2e7409842d25f0995cbfa381d1683548 Mon Sep 17 00:00:00 2001 From: Carsten Varming Date: Thu, 3 May 2018 03:06:58 +0000 Subject: [PATCH 2/6] Specify encoding of source files in mk_util.py --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 99de61703..3e40187c3 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -780,7 +780,7 @@ def extract_c_includes(fname): # We should generate and error for any occurrence of #include that does not match the previous pattern. non_std_inc_pat = re.compile(".*#include.*") - f = open(fname, 'r') + f = open(fname, encoding='utf-8', mode='r') linenum = 1 for line in f: m1 = std_inc_pat.match(line) From 6e03c7a54216f9da0a5cdbfb29a3a131a2b1ae09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 May 2018 03:23:54 -0700 Subject: [PATCH 3/6] fix #1607 by filtering exceptions when the context is canceled Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 4 +++- src/api/api_solver.cpp | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 2712eef6f..7b8866b59 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -139,7 +139,9 @@ extern "C" { r = to_optimize_ptr(o)->optimize(); } catch (z3_exception& ex) { - mk_c(c)->handle_exception(ex); + if (!mk_c(c)->m().canceled()) { + mk_c(c)->handle_exception(ex); + } r = l_undef; } // to_optimize_ref(d).cleanup(); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 1b2e9dcc3..88ce8b144 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -361,7 +361,9 @@ extern "C" { } catch (z3_exception & ex) { to_solver_ref(s)->set_reason_unknown(eh); - mk_c(c)->handle_exception(ex); + if (!mk_c(c)->m().canceled()) { + mk_c(c)->handle_exception(ex); + } return Z3_L_UNDEF; } } From 888699548d4dea5b6729aa2b91a63ebb551df12d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 May 2018 11:59:49 -0700 Subject: [PATCH 4/6] Revert "Specify encoding of source files in mk_util.py" --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3e40187c3..99de61703 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -780,7 +780,7 @@ def extract_c_includes(fname): # We should generate and error for any occurrence of #include that does not match the previous pattern. non_std_inc_pat = re.compile(".*#include.*") - f = open(fname, encoding='utf-8', mode='r') + f = open(fname, 'r') linenum = 1 for line in f: m1 = std_inc_pat.match(line) From 2d5dd802386d78117d5ed9ddcbf8bc22ab3cb461 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Mon, 7 May 2018 23:33:04 +0200 Subject: [PATCH 5/6] The Permutation Matrix' `values` function attempted an incorrect conversion. This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE. --- src/util/lp/permutation_matrix.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/permutation_matrix.h b/src/util/lp/permutation_matrix.h index 3c89b3646..8e664bba0 100644 --- a/src/util/lp/permutation_matrix.h +++ b/src/util/lp/permutation_matrix.h @@ -132,7 +132,7 @@ class permutation_matrix : public tail_matrix { unsigned size() const { return static_cast(m_rev.size()); } - unsigned * values() const { return m_permutation; } + unsigned * values() const { return m_permutation.c_ptr(); } void resize(unsigned size) { unsigned old_size = m_permutation.size(); From d097d90731a954f29937facbab9b1fcf17134363 Mon Sep 17 00:00:00 2001 From: corrodedHash Date: Tue, 8 May 2018 19:26:14 +0200 Subject: [PATCH 6/6] Fixed Segfault when failing to load datalog file --- src/muz/fp/datalog_parser.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index dddca492b..a23d654b0 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -108,7 +108,9 @@ public: #endif } ~line_reader() { - fclose(m_file); + if (m_file != nullptr){ + fclose(m_file); + } } bool operator()() { return m_ok; }