From 371880da04b0260c0db1bf5f4c3c6975fd8cfc70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 May 2018 07:13:03 -0700 Subject: [PATCH 01/20] n/a Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 54 ++++++++------------------------------ src/smt/smt_context_pp.cpp | 5 +--- src/smt/smt_enode.h | 41 +++++++++++++++++++++++------ 3 files changed, 45 insertions(+), 55 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e20eae0bd..177dbb355 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -627,10 +627,7 @@ namespace smt { */ void context::remove_parents_from_cg_table(enode * r1) { // Remove parents from the congruence table - enode_vector::iterator it = r1->begin_parents(); - enode_vector::iterator end = r1->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode * parent : r1->get_parents()) { #if 0 { static unsigned num_eqs = 0; @@ -675,10 +672,7 @@ namespace smt { */ void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) { enode_vector & r2_parents = r2->m_parents; - enode_vector::iterator it = r1->begin_parents(); - enode_vector::iterator end = r1->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode * parent : r1->get_parents()) { if (!parent->is_marked()) continue; parent->unset_mark(); @@ -1008,10 +1002,7 @@ namespace smt { r2->m_parents.shrink(r2_num_parents); // try to reinsert parents of r1 that are not cgr - it = r1->begin_parents(); - end = r1->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode * parent : r1->get_parents()) { TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";); if (parent->is_cgc_enabled()) { enode * cg = parent->m_cg; @@ -1206,10 +1197,7 @@ namespace smt { bool context::is_diseq_slow(enode * n1, enode * n2) const { if (n1->get_num_parents() > n2->get_num_parents()) std::swap(n1, n2); - enode_vector::iterator it = n1->begin_parents(); - enode_vector::iterator end = n1->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode * parent : n1->get_parents()) { if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false && ((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) || (parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) { @@ -1241,10 +1229,7 @@ namespace smt { return false; if (r1->get_num_parents() < SMALL_NUM_PARENTS) { TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";); - enode_vector::iterator it1 = r1->begin_parents(); - enode_vector::iterator end1 = r1->end_parents(); - for (; it1 != end1; ++it1) { - enode * p1 = *it1; + for (enode* p1 : r1->get_parents()) { if (!is_relevant(p1)) continue; if (p1->is_eq()) @@ -1254,10 +1239,7 @@ namespace smt { func_decl * f = p1->get_decl(); TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";); unsigned num_args = p1->get_num_args(); - enode_vector::iterator it2 = r2->begin_parents(); - enode_vector::iterator end2 = r2->end_parents(); - for (; it2 != end2; ++it2) { - enode * p2 = *it2; + for (enode * p2 : r2->get_parents()) { if (!is_relevant(p2)) continue; if (p2->is_eq()) @@ -1295,10 +1277,7 @@ namespace smt { } almost_cg_table & table = *(m_almost_cg_tables[depth]); table.reset(r1, r2); - enode_vector::iterator it1 = r1->begin_parents(); - enode_vector::iterator end1 = r1->end_parents(); - for (; it1 != end1; ++it1) { - enode * p1 = *it1; + for (enode* p1 : r1->get_parents()) { if (!is_relevant(p1)) continue; if (p1->is_eq()) @@ -1309,10 +1288,7 @@ namespace smt { } if (table.empty()) return false; - enode_vector::iterator it2 = r2->begin_parents(); - enode_vector::iterator end2 = r2->end_parents(); - for (; it2 != end2; ++it2) { - enode * p2 = *it2; + for (enode * p2 : r2->get_parents()) { if (!is_relevant(p2)) continue; if (p2->is_eq()) @@ -1519,10 +1495,7 @@ namespace smt { } TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " v" << v << "\n";); theory_id th_id = th->get_id(); - enode_vector::iterator it = r->begin_parents(); - enode_vector::iterator end = r->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode * parent : r->get_parents()) { CTRACE("parent_bug", parent == 0, tout << "#" << r->get_owner_id() << ", num_parents: " << r->get_num_parents() << "\n"; display(tout);); if (parent->is_eq()) { bool_var bv = get_bool_var_of_id(parent->get_owner_id()); @@ -2197,9 +2170,7 @@ namespace smt { TRACE("cached_generation", tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";); m_cached_generation.insert(n, e->get_generation()); } - unsigned num_args = to_app(n)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = to_app(n)->get_arg(i); + for (expr * arg : *to_app(n)) { if (is_app(arg) || is_quantifier(arg)) todo.push_back(arg); } @@ -4228,10 +4199,7 @@ namespace smt { theory_var_list * l = n->get_th_var_list(); theory_id th_id = l->get_th_id(); - enode_vector::const_iterator it = n->begin_parents(); - enode_vector::const_iterator end = n->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode* parent : n->get_parents()) { family_id fid = parent->get_owner()->get_family_id(); if (fid != th_id && fid != m_manager.get_basic_family_id()) { TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index f4f56df5d..615cd2512 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -341,10 +341,7 @@ namespace smt { } void context::display_parent_eqs(std::ostream & out, enode * n) const { - enode_vector::iterator it = n->begin_parents(); - enode_vector::iterator end = n->end_parents(); - for (; it != end; ++it) { - enode * parent = *it; + for (enode* parent : n->get_parents()) { if (parent->is_eq()) display_eq_detail(out, parent); } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index df6309424..6c8d156b4 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -216,15 +216,28 @@ namespace smt { return m_args; } - class args { + class const_args { enode const& n; public: - args(enode const& n):n(n) {} - args(enode const* n):n(*n) {} - enode_vector::const_iterator begin() const { return n.get_args(); } - enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); } + const_args(enode const& n):n(n) {} + const_args(enode const* n):n(*n) {} + enode_vector::const_iterator begin() const { return n.m_args; } + enode_vector::const_iterator end() const { return n.m_args + n.get_num_args(); } }; + class args { + enode & n; + public: + args(enode & n):n(n) {} + args(enode * n):n(*n) {} + enode_vector::iterator begin() const { return n.m_args; } + enode_vector::iterator end() const { return n.m_args + n.get_num_args(); } + }; + + const_args get_const_args() const { return const_args(this); } + + // args get_args() { return args(this); } + // unsigned get_id() const { // return m_id; // } @@ -294,15 +307,27 @@ namespace smt { return m_commutative; } - class parents { + class const_parents { enode const& n; public: - parents(enode const& _n):n(_n) {} - parents(enode const* _n):n(*_n) {} + const_parents(enode const& _n):n(_n) {} + const_parents(enode const* _n):n(*_n) {} enode_vector::const_iterator begin() const { return n.begin_parents(); } enode_vector::const_iterator end() const { return n.end_parents(); } }; + class parents { + enode& n; + public: + parents(enode & _n):n(_n) {} + parents(enode * _n):n(*_n) {} + enode_vector::iterator begin() const { return n.begin_parents(); } + enode_vector::iterator end() const { return n.end_parents(); } + }; + + parents get_parents() { return parents(this); } + + const_parents get_const_parents() const { return const_parents(this); } unsigned get_num_parents() const { return m_parents.size(); From c279fd9f2e7409842d25f0995cbfa381d1683548 Mon Sep 17 00:00:00 2001 From: Carsten Varming Date: Thu, 3 May 2018 03:06:58 +0000 Subject: [PATCH 02/20] 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 888699548d4dea5b6729aa2b91a63ebb551df12d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 May 2018 11:59:49 -0700 Subject: [PATCH 03/20] 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 04/20] 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 05/20] 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; } From c198b12743c10934c15d7574b13634f0f0d51b21 Mon Sep 17 00:00:00 2001 From: Sapan Bhatia Date: Tue, 15 May 2018 04:55:57 +0530 Subject: [PATCH 06/20] Big_int is no longer a part of OCaml's standard library and must be included via the num package: https://github.com/ocaml/num --- scripts/mk_util.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 99de61703..aab4bcb21 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1932,8 +1932,14 @@ class MLComponent(Component): OCAML_FLAGS = '' if DEBUG_MODE: OCAML_FLAGS += '-g' - OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS - OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS + + if OCAMLFIND: + # Load Big_int, which is no longer part of the standard library, via the num package: https://github.com/ocaml/num + OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package num' + ' ' + OCAML_FLAGS + OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package num' + ' ' + OCAML_FLAGS + else: + OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS + OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS src_dir = self.to_src_dir mk_dir(os.path.join(BUILD_DIR, self.sub_dir)) From e5b14ab6825f48fffd09c758066b6a0b7b930f2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 May 2018 14:03:32 -0700 Subject: [PATCH 07/20] fix #1625 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b81927474..4bb1acded 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2292,6 +2292,7 @@ namespace z3 { class optimize : public object { Z3_optimize m_opt; + public: class handle { unsigned m_h; @@ -2300,6 +2301,17 @@ namespace z3 { unsigned h() const { return m_h; } }; optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } + optimize(optimize& o):object(c) { + Z3_optimize_inc_ref(o.ctx(), o.m_opt); + m_opt = o.m_opt; + } + optimize& operator=(optimize const& o) { + Z3_optimize_inc_rec(o.ctx(), o.m_opt); + Z3_optimize_dec_ref(ctx(), m_opt); + m_opt = o.m_opt; + m_ctx = o.m_ctx; + return *this; + } ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } operator Z3_optimize() const { return m_opt; } void add(expr const& e) { From 925867dc3ee4e4f0085d07d912cd9f7b7b904fa9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 May 2018 14:14:00 -0700 Subject: [PATCH 08/20] fix #1621 Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 2 +- src/util/smt2_util.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index aeaebc6bf..ade12de62 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -912,7 +912,7 @@ class smt2_printer { var_name = mk_smt2_quoted_symbol (*it); } else { - var_name = it->str ();\ + var_name = it->str (); } buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name.c_str ())); } diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp index 8358c67ac..a218f0c27 100644 --- a/src/util/smt2_util.cpp +++ b/src/util/smt2_util.cpp @@ -34,6 +34,12 @@ bool is_smt2_quoted_symbol(char const * s) { if ('0' <= s[0] && s[0] <= '9') return true; unsigned len = static_cast(strlen(s)); + if (len > 2 && s[0] == '|' && s[len-1] == '|') { + for (unsigned i = 1; i + 1 < len; i++) + if (!is_smt2_simple_symbol_char(s[i])) + return true; + return false; + } for (unsigned i = 0; i < len; i++) if (!is_smt2_simple_symbol_char(s[i])) return true; From 83023603213157c06ad9eaf77b4f5eb96262bd1c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 May 2018 14:24:12 -0700 Subject: [PATCH 09/20] fix #1625 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4bb1acded..903086daa 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2301,12 +2301,12 @@ namespace z3 { unsigned h() const { return m_h; } }; optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } - optimize(optimize& o):object(c) { + optimize(optimize& o):object(o) { Z3_optimize_inc_ref(o.ctx(), o.m_opt); m_opt = o.m_opt; } optimize& operator=(optimize const& o) { - Z3_optimize_inc_rec(o.ctx(), o.m_opt); + Z3_optimize_inc_ref(o.ctx(), o.m_opt); Z3_optimize_dec_ref(ctx(), m_opt); m_opt = o.m_opt; m_ctx = o.m_ctx; From d462ed3f0057a24fc1872a6a7a1e6ead34c970e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 May 2018 14:30:27 -0700 Subject: [PATCH 10/20] fix #1621 Signed-off-by: Nikolaj Bjorner --- src/util/smt2_util.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp index a218f0c27..365d8fe70 100644 --- a/src/util/smt2_util.cpp +++ b/src/util/smt2_util.cpp @@ -34,10 +34,14 @@ bool is_smt2_quoted_symbol(char const * s) { if ('0' <= s[0] && s[0] <= '9') return true; unsigned len = static_cast(strlen(s)); - if (len > 2 && s[0] == '|' && s[len-1] == '|') { - for (unsigned i = 1; i + 1 < len; i++) - if (!is_smt2_simple_symbol_char(s[i])) + if (len >= 2 && s[0] == '|' && s[len-1] == '|') { + for (unsigned i = 1; i + 1 < len; i++) { + if (s[i] == '\\' && i + 2 < len && (s[i+1] == '\\' || s[i+1] == '|')) { + i++; + } + else if (s[i] == '\\' || s[i] == '|') return true; + } return false; } for (unsigned i = 0; i < len; i++) From 1cc4a4ccc5ac7eb8a9e669ace3db89b9e0d607ff Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 19 May 2018 02:56:46 +0200 Subject: [PATCH 11/20] remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized --- src/util/lp/lar_constraints.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h index 9d3a0e0aa..5c33db8c6 100644 --- a/src/util/lp/lar_constraints.h +++ b/src/util/lp/lar_constraints.h @@ -84,7 +84,6 @@ struct lar_term_constraint: public lar_base_constraint { class lar_constraint : public lar_base_constraint { public: vector> m_coeffs; - lar_constraint() {} lar_constraint(const vector> & left_side, lconstraint_kind kind, const mpq & right_side) : lar_base_constraint(kind, right_side), m_coeffs(left_side) {} From 5134c168332147029a4d0fdb7cf945e0be18354f Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 19 May 2018 03:19:57 +0200 Subject: [PATCH 12/20] NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized --- src/ast/rewriter/poly_rewriter_def.h | 3 ++- src/ast/rewriter/rewriter_def.h | 6 +++--- src/smt/theory_str.cpp | 20 ++++++++++---------- src/tactic/core/solve_eqs_tactic.cpp | 4 ++-- 4 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index f27c9ffcf..d65960857 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -431,7 +431,8 @@ struct poly_rewriter::hoist_cmul_lt { hoist_cmul_lt(poly_rewriter & r):m_r(r) {} bool operator()(expr * t1, expr * t2) const { - expr * pp1, * pp2; + expr * pp1 = nullptr; + expr * pp2 = nullptr; numeral c1, c2; bool is_mul1 = m_r.is_mul(t1, c1, pp1); bool is_mul2 = m_r.is_mul(t2, c2, pp2); diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index dfb6542d6..4d4c4f708 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -336,9 +336,9 @@ void rewriter_tpl::process_app(app * t, frame & fr) { UNREACHABLE(); } // TODO: add rewrite rules support - expr * def; - proof * def_pr; - quantifier * def_q; + expr * def = nullptr; + proof * def_pr = nullptr; + quantifier * def_q = nullptr; // When get_macro succeeds, then // we know that: // forall X. f(X) = def[X] diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 126594b06..0c4d11420 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1423,9 +1423,9 @@ namespace smt { // len(hd) = i // str.indexof(tl, N, 0) - expr * H; // "haystack" - expr * N; // "needle" - expr * i; // start index + expr * H = nullptr; // "haystack" + expr * N = nullptr; // "needle" + expr * i = nullptr; // start index u.str.is_index(e, H, N, i); expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m); @@ -6951,8 +6951,8 @@ namespace smt { ast_manager & m = get_manager(); expr_ref_vector rhs(m); - expr * str; - expr * re; + expr * str = nullptr; + expr * re = nullptr; u.str.is_in_re(str_in_re, str, re); expr_ref strlen(mk_strlen(str), m); @@ -9929,8 +9929,8 @@ namespace smt { bool regex_axiom_add = false; for (obj_hashtable::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) { expr * str_in_re = *it; - expr * str; - expr * re; + expr * str = nullptr; + expr * re = nullptr; u.str.is_in_re(str_in_re, str, re); lbool current_assignment = ctx.get_assignment(str_in_re); TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;); @@ -9944,7 +9944,7 @@ namespace smt { if (regex_term_to_length_constraint.contains(str_in_re)) { // use existing length constraint - expr * top_level_length_constraint; + expr * top_level_length_constraint = nullptr; regex_term_to_length_constraint.find(str_in_re, top_level_length_constraint); ptr_vector extra_length_vars; @@ -10473,8 +10473,8 @@ namespace smt { // that's consistent with the current length information for (ptr_vector::iterator term_it = str_in_re_terms.begin(); term_it != str_in_re_terms.end(); ++term_it) { - expr * _unused; - expr * re; + expr * _unused = nullptr; + expr * re = nullptr; SASSERT(u.str.is_in_re(*term_it)); u.str.is_in_re(*term_it, _unused, re); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 9253b7172..c95a79ff7 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -263,8 +263,8 @@ class solve_eqs_tactic : public tactic { bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) { SASSERT(m_a_util.is_add(lhs)); bool is_int = m_a_util.is_int(lhs); - expr * a; - expr * v; + expr * a = nullptr; + expr * v = nullptr; rational a_val; unsigned num = lhs->get_num_args(); unsigned i; From f02d031d119c413cebd3432a644206caed0459e6 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 19 May 2018 03:47:11 +0200 Subject: [PATCH 13/20] As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value --- src/cmd_context/basic_cmds.cpp | 4 ++-- src/interp/iz3translate_direct.cpp | 8 ++++---- src/math/subpaving/subpaving.cpp | 12 ++++++------ src/math/subpaving/subpaving_t_def.h | 4 ++-- src/shell/datalog_frontend.cpp | 2 +- src/tactic/aig/aig.cpp | 2 +- src/test/mpff.cpp | 6 +++--- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 4e8806d62..56a354ee8 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -395,7 +395,7 @@ class set_option_cmd : public set_get_option_cmd { env_params::updt_params(); ctx.global_params_updated(); } - catch (gparams::exception ex) { + catch (const gparams::exception & ex) { throw cmd_exception(ex.msg()); } } @@ -620,7 +620,7 @@ public: try { ctx.regular_stream() << gparams::get_value(opt) << std::endl; } - catch (gparams::exception ex) { + catch (const gparams::exception & ex) { ctx.print_unsupported(opt, m_line, m_pos); } } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 8c2016149..9efb1a383 100644 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -912,7 +912,7 @@ public: if(!add_local_antes(arg, hyps, dk == PR_UNIT_RESOLUTION && i == 0)) return false; } - catch (non_lit_local_ante) { + catch (const non_lit_local_ante &) { std::cout << "\n"; show_step(proof); show(conc(proof)); @@ -1138,7 +1138,7 @@ public: try { res = iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "\nresolution error in theory lemma\n"; std::cout << "lits:\n"; for(unsigned j = 0; j < lits.size(); j++) @@ -1212,7 +1212,7 @@ public: try { res = iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "\nresolution error in theory lemma\n"; std::cout << "lits:\n"; for(unsigned j = 0; j < lits.size(); j++) @@ -1418,7 +1418,7 @@ public: try { return iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "resolution error in unit_resolution, position" << position << "\n"; show_step(proof); throw invalid_lemma(); diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index 16a9a9a9e..c43b74f0d 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -121,7 +121,7 @@ namespace subpaving { int2mpf(c, m_c); return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -135,7 +135,7 @@ namespace subpaving { m.set(m_c, k); return reinterpret_cast(m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -178,7 +178,7 @@ namespace subpaving { int2hwf(c, m_c); return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -192,7 +192,7 @@ namespace subpaving { m.set(m_c, k); return reinterpret_cast(m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -236,7 +236,7 @@ namespace subpaving { int2fpoint(c, m_c); return this->m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (typename context_fpoint::numeral_manager::exception) { + catch (const typename context_fpoint::numeral_manager::exception &) { throw subpaving::exception(); } } @@ -251,7 +251,7 @@ namespace subpaving { m.set(m_c, m_qm, k); return reinterpret_cast(this->m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (typename context_fpoint::numeral_manager::exception) { + catch (const typename context_fpoint::numeral_manager::exception &) { throw subpaving::exception(); } } diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index bb129fee7..cf93fbfad 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -1310,7 +1310,7 @@ bool context_t::relevant_new_bound(var x, numeral const & k, bool lower, bool TRACE("subpaving_relevant_bound", tout << "new bound is relevant\n";); return true; } - catch (typename C::exception) { + catch (const typename C::exception &) { // arithmetic module failed. set_arith_failed(); return false; @@ -1722,7 +1722,7 @@ void context_t::propagate(node * n, bound * b) { } } } - catch (typename C::exception) { + catch (const typename C::exception &) { // arithmetic module failed, ignore constraint set_arith_failed(); } diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 9cc13b897..6596cc3b7 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -246,7 +246,7 @@ unsigned read_datalog(char const * file) { false); } - catch (out_of_memory_error) { + catch (const out_of_memory_error &) { std::cout << "\n\nOUT OF MEMORY!\n\n"; display_statistics( std::cout, diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 6afac32b8..f6e12275f 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -1522,7 +1522,7 @@ public: } SASSERT(ref_count(r) >= 1); } - catch (aig_exception ex) { + catch (const aig_exception & ex) { dec_ref(r); throw ex; } diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index dd934831c..c78489f21 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -35,7 +35,7 @@ static void tst1() { std::cout << i << ": " << a << "\n"; } } - catch (z3_exception & ex) { + catch (const z3_exception & ex) { std::cout << ex.msg() << "\n"; } } @@ -432,7 +432,7 @@ static void tst_limits(unsigned prec) { m.round_to_plus_inf(); bool overflow = false; try { m.inc(a); } - catch (mpff_manager::overflow_exception) { overflow = true; } + catch (const mpff_manager::overflow_exception &) { overflow = true; } VERIFY(overflow); m.set_max(a); m.dec(a); @@ -446,7 +446,7 @@ static void tst_limits(unsigned prec) { ENSURE(m.eq(a, b)); overflow = true; try { m.dec(a); } - catch (mpff_manager::overflow_exception) { overflow = true; } + catch (const mpff_manager::overflow_exception &) { overflow = true; } ENSURE(overflow); m.round_to_plus_inf(); m.set_min(a); From 7d51353b8b097a22b0278cb50006c6b4ff5e0fe1 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sat, 19 May 2018 11:13:53 +0200 Subject: [PATCH 14/20] Implement parallel python example --- examples/python/parallel.py | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 examples/python/parallel.py diff --git a/examples/python/parallel.py b/examples/python/parallel.py new file mode 100644 index 000000000..7903f58c9 --- /dev/null +++ b/examples/python/parallel.py @@ -0,0 +1,33 @@ +from z3 import * +from multiprocessing.pool import ThreadPool +from copy import deepcopy + +pool = ThreadPool(8) +x = Int('x') + +assert x.ctx == main_ctx() + + +def calculate(x, n, ctx): + """ Do a simple computation with a context""" + assert x.ctx == ctx + assert x.ctx != main_ctx() + + condition = And(x < 2, x > n, ctx) + solver = Solver(ctx=ctx) + solver.add(condition) + solver.check() + + +for i in range(100): + # Create new context for the computation + # Note that we need to do this sequentially, as parallel access to the current context or its objects + # will result in a segfault + i_context = Context() + x_i = deepcopy(x).translate(i_context) + + # Kick off parallel computation + pool.apply_async(calculate, [x_i, i, i_context]) + +pool.close() +pool.join() From e32dfad81e7fc14816c034d1a527975d0cc97138 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sat, 19 May 2018 11:16:20 +0200 Subject: [PATCH 15/20] Add comments --- examples/python/parallel.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/examples/python/parallel.py b/examples/python/parallel.py index 7903f58c9..42ff50927 100644 --- a/examples/python/parallel.py +++ b/examples/python/parallel.py @@ -13,7 +13,10 @@ def calculate(x, n, ctx): assert x.ctx == ctx assert x.ctx != main_ctx() + # Parallel creation of z3 object condition = And(x < 2, x > n, ctx) + + # Parallel solving solver = Solver(ctx=ctx) solver.add(condition) solver.check() From 9c5a0ee8102dc248b29fbb930ecdb8158965ca21 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 19 May 2018 04:17:52 +0200 Subject: [PATCH 16/20] Remove unnecessary (and confusing) parantheses around variable name in its declaration. Also fixes GCC warning [-Wparentheses]. --- src/interp/iz3base.cpp | 2 +- src/smt/theory_str.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 43e7bdff8..773f328ab 100644 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -281,7 +281,7 @@ bool iz3base::is_sat(const std::vector &q, ast &_proof, std::vector &v _proof = cook(proof); } else if(vars.size()) { - model_ref(_m); + model_ref _m; s.get_model(_m); if (!_m.get()) { SASSERT(l_undef == res); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0c4d11420..dde75c4bc 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6768,7 +6768,7 @@ namespace smt { expr * sub2; if (u.re.is_to_re(re, sub1)) { SASSERT(u.str.is_string(sub1)); - zstring(str); + zstring str; u.str.is_string(sub1, str); lens.insert(str.length()); } else if (u.re.is_concat(re, sub1, sub2)) { From 78087483ca065c6518b3b09e2b945c9041862624 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 19 May 2018 04:25:43 +0200 Subject: [PATCH 17/20] Add missing include The code should not have compiled previously, as smt::context was only forward declared at this point. --- src/smt/theory_arith.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 5040f1034..944efe6ce 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -31,6 +31,7 @@ Revision History: #include "smt/params/theory_arith_params.h" #include "smt/arith_eq_adapter.h" #include "smt/proto_model/numeral_factory.h" +#include "smt/smt_context.h" #include "util/obj_pair_hashtable.h" #include "smt/old_interval.h" #include "math/grobner/grobner.h" From 7467368266629486b3e11698f6e52ad8dd4a256f Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Mon, 21 May 2018 07:26:29 +0200 Subject: [PATCH 18/20] Use CMake's own mechanism for selecting language version if CMake version is new enough --- CMakeLists.txt | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index e4732ef67..420c1a122 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -218,12 +218,17 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake) ################################################################################ # C++ language version ################################################################################ -# FIXME: Use CMake's own mechanism for selecting language version -if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) - z3_add_cxx_flag("-std=c++11" REQUIRED) -else() - message(AUTHOR_WARNING "Not setting C++ language version for compiler") -endif() +if ("${CMAKE_VERSION}" VERSION_LESS "3.1") + # FIXME: Drop this when we upgrade to newer CMake versions. + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) + z3_add_cxx_flag("-std=c++11" REQUIRED) + else() + message(AUTHOR_WARNING "Not setting C++ language version for compiler") + endif() +else () + set(CMAKE_CXX_STANDARD 11) + set(CMAKE_CXX_STANDARD_REQUIRED ON) +endif () ################################################################################ # Platform detection From 3b1b82bef05a1b5fd69ece79c80a95fb6d72a990 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 May 2018 10:19:38 -0700 Subject: [PATCH 19/20] bumping version number by 1 for release tagging Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 420c1a122..afea250cb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,7 @@ endif() ################################################################################ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 7) -set(Z3_VERSION_PATCH 0) +set(Z3_VERSION_PATCH 1) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 8f601f4fe..af4c92658 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 7, 0, 0) + set_version(4, 7, 1, 0) add_lib('util', []) add_lib('lp', ['util'], 'util/lp') add_lib('polynomial', ['util'], 'math/polynomial') From f2aae7cffa58686a8d251c87301c82cd4c2db200 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 May 2018 16:59:11 -0700 Subject: [PATCH 20/20] release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 86e7039dd..a99ec6b1e 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,22 @@ RELEASE NOTES +Version 4.7.1 +============= + +- New requirements: + - uses stdbool and stdint as part of z3.h + +- New features: + - none + +- Removed features: + - none + +- Notes: + This is a minor release prior to a set of planned major updates. + It uses minor version 7 to indicate that the use of stdbool and + stdint are breaking changes to consumers of the C-based API. + Version 4.6.0 =============