diff --git a/CMakeLists.txt b/CMakeLists.txt index e4732ef67..b109eb50b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -33,7 +33,7 @@ endif() # Project version ################################################################################ set(Z3_VERSION_MAJOR 4) -set(Z3_VERSION_MINOR 7) +set(Z3_VERSION_MINOR 8) set(Z3_VERSION_PATCH 0) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3a2f30938..0590a8693 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, 8, 0, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index d1231c615..6318283c6 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -421,35 +421,7 @@ extern "C" { expr * r = to_func_entry(e)->m_func_entry->get_arg(i); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(nullptr); - } - - // ---------------------------- - // - // DEPRECATED API - // - // ---------------------------- - -#if 0 - void Z3_API Z3_del_model(Z3_context c, Z3_model m) { - Z3_model_dec_ref(c, m); - } - unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m) { - return Z3_model_get_num_consts(c, m); - } - - Z3_func_decl Z3_API Z3_get_model_constant(Z3_context c, Z3_model m, unsigned i) { - return Z3_model_get_const_decl(c, m, i); - } - - unsigned Z3_API Z3_get_model_num_funcs(Z3_context c, Z3_model m) { - return Z3_model_get_num_funcs(c, m); - } - - Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i) { - return Z3_model_get_func_decl(c, m, i); - } -#endif - + } unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) { RESET_ERROR_CODE(); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index c17d71518..b4dab6926 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1555,12 +1555,6 @@ namespace z3 { m_vector = s.m_vector; return *this; } -<<<<<<< HEAD - bool contains(T const& x) const { - for (auto y : *this) if (eq(x, y)) return true; - return false; - } -======= /* Disabled pending C++98 build upgrade bool contains(T const& x) const { @@ -1568,7 +1562,6 @@ namespace z3 { return false; } */ ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 class iterator { ast_vector_tpl const* m_vector; @@ -1990,14 +1983,9 @@ namespace z3 { } // fails for some compilers: // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } -<<<<<<< HEAD - void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); check_error(); } - void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); check_error(); } -======= void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); } void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); } ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); } check_result check(unsigned n, expr * const assumptions) { array _assumptions(n); @@ -2169,10 +2157,6 @@ namespace z3 { return *this; } void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); } -<<<<<<< HEAD -======= - // fails for some compilers: ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } unsigned size() const { return Z3_goal_size(ctx(), m_goal); } expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); } @@ -2232,28 +2216,6 @@ namespace z3 { } unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); } goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); } -<<<<<<< HEAD -======= - model convert_model(model const & m, unsigned i = 0) const { - check_context(*this, m); - Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); - check_error(); - return model(ctx(), new_m); - } - expr as_expr() const { - unsigned n = size(); - if (n == 0) - return ctx().bool_val(true); - else if (n == 1) - return operator[](0).as_expr(); - else { - array args(n); - for (unsigned i = 0; i < n; i++) - args[i] = operator[](i).as_expr(); - return expr(ctx(), Z3_mk_or(ctx(), n, args.ptr())); - } - } ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 friend std::ostream & operator<<(std::ostream & out, apply_result const & r); }; inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; } @@ -2999,7 +2961,6 @@ namespace z3 { return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a)); } -<<<<<<< HEAD inline expr_vector context::parse_string(char const* s) { Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); check_error(); @@ -3010,17 +2971,6 @@ namespace z3 { Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); check_error(); return expr_vector(*this, r); -======= - inline expr context::parse_string(char const* s) { - Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); - check_parser_error(); - return expr(*this, r); - } - inline expr context::parse_file(char const* s) { - Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); - check_parser_error(); - return expr(*this, r); ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 } inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { @@ -3034,15 +2984,10 @@ namespace z3 { for (unsigned i = 0; i < decls.size(); ++i) { decl_names[i] = decls[i].name(); } -<<<<<<< HEAD + Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); check_error(); return expr_vector(*this, r); -======= - Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); - check_parser_error(); - return expr(*this, r); ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 } inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { @@ -3056,15 +3001,9 @@ namespace z3 { for (unsigned i = 0; i < decls.size(); ++i) { decl_names[i] = decls[i].name(); } -<<<<<<< HEAD Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); check_error(); return expr_vector(*this, r); -======= - Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); - check_parser_error(); - return expr(*this, r); ->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5 } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5906281df..4f9a72174 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -33,11 +33,6 @@ using namespace format_ns; format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bool is_skolem) const { ast_manager & m = get_manager(); -#if 0 - symbol s1 = m_renaming.get_symbol(s, is_skolem); - len = static_cast(strlen(s1.bare_str())); - return mk_string(m, s1.bare_str()); -#else if (is_smt2_quoted_symbol(s)) { std::string str = mk_smt2_quoted_symbol(s); len = static_cast(str.length()); @@ -56,7 +51,6 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo len = static_cast(strlen(s.bare_str())); return mk_string(m, s.bare_str()); } -#endif } format * smt2_pp_environment::pp_fdecl_name(func_decl * f, unsigned & len) const { diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 4e1024202..47a8a044a 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -5,7 +5,7 @@ Module Name: pb2bv_rewriter.cpp -Abstralct: +Abstract: Conversion from pseudo-booleans to bit-vectors. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index cf8ed5087..5ee49ef16 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -429,7 +429,7 @@ public: #pragma omp critical (gparams) { if (m_module_params.find(module_name, ps)) { - result = *ps; + result.copy(*ps); } } return result;