From 50c323dc74c0947236f28c16514517924cf1f753 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Nov 2016 14:35:48 +0000 Subject: [PATCH 01/10] Whitespace --- src/smt/smt_quantifier.h | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index e814afcb1..bc731bf9c 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -37,7 +37,7 @@ namespace smt { public: quantifier_manager(context & ctx, smt_params & fp, params_ref const & p); ~quantifier_manager(); - + context & get_context() const; void set_plugin(quantifier_manager_plugin * plugin); @@ -51,12 +51,12 @@ namespace smt { quantifier_stat * get_stat(quantifier * q) const; unsigned get_generation(quantifier * q) const; - bool add_instance(quantifier * q, app * pat, - unsigned num_bindings, - enode * const * bindings, - unsigned max_generation, - unsigned min_top_generation, - unsigned max_top_generation, + bool add_instance(quantifier * q, app * pat, + unsigned num_bindings, + enode * const * bindings, + unsigned max_generation, + unsigned min_top_generation, + unsigned max_top_generation, ptr_vector & used_enodes); bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0); @@ -78,11 +78,11 @@ namespace smt { bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); - + void push(); void pop(unsigned num_scopes); void reset(); - + void display(std::ostream & out) const; void display_stats(std::ostream & out, quantifier * q) const; @@ -97,7 +97,7 @@ namespace smt { public: quantifier_manager_plugin() {} virtual ~quantifier_manager_plugin() {} - + virtual void set_manager(quantifier_manager & qm) = 0; virtual quantifier_manager_plugin * mk_fresh() = 0; @@ -106,7 +106,7 @@ namespace smt { virtual void del(quantifier * q) = 0; virtual bool is_shared(enode * n) const = 0; - + /** \brief This method is invoked whenever q is assigned to true. */ @@ -131,9 +131,9 @@ namespace smt { \brief This method is invoked whenever the solver restarts. */ virtual void restart_eh() = 0; - + /** - \brief Return true if the quantifier_manager can propagate information + \brief Return true if the quantifier_manager can propagate information information back into the core. */ virtual bool can_propagate() const = 0; @@ -143,11 +143,11 @@ namespace smt { \brief Return true if the plugin is "model based" */ virtual bool model_based() const = 0; - + /** \brief Is "model based" instantiate allowed to instantiate this quantifier? */ - virtual bool mbqi_enabled(quantifier *q) const {return true;} + virtual bool mbqi_enabled(quantifier *q) const {return true;} /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. @@ -161,10 +161,10 @@ namespace smt { It also provides a mapping from enodes to their interpretations. */ virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map const & root2value) = 0; - + virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; - + }; }; From 5ef7d38d728a77f6825fe6526523dce7a157a459 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Nov 2016 14:39:23 +0000 Subject: [PATCH 02/10] Whitespace --- src/smt/smt_quantifier.cpp | 97 ++++++++++++++++++-------------------- 1 file changed, 47 insertions(+), 50 deletions(-) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index a5e15a201..5787d6732 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -27,7 +27,7 @@ Revision History: #include"ast_smt2_pp.h" namespace smt { - + quantifier_manager_plugin * mk_default_plugin(); struct quantifier_manager::imp { @@ -40,7 +40,7 @@ namespace smt { ptr_vector m_quantifiers; scoped_ptr m_plugin; unsigned m_num_instances; - + imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin): m_wrapper(wrapper), m_context(ctx), @@ -85,7 +85,7 @@ namespace smt { out << max_generation << " : " << max_cost << "\n"; } } - + void del(quantifier * q) { if (m_params.m_qi_profile) { display_stats(verbose_stream(), q); @@ -99,15 +99,15 @@ namespace smt { } bool is_shared(enode * n) const { - return m_plugin->is_shared(n); + return m_plugin->is_shared(n); } - bool add_instance(quantifier * q, app * pat, - unsigned num_bindings, - enode * const * bindings, - unsigned max_generation, - unsigned min_top_generation, - unsigned max_top_generation, + bool add_instance(quantifier * q, app * pat, + unsigned num_bindings, + enode * const * bindings, + unsigned max_generation, + unsigned min_top_generation, + unsigned max_top_generation, ptr_vector & used_enodes) { max_generation = std::max(max_generation, get_generation(q)); if (m_num_instances > m_params.m_qi_max_instances) @@ -136,7 +136,7 @@ namespace smt { } return false; } - + void init_search_eh() { m_num_instances = 0; ptr_vector::iterator it2 = m_quantifiers.begin(); @@ -149,7 +149,7 @@ namespace smt { m_plugin->init_search_eh(); TRACE("smt_params", m_params.display(tout); ); } - + void assign_eh(quantifier * q) { m_plugin->assign_eh(q); } @@ -175,7 +175,7 @@ namespace smt { m_plugin->pop(num_scopes); m_qi_queue.pop_scope(num_scopes); } - + bool can_propagate() { return m_qi_queue.has_work() || m_plugin->can_propagate(); } @@ -184,7 +184,7 @@ namespace smt { m_plugin->propagate(); m_qi_queue.instantiate(); } - + bool check_quantifier(quantifier* q) { return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q); } @@ -251,7 +251,7 @@ namespace smt { quantifier_manager::~quantifier_manager() { dealloc(m_imp); } - + context & quantifier_manager::get_context() const { return m_imp->m_context; } @@ -285,16 +285,16 @@ namespace smt { return m_imp->get_generation(q); } - bool quantifier_manager::add_instance(quantifier * q, app * pat, - unsigned num_bindings, - enode * const * bindings, - unsigned max_generation, - unsigned min_top_generation, - unsigned max_top_generation, + bool quantifier_manager::add_instance(quantifier * q, app * pat, + unsigned num_bindings, + enode * const * bindings, + unsigned max_generation, + unsigned min_top_generation, + unsigned max_top_generation, ptr_vector & used_enodes) { return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes); } - + bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) { ptr_vector tmp; return add_instance(q, 0, num_bindings, bindings, generation, generation, generation, tmp); @@ -347,7 +347,7 @@ namespace smt { quantifier_manager::check_model_result quantifier_manager::check_model(proto_model * m, obj_map const & root2value) { return m_imp->check_model(m, root2value); } - + void quantifier_manager::push() { m_imp->push(); } @@ -367,7 +367,7 @@ namespace smt { plugin->set_manager(*this); } } - + void quantifier_manager::display(std::ostream & out) const { } @@ -382,12 +382,12 @@ namespace smt { m_imp->display_stats(out, q); } - ptr_vector::const_iterator quantifier_manager::begin_quantifiers() const { - return m_imp->m_quantifiers.begin(); + ptr_vector::const_iterator quantifier_manager::begin_quantifiers() const { + return m_imp->m_quantifiers.begin(); } - - ptr_vector::const_iterator quantifier_manager::end_quantifiers() const { - return m_imp->m_quantifiers.end(); + + ptr_vector::const_iterator quantifier_manager::end_quantifiers() const { + return m_imp->m_quantifiers.end(); } // The default plugin uses E-matching, MBQI and quick-checker @@ -404,13 +404,13 @@ namespace smt { bool m_active; public: default_qm_plugin(): - m_qm(0), - m_context(0), - m_new_enode_qhead(0), + m_qm(0), + m_context(0), + m_new_enode_qhead(0), m_lazy_matching_idx(0), m_active(false) { } - + virtual ~default_qm_plugin() { } @@ -434,20 +434,18 @@ namespace smt { virtual bool model_based() const { return m_fparams->m_mbqi; } - virtual bool mbqi_enabled(quantifier *q) const { - if(!m_fparams->m_mbqi_id) return true; + virtual bool mbqi_enabled(quantifier *q) const { + if (!m_fparams->m_mbqi_id) return true; const symbol &s = q->get_qid(); size_t len = strlen(m_fparams->m_mbqi_id); - if(s == symbol::null || s.is_numerical()) + if (s == symbol::null || s.is_numerical()) return len == 0; - return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; - } + return strncmp(s.bare_str(), m_fparams->m_mbqi_id, len) == 0; + } - /* Quantifier id's must begin with the prefix specified by - parameter mbqi.id to be instantiated with MBQI. The default - value is the empty string, so all quantifiers are - instantiated. - */ + /* Quantifier id's must begin with the prefix specified by parameter + mbqi.id to be instantiated with MBQI. The default value is the + empty string, so all quantifiers are instantiated. */ virtual void add(quantifier * q) { if (m_fparams->m_mbqi && mbqi_enabled(q)) { m_active = true; @@ -455,8 +453,7 @@ namespace smt { } } - virtual void del(quantifier * q) { - } + virtual void del(quantifier * q) { } virtual void push() { m_mam->push_scope(); @@ -465,7 +462,7 @@ namespace smt { m_model_finder->push_scope(); } } - + virtual void pop(unsigned num_scopes) { m_mam->pop_scope(num_scopes); m_lazy_mam->pop_scope(num_scopes); @@ -473,7 +470,7 @@ namespace smt { m_model_finder->pop_scope(num_scopes); } } - + virtual void init_search_eh() { m_lazy_matching_idx = 0; if (m_fparams->m_mbqi) { @@ -516,7 +513,7 @@ namespace smt { } } } - + bool use_ematching() const { return m_fparams->m_ematching && !m_qm->empty(); } @@ -538,7 +535,7 @@ namespace smt { } virtual void restart_eh() { - if (m_fparams->m_mbqi) { + if (m_fparams->m_mbqi) { m_model_finder->restart_eh(); m_model_checker->restart_eh(); } @@ -613,7 +610,7 @@ namespace smt { } return FC_DONE; } - + }; quantifier_manager_plugin * mk_default_plugin() { From 75cfd14e5a6cfe43eca6f273988360507f46d47e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 14:14:45 +0000 Subject: [PATCH 03/10] bugfix for macro finder --- src/ast/macros/macro_util.cpp | 118 +++++++++++++++++----------------- 1 file changed, 60 insertions(+), 58 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 166b9c4b0..e1f44e927 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -34,7 +34,7 @@ macro_util::macro_util(ast_manager & m, simplifier & s): m_simplifier(s), m_arith_simp(0), m_bv_simp(0), - m_basic_simp(0), + m_basic_simp(0), m_forbidden_set(0), m_curr_clause(0) { } @@ -64,23 +64,23 @@ basic_simplifier_plugin * macro_util::get_basic_simp() const { } bool macro_util::is_bv(expr * n) const { - return get_bv_simp()->is_bv(n); + return get_bv_simp()->is_bv(n); } bool macro_util::is_bv_sort(sort * s) const { - return get_bv_simp()->is_bv_sort(s); + return get_bv_simp()->is_bv_sort(s); } bool macro_util::is_add(expr * n) const { - return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n); + return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n); } bool macro_util::is_times_minus_one(expr * n, expr * & arg) const { return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg); } -bool macro_util::is_le(expr * n) const { - return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n); +bool macro_util::is_le(expr * n) const { + return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n); } bool macro_util::is_le_ge(expr * n) const { @@ -130,7 +130,7 @@ void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_r /** \brief Return true if \c n is an application of the form - + (f x_{k_1}, ..., x_{k_n}) where f is uninterpreted @@ -147,7 +147,7 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const { var2pos.resize(num_decls, -1); for (unsigned i = 0; i < num_decls; i++) { expr * c = to_app(n)->get_arg(i); - if (!is_var(c)) + if (!is_var(c)) return false; unsigned idx = to_var(c)->get_idx(); if (idx >= num_decls || var2pos[idx] != -1) @@ -161,12 +161,12 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const { /** \brief Return true if n is of the form - + (= (f x_{k_1}, ..., x_{k_n}) t) OR - (iff (f x_{k_1}, ..., x_{k_n}) t) + (iff (f x_{k_1}, ..., x_{k_n}) t) where - + is_macro_head((f x_{k_1}, ..., x_{k_n})) returns true AND t does not contain f AND f is not in forbidden_set @@ -180,7 +180,8 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he if (m_manager.is_eq(n) || m_manager.is_iff(n)) { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); - if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && !occurs(to_app(lhs)->get_decl(), rhs)) { + if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && + !occurs(to_app(lhs)->get_decl(), rhs) && !has_quantifiers(rhs)) { head = to_app(lhs); def = rhs; return true; @@ -192,12 +193,12 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he /** \brief Return true if n is of the form - + (= t (f x_{k_1}, ..., x_{k_n})) OR (iff t (f x_{k_1}, ..., x_{k_n})) where - + is_macro_head((f x_{k_1}, ..., x_{k_n})) returns true AND t does not contain f AND f is not in forbidden_set @@ -211,7 +212,8 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h if (m_manager.is_eq(n) || m_manager.is_iff(n)) { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); - if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && !occurs(to_app(rhs)->get_decl(), lhs)) { + if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && + !occurs(to_app(rhs)->get_decl(), lhs) && !has_quantifiers(lhs)) { head = to_app(rhs); def = lhs; return true; @@ -254,7 +256,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex if (!as->is_numeral(rhs)) return false; - + inv = false; ptr_buffer args; expr * h = 0; @@ -271,15 +273,15 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex for (unsigned i = 0; i < lhs_num_args; i++) { expr * arg = lhs_args[i]; expr * neg_arg; - if (h == 0 && - is_macro_head(arg, num_decls) && - !is_forbidden(to_app(arg)->get_decl()) && + if (h == 0 && + is_macro_head(arg, num_decls) && + !is_forbidden(to_app(arg)->get_decl()) && !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) { h = arg; } else if (h == 0 && as->is_times_minus_one(arg, neg_arg) && - is_macro_head(neg_arg, num_decls) && - !is_forbidden(to_app(neg_arg)->get_decl()) && + is_macro_head(neg_arg, num_decls) && + !is_forbidden(to_app(neg_arg)->get_decl()) && !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) { h = neg_arg; inv = true; @@ -304,7 +306,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex \brief Auxiliary function for is_pseudo_predicate_macro. It detects the pattern (= (f X) t) */ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) { - if (!m_manager.is_eq(n)) + if (!m_manager.is_eq(n)) return false; expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); @@ -331,7 +333,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, ap /** \brief Returns true if n if of the form (forall (X) (iff (= (f X) t) def[X])) - where t is a ground term, (f X) is the head. + where t is a ground term, (f X) is the head. */ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) { if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) @@ -343,14 +345,14 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t return false; expr * lhs = to_app(body)->get_arg(0); expr * rhs = to_app(body)->get_arg(1); - if (is_pseudo_head(lhs, num_decls, head, t) && - !is_forbidden(head->get_decl()) && + if (is_pseudo_head(lhs, num_decls, head, t) && + !is_forbidden(head->get_decl()) && !occurs(head->get_decl(), rhs)) { def = rhs; return true; } - if (is_pseudo_head(rhs, num_decls, head, t) && - !is_forbidden(head->get_decl()) && + if (is_pseudo_head(rhs, num_decls, head, t) && + !is_forbidden(head->get_decl()) && !occurs(head->get_decl(), lhs)) { def = lhs; return true; @@ -361,7 +363,7 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t /** \brief A quasi-macro head is of the form f[X_1, ..., X_n], where n == num_decls, f[X_1, ..., X_n] is a term starting with symbol f, f is uninterpreted, - contains all universally quantified variables as arguments. + contains all universally quantified variables as arguments. Note that, some arguments of f[X_1, ..., X_n] may not be variables. Examples of quasi-macros: @@ -477,16 +479,16 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { else var_mapping.setx(max_var_idx - i, v); } - + for (unsigned i = num_args; i <= max_var_idx; i++) - // CMW: Won't be used, but dictates a larger binding size, + // CMW: Won't be used, but dictates a larger binding size, // so that the indexes between here and in the rewriter match. // It's possible that we don't see the true max idx of all vars here. - var_mapping.setx(max_var_idx - i, 0); + var_mapping.setx(max_var_idx - i, 0); if (changed) { // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution. - var_subst subst(m_manager, true); + var_subst subst(m_manager, true); TRACE("macro_util_bug", tout << "head: " << mk_pp(head, m_manager) << "\n"; tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; @@ -503,8 +505,8 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { // ----------------------------- // -// "Hint" support -// See comment at is_hint_atom +// "Hint" support +// See comment at is_hint_atom // for a definition of what a hint is. // // ----------------------------- @@ -516,7 +518,7 @@ bool is_hint_head(expr * n, ptr_buffer & vars) { return false; 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); + expr * arg = to_app(n)->get_arg(i); if (is_var(arg)) vars.push_back(to_var(arg)); } @@ -552,7 +554,7 @@ bool vars_of_is_subset(expr * n, ptr_buffer const & vars) { } } else { - SASSERT(is_quantifier(curr)); + SASSERT(is_quantifier(curr)); return false; // do no support nested quantifier... being conservative. } } @@ -560,7 +562,7 @@ bool vars_of_is_subset(expr * n, ptr_buffer const & vars) { } /** - \brief (= lhs rhs) is a hint atom if + \brief (= lhs rhs) is a hint atom if lhs is of the form (f t_1 ... t_n) and all variables occurring in rhs are direct arguments of lhs. */ @@ -598,7 +600,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref /** \brief Return true if n can be viewed as a polynomial "hint" based on head. That is, n (but the monomial exception) only uses the variables in head, and does not use - head->get_decl(). + head->get_decl(). is_hint_head(head, vars) must also return true */ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { @@ -630,7 +632,7 @@ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { } TRACE("macro_util_hint", tout << "succeeded\n";); return true; - + } // ----------------------------- @@ -681,7 +683,7 @@ void macro_util::insert_macro(app * head, expr * def, expr * cond, bool ineq, bo r.insert(head->get_decl(), norm_def.get(), norm_cond.get(), ineq, satisfy_atom, hint); } -void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, +void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) { if (!is_macro_head(head, head->get_num_args())) { app_ref new_head(m_manager); @@ -783,8 +785,8 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a if (!is_app(arg)) continue; func_decl * f = to_app(arg)->get_decl(); - - bool _is_arith_macro = + + bool _is_arith_macro = is_quasi_macro_head(arg, num_decls) && !is_forbidden(f) && !poly_contains_head(lhs, f, arg) && @@ -805,14 +807,14 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a } else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) { f = to_app(neg_arg)->get_decl(); - bool _is_arith_macro = + bool _is_arith_macro = is_quasi_macro_head(neg_arg, num_decls) && !is_forbidden(f) && !poly_contains_head(lhs, f, arg) && !occurs(f, rhs) && !rest_contains_decl(f, atom); bool _is_poly_hint = !_is_arith_macro && is_poly_hint(lhs, to_app(neg_arg), arg); - + if (_is_arith_macro || _is_poly_hint) { collect_poly_args(lhs, arg, args); expr_ref rest(m_manager); @@ -842,34 +844,34 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls, /** \brief Collect macro candidates for atom \c atom. The candidates are stored in \c r. - + The following post-condition holds: for each i in [0, r.size() - 1] we have a conditional macro of the form - + r.get_cond(i) IMPLIES f(x_1, ..., x_n) = r.get_def(i) - + where f == r.get_fs(i) .., x_n), f is uninterpreted and x_1, ..., x_n are variables. r.get_cond(i) and r.get_defs(i) do not contain f or variables not in {x_1, ..., x_n} The idea is to use r.get_defs(i) as the interpretation for f in a model M whenever r.get_cond(i) - - Given a model M and values { v_1, ..., v_n } + + Given a model M and values { v_1, ..., v_n } Let M' be M{x_1 -> v_1, ..., v_n -> v_n} - + Note that M'(f(x_1, ..., x_n)) = M(f)(v_1, ..., v_n) - + Then, IF we have that M(f)(v_1, ..., v_n) = M'(r.get_def(i)) AND M'(r.get_cond(i)) = true THEN M'(atom) = true That is, if the conditional macro is used then the atom is satisfied when M'(r.get_cond(i)) = true - + IF r.is_ineq(i) = false, then M(f)(v_1, ..., v_n) ***MUST BE*** M'(r.get_def(i)) whenever M'(r.get_cond(i)) = true - + IF r.satisfy_atom(i) = true, then we have the stronger property: Then, IF we have that (M'(r.get_cond(i)) = true IMPLIES M(f)(v_1, ..., v_n) = M'(r.get_def(i))) @@ -878,8 +880,8 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls, void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) { expr* lhs, *rhs; if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) { - if (is_quasi_macro_head(lhs, num_decls) && - !is_forbidden(to_app(lhs)->get_decl()) && + if (is_quasi_macro_head(lhs, num_decls) && + !is_forbidden(to_app(lhs)->get_decl()) && !occurs(to_app(lhs)->get_decl(), rhs) && !rest_contains_decl(to_app(lhs)->get_decl(), atom)) { expr_ref cond(m_manager); @@ -889,9 +891,9 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, else if (is_hint_atom(lhs, rhs)) { insert_quasi_macro(to_app(lhs), num_decls, rhs, 0, false, true, true, r); } - - if (is_quasi_macro_head(rhs, num_decls) && - !is_forbidden(to_app(rhs)->get_decl()) && + + if (is_quasi_macro_head(rhs, num_decls) && + !is_forbidden(to_app(rhs)->get_decl()) && !occurs(to_app(rhs)->get_decl(), lhs) && !rest_contains_decl(to_app(rhs)->get_decl(), atom)) { expr_ref cond(m_manager); From ef9230d8f8ae1a39efa6c4d2e45c9ce9b72fd754 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Nov 2016 06:56:36 -0800 Subject: [PATCH 04/10] detect quantifiers in model expressions to quiet down failing model validation Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 4 ++-- src/cmd_context/cmd_context.cpp | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index e1f44e927..91bff5ab5 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -181,7 +181,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && - !occurs(to_app(lhs)->get_decl(), rhs) && !has_quantifiers(rhs)) { + !occurs(to_app(lhs)->get_decl(), rhs)) { head = to_app(lhs); def = rhs; return true; @@ -213,7 +213,7 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && - !occurs(to_app(rhs)->get_decl(), lhs) && !has_quantifiers(lhs)) { + !occurs(to_app(rhs)->get_decl(), lhs)) { head = to_app(rhs); def = lhs; return true; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3cf00c154..eb7b3ff44 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1568,6 +1568,9 @@ void cmd_context::validate_model() { // If r contains as_array/store/map/const expressions, then we do not generate the error. // TODO: improve evaluator for model expressions. // Note that, if "a" evaluates to false, then the error will be generated. + if (has_quantifiers(r)) { + continue; + } try { for_each_expr(contains_array, r); } From 7f923c6a33cde36fc162e859a9c327545dc2b80e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 16:16:55 +0000 Subject: [PATCH 05/10] Include Python API files in distributions. --- examples/python/example.py | 28 +++++++++++++++++++- scripts/mk_project.py | 1 + scripts/mk_unix_dist.py | 10 ++++++- scripts/mk_util.py | 53 +++++++++++++++++++++++++++++++++----- scripts/mk_win_dist.py | 12 +++++++-- 5 files changed, 94 insertions(+), 10 deletions(-) diff --git a/examples/python/example.py b/examples/python/example.py index e0c9374e7..a17668506 100644 --- a/examples/python/example.py +++ b/examples/python/example.py @@ -1,4 +1,30 @@ -# Copyright (c) Microsoft Corporation 2015 +# Copyright (c) Microsoft Corporation 2015, 2016 + +# The Z3 Python API requires libz3.dll/.so/.dylib in the +# PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH +# environment variable and the PYTHON_PATH environment variable +# needs to point to the `python' directory that contains `z3/z3.py' +# (which is at bin/python in our binary releases). + +# If you obtained example.py as part of our binary release zip files, +# which you unzipped into a directory called `MYZ3', then follow these +# instructions to run the example: + +# Running this example on Windows: +# set PATH=%PATH%;MYZ3\bin +# set PYTHONPATH=MYZ3\bin\python +# python example.py + +# Running this example on Linux: +# export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin +# export PYTHONPATH=MYZ3/bin/python +# python example.py + +# Running this example on OSX: +# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin +# export PYTHONPATH=MYZ3/bin/python +# python example.py + from z3 import * diff --git a/scripts/mk_project.py b/scripts/mk_project.py index c03d76b5f..b18e7801b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -94,6 +94,7 @@ def init_project_def(): add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') + add_python(_libz3Component) add_python_install(_libz3Component) # Examples add_cpp_example('cpp_example', 'c++') diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 4905a7141..527797e66 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -26,6 +26,7 @@ DOTNET_ENABLED=True DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False +PYTHON_ENABLED=True def set_verbose(flag): global VERBOSE @@ -55,6 +56,7 @@ def display_help(): print(" --nodotnet do not include .NET bindings in the binary distribution files.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") + print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") exit(0) @@ -69,7 +71,8 @@ def parse_options(): 'nojava', 'nodotnet', 'dotnet-key=', - 'githash' + 'githash', + 'nopython' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -84,6 +87,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--nopython': + PYTHON_ENABLED = False elif opt == '--dotnet-key': DOTNET_KEY_FILE = arg elif opt == '--nojava': @@ -111,6 +116,8 @@ def mk_build_dir(path): if GIT_HASH: opts.append('--githash=%s' % mk_util.git_hash()) opts.append('--git-describe') + if PYTHON_ENABLED: + opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) @@ -181,6 +188,7 @@ def mk_dist_dir(): mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED + mk_util.PYTHON_ENABLED = PYTHON_ENABLED mk_unix_dist(build_path, dist_path) if is_verbose(): print("Generated distribution folder at '%s'" % dist_path) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 873af8432..cf06a10a7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -63,6 +63,7 @@ DOTNET_COMPONENT='dotnet' JAVA_COMPONENT='java' ML_COMPONENT='ml' CPP_COMPONENT='cpp' +PYTHON_COMPONENT='python' ##################### IS_WINDOWS=False IS_LINUX=False @@ -81,6 +82,7 @@ ONLY_MAKEFILES = False Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False +PYTHON_ENABLED=False DOTNET_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False @@ -675,7 +677,7 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED + global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], @@ -748,6 +750,7 @@ def parse_options(): elif opt in ('', '--noomp'): USE_OMP = False elif opt in ('--python'): + PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True else: print("ERROR: Invalid command line option '%s'" % opt) @@ -844,6 +847,9 @@ def is_ml_enabled(): def is_dotnet_enabled(): return DOTNET_ENABLED +def is_python_enabled(): + return PYTHON_ENABLED + def is_python_install_enabled(): return PYTHON_INSTALL_ENABLED @@ -1382,6 +1388,32 @@ class DLLComponent(Component): shutil.copy('%s.a' % os.path.join(build_path, self.dll_name), '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) +class PythonComponent(Component): + def __init__(self, name, libz3Component): + assert isinstance(libz3Component, DLLComponent) + global PYTHON_ENABLED + Component.__init__(self, name, None, []) + self.libz3Component = libz3Component + + def main_component(self): + return False + + def mk_win_dist(self, build_path, dist_path): + if not is_python_enabled(): + return + + src = os.path.join(build_path, 'python', 'z3') + dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3') + if os.path.exists(dst): + shutil.rmtree(dst) + shutil.copytree(src, dst) + + def mk_unix_dist(self, build_path, dist_path): + self.mk_win_dist(build_path, dist_path) + + def mk_makefile(self, out): + return + class PythonInstallComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) @@ -1484,6 +1516,7 @@ class PythonInstallComponent(Component): os.path.join('python', 'z3', '*.pyc'), os.path.join(self.pythonPkgDir,'z3'), in_prefix=self.in_prefix_install) + if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) @@ -2173,6 +2206,15 @@ class PythonExampleComponent(ExampleComponent): print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python'))) out.write('_ex_%s: \n\n' % self.name) + def mk_win_dist(self, build_path, dist_path): + full = os.path.join(EXAMPLE_DIR, self.path) + py = 'example.py' + shutil.copyfile(os.path.join(full, py), + os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py)) + + def mk_unix_dist(self, build_path, dist_path): + self.mk_win_dist(build_path, dist_path) + def reg_component(name, c): global _Id, _Components, _ComponentNames, _Name2Component @@ -2213,6 +2255,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps) reg_component(name, c) +def add_python(libz3Component): + name = 'python' + reg_component(name, PythonComponent(name, libz3Component)) + def add_python_install(libz3Component): name = 'python_install' reg_component(name, PythonInstallComponent(name, libz3Component)) @@ -3230,11 +3276,6 @@ def mk_vs_proj_dll(name, components): def mk_win_dist(build_path, dist_path): for c in get_components(): c.mk_win_dist(build_path, dist_path) - # Add Z3Py to bin directory - print("Adding to %s\n" % dist_path) - for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)): - shutil.copy(os.path.join(build_path, pyc), - os.path.join(dist_path, INSTALL_BIN_DIR, pyc)) def mk_unix_dist(build_path, dist_path): for c in get_components(): diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 145e356fb..65d780f0d 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -28,6 +28,7 @@ DOTNET_ENABLED=True DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False +PYTHON_ENABLED=True def set_verbose(flag): global VERBOSE @@ -60,12 +61,13 @@ def display_help(): print(" --nodotnet do not include .NET bindings in the binary distribution files.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") + print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") exit(0) # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -74,7 +76,8 @@ def parse_options(): 'nojava', 'nodotnet', 'dotnet-key=', - 'githash' + 'githash', + 'nopython' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -89,6 +92,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--nopython': + PYTHON_ENABLED = False elif opt == '--dotnet-key': DOTNET_KEY_FILE = arg elif opt == '--nojava': @@ -118,6 +123,8 @@ def mk_build_dir(path, x64): if GIT_HASH: opts.append('--githash=%s' % mk_util.git_hash()) opts.append('--git-describe') + if PYTHON_ENABLED: + opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) @@ -192,6 +199,7 @@ def mk_dist_dir_core(x64): mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED + mk_util.PYTHON_ENABLED = PYTHON_ENABLED mk_win_dist(build_path, dist_path) if is_verbose(): print("Generated %s distribution folder at '%s'" % (platform, dist_path)) From d57a2a6dce9291acf9c71a561252f3e133f0c894 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 15:32:52 +0000 Subject: [PATCH 06/10] Bumped version to 4.5.0 --- scripts/mk_project.py | 2 +- src/api/python/setup.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b18e7801b..986e92bde 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, 4, 2, 1) + set_version(4, 5, 0, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 95843aac0..d7d3722b3 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -139,7 +139,7 @@ class sdist(_sdist): setup( name='z3-solver', - version='4.4.2.1', + version='4.5.0.0', description='an efficient SMT solver library', long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3', author="The Z3 Theorem Prover Project", From 00ada5305ff672448576c61525cef3958f9457de Mon Sep 17 00:00:00 2001 From: Dominic Chen Date: Mon, 7 Nov 2016 17:42:44 -0500 Subject: [PATCH 07/10] Standardize on __uint64 instead of unsigned __int64 --- src/api/api_datalog.cpp | 4 ++-- src/api/z3_api.h | 12 ++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 903fedd0f..cc512c08e 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -189,7 +189,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size) { + Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size) { Z3_TRY; LOG_Z3_mk_finite_domain_sort(c, name, size); RESET_ERROR_CODE(); @@ -199,7 +199,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64 * out) { + Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64 * out) { Z3_TRY; if (out) { *out = 0; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 069f83340..c7749ebef 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1807,7 +1807,7 @@ extern "C" { def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64))) */ - Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size); + Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size); /** \brief Create an array type. @@ -3143,14 +3143,14 @@ extern "C" { /** \brief Create a numeral of a int, bit-vector, or finite-domain sort. - This function can be use to create numerals that fit in a machine unsigned __int64 integer. + This function can be use to create numerals that fit in a machine __uint64 integer. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. \sa Z3_mk_numeral def_API('Z3_mk_unsigned_int64', AST, (_in(CONTEXT), _in(UINT64), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned __int64 v, Z3_sort ty); + Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty); /*@}*/ @@ -3722,7 +3722,7 @@ extern "C" { def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) */ - Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64* r); + Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64* r); /** \brief Return the domain of the given array sort. @@ -4288,7 +4288,7 @@ extern "C" { /** \brief Similar to #Z3_get_numeral_string, but only succeeds if - the value can fit in a machine unsigned __int64 int. Return Z3_TRUE if the call succeeded. + the value can fit in a machine __uint64 int. Return Z3_TRUE if the call succeeded. \pre Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST @@ -4296,7 +4296,7 @@ extern "C" { def_API('Z3_get_numeral_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64))) */ - Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64* u); + Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, __uint64* u); /** \brief Similar to #Z3_get_numeral_string, but only succeeds if From 889e5e93884699a972c2c644701e1d63b897dc9e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 23:19:59 +0000 Subject: [PATCH 08/10] Bumped version number. --- scripts/mk_project.py | 2 +- src/api/python/setup.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 986e92bde..7ba88c1b3 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, 5, 0, 0) + set_version(4, 5, 1, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index d7d3722b3..9c18da01e 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -139,7 +139,7 @@ class sdist(_sdist): setup( name='z3-solver', - version='4.5.0.0', + version='4.5.1.0', description='an efficient SMT solver library', long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3', author="The Z3 Theorem Prover Project", From 18e7b2d28e6bcea76b7b3bd9414d15caf21a5a6f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Nov 2016 08:29:38 +0000 Subject: [PATCH 09/10] [CMake] Bump the version number in the CMake build. --- CMakeLists.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 6a2ed0ebd..1ca94689e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -32,9 +32,9 @@ project(Z3 C CXX) # Project version ################################################################################ set(Z3_VERSION_MAJOR 4) -set(Z3_VERSION_MINOR 4) -set(Z3_VERSION_PATCH 2) -set(Z3_VERSION_TWEAK 1) +set(Z3_VERSION_MINOR 5) +set(Z3_VERSION_PATCH 1) +set(Z3_VERSION_TWEAK 0) set(Z3_FULL_VERSION 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") message(STATUS "Z3 version ${Z3_VERSION}") From a3e4629996df0a9cc126e420db912fdf567e37a1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Nov 2016 15:12:04 +0000 Subject: [PATCH 10/10] fixed hard-coded version number in setup.py --- src/api/python/setup.py | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 9c18da01e..ff3b0736d 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -4,6 +4,7 @@ import shutil import platform import subprocess import multiprocessing +import re from setuptools import setup from distutils.errors import LibError from distutils.command.build import build as _build @@ -43,6 +44,16 @@ def _clean_bins(): shutil.rmtree(BINS_DIR, ignore_errors=True) shutil.rmtree(HEADERS_DIR, ignore_errors=True) +def _z3_version(): + fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') + if os.path.exists(fn): + with open(fn) as f: + for line in f: + n = re.match(".*set_version\((.*), (.*), (.*), (.*)\).*", line) + if not n is None: + return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + return "?.?.?.?" + def _configure_z3(): # bail out early if we don't need to do this - it forces a rebuild every time otherwise if os.path.exists(BUILD_DIR): @@ -139,7 +150,7 @@ class sdist(_sdist): setup( name='z3-solver', - version='4.5.1.0', + version=_z3_version(), description='an efficient SMT solver library', long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3', author="The Z3 Theorem Prover Project",