diff --git a/CMakeLists.txt b/CMakeLists.txt index e4732ef67..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 @@ -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 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 ============= diff --git a/examples/python/parallel.py b/examples/python/parallel.py new file mode 100644 index 000000000..42ff50927 --- /dev/null +++ b/examples/python/parallel.py @@ -0,0 +1,36 @@ +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() + + # Parallel creation of z3 object + condition = And(x < 2, x > n, ctx) + + # Parallel solving + 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() 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') 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/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/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/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/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" diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 126594b06..dde75c4bc 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); @@ -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)) { @@ -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/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/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; 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); 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) {}