From 7e2afca2c60b4418f11a42bc7cb9762819d07623 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2019 13:24:07 -0700 Subject: [PATCH 01/13] add card operator to bapa Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 27 +++++++++++++++++++++--- src/ast/array_decl_plugin.h | 6 ++++++ src/ast/rewriter/array_rewriter.cpp | 15 +++++++------- src/smt/theory_array_bapa.cpp | 32 +++++++++++++++++++++++------ src/smt/theory_array_bapa.h | 2 +- src/smt/theory_array_base.h | 2 ++ src/smt/theory_array_full.cpp | 6 +++--- 7 files changed, 70 insertions(+), 20 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index f7a299131..071a35af0 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -36,7 +36,8 @@ array_decl_plugin::array_decl_plugin(): m_set_subset_sym("subset"), m_array_ext_sym("array-ext"), m_as_array_sym("as-array"), - m_set_has_size_sym("set-has-size") { + m_set_has_size_sym("set-has-size"), + m_set_card_sym("card") { } #define ARRAY_SORT_STR "Array" @@ -440,6 +441,21 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma func_decl_info(m_family_id, OP_SET_SUBSET)); } +func_decl * array_decl_plugin::mk_set_card(unsigned arity, sort * const* domain) { + if (arity != 1) { + m_manager->raise_exception("card takes only one argument"); + return nullptr; + } + + arith_util arith(*m_manager); + if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) { + m_manager->raise_exception("card expects an array of Booleans"); + } + sort * int_sort = arith.mk_int(); + return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort, + func_decl_info(m_family_id, OP_SET_CARD)); +} + func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) { if (arity != 2) { m_manager->raise_exception("set-has-size takes two arguments"); @@ -525,6 +541,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_set_subset(arity, domain); case OP_SET_HAS_SIZE: return mk_set_has_size(arity, domain); + case OP_SET_CARD: + return mk_set_card(arity, domain); case OP_AS_ARRAY: { if (num_parameters != 1 || !parameters[0].is_ast() || @@ -548,8 +566,10 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters void array_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT)); sort_names.push_back(builtin_name("=>", ARRAY_SORT)); - // TBD: this could easily break users even though it is already used in CVC4: - // sort_names.push_back(builtin_name("Set", _SET_SORT)); + if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) { + // this could easily break users even though it is already used in CVC4: + sort_names.push_back(builtin_name("Set", _SET_SORT)); + } } void array_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { @@ -568,6 +588,7 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT)); op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE)); + op_names.push_back(builtin_name("card", OP_SET_CARD)); } } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 6ba129444..e4725901e 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -52,6 +52,7 @@ enum array_op_kind { OP_SET_COMPLEMENT, OP_SET_SUBSET, OP_SET_HAS_SIZE, + OP_SET_CARD, OP_AS_ARRAY, // used for model construction LAST_ARRAY_OP }; @@ -70,6 +71,7 @@ class array_decl_plugin : public decl_plugin { symbol m_array_ext_sym; symbol m_as_array_sym; symbol m_set_has_size_sym; + symbol m_set_card_sym; bool check_set_arguments(unsigned arity, sort * const * domain); @@ -99,6 +101,8 @@ class array_decl_plugin : public decl_plugin { func_decl* mk_set_has_size(unsigned arity, sort * const* domain); + func_decl* mk_set_card(unsigned arity, sort * const* domain); + bool is_array_sort(sort* s) const; public: array_decl_plugin(); @@ -149,12 +153,14 @@ public: bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); } bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); } bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); } + bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); } bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); } bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); } bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); } bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); } bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); } bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); } + bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); } bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 61860ec4b..3aef589b6 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -69,14 +69,15 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c st = mk_set_difference(args[0], args[1], result); break; default: - return BR_FAILED; + st = BR_FAILED; + break; } - TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n"; - for (unsigned i = 0; i < num_args; ++i) { - tout << mk_pp(args[i], m()) << "\n"; - } - tout << "\n --> " << result << "\n"; - ); + CTRACE("array_rewriter", st != BR_FAILED, + tout << mk_pp(f, m()) << "\n"; + for (unsigned i = 0; i < num_args; ++i) { + tout << mk_pp(args[i], m()) << "\n"; + } + tout << "\n --> " << result << "\n";); return st; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 1dce9832d..47a57c6d0 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -204,7 +204,7 @@ namespace smt { return l_true; } - lbool ensure_disjoint(app* sz1, app* sz2) { + bool ensure_disjoint(app* sz1, app* sz2) { sz_info& i1 = *m_sizeof[sz1]; sz_info& i2 = *m_sizeof[sz2]; SASSERT(i1.m_is_leaf); @@ -214,16 +214,16 @@ namespace smt { enode* r1 = get_root(s); enode* r2 = get_root(t); if (r1 == r2) { - return l_true; + return true; } if (!ctx().is_diseq(r1, r2) && ctx().assume_eq(r1, r2)) { - return l_false; + return false; } if (do_intersect(i1.m_selects, i2.m_selects)) { add_disjoint(sz1, sz2); - return l_false; + return false; } - return l_true; + return true; } bool do_intersect(obj_map const& s, obj_map const& t) const { @@ -436,6 +436,15 @@ namespace smt { reset(); } + void internalize_term(app* term) { + if (th.is_set_has_size(term)) { + internalize_size(term); + } + else if (th.is_set_card(term)) { + internalize_card(term); + } + } + /** * Size(S, n) => n >= 0, default(S) = false */ @@ -458,6 +467,17 @@ namespace smt { ctx().push_trail(remove_sz(m_sizeof, term)); } + /** + \brief whenever there is a cardinality function, it includes an axiom + that entails the set is finite. + */ + void internalize_card(app* term) { + SASSERT(ctx().e_internalized(term)); + app_ref has_size(m_autil.mk_has_size(term->get_arg(0), term), m); + literal lit = mk_literal(has_size); + ctx().assign(lit, nullptr); + } + final_check_status final_check() { lbool r = ensure_functional(); if (r == l_true) update_indices(); @@ -494,7 +514,7 @@ namespace smt { theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); } - void theory_array_bapa::internalize_size(app* term) { m_imp->internalize_size(term); } + void theory_array_bapa::internalize_term(app* term) { m_imp->internalize_term(term); } final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); } diff --git a/src/smt/theory_array_bapa.h b/src/smt/theory_array_bapa.h index e99843cdd..5ac51f8a9 100644 --- a/src/smt/theory_array_bapa.h +++ b/src/smt/theory_array_bapa.h @@ -32,7 +32,7 @@ namespace smt { public: theory_array_bapa(theory_array_full& th); ~theory_array_bapa(); - void internalize_size(app* term); + void internalize_term(app* term); final_check_status final_check(); void init_model(); }; diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 5a6321379..3fc8be613 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -43,6 +43,7 @@ namespace smt { bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); } bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); } bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); } + bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); } bool is_store(enode const * n) const { return is_store(n->get_owner()); } bool is_map(enode const* n) const { return is_map(n->get_owner()); } @@ -52,6 +53,7 @@ namespace smt { bool is_default(enode const* n) const { return is_default(n->get_owner()); } bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); } bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); } + bool is_set_carde(enode const* n) const { return is_set_card(n->get_owner()); } app * mk_select(unsigned num_args, expr * const * args); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 4457d99ff..ce8def177 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -250,7 +250,7 @@ namespace smt { return theory_array::internalize_term(n); } - if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n)) { + if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n) && !is_set_card(n)) { if (!is_array_ext(n)) found_unsupported_op(n); return false; @@ -274,11 +274,11 @@ namespace smt { mk_var(arg0); } } - else if (is_set_has_size(n)) { + else if (is_set_has_size(n) || is_set_card(n)) { if (!m_bapa) { m_bapa = alloc(theory_array_bapa, *this); } - m_bapa->internalize_size(n); + m_bapa->internalize_term(n); } enode* node = ctx.get_enode(n); From fa88bdb07550afbb12cc69c0ef6895f766ced290 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 09:44:18 -0700 Subject: [PATCH 02/13] fix #2251 thanks to Clark Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 2 +- src/ast/array_decl_plugin.cpp | 15 +++-- src/ast/array_decl_plugin.h | 24 ++++++++ src/ast/ast_smt_pp.cpp | 11 ++-- src/ast/decl_collector.h | 4 +- src/ast/rewriter/array_rewriter.cpp | 88 ++++++++++++++++++++++++++--- src/ast/rewriter/array_rewriter.h | 3 + src/cmd_context/cmd_context.cpp | 6 +- src/smt/theory_array_bapa.cpp | 13 ++++- src/tactic/tactical.cpp | 2 +- 10 files changed, 138 insertions(+), 30 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index d48ce76e2..04d7793a0 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -580,7 +580,7 @@ extern "C" { expr* args[2] = { _t, _v }; sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; parameter param(_f); - func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); + func_decl * d = m.mk_func_decl(mk_c(c)->get_dt_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); app* r = m.mk_app(d, 2, args); mk_c(c)->save_ast_trail(r); check_sorts(c, r); diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 071a35af0..66cf0e742 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -30,8 +30,8 @@ array_decl_plugin::array_decl_plugin(): m_default_sym("default"), m_map_sym("map"), m_set_union_sym("union"), - m_set_intersect_sym("intersect"), - m_set_difference_sym("difference"), + m_set_intersect_sym("intersection"), + m_set_difference_sym("setminus"), m_set_complement_sym("complement"), m_set_subset_sym("subset"), m_array_ext_sym("array-ext"), @@ -581,8 +581,8 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("map",OP_ARRAY_MAP)); op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT)); op_names.push_back(builtin_name("union",OP_SET_UNION)); - op_names.push_back(builtin_name("intersect",OP_SET_INTERSECT)); - op_names.push_back(builtin_name("difference",OP_SET_DIFFERENCE)); + op_names.push_back(builtin_name("intersection",OP_SET_INTERSECT)); + op_names.push_back(builtin_name("setminus",OP_SET_DIFFERENCE)); op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT)); op_names.push_back(builtin_name("subset",OP_SET_SUBSET)); op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); @@ -616,6 +616,13 @@ func_decl * array_recognizers::get_as_array_func_decl(expr * n) const { return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast()); } +func_decl * array_recognizers::get_map_func_decl(func_decl* f) const { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_ast()); + SASSERT(is_func_decl(f->get_parameter(0).get_ast())); + return to_func_decl(f->get_parameter(0).get_ast()); +} + func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const { SASSERT(is_as_array(f)); return to_func_decl(f->get_parameter(0).get_ast()); diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index e4725901e..130184a6e 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -164,6 +164,8 @@ public: bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; + func_decl * get_map_func_decl(func_decl* f) const; + func_decl * get_map_func_decl(expr* e) const { return get_map_func_decl(to_app(e)->get_decl()); } bool is_const(expr* e, expr*& v) const; @@ -190,6 +192,16 @@ public: parameter p(f); return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args); } + + expr * mk_map_assoc(func_decl * f, unsigned num_args, expr * const * args) { + expr* r = args[0]; + for (unsigned i = 1; i < num_args; ++i) { + expr* es[2] = { r, args[i] }; + r = mk_map(f, 2, es); + } + return r; + } + app * mk_const_array(sort * s, expr * v) { parameter param(s); return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, &v); @@ -201,6 +213,18 @@ public: return mk_const_array(s, m_manager.mk_true()); } + app * mk_setminus(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, s1, s2); + } + + app * mk_intersection(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_INTERSECT, s1, s2); + } + + app * mk_union(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_UNION, s1, s2); + } + app* mk_has_size(expr* set, expr* n) { return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 48daf6988..e9b6a9766 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -924,11 +924,11 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { decl_collector decls(m); smt_renaming rn; - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - decls.visit(m_assumptions[i].get()); + for (expr* a : m_assumptions) { + decls.visit(a); } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - decls.visit(m_assumptions_star[i].get()); + for (expr* a : m_assumptions_star) { + decls.visit(a); } decls.visit(n); @@ -959,8 +959,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { #else decls.order_deps(); ast_mark sort_mark; - for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { - sort* s = decls.get_sorts()[i]; + for (sort* s : decls.get_sorts()) { if (!(*m_is_declared)(s)) { smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p.pp_sort_decl(sort_mark, s); diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 8945c0bec..a567f759c 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -57,8 +57,8 @@ public: unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); } - sort * const * get_sorts() const { return m_sorts.c_ptr(); } - func_decl * const * get_func_decls() const { return m_decls.c_ptr(); } + ptr_vector const& get_sorts() const { return m_sorts; } + ptr_vector const& get_func_decls() const { return m_decls; } }; #endif diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 3aef589b6..3fc413d67 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -45,10 +45,7 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c st = mk_store_core(num_args, args, result); break; case OP_ARRAY_MAP: - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_ast()); - SASSERT(is_func_decl(f->get_parameter(0).get_ast())); - st = mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result); + st = mk_map_core(m_util.get_map_func_decl(f), num_args, args, result); break; case OP_SET_UNION: st = mk_set_union(num_args, args, result); @@ -242,6 +239,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, return BR_FAILED; } +sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) { + sort* s0 = m().get_sort(args[0]); + unsigned sz = get_array_arity(s0); + ptr_vector domain; + for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); + return sort_ref(m_util.mk_array_sort(sz, domain.c_ptr(), f->get_range()), m()); +} + br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { app* store_expr = nullptr; @@ -292,11 +297,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c } else { expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m()); - sort* s0 = m().get_sort(args[0]); - unsigned sz = get_array_arity(s0); - ptr_vector domain; - for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); - sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m()); + sort_ref s = get_map_array_sort(f, num_args, args); result = m_util.mk_const_array(s, value); } return BR_REWRITE2; @@ -337,6 +338,75 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c return BR_REWRITE3; } + if (m().is_and(f)) { + ast_mark mark; + ptr_buffer es; + bool change = false; + unsigned j = 0; + es.append(num_args, args); + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (mark.is_marked(e)) { + change = true; + } + else if (m_util.is_map(e) && m().is_and(m_util.get_map_func_decl(e))) { + mark.mark(e, true); + es.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + mark.mark(e, true); + es[j++] = es[i]; + } + } + es.shrink(j); + for (expr* e : es) { + if (m().is_not(e, e) && mark.is_marked(e)) { + sort_ref s = get_map_array_sort(f, num_args, args); + result = m_util.mk_const_array(s, m().mk_false()); + return BR_DONE; + } + } + if (change) { + result = m_util.mk_map_assoc(f, es.size(), es.c_ptr()); + return BR_DONE; + } + } + + if (m().is_or(f)) { + ast_mark mark; + ptr_buffer es; + es.append(num_args, args); + unsigned j = 0; + bool change = false; + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (mark.is_marked(e)) { + change = true; + } + else if (m_util.is_map(e) && m().is_or(m_util.get_map_func_decl(e))) { + mark.mark(e, true); + es.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + mark.mark(e, true); + es[j++] = es[i]; + } + } + es.shrink(j); + for (expr* e : es) { + if (m().is_not(e, e) && mark.is_marked(e)) { + sort_ref s = get_map_array_sort(f, num_args, args); + result = m_util.mk_const_array(s, m().mk_true()); + return BR_DONE; + } + } + if (change) { + result = m_util.mk_map_assoc(f, es.size(), es.c_ptr()); + return BR_DONE; + } + } + + return BR_FAILED; } diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index 056ef66c4..18fb74adb 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -37,6 +37,9 @@ class array_rewriter { lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2); bool has_index_set(expr* e, expr_ref& e0, vector& indices); void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls); + + sort_ref get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args); + public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 9fbeced71..50d87029e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2033,10 +2033,8 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr // TODO: display uninterpreted sort decls, and datatype decls. - unsigned num_decls = decls.get_num_decls(); - func_decl * const * fs = decls.get_func_decls(); - for (unsigned i = 0; i < num_decls; i++) { - display(out, fs[i]); + for (func_decl* f : decls.get_func_decls()) { + display(out, f); out << std::endl; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 47a57c6d0..872b8c3e7 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -102,7 +102,7 @@ namespace smt { theory_array_full& th; arith_util m_arith; array_util m_autil; - array_rewriter m_rw; + th_rewriter m_rw; arith_value m_arith_value; ast_ref_vector m_pinned; obj_map m_sizeof; @@ -211,6 +211,9 @@ namespace smt { SASSERT(i2.m_is_leaf); expr* s = sz1->get_arg(0); expr* t = sz2->get_arg(0); + if (m.get_sort(s) != m.get_sort(t)) { + return true; + } enode* r1 = get_root(s); enode* r2 = get_root(t); if (r1 == r2) { @@ -265,11 +268,15 @@ namespace smt { } expr_ref mk_subtract(expr* t, expr* s) { - return m_rw.mk_set_difference(t, s); + expr_ref d(m_autil.mk_setminus(t, s), m); + m_rw(d); + return d; } expr_ref mk_intersect(expr* t, expr* s) { - return m_rw.mk_set_intersect(t, s); + expr_ref i(m_autil.mk_intersection(t, s), m); + m_rw(i); + return i; } void propagate(expr* assumption, expr* conseq) { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 98f6be343..00ea59869 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -917,7 +917,7 @@ public: { // Warning: scoped_timer is not thread safe in Linux. scoped_timer timer(m_timeout, &eh); - m_t->operator()(in, result); + m_t->operator()(in, result); } } From 40e329fc92e91acc9efda668e8d6d034221fe887 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 10:13:15 -0700 Subject: [PATCH 03/13] remove push/pop for fixedpoint objects from API #2249 Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 17 ----------------- src/api/c++/z3++.h | 2 -- src/api/dotnet/Fixedpoint.cs | 20 -------------------- src/api/java/Fixedpoint.java | 19 ------------------- src/api/ml/z3.ml | 2 -- src/api/ml/z3.mli | 10 ---------- src/api/python/z3/z3.py | 8 -------- src/api/z3_fixedpoint.h | 23 ----------------------- 8 files changed, 101 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 57037f1a8..e872bc12d 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -588,23 +588,6 @@ extern "C" { Z3_CATCH; } - void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d) { - Z3_TRY; - LOG_Z3_fixedpoint_push(c, d); - RESET_ERROR_CODE(); - to_fixedpoint_ref(d)->ctx().push(); - Z3_CATCH; - } - - void Z3_API Z3_fixedpoint_pop(Z3_context c,Z3_fixedpoint d) { - Z3_TRY; - LOG_Z3_fixedpoint_pop(c, d); - RESET_ERROR_CODE(); - to_fixedpoint_ref(d)->ctx().pop(); - Z3_CATCH; - - } - void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d, void *state, Z3_fixedpoint_new_lemma_eh new_lemma_eh, diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6af38cb82..175fe87fc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2787,8 +2787,6 @@ namespace z3 { array qs(queries); return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr()); } - void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); } - void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); } }; inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 51ee79b55..dc4de8925 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -161,26 +161,6 @@ namespace Microsoft.Z3 } } - /// - /// Creates a backtracking point. - /// - /// - public void Push() - { - Native.Z3_fixedpoint_push(Context.nCtx, NativeObject); - } - - /// - /// Backtrack one backtracking point. - /// - /// Note that an exception is thrown if Pop is called without a corresponding Push - /// - public void Pop() - { - Native.Z3_fixedpoint_pop(Context.nCtx, NativeObject); - } - - /// /// Update named rule into in the fixedpoint solver. /// diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 7bb0fda58..8560b6292 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -157,25 +157,6 @@ public class Fixedpoint extends Z3Object } } - /** - * Creates a backtracking point. - * @see #pop - **/ - public void push() { - Native.fixedpointPush(getContext().nCtx(), getNativeObject()); - } - - /** - * Backtrack one backtracking point. - * Remarks: Note that an exception is thrown if {@code pop} - * is called without a corresponding {@code push} - * - * @see #push - **/ - public void pop() { - Native.fixedpointPop(getContext().nCtx(), getNativeObject()); - } - /** * Update named rule into in the fixedpoint solver. * diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 50735a57c..825f3606c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1883,8 +1883,6 @@ struct | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - let push x = Z3native.fixedpoint_push (gc x) x - let pop x = Z3native.fixedpoint_pop (gc x) x let update_rule x = Z3native.fixedpoint_update_rule (gc x) x let get_answer x = diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 69dbfa23d..678f99443 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3256,16 +3256,6 @@ sig The query is unsatisfiable if there are no derivations satisfying any of the relations. *) val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status - (** Creates a backtracking point. - {!pop} *) - val push : fixedpoint -> unit - - (** Backtrack one backtracking point. - - Note that an exception is thrown if Pop is called without a corresponding [Push] - {!push} *) - val pop : fixedpoint -> unit - (** Update named rule into in the fixedpoint solver. *) val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6d6220fb5..3bd0df612 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7047,14 +7047,6 @@ class Fixedpoint(Z3PPObject): r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl) return CheckSatResult(r) - def push(self): - """create a backtracking point for added rules, facts and assertions""" - Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint) - - def pop(self): - """restore to previously created backtracking point""" - Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint) - def update_rule(self, head, body, name): """update rule""" if name is None: diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index 54a42e9bf..33b970371 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -334,29 +334,6 @@ extern "C" { Z3_fixedpoint f, Z3_string s); - /** - \brief Create a backtracking point. - - The fixedpoint solver contains a set of rules, added facts and assertions. - The set of rules, facts and assertions are restored upon calling #Z3_fixedpoint_pop. - - \sa Z3_fixedpoint_pop - - def_API('Z3_fixedpoint_push', VOID, (_in(CONTEXT), _in(FIXEDPOINT))) - */ - void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d); - - /** - \brief Backtrack one backtracking point. - - \sa Z3_fixedpoint_push - - \pre The number of calls to pop cannot exceed calls to push. - - def_API('Z3_fixedpoint_pop', VOID, (_in(CONTEXT), _in(FIXEDPOINT))) - */ - void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d); - /** \brief The following utilities allows adding user-defined domains. */ typedef void Z3_fixedpoint_reduce_assign_callback_fptr( From e1b52c323c5c7dc717561a589068aed0ea996879 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 10:19:06 -0700 Subject: [PATCH 04/13] add quotes to install path for .net Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 8792f825e..b8122348c 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -178,7 +178,7 @@ option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install targ if(INSTALL_DOTNET_BINDINGS) install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget") # move the local repo to the installation directory (cancel the build-time repo) - install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)") + install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" \"${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget\")") install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget") # TODO GAC? # set(GAC_PKG_NAME "Microsoft.Z3.Sharp") From 6af6617e36cefe2838ccc9d165dd79f8a5d449ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 10:39:44 -0700 Subject: [PATCH 05/13] fix #2248 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq_empty.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 93b4be173..81f1af06f 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -117,6 +117,7 @@ namespace smt { } if (u.is_seq(s, ch)) { expr* v = m_model.get_fresh_value(ch); + if (!v) return nullptr; return u.str.mk_unit(v); } UNREACHABLE(); From 944ce1135b8d2ffb83656f25cd473bb7161b2c1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 13:47:53 -0700 Subject: [PATCH 06/13] replace __debug__ by Z3_DEBUG #2225 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 272 +++++++++++++++--------------- src/api/python/z3/z3util.py | 18 +- src/nlsat/nlsat_solver.cpp | 11 +- src/nlsat/tactic/nlsat_tactic.cpp | 7 + 4 files changed, 162 insertions(+), 146 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 3bd0df612..5475af254 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -53,6 +53,8 @@ import io import math import copy +Z3_DEUBG = __debug__ + if sys.version < '3': def _is_int(v): return isinstance(v, (int, long)) @@ -166,7 +168,7 @@ class Context: The initialization method receives global configuration options for the new context. """ def __init__(self, *args, **kws): - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") conf = Z3_mk_config() for key in kws: @@ -235,7 +237,7 @@ def set_param(*args, **kws): >>> set_param(precision=10) """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") new_kws = {} for k in kws: @@ -360,7 +362,7 @@ class AstRef(Z3PPObject): >>> n1.eq(n2) True """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_ast(other), "Z3 AST expected") return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast()) @@ -376,7 +378,7 @@ class AstRef(Z3PPObject): >>> x.translate(c2) + y x + y """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(target, Context), "argument must be a Z3 context") return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target) @@ -427,7 +429,7 @@ def eq(a, b): >>> eq(simplify(x + 1), simplify(1 + x)) True """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected") return a.eq(b) @@ -443,7 +445,7 @@ def _ctx_from_ast_arg_list(args, default_ctx=None): if ctx is None: ctx = a.ctx else: - if __debug__: + if Z3_DEBUG: _z3_assert(ctx == a.ctx, "Context mismatch") if ctx is None: ctx = default_ctx @@ -534,7 +536,7 @@ class SortRef(AstRef): >>> RealSort().cast(x) ToReal(x) """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_expr(val), "Z3 expression expected") _z3_assert(self.eq(val.sort()), "Sort mismatch") return val @@ -590,7 +592,7 @@ def is_sort(s): return isinstance(s, SortRef) def _to_sort_ref(s, ctx): - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(s, Sort), "Z3 Sort expected") k = _sort_kind(ctx, s) if k == Z3_BOOL_SORT: @@ -687,7 +689,7 @@ class FuncDeclRef(AstRef): >>> f.domain(1) Real """ - if __debug__: + if Z3_DEBUG: _z3_assert(i < self.arity(), "Index out of bounds") return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx) @@ -756,7 +758,7 @@ class FuncDeclRef(AstRef): """ args = _get_args(args) num = len(args) - if __debug__: + if Z3_DEBUG: _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self) _args = (Ast * num)() saved = [] @@ -788,15 +790,15 @@ def Function(name, *sig): f(f(0)) """ sig = _get_args(sig) - if __debug__: + if Z3_DEBUG: _z3_assert(len(sig) > 0, "At least two arguments expected") arity = len(sig) - 1 rng = sig[arity] - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(rng), "Z3 sort expected") dom = (Sort * arity)() for i in range(arity): - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(sig[i]), "Z3 sort expected") dom[i] = sig[i].ast ctx = rng.ctx @@ -808,15 +810,15 @@ def _to_func_decl_ref(a, ctx): def RecFunction(name, *sig): """Create a new Z3 recursive with the given sorts.""" sig = _get_args(sig) - if __debug__: + if Z3_DEBUG: _z3_assert(len(sig) > 0, "At least two arguments expected") arity = len(sig) - 1 rng = sig[arity] - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(rng), "Z3 sort expected") dom = (Sort * arity)() for i in range(arity): - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(sig[i]), "Z3 sort expected") dom[i] = sig[i].ast ctx = rng.ctx @@ -946,7 +948,7 @@ class ExprRef(AstRef): >>> (a + 1).decl() + """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) @@ -962,7 +964,7 @@ class ExprRef(AstRef): >>> t.num_args() 3 """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_app(self), "Z3 application expected") return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast())) @@ -982,7 +984,7 @@ class ExprRef(AstRef): >>> t.arg(2) 0 """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_app(self), "Z3 application expected") _z3_assert(idx < self.num_args(), "Invalid argument index") return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx) @@ -1061,7 +1063,7 @@ def _coerce_expr_merge(s, a): elif s1.subsort(s): return s else: - if __debug__: + if Z3_DEBUG: _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") else: @@ -1213,7 +1215,7 @@ def get_var_index(a): >>> get_var_index(v2) 0 """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_var(a), "Z3 bound variable expected") return int(Z3_get_index_value(a.ctx.ref(), a.as_ast())) @@ -1247,7 +1249,7 @@ def If(a, b, c, ctx=None): s = BoolSort(ctx) a = s.cast(a) b, c = _coerce_exprs(b, c, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(a.ctx == b.ctx, "Context mismatch") return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) @@ -1268,7 +1270,7 @@ def Distinct(*args): """ args = _get_args(args) ctx = _ctx_from_ast_arg_list(args) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) _args, sz = _to_ast_array(args) @@ -1276,7 +1278,7 @@ def Distinct(*args): def _mk_bin(f, a, b): args = (Ast * 2)() - if __debug__: + if Z3_DEBUG: _z3_assert(a.ctx == b.ctx, "Context mismatch") args[0] = a.as_ast() args[1] = b.as_ast() @@ -1288,7 +1290,7 @@ def Const(name, sort): >>> Const('x', IntSort()) x """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(sort, SortRef), "Z3 sort expected") ctx = sort.ctx return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx) @@ -1320,7 +1322,7 @@ def Var(idx, s): >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(s), "Z3 sort expected") return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx) @@ -1368,7 +1370,7 @@ class BoolSortRef(SortRef): """ if isinstance(val, bool): return BoolVal(val, self.ctx) - if __debug__: + if Z3_DEBUG: if not is_expr(val): _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) if not self.eq(val.sort()): @@ -1686,7 +1688,7 @@ def And(*args): ctx = main_ctx() args = _get_args(args) ctx_args = _ctx_from_ast_arg_list(args, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): @@ -1716,7 +1718,7 @@ def Or(*args): ctx = main_ctx() args = _get_args(args) ctx_args = _ctx_from_ast_arg_list(args, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): @@ -1775,7 +1777,7 @@ def MultiPattern(*args): >>> q.pattern(0) MultiPattern(f(Var(0)), g(Var(0))) """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 0, "At least one argument expected") _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") ctx = args[0].ctx @@ -1891,7 +1893,7 @@ class QuantifierRef(BoolRef): >>> q.pattern(1) g(Var(0)) """ - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1901,7 +1903,7 @@ class QuantifierRef(BoolRef): def no_pattern(self, idx): """Return a no-pattern.""" - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1940,7 +1942,7 @@ class QuantifierRef(BoolRef): >>> q.var_name(1) 'y' """ - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_vars(), "Invalid variable idx") return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) @@ -1956,7 +1958,7 @@ class QuantifierRef(BoolRef): >>> q.var_sort(1) Real """ - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_vars(), "Invalid variable idx") return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1985,7 +1987,7 @@ def is_quantifier(a): return isinstance(a, QuantifierRef) def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): - if __debug__: + if Z3_DEBUG: _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") @@ -2131,7 +2133,7 @@ class ArithSortRef(SortRef): True """ if is_expr(val): - if __debug__: + if Z3_DEBUG: _z3_assert(self.ctx == val.ctx, "Context mismatch") val_s = val.sort() if self.eq(val_s): @@ -2142,14 +2144,14 @@ class ArithSortRef(SortRef): return If(val, 1, 0) if val_s.is_bool() and self.is_real(): return ToReal(If(val, 1, 0)) - if __debug__: + if Z3_DEBUG: _z3_assert(False, "Z3 Integer/Real expression expected" ) else: if self.is_int(): return IntVal(val, self.ctx) if self.is_real(): return RealVal(val, self.ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) def is_arith_sort(s): @@ -2363,7 +2365,7 @@ class ArithRef(ExprRef): 1 """ a, b = _coerce_exprs(self, other) - if __debug__: + if Z3_DEBUG: _z3_assert(a.is_int(), "Z3 integer expression expected") return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) @@ -2375,7 +2377,7 @@ class ArithRef(ExprRef): 10%x """ a, b = _coerce_exprs(self, other) - if __debug__: + if Z3_DEBUG: _z3_assert(a.is_int(), "Z3 integer expression expected") return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) @@ -2736,7 +2738,7 @@ class IntNumRef(ArithRef): >>> v.as_long() + 1 2 """ - if __debug__: + if Z3_DEBUG: _z3_assert(self.is_int(), "Integer value expected") return int(self.as_string()) @@ -2878,7 +2880,7 @@ def _py2expr(a, ctx=None): return RealVal(a, ctx) if is_expr(a): return a - if __debug__: + if Z3_DEBUG: _z3_assert(False, "Python bool, int, long or float expected") def IntSort(ctx=None): @@ -2925,7 +2927,7 @@ def _to_int_str(val): return str(val) elif isinstance(val, str): return val - if __debug__: + if Z3_DEBUG: _z3_assert(False, "Python value cannot be used as a Z3 integer") def IntVal(val, ctx=None): @@ -2967,7 +2969,7 @@ def RatVal(a, b, ctx=None): >>> RatVal(3,5).sort() Real """ - if __debug__: + if Z3_DEBUG: _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") return simplify(RealVal(a, ctx)/RealVal(b, ctx)) @@ -3096,7 +3098,7 @@ def ToReal(a): >>> n.sort() Real """ - if __debug__: + if Z3_DEBUG: _z3_assert(a.is_int(), "Z3 integer expression expected.") ctx = a.ctx return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) @@ -3113,7 +3115,7 @@ def ToInt(a): >>> n.sort() Int """ - if __debug__: + if Z3_DEBUG: _z3_assert(a.is_real(), "Z3 real expression expected.") ctx = a.ctx return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) @@ -3129,7 +3131,7 @@ def IsInt(a): >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") no solution """ - if __debug__: + if Z3_DEBUG: _z3_assert(a.is_real(), "Z3 real expression expected.") ctx = a.ctx return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) @@ -3189,7 +3191,7 @@ class BitVecSortRef(SortRef): '#x0000000a' """ if is_expr(val): - if __debug__: + if Z3_DEBUG: _z3_assert(self.ctx == val.ctx, "Context mismatch") # Idea: use sign_extend if sort of val is a bitvector of smaller size return val @@ -3700,7 +3702,7 @@ def BV2Int(a, is_signed=False): >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2] """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_bv(a), "Z3 bit-vector expression expected") ctx = a.ctx ## investigate problem with bv2int @@ -3800,7 +3802,7 @@ def Concat(*args): """ args = _get_args(args) sz = len(args) - if __debug__: + if Z3_DEBUG: _z3_assert(sz >= 2, "At least two arguments expected.") ctx = None @@ -3810,7 +3812,7 @@ def Concat(*args): break if is_seq(args[0]) or isinstance(args[0], str): args = [_coerce_seq(s, ctx) for s in args] - if __debug__: + if Z3_DEBUG: _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") v = (Ast * sz)() for i in range(sz): @@ -3818,14 +3820,14 @@ def Concat(*args): return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) if is_re(args[0]): - if __debug__: + if Z3_DEBUG: _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") v = (Ast * sz)() for i in range(sz): v[i] = args[i].as_ast() return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") r = args[0] for i in range(sz - 1): @@ -3849,14 +3851,14 @@ def Extract(high, low, a): s = high offset, length = _coerce_exprs(low, a, s.ctx) return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(low <= high, "First argument must be greater than or equal to second argument") _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) def _check_bv_args(a, b): - if __debug__: + if Z3_DEBUG: _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") def ULE(a, b): @@ -4072,7 +4074,7 @@ def SignExt(n, a): >>> print("%.x" % v.as_long()) fe """ - if __debug__: + if Z3_DEBUG: _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) @@ -4099,7 +4101,7 @@ def ZeroExt(n, a): >>> v.size() 8 """ - if __debug__: + if Z3_DEBUG: _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) @@ -4122,20 +4124,20 @@ def RepeatBitVec(n, a): >>> print("%.x" % v.as_long()) aaaa """ - if __debug__: + if Z3_DEBUG: _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) def BVRedAnd(a): """Return the reduction-and expression of `a`.""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) def BVRedOr(a): """Return the reduction-or expression of `a`.""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) @@ -4172,7 +4174,7 @@ def BVSDivNoOverflow(a, b): def BVSNegNoOverflow(a): """A predicate the determines that bit-vector unary negation does not overflow""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_bv(a), "Argument should be a bit-vector") return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) @@ -4338,7 +4340,7 @@ def get_map_func(a): >>> get_map_func(a)(0) f(0) """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_map(a), "Z3 array map expression expected.") return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) @@ -4357,12 +4359,12 @@ def ArraySort(*sig): Array(Int, Array(Int, Bool)) """ sig = _get_args(sig) - if __debug__: + if Z3_DEBUG: _z3_assert(len(sig) > 1, "At least two arguments expected") arity = len(sig) - 1 r = sig[arity] d = sig[0] - if __debug__: + if Z3_DEBUG: for s in sig: _z3_assert(is_sort(s), "Z3 sort expected") _z3_assert(s.ctx == r.ctx, "Context mismatch") @@ -4401,7 +4403,7 @@ def Update(a, i, v): >>> prove(Implies(i != j, s[j] == a[j])) proved """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_array(a), "First argument must be a Z3 array expression") i = a.domain().cast(i) v = a.range().cast(v) @@ -4414,7 +4416,7 @@ def Default(a): >>> prove(Default(b) == 1) proved """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_array(a), "First argument must be a Z3 array expression") return a.default() @@ -4445,7 +4447,7 @@ def Select(a, i): >>> eq(Select(a, i), a[i]) True """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_array(a), "First argument must be a Z3 array expression") return a[i] @@ -4463,7 +4465,7 @@ def Map(f, *args): proved """ args = _get_args(args) - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 0, "At least one Z3 array expression expected") _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") @@ -4486,7 +4488,7 @@ def K(dom, v): >>> simplify(a[i]) 10 """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(dom), "Z3 sort expected") ctx = dom.ctx if not is_expr(v): @@ -4500,7 +4502,7 @@ def Ext(a, b): Ext(a, b) """ ctx = a.ctx - if __debug__: + if Z3_DEBUG: _z3_assert(is_array(a) and is_array(b), "arguments must be arrays") return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) @@ -4690,7 +4692,7 @@ class Datatype: return r def declare_core(self, name, rec_name, *args): - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(name, str), "String expected") _z3_assert(isinstance(rec_name, str), "String expected") _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") @@ -4711,7 +4713,7 @@ class Datatype: >>> List.declare('nil') >>> List = List.create() """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(name, str), "String expected") _z3_assert(name != "", "Constructor name cannot be empty") return self.declare_core(name, "is-" + name, *args) @@ -4781,7 +4783,7 @@ def CreateDatatypes(*ds): True """ ds = _get_args(ds) - if __debug__: + if Z3_DEBUG: _z3_assert(len(ds) > 0, "At least one Datatype must be specified") _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") @@ -4811,12 +4813,12 @@ def CreateDatatypes(*ds): ftype = fs[k][1] fnames[k] = to_symbol(fname, ctx) if isinstance(ftype, Datatype): - if __debug__: + if Z3_DEBUG: _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") sorts[k] = None refs[k] = ds.index(ftype) else: - if __debug__: + if Z3_DEBUG: _z3_assert(is_sort(ftype), "Z3 sort expected") sorts[k] = ftype.ast refs[k] = 0 @@ -4875,7 +4877,7 @@ class DatatypeSortRef(SortRef): >>> List.constructor(1) nil """ - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_constructors(), "Invalid constructor index") return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) @@ -4903,7 +4905,7 @@ class DatatypeSortRef(SortRef): >>> simplify(List.is_cons(l)) is(cons, l) """ - if __debug__: + if Z3_DEBUG: _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) @@ -4931,7 +4933,7 @@ class DatatypeSortRef(SortRef): >>> num_accs 0 """ - if __debug__: + if Z3_DEBUG: _z3_assert(i < self.num_constructors(), "Invalid constructor index") _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) @@ -4972,7 +4974,7 @@ def EnumSort(name, values, ctx=None): Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(name, str), "Name must be a string") _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") _z3_assert(len(values) > 0, "At least one value expected") @@ -5019,7 +5021,7 @@ class ParamsRef: def set(self, name, val): """Set parameter name with value val.""" - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(name, str), "parameter name must be a string") name_sym = to_symbol(name, self.ctx) if isinstance(val, bool): @@ -5031,7 +5033,7 @@ class ParamsRef: elif isinstance(val, str): Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) else: - if __debug__: + if Z3_DEBUG: _z3_assert(False, "invalid parameter value") def __repr__(self): @@ -5048,7 +5050,7 @@ def args2params(arguments, keywords, ctx=None): >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true) """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") prev = None r = ParamsRef(ctx) @@ -5128,7 +5130,7 @@ class Goal(Z3PPObject): """ def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): - if __debug__: + if Z3_DEBUG: _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") self.ctx = _get_ctx(ctx) self.goal = goal @@ -5335,7 +5337,7 @@ class Goal(Z3PPObject): >>> r[1].convert_model(s.model()) [b = 0, a = 1] """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) @@ -5369,7 +5371,7 @@ class Goal(Z3PPObject): >>> g2.ctx == main_ctx() False """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(target, Context), "target must be a context") return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) @@ -6036,7 +6038,7 @@ class ModelRef(Z3PPObject): >>> m[f] [else -> 0] """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") if is_const(decl): decl = decl.decl() @@ -6123,7 +6125,7 @@ class ModelRef(Z3PPObject): >>> m.get_universe(A) [A!val!0, A!val!1] """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(s, SortRef), "Z3 sort expected") try: return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) @@ -6170,7 +6172,7 @@ class ModelRef(Z3PPObject): return self.get_interp(idx.decl()) if isinstance(idx, SortRef): return self.get_universe(idx) - if __debug__: + if Z3_DEBUG: _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") return None @@ -6196,7 +6198,7 @@ class ModelRef(Z3PPObject): def translate(self, target): """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(target, Context), "argument must be a Z3 context") model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) return Model(model, target) @@ -6217,7 +6219,7 @@ def is_as_array(n): def get_as_array_func(n): """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_as_array(n), "as-array Z3 expression expected.") return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) @@ -6833,7 +6835,7 @@ class Solver(Z3PPObject): >>> s1 = Solver(ctx=c1) >>> s2 = s1.translate(c2) """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(target, Context), "argument must be a Z3 context") solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) return Solver(solver, target) @@ -7262,7 +7264,7 @@ def FiniteDomainVal(val, sort, ctx=None): >>> FiniteDomainVal('100', s) 100 """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" ) ctx = sort.ctx return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx) @@ -7616,7 +7618,7 @@ class Tactic: if isinstance(tactic, TacticObj): self.tactic = tactic else: - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(tactic, str), "tactic name expected") try: self.tactic = Z3_mk_tactic(self.ctx.ref(), str(tactic)) @@ -7656,7 +7658,7 @@ class Tactic: >>> t.apply(And(x == 0, y >= x + 1)) [[y >= 1]] """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected") goal = _to_goal(goal) if len(arguments) > 0 or len(keywords) > 0: @@ -7700,14 +7702,14 @@ def _to_tactic(t, ctx=None): def _and_then(t1, t2, ctx=None): t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) def _or_else(t1, t2, ctx=None): t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) @@ -7721,7 +7723,7 @@ def AndThen(*ts, **ks): >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1) """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = ks.get('ctx', None) num = len(ts) @@ -7753,7 +7755,7 @@ def OrElse(*ts, **ks): >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]] """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = ks.get('ctx', None) num = len(ts) @@ -7770,7 +7772,7 @@ def ParOr(*ts, **ks): >>> t(x + 1 == 2) [[x == 1]] """ - if __debug__: + if Z3_DEBUG: _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = _get_ctx(ks.get('ctx', None)) ts = [ _to_tactic(t, ctx) for t in ts ] @@ -7790,7 +7792,7 @@ def ParThen(t1, t2, ctx=None): """ t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) @@ -7904,7 +7906,7 @@ class Probe: else: self.probe = Z3_probe_const(self.ctx.ref(), 0.0) else: - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(probe, str), "probe name expected") try: self.probe = Z3_mk_probe(self.ctx.ref(), probe) @@ -8021,7 +8023,7 @@ class Probe: >>> p(g) 1.0 """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected") goal = _to_goal(goal) return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal) @@ -8079,7 +8081,7 @@ def describe_probes(): print('%s : %s' % (p, probe_description(p))) def _probe_nary(f, args, ctx): - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 0, "At least one argument expected") num = len(args) r = _to_probe(args[0], ctx) @@ -8162,7 +8164,7 @@ def simplify(a, *arguments, **keywords): >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1))) """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_expr(a), "Z3 expression expected") if len(arguments) > 0 or len(keywords) > 0: p = args2params(arguments, keywords, a.ctx) @@ -8193,7 +8195,7 @@ def substitute(t, *m): m1 = _get_args(m) if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1): m = m1 - if __debug__: + if Z3_DEBUG: _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") num = len(m) @@ -8215,7 +8217,7 @@ def substitute_vars(t, *m): >>> substitute_vars(f(v0, v1), x + 1, x) f(x + 1, x) """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.") num = len(m) @@ -8282,10 +8284,10 @@ def AtMost(*args): >>> f = AtMost(a, b, c, 2) """ args = _get_args(args) - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 1, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args1 = _coerce_expr_list(args[:-1], ctx) k = args[-1] @@ -8299,10 +8301,10 @@ def AtLeast(*args): >>> f = AtLeast(a, b, c, 2) """ args = _get_args(args) - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 1, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args1 = _coerce_expr_list(args[:-1], ctx) k = args[-1] @@ -8315,10 +8317,10 @@ def _pb_args_coeffs(args, default_ctx = None): if len(args) == 0: return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)() args, coeffs = zip(*args) - if __debug__: + if Z3_DEBUG: _z3_assert(len(args) > 0, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if __debug__: + if Z3_DEBUG: _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) _args, sz = _to_ast_array(args) @@ -8395,7 +8397,7 @@ def solve_using(s, *args, **keywords): It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check. """ - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) s.add(*args) @@ -8426,7 +8428,7 @@ def prove(claim, **keywords): >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) proved """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver() s.set(**keywords) @@ -8467,7 +8469,7 @@ def _solve_html(*args, **keywords): def _solve_using_html(s, *args, **keywords): """Version of function `solve_using` used in RiSE4Fun.""" - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) s.add(*args) @@ -8490,7 +8492,7 @@ def _solve_using_html(s, *args, **keywords): def _prove_html(claim, **keywords): """Version of function `prove` used in RiSE4Fun.""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver() s.set(**keywords) @@ -8514,7 +8516,7 @@ def _dict2sarray(sorts, ctx): i = 0 for k in sorts: v = sorts[k] - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_sort(v), "Z3 sort expected") _names[i] = to_symbol(k, ctx) @@ -8529,7 +8531,7 @@ def _dict2darray(decls, ctx): i = 0 for k in decls: v = decls[k] - if __debug__: + if Z3_DEBUG: _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected") _names[i] = to_symbol(k, ctx) @@ -8680,7 +8682,7 @@ class FPSortRef(SortRef): '(fp #b0 #x7f #b00000000000000000000000)' """ if is_expr(val): - if __debug__: + if Z3_DEBUG: _z3_assert(self.ctx == val.ctx, "Context mismatch") return val else: @@ -9192,7 +9194,7 @@ def _to_float_str(val, exp=0): exp = str(int(val[inx+5:-1]) + int(exp)) else: _z3_assert(False, "String does not have floating-point numeral form.") - elif __debug__: + elif Z3_DEBUG: _z3_assert(False, "Python value cannot be used to create floating-point numerals.") if exp == 0: return res @@ -9384,7 +9386,7 @@ def fpNeg(a, ctx=None): def _mk_fp_unary(f, rm, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) @@ -9392,21 +9394,21 @@ def _mk_fp_unary(f, rm, a, ctx): def _mk_fp_unary_norm(f, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_unary_pred(f, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return BoolRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_bin(f, rm, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) @@ -9414,21 +9416,21 @@ def _mk_fp_bin(f, rm, a, b, ctx): def _mk_fp_bin_norm(f, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) def _mk_fp_bin_pred(f, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) def _mk_fp_tern(f, rm, a, b, c, ctx): ctx = _get_ctx(ctx) [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "At least one of the arguments must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) @@ -9595,7 +9597,7 @@ def fpIsPositive(a, ctx=None): return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) def _check_fp_args(a, b): - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") def fpLT(a, b, ctx=None): @@ -9818,7 +9820,7 @@ def fpUnsignedToFP(rm, v, sort, ctx=None): def fpToFPUnsigned(rm, x, s, ctx=None): """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") @@ -9839,7 +9841,7 @@ def fpToSBV(rm, x, s, ctx=None): >>> print(is_bv(x)) False """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") @@ -9860,7 +9862,7 @@ def fpToUBV(rm, x, s, ctx=None): >>> print(is_bv(x)) False """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") @@ -9881,7 +9883,7 @@ def fpToReal(x, ctx=None): >>> print(is_real(x)) False """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") ctx = _get_ctx(ctx) return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) @@ -9906,7 +9908,7 @@ def fpToIEEEBV(x, ctx=None): >>> print(is_bv(x)) False """ - if __debug__: + if Z3_DEBUG: _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") ctx = _get_ctx(ctx) return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) @@ -10282,7 +10284,7 @@ def Union(*args): """ args = _get_args(args) sz = len(args) - if __debug__: + if Z3_DEBUG: _z3_assert(sz > 0, "At least one argument expected.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") if sz == 1: @@ -10299,7 +10301,7 @@ def Intersect(*args): """ args = _get_args(args) sz = len(args) - if __debug__: + if Z3_DEBUG: _z3_assert(sz > 0, "At least one argument expected.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") if sz == 1: diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py index 6e5165c9a..ba9926076 100644 --- a/src/api/python/z3/z3util.py +++ b/src/api/python/z3/z3util.py @@ -75,7 +75,7 @@ def ehash(v): x_783810685_1 x_783810685_1 x_783810685_2 """ - if __debug__: + if Z3_DEBUG: assert is_expr(v) return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind()) @@ -148,7 +148,7 @@ def get_vars(f,rs=[]): [x, y, a, b] """ - if __debug__: + if Z3_DEBUG: assert is_expr(f) if is_const(f): @@ -228,13 +228,13 @@ def prove(claim,assume=None,verbose=0): """ - if __debug__: + if Z3_DEBUG: assert not assume or is_expr(assume) to_prove = claim if assume: - if __debug__: + if Z3_DEBUG: is_proved,_ = prove(Not(assume)) def _f(): @@ -266,7 +266,7 @@ def prove(claim,assume=None,verbose=0): elif models == False: #unsat return True,None else: #sat - if __debug__: + if Z3_DEBUG: assert isinstance(models,list) if models: @@ -312,7 +312,7 @@ def get_models(f,k): """ - if __debug__: + if Z3_DEBUG: assert is_expr(f) assert k>=1 @@ -448,13 +448,13 @@ def myBinOp(op,*L): AssertionError """ - if __debug__: + if Z3_DEBUG: assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)): L = L[0] - if __debug__: + if Z3_DEBUG: assert all(not isinstance(l,bool) for l in L) L = [l for l in L if is_expr(l)] @@ -493,7 +493,7 @@ def model_str(m,as_str=True): see doctest exampels from function prove() """ - if __debug__: + if Z3_DEBUG: assert m is None or m == [] or isinstance(m,ModelRef) if m : diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6ea764a0a..cd7111d05 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1347,6 +1347,7 @@ namespace nlsat { restore_order(); CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); CTRACE("nlsat", r == l_false, display(tout);); + VERIFY(r != l_true || check_satisfied(m_clauses)); return r; } @@ -1867,11 +1868,17 @@ namespace nlsat { if (m_bk != null_bool_var) num = m_bk; for (bool_var b = 0; b < num; b++) { - SASSERT(check_satisfied(m_bwatches[b])); + if (!check_satisfied(m_bwatches[b])) { + UNREACHABLE(); + return false; + } } if (m_xk != null_var) { for (var x = 0; x < m_xk; x++) { - SASSERT(check_satisfied(m_watches[x])); + if (!check_satisfied(m_watches[x])) { + UNREACHABLE(); + return false; + } } } return true; diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 5e536bbe6..f3f984e28 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -85,6 +85,9 @@ class nlsat_tactic : public tactic { for (unsigned i = 0; i < sz; i++) { if (!model.is_true(g.form(i))) { TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";); + IF_VERBOSE(0, verbose_stream() << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";); + IF_VERBOSE(1, verbose_stream() << model << "\n"); + IF_VERBOSE(1, m_solver.display(verbose_stream())); return false; } } @@ -123,6 +126,7 @@ class nlsat_tactic : public tactic { md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false()); } DEBUG_CODE(eval_model(*md.get(), g);); + // VERIFY(eval_model(*md.get(), g)); mc = model2model_converter(md.get()); return ok; } @@ -149,6 +153,9 @@ class nlsat_tactic : public tactic { t2x.mk_inv(m_display_var.m_var2expr); m_solver.set_display_var(m_display_var); + IF_VERBOSE(10000, m_solver.display(verbose_stream())); + IF_VERBOSE(10000, g->display(verbose_stream())); + lbool st = m_solver.check(); if (st == l_undef) { From 28773c8d5cb3b09b5988cb76322129fa2a781c53 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 13:49:44 -0700 Subject: [PATCH 07/13] na Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index cd7111d05..523e5a929 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1347,7 +1347,7 @@ namespace nlsat { restore_order(); CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); CTRACE("nlsat", r == l_false, display(tout);); - VERIFY(r != l_true || check_satisfied(m_clauses)); + SASSERT(r != l_true || check_satisfied(m_clauses)); return r; } From 92613f26b389febe3bc6d568d3fd00156bc47615 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 13:56:16 -0700 Subject: [PATCH 08/13] remove additional push/pop on fixedpoint Signed-off-by: Nikolaj Bjorner --- src/muz/fp/dl_cmds.cpp | 40 ---------------------------------------- 1 file changed, 40 deletions(-) diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 8bea46bea..811511050 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -479,44 +479,6 @@ public: } }; -/** - \brief fixedpoint-push command. -*/ -class dl_push_cmd : public cmd { - ref m_dl_ctx; -public: - dl_push_cmd(dl_context * dl_ctx): - cmd("fixedpoint-push"), - m_dl_ctx(dl_ctx) - {} - - char const * get_usage() const override { return ""; } - char const * get_descr(cmd_context & ctx) const override { return "push the fixedpoint context"; } - unsigned get_arity() const override { return 0; } - void execute(cmd_context & ctx) override { - m_dl_ctx->push(); - } -}; - -/** - \brief fixedpoint-pop command. -*/ -class dl_pop_cmd : public cmd { - ref m_dl_ctx; -public: - dl_pop_cmd(dl_context * dl_ctx): - cmd("fixedpoint-pop"), - m_dl_ctx(dl_ctx) - {} - - char const * get_usage() const override { return ""; } - char const * get_descr(cmd_context & ctx) const override { return "pop the fixedpoint context"; } - unsigned get_arity() const override { return 0; } - void execute(cmd_context & ctx) override { - m_dl_ctx->pop(); - } -}; - static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) { dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds); @@ -524,8 +486,6 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c ctx.insert(alloc(dl_query_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_var_cmd, dl_ctx)); - ctx.insert(alloc(dl_push_cmd, dl_ctx)); - ctx.insert(alloc(dl_pop_cmd, dl_ctx)); } void install_dl_cmds(cmd_context & ctx) { From c9b906a5181d2769270b23fa37a20f3f3254162c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 14:03:26 -0700 Subject: [PATCH 09/13] deal with python globals Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 276 ++++++++++++++++++------------------ src/api/python/z3/z3util.py | 18 +-- 2 files changed, 149 insertions(+), 145 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5475af254..1bd495a87 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -53,7 +53,11 @@ import io import math import copy -Z3_DEUBG = __debug__ +Z3_DEBUG = __debug__ + +def z3_debug(): + global Z3_DEBUG + return Z3_DEBUG if sys.version < '3': def _is_int(v): @@ -168,7 +172,7 @@ class Context: The initialization method receives global configuration options for the new context. """ def __init__(self, *args, **kws): - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") conf = Z3_mk_config() for key in kws: @@ -237,7 +241,7 @@ def set_param(*args, **kws): >>> set_param(precision=10) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") new_kws = {} for k in kws: @@ -362,7 +366,7 @@ class AstRef(Z3PPObject): >>> n1.eq(n2) True """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_ast(other), "Z3 AST expected") return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast()) @@ -378,7 +382,7 @@ class AstRef(Z3PPObject): >>> x.translate(c2) + y x + y """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(target, Context), "argument must be a Z3 context") return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target) @@ -429,7 +433,7 @@ def eq(a, b): >>> eq(simplify(x + 1), simplify(1 + x)) True """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected") return a.eq(b) @@ -445,7 +449,7 @@ def _ctx_from_ast_arg_list(args, default_ctx=None): if ctx is None: ctx = a.ctx else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx == a.ctx, "Context mismatch") if ctx is None: ctx = default_ctx @@ -536,7 +540,7 @@ class SortRef(AstRef): >>> RealSort().cast(x) ToReal(x) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_expr(val), "Z3 expression expected") _z3_assert(self.eq(val.sort()), "Sort mismatch") return val @@ -592,7 +596,7 @@ def is_sort(s): return isinstance(s, SortRef) def _to_sort_ref(s, ctx): - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(s, Sort), "Z3 Sort expected") k = _sort_kind(ctx, s) if k == Z3_BOOL_SORT: @@ -689,7 +693,7 @@ class FuncDeclRef(AstRef): >>> f.domain(1) Real """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(i < self.arity(), "Index out of bounds") return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx) @@ -758,7 +762,7 @@ class FuncDeclRef(AstRef): """ args = _get_args(args) num = len(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self) _args = (Ast * num)() saved = [] @@ -790,15 +794,15 @@ def Function(name, *sig): f(f(0)) """ sig = _get_args(sig) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(sig) > 0, "At least two arguments expected") arity = len(sig) - 1 rng = sig[arity] - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(rng), "Z3 sort expected") dom = (Sort * arity)() for i in range(arity): - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(sig[i]), "Z3 sort expected") dom[i] = sig[i].ast ctx = rng.ctx @@ -810,15 +814,15 @@ def _to_func_decl_ref(a, ctx): def RecFunction(name, *sig): """Create a new Z3 recursive with the given sorts.""" sig = _get_args(sig) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(sig) > 0, "At least two arguments expected") arity = len(sig) - 1 rng = sig[arity] - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(rng), "Z3 sort expected") dom = (Sort * arity)() for i in range(arity): - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(sig[i]), "Z3 sort expected") dom[i] = sig[i].ast ctx = rng.ctx @@ -948,7 +952,7 @@ class ExprRef(AstRef): >>> (a + 1).decl() + """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) @@ -964,7 +968,7 @@ class ExprRef(AstRef): >>> t.num_args() 3 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_app(self), "Z3 application expected") return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast())) @@ -984,7 +988,7 @@ class ExprRef(AstRef): >>> t.arg(2) 0 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_app(self), "Z3 application expected") _z3_assert(idx < self.num_args(), "Invalid argument index") return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx) @@ -1063,7 +1067,7 @@ def _coerce_expr_merge(s, a): elif s1.subsort(s): return s else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") else: @@ -1215,7 +1219,7 @@ def get_var_index(a): >>> get_var_index(v2) 0 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_var(a), "Z3 bound variable expected") return int(Z3_get_index_value(a.ctx.ref(), a.as_ast())) @@ -1249,7 +1253,7 @@ def If(a, b, c, ctx=None): s = BoolSort(ctx) a = s.cast(a) b, c = _coerce_exprs(b, c, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.ctx == b.ctx, "Context mismatch") return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) @@ -1270,7 +1274,7 @@ def Distinct(*args): """ args = _get_args(args) ctx = _ctx_from_ast_arg_list(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) _args, sz = _to_ast_array(args) @@ -1278,7 +1282,7 @@ def Distinct(*args): def _mk_bin(f, a, b): args = (Ast * 2)() - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.ctx == b.ctx, "Context mismatch") args[0] = a.as_ast() args[1] = b.as_ast() @@ -1290,7 +1294,7 @@ def Const(name, sort): >>> Const('x', IntSort()) x """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(sort, SortRef), "Z3 sort expected") ctx = sort.ctx return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx) @@ -1322,7 +1326,7 @@ def Var(idx, s): >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(s), "Z3 sort expected") return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx) @@ -1370,7 +1374,7 @@ class BoolSortRef(SortRef): """ if isinstance(val, bool): return BoolVal(val, self.ctx) - if Z3_DEBUG: + if z3_debug(): if not is_expr(val): _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) if not self.eq(val.sort()): @@ -1688,7 +1692,7 @@ def And(*args): ctx = main_ctx() args = _get_args(args) ctx_args = _ctx_from_ast_arg_list(args, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): @@ -1718,7 +1722,7 @@ def Or(*args): ctx = main_ctx() args = _get_args(args) ctx_args = _ctx_from_ast_arg_list(args, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): @@ -1777,7 +1781,7 @@ def MultiPattern(*args): >>> q.pattern(0) MultiPattern(f(Var(0)), g(Var(0))) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 0, "At least one argument expected") _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") ctx = args[0].ctx @@ -1893,7 +1897,7 @@ class QuantifierRef(BoolRef): >>> q.pattern(1) g(Var(0)) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1903,7 +1907,7 @@ class QuantifierRef(BoolRef): def no_pattern(self, idx): """Return a no-pattern.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1942,7 +1946,7 @@ class QuantifierRef(BoolRef): >>> q.var_name(1) 'y' """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_vars(), "Invalid variable idx") return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) @@ -1958,7 +1962,7 @@ class QuantifierRef(BoolRef): >>> q.var_sort(1) Real """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_vars(), "Invalid variable idx") return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) @@ -1987,7 +1991,7 @@ def is_quantifier(a): return isinstance(a, QuantifierRef) def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") @@ -2133,7 +2137,7 @@ class ArithSortRef(SortRef): True """ if is_expr(val): - if Z3_DEBUG: + if z3_debug(): _z3_assert(self.ctx == val.ctx, "Context mismatch") val_s = val.sort() if self.eq(val_s): @@ -2144,14 +2148,14 @@ class ArithSortRef(SortRef): return If(val, 1, 0) if val_s.is_bool() and self.is_real(): return ToReal(If(val, 1, 0)) - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "Z3 Integer/Real expression expected" ) else: if self.is_int(): return IntVal(val, self.ctx) if self.is_real(): return RealVal(val, self.ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) def is_arith_sort(s): @@ -2365,7 +2369,7 @@ class ArithRef(ExprRef): 1 """ a, b = _coerce_exprs(self, other) - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.is_int(), "Z3 integer expression expected") return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) @@ -2377,7 +2381,7 @@ class ArithRef(ExprRef): 10%x """ a, b = _coerce_exprs(self, other) - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.is_int(), "Z3 integer expression expected") return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) @@ -2738,7 +2742,7 @@ class IntNumRef(ArithRef): >>> v.as_long() + 1 2 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(self.is_int(), "Integer value expected") return int(self.as_string()) @@ -2880,7 +2884,7 @@ def _py2expr(a, ctx=None): return RealVal(a, ctx) if is_expr(a): return a - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "Python bool, int, long or float expected") def IntSort(ctx=None): @@ -2927,7 +2931,7 @@ def _to_int_str(val): return str(val) elif isinstance(val, str): return val - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "Python value cannot be used as a Z3 integer") def IntVal(val, ctx=None): @@ -2969,7 +2973,7 @@ def RatVal(a, b, ctx=None): >>> RatVal(3,5).sort() Real """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") return simplify(RealVal(a, ctx)/RealVal(b, ctx)) @@ -3098,7 +3102,7 @@ def ToReal(a): >>> n.sort() Real """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.is_int(), "Z3 integer expression expected.") ctx = a.ctx return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) @@ -3115,7 +3119,7 @@ def ToInt(a): >>> n.sort() Int """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.is_real(), "Z3 real expression expected.") ctx = a.ctx return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) @@ -3131,7 +3135,7 @@ def IsInt(a): >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") no solution """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(a.is_real(), "Z3 real expression expected.") ctx = a.ctx return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) @@ -3191,7 +3195,7 @@ class BitVecSortRef(SortRef): '#x0000000a' """ if is_expr(val): - if Z3_DEBUG: + if z3_debug(): _z3_assert(self.ctx == val.ctx, "Context mismatch") # Idea: use sign_extend if sort of val is a bitvector of smaller size return val @@ -3702,7 +3706,7 @@ def BV2Int(a, is_signed=False): >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bv(a), "Z3 bit-vector expression expected") ctx = a.ctx ## investigate problem with bv2int @@ -3802,7 +3806,7 @@ def Concat(*args): """ args = _get_args(args) sz = len(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(sz >= 2, "At least two arguments expected.") ctx = None @@ -3812,7 +3816,7 @@ def Concat(*args): break if is_seq(args[0]) or isinstance(args[0], str): args = [_coerce_seq(s, ctx) for s in args] - if Z3_DEBUG: + if z3_debug(): _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") v = (Ast * sz)() for i in range(sz): @@ -3820,14 +3824,14 @@ def Concat(*args): return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) if is_re(args[0]): - if Z3_DEBUG: + if z3_debug(): _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") v = (Ast * sz)() for i in range(sz): v[i] = args[i].as_ast() return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") r = args[0] for i in range(sz - 1): @@ -3851,14 +3855,14 @@ def Extract(high, low, a): s = high offset, length = _coerce_exprs(low, a, s.ctx) return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(low <= high, "First argument must be greater than or equal to second argument") _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) def _check_bv_args(a, b): - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") def ULE(a, b): @@ -4074,7 +4078,7 @@ def SignExt(n, a): >>> print("%.x" % v.as_long()) fe """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) @@ -4101,7 +4105,7 @@ def ZeroExt(n, a): >>> v.size() 8 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) @@ -4124,20 +4128,20 @@ def RepeatBitVec(n, a): >>> print("%.x" % v.as_long()) aaaa """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(_is_int(n), "First argument must be an integer") _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) def BVRedAnd(a): """Return the reduction-and expression of `a`.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) def BVRedOr(a): """Return the reduction-or expression of `a`.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) @@ -4174,7 +4178,7 @@ def BVSDivNoOverflow(a, b): def BVSNegNoOverflow(a): """A predicate the determines that bit-vector unary negation does not overflow""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bv(a), "Argument should be a bit-vector") return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) @@ -4340,7 +4344,7 @@ def get_map_func(a): >>> get_map_func(a)(0) f(0) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_map(a), "Z3 array map expression expected.") return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) @@ -4359,12 +4363,12 @@ def ArraySort(*sig): Array(Int, Array(Int, Bool)) """ sig = _get_args(sig) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(sig) > 1, "At least two arguments expected") arity = len(sig) - 1 r = sig[arity] d = sig[0] - if Z3_DEBUG: + if z3_debug(): for s in sig: _z3_assert(is_sort(s), "Z3 sort expected") _z3_assert(s.ctx == r.ctx, "Context mismatch") @@ -4403,7 +4407,7 @@ def Update(a, i, v): >>> prove(Implies(i != j, s[j] == a[j])) proved """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_array(a), "First argument must be a Z3 array expression") i = a.domain().cast(i) v = a.range().cast(v) @@ -4416,7 +4420,7 @@ def Default(a): >>> prove(Default(b) == 1) proved """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_array(a), "First argument must be a Z3 array expression") return a.default() @@ -4447,7 +4451,7 @@ def Select(a, i): >>> eq(Select(a, i), a[i]) True """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_array(a), "First argument must be a Z3 array expression") return a[i] @@ -4465,7 +4469,7 @@ def Map(f, *args): proved """ args = _get_args(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 0, "At least one Z3 array expression expected") _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") @@ -4488,7 +4492,7 @@ def K(dom, v): >>> simplify(a[i]) 10 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(dom), "Z3 sort expected") ctx = dom.ctx if not is_expr(v): @@ -4502,7 +4506,7 @@ def Ext(a, b): Ext(a, b) """ ctx = a.ctx - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_array(a) and is_array(b), "arguments must be arrays") return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) @@ -4692,7 +4696,7 @@ class Datatype: return r def declare_core(self, name, rec_name, *args): - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(name, str), "String expected") _z3_assert(isinstance(rec_name, str), "String expected") _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") @@ -4713,7 +4717,7 @@ class Datatype: >>> List.declare('nil') >>> List = List.create() """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(name, str), "String expected") _z3_assert(name != "", "Constructor name cannot be empty") return self.declare_core(name, "is-" + name, *args) @@ -4783,7 +4787,7 @@ def CreateDatatypes(*ds): True """ ds = _get_args(ds) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(ds) > 0, "At least one Datatype must be specified") _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") @@ -4813,12 +4817,12 @@ def CreateDatatypes(*ds): ftype = fs[k][1] fnames[k] = to_symbol(fname, ctx) if isinstance(ftype, Datatype): - if Z3_DEBUG: + if z3_debug(): _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") sorts[k] = None refs[k] = ds.index(ftype) else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_sort(ftype), "Z3 sort expected") sorts[k] = ftype.ast refs[k] = 0 @@ -4877,7 +4881,7 @@ class DatatypeSortRef(SortRef): >>> List.constructor(1) nil """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_constructors(), "Invalid constructor index") return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) @@ -4905,7 +4909,7 @@ class DatatypeSortRef(SortRef): >>> simplify(List.is_cons(l)) is(cons, l) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) @@ -4933,7 +4937,7 @@ class DatatypeSortRef(SortRef): >>> num_accs 0 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(i < self.num_constructors(), "Invalid constructor index") _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) @@ -4974,7 +4978,7 @@ def EnumSort(name, values, ctx=None): Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(name, str), "Name must be a string") _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") _z3_assert(len(values) > 0, "At least one value expected") @@ -5021,7 +5025,7 @@ class ParamsRef: def set(self, name, val): """Set parameter name with value val.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(name, str), "parameter name must be a string") name_sym = to_symbol(name, self.ctx) if isinstance(val, bool): @@ -5033,7 +5037,7 @@ class ParamsRef: elif isinstance(val, str): Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "invalid parameter value") def __repr__(self): @@ -5050,7 +5054,7 @@ def args2params(arguments, keywords, ctx=None): >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") prev = None r = ParamsRef(ctx) @@ -5130,7 +5134,7 @@ class Goal(Z3PPObject): """ def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): - if Z3_DEBUG: + if z3_debug(): _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") self.ctx = _get_ctx(ctx) self.goal = goal @@ -5337,7 +5341,7 @@ class Goal(Z3PPObject): >>> r[1].convert_model(s.model()) [b = 0, a = 1] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) @@ -5371,7 +5375,7 @@ class Goal(Z3PPObject): >>> g2.ctx == main_ctx() False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(target, Context), "target must be a context") return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) @@ -6038,7 +6042,7 @@ class ModelRef(Z3PPObject): >>> m[f] [else -> 0] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") if is_const(decl): decl = decl.decl() @@ -6125,7 +6129,7 @@ class ModelRef(Z3PPObject): >>> m.get_universe(A) [A!val!0, A!val!1] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(s, SortRef), "Z3 sort expected") try: return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) @@ -6172,7 +6176,7 @@ class ModelRef(Z3PPObject): return self.get_interp(idx.decl()) if isinstance(idx, SortRef): return self.get_universe(idx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") return None @@ -6198,7 +6202,7 @@ class ModelRef(Z3PPObject): def translate(self, target): """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(target, Context), "argument must be a Z3 context") model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) return Model(model, target) @@ -6219,7 +6223,7 @@ def is_as_array(n): def get_as_array_func(n): """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_as_array(n), "as-array Z3 expression expected.") return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) @@ -6835,7 +6839,7 @@ class Solver(Z3PPObject): >>> s1 = Solver(ctx=c1) >>> s2 = s1.translate(c2) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(target, Context), "argument must be a Z3 context") solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) return Solver(solver, target) @@ -7264,7 +7268,7 @@ def FiniteDomainVal(val, sort, ctx=None): >>> FiniteDomainVal('100', s) 100 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" ) ctx = sort.ctx return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx) @@ -7618,7 +7622,7 @@ class Tactic: if isinstance(tactic, TacticObj): self.tactic = tactic else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(tactic, str), "tactic name expected") try: self.tactic = Z3_mk_tactic(self.ctx.ref(), str(tactic)) @@ -7658,7 +7662,7 @@ class Tactic: >>> t.apply(And(x == 0, y >= x + 1)) [[y >= 1]] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected") goal = _to_goal(goal) if len(arguments) > 0 or len(keywords) > 0: @@ -7702,14 +7706,14 @@ def _to_tactic(t, ctx=None): def _and_then(t1, t2, ctx=None): t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) def _or_else(t1, t2, ctx=None): t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) @@ -7723,7 +7727,7 @@ def AndThen(*ts, **ks): >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = ks.get('ctx', None) num = len(ts) @@ -7755,7 +7759,7 @@ def OrElse(*ts, **ks): >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = ks.get('ctx', None) num = len(ts) @@ -7772,7 +7776,7 @@ def ParOr(*ts, **ks): >>> t(x + 1 == 2) [[x == 1]] """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = _get_ctx(ks.get('ctx', None)) ts = [ _to_tactic(t, ctx) for t in ts ] @@ -7792,7 +7796,7 @@ def ParThen(t1, t2, ctx=None): """ t1 = _to_tactic(t1, ctx) t2 = _to_tactic(t2, ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(t1.ctx == t2.ctx, "Context mismatch") return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx) @@ -7906,7 +7910,7 @@ class Probe: else: self.probe = Z3_probe_const(self.ctx.ref(), 0.0) else: - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(probe, str), "probe name expected") try: self.probe = Z3_mk_probe(self.ctx.ref(), probe) @@ -8023,7 +8027,7 @@ class Probe: >>> p(g) 1.0 """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected") goal = _to_goal(goal) return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal) @@ -8081,7 +8085,7 @@ def describe_probes(): print('%s : %s' % (p, probe_description(p))) def _probe_nary(f, args, ctx): - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 0, "At least one argument expected") num = len(args) r = _to_probe(args[0], ctx) @@ -8164,7 +8168,7 @@ def simplify(a, *arguments, **keywords): >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1))) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_expr(a), "Z3 expression expected") if len(arguments) > 0 or len(keywords) > 0: p = args2params(arguments, keywords, a.ctx) @@ -8195,7 +8199,7 @@ def substitute(t, *m): m1 = _get_args(m) if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1): m = m1 - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") num = len(m) @@ -8217,7 +8221,7 @@ def substitute_vars(t, *m): >>> substitute_vars(f(v0, v1), x + 1, x) f(x + 1, x) """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.") num = len(m) @@ -8284,10 +8288,10 @@ def AtMost(*args): >>> f = AtMost(a, b, c, 2) """ args = _get_args(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 1, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args1 = _coerce_expr_list(args[:-1], ctx) k = args[-1] @@ -8301,10 +8305,10 @@ def AtLeast(*args): >>> f = AtLeast(a, b, c, 2) """ args = _get_args(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 1, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args1 = _coerce_expr_list(args[:-1], ctx) k = args[-1] @@ -8317,10 +8321,10 @@ def _pb_args_coeffs(args, default_ctx = None): if len(args) == 0: return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)() args, coeffs = zip(*args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(len(args) > 0, "Non empty list of arguments expected") ctx = _ctx_from_ast_arg_list(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) _args, sz = _to_ast_array(args) @@ -8397,7 +8401,7 @@ def solve_using(s, *args, **keywords): It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check. """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) s.add(*args) @@ -8428,7 +8432,7 @@ def prove(claim, **keywords): >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) proved """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver() s.set(**keywords) @@ -8469,7 +8473,7 @@ def _solve_html(*args, **keywords): def _solve_using_html(s, *args, **keywords): """Version of function `solve_using` used in RiSE4Fun.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) s.add(*args) @@ -8492,7 +8496,7 @@ def _solve_using_html(s, *args, **keywords): def _prove_html(claim, **keywords): """Version of function `prove` used in RiSE4Fun.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver() s.set(**keywords) @@ -8516,7 +8520,7 @@ def _dict2sarray(sorts, ctx): i = 0 for k in sorts: v = sorts[k] - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_sort(v), "Z3 sort expected") _names[i] = to_symbol(k, ctx) @@ -8531,7 +8535,7 @@ def _dict2darray(decls, ctx): i = 0 for k in decls: v = decls[k] - if Z3_DEBUG: + if z3_debug(): _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected") _names[i] = to_symbol(k, ctx) @@ -8682,7 +8686,7 @@ class FPSortRef(SortRef): '(fp #b0 #x7f #b00000000000000000000000)' """ if is_expr(val): - if Z3_DEBUG: + if z3_debug(): _z3_assert(self.ctx == val.ctx, "Context mismatch") return val else: @@ -9194,7 +9198,7 @@ def _to_float_str(val, exp=0): exp = str(int(val[inx+5:-1]) + int(exp)) else: _z3_assert(False, "String does not have floating-point numeral form.") - elif Z3_DEBUG: + elif z3_debug(): _z3_assert(False, "Python value cannot be used to create floating-point numerals.") if exp == 0: return res @@ -9386,7 +9390,7 @@ def fpNeg(a, ctx=None): def _mk_fp_unary(f, rm, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) @@ -9394,21 +9398,21 @@ def _mk_fp_unary(f, rm, a, ctx): def _mk_fp_unary_norm(f, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_unary_pred(f, a, ctx): ctx = _get_ctx(ctx) [a] = _coerce_fp_expr_list([a], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return BoolRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_bin(f, rm, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) @@ -9416,21 +9420,21 @@ def _mk_fp_bin(f, rm, a, b, ctx): def _mk_fp_bin_norm(f, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) def _mk_fp_bin_pred(f, a, b, ctx): ctx = _get_ctx(ctx) [a, b] = _coerce_fp_expr_list([a, b], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) def _mk_fp_tern(f, rm, a, b, c, ctx): ctx = _get_ctx(ctx) [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "At least one of the arguments must be a Z3 floating-point expression") return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) @@ -9597,7 +9601,7 @@ def fpIsPositive(a, ctx=None): return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) def _check_fp_args(a, b): - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") def fpLT(a, b, ctx=None): @@ -9820,7 +9824,7 @@ def fpUnsignedToFP(rm, v, sort, ctx=None): def fpToFPUnsigned(rm, x, s, ctx=None): """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") @@ -9841,7 +9845,7 @@ def fpToSBV(rm, x, s, ctx=None): >>> print(is_bv(x)) False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") @@ -9862,7 +9866,7 @@ def fpToUBV(rm, x, s, ctx=None): >>> print(is_bv(x)) False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") @@ -9883,7 +9887,7 @@ def fpToReal(x, ctx=None): >>> print(is_real(x)) False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") ctx = _get_ctx(ctx) return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) @@ -9908,7 +9912,7 @@ def fpToIEEEBV(x, ctx=None): >>> print(is_bv(x)) False """ - if Z3_DEBUG: + if z3_debug(): _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") ctx = _get_ctx(ctx) return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) @@ -10284,7 +10288,7 @@ def Union(*args): """ args = _get_args(args) sz = len(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(sz > 0, "At least one argument expected.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") if sz == 1: @@ -10301,7 +10305,7 @@ def Intersect(*args): """ args = _get_args(args) sz = len(args) - if Z3_DEBUG: + if z3_debug(): _z3_assert(sz > 0, "At least one argument expected.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") if sz == 1: diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py index ba9926076..5734d2804 100644 --- a/src/api/python/z3/z3util.py +++ b/src/api/python/z3/z3util.py @@ -75,7 +75,7 @@ def ehash(v): x_783810685_1 x_783810685_1 x_783810685_2 """ - if Z3_DEBUG: + if z3_debug(): assert is_expr(v) return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind()) @@ -148,7 +148,7 @@ def get_vars(f,rs=[]): [x, y, a, b] """ - if Z3_DEBUG: + if z3_debug(): assert is_expr(f) if is_const(f): @@ -228,13 +228,13 @@ def prove(claim,assume=None,verbose=0): """ - if Z3_DEBUG: + if z3_debug(): assert not assume or is_expr(assume) to_prove = claim if assume: - if Z3_DEBUG: + if z3_debug(): is_proved,_ = prove(Not(assume)) def _f(): @@ -266,7 +266,7 @@ def prove(claim,assume=None,verbose=0): elif models == False: #unsat return True,None else: #sat - if Z3_DEBUG: + if z3_debug(): assert isinstance(models,list) if models: @@ -312,7 +312,7 @@ def get_models(f,k): """ - if Z3_DEBUG: + if z3_debug(): assert is_expr(f) assert k>=1 @@ -448,13 +448,13 @@ def myBinOp(op,*L): AssertionError """ - if Z3_DEBUG: + if z3_debug(): assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)): L = L[0] - if Z3_DEBUG: + if z3_debug(): assert all(not isinstance(l,bool) for l in L) L = [l for l in L if is_expr(l)] @@ -493,7 +493,7 @@ def model_str(m,as_str=True): see doctest exampels from function prove() """ - if Z3_DEBUG: + if z3_debug(): assert m is None or m == [] or isinstance(m,ModelRef) if m : From 9f1b8db870b0f00762b9c2f0131cf7fde9fee55d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 14:13:23 -0700 Subject: [PATCH 10/13] adjust for SMTLIBification name change of set operations Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ++-- src/opt/opt_context.cpp | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1bd495a87..042cdde6f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4582,7 +4582,7 @@ def SetIntersect(*args): >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetIntersect(a, b) - intersect(a, b) + intersection(a, b) """ args = _get_args(args) ctx = _ctx_from_ast_arg_list(args) @@ -4623,7 +4623,7 @@ def SetDifference(a, b): >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetDifference(a, b) - difference(a, b) + setminus(a, b) """ ctx = _ctx_from_ast_arg_list([a, b]) return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b43147c33..7ca2c774b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1116,7 +1116,9 @@ namespace opt { val = (*mdl)(term); unsigned bvsz; if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) { - TRACE("opt", tout << "model does not evaluate objective to a value\n";); + TRACE("opt", tout << "model does not evaluate objective to a value but instead " << val << "\n"; + tout << *mdl << "\n"; + ); return false; } if (r != v) { From 9cb1a0f09483babff5bce783629104d3d82c8e33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 14:24:53 -0700 Subject: [PATCH 11/13] fix #2253 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 ++- src/tactic/arith/lia2card_tactic.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 7ca2c774b..25d3640ac 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -361,7 +361,8 @@ namespace opt { void context::fix_model(model_ref& mdl) { if (mdl && !m_model_fixed.contains(mdl.get())) { - TRACE("opt", tout << "fix-model\n";); + TRACE("opt", m_fm->display(tout << "fix-model\n"); + m_model_converter->display(tout);); (*m_fm)(mdl); apply(m_model_converter, mdl); m_model_fixed.push_back(mdl.get()); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 027b6d91c..c2c90284c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -143,7 +143,9 @@ public: expr_ref last_v(m); if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card"); if (hi == 0) { - return expr_ref(a.mk_int(0), m); + expr* r = a.mk_int(0); + m_mc->add(x->get_decl(), r); + return expr_ref(r, m); } if (lo > 0) { xs.push_back(a.mk_int(lo)); From bd46c52f959e01ac7c65bbf634994c6e9649f927 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 15:51:23 -0700 Subject: [PATCH 12/13] fix #2257, remove unsound length constraints for str.to.int because leading digits can be 0 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7a899d5ae..71f98b22b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3576,7 +3576,7 @@ expr_ref theory_seq::digit2int(expr* ch) { // n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1 // n >= 0 & len(e) = k => n = sum 10^i*digit(e_i) // n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1 -// 10^k <= n < 10^{k+1}-1 => len(e) = k +// 10^k <= n < 10^{k+1}-1 => len(e) => k void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { context& ctx = get_context(); @@ -3618,15 +3618,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { rational ub = power(rational(10), k) - 1; arith_util& a = m_autil; literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb))); - literal ubl = mk_literal(a.mk_le(n, a.mk_int(ub))); literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k))); - literal le_k = mk_literal(a.mk_le(len, a.mk_int(k))); // n >= lb => len(s) >= k - // n >= 0 & len(s) >= k => n >= lb - // 0 <= n <= ub => len(s) <= k add_axiom(~lbl, ge_k); - add_axiom(~ge0, lbl, ~ge_k); - add_axiom(~ge0, ~ubl, le_k); } From 606754c09a6839e687c94d31e6f65c76a20e7c91 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2019 19:04:02 -0700 Subject: [PATCH 13/13] fix #2262 Signed-off-by: Nikolaj Bjorner --- src/math/automata/automaton.h | 27 ++++++++++++-- src/math/automata/symbolic_automata_def.h | 16 +++++++- src/util/critical_flet.h | 45 ----------------------- 3 files changed, 37 insertions(+), 51 deletions(-) delete mode 100644 src/util/critical_flet.h diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index d642d2379..856d64044 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -348,6 +348,7 @@ public: // void compress() { SASSERT(!m_delta.empty()); + TRACE("seq", display(tout);); for (unsigned i = 0; i < m_delta.size(); ++i) { for (unsigned j = 0; j < m_delta[i].size(); ++j) { move const& mv = m_delta[i][j]; @@ -460,6 +461,7 @@ public: } } sinkify_dead_states(); + TRACE("seq", display(tout);); } bool is_sequence(unsigned& length) const { @@ -559,9 +561,8 @@ public: template std::ostream& display(std::ostream& out, D& displayer = D()) const { out << "init: " << init() << "\n"; - out << "final: "; - for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " "; - out << "\n"; + out << "final: " << m_final_states << "\n"; + for (unsigned i = 0; i < m_delta.size(); ++i) { moves const& mvs = m_delta[i]; for (move const& mv : mvs) { @@ -577,6 +578,22 @@ public: } private: + std::ostream& display(std::ostream& out) const { + out << "init: " << init() << "\n"; + out << "final: " << m_final_states << "\n"; + + for (unsigned i = 0; i < m_delta.size(); ++i) { + moves const& mvs = m_delta[i]; + for (move const& mv : mvs) { + out << i << " -> " << mv.dst() << " "; + if (mv.t()) { + out << "if *** "; + } + out << "\n"; + } + } + return out; + } void sinkify_dead_states() { uint_set dead_states; for (unsigned i = 0; i < m_delta.size(); ++i) { @@ -604,7 +621,9 @@ private: } to_remove.reset(); } - TRACE("seq", tout << "remove: " << dead_states << "\n";); + TRACE("seq", tout << "remove: " << dead_states << "\n"; + tout << "final: " << m_final_states << "\n"; + ); for (unsigned s : dead_states) { CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";); m_delta[s].reset(); diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 17a53fc33..62f87b135 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -379,9 +379,21 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_produ pair2id.insert(init_pair, 0); moves_t mvs; unsigned_vector final; - if (a.is_final_state(a.init()) && b.is_final_state(b.init())) { - final.push_back(0); + unsigned_vector a_init, b_init; + a.get_epsilon_closure(a.init(), a_init); + for (unsigned ia : a_init) { + if (a.is_final_state(ia)) { + b.get_epsilon_closure(b.init(), b_init); + for (unsigned ib : b_init) { + if (b.is_final_state(ib)) { + final.push_back(0); + break; + } + } + break; + } } + unsigned n = 1; moves_t mvsA, mvsB; while (!todo.empty()) { diff --git a/src/util/critical_flet.h b/src/util/critical_flet.h deleted file mode 100644 index 3af2fac24..000000000 --- a/src/util/critical_flet.h +++ /dev/null @@ -1,45 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - critical flet.cpp - -Abstract: - - Version of flet using "omp critical" directive. - - Warning: it uses omp critical section "critical_flet" - -Author: - - Leonardo de Moura (leonardo) 2011-05-12 - -Revision History: - ---*/ -#ifndef CRITICAL_FLET_H_ -#define CRITICAL_FLET_H_ - -template -class critical_flet { - T & m_ref; - T m_old_value; -public: - critical_flet(T & ref, const T & new_value): - m_ref(ref), - m_old_value(ref) { - #pragma omp critical (critical_flet) - { - m_ref = new_value; - } - } - ~critical_flet() { - #pragma omp critical (critical_flet) - { - m_ref = m_old_value; - } - } -}; - -#endif