mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-03-14 07:47:51 -07:00
commit 7634f8b93e
2 changed files with 29 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/api/c++/z3++.h
View file

@ -86,7 +86,13 @@ namespace z3 {
}; };
inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; } inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
#if !defined(Z3_THROW)
#if __cpp_exceptions || _CPPUNWIND
#define Z3_THROW(x) throw x
#else
#define Z3_THROW(x) {}
#endif
#endif // !defined(Z3_THROW)
/** /**
\brief Z3 global configuration object. \brief Z3 global configuration object.
@ -165,7 +171,7 @@ namespace z3 {
Z3_error_code check_error() const { Z3_error_code check_error() const {
Z3_error_code e = Z3_get_error_code(m_ctx); Z3_error_code e = Z3_get_error_code(m_ctx);
if (e != Z3_OK && enable_exceptions()) if (e != Z3_OK && enable_exceptions())
throw exception(Z3_get_error_msg(m_ctx, e)); Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
return e; return e;
} }
@ -701,7 +707,7 @@ namespace z3 {
if (!is_numeral_i(result)) { if (!is_numeral_i(result)) {
assert(ctx().enable_exceptions()); assert(ctx().enable_exceptions());
if (!ctx().enable_exceptions()) return 0; if (!ctx().enable_exceptions()) return 0;
throw exception("numeral does not fit in machine int"); Z3_THROW(exception("numeral does not fit in machine int"));
} }
return result; return result;
} }
@ -721,7 +727,7 @@ namespace z3 {
if (!is_numeral_u(result)) { if (!is_numeral_u(result)) {
assert(ctx().enable_exceptions()); assert(ctx().enable_exceptions());
if (!ctx().enable_exceptions()) return 0; if (!ctx().enable_exceptions()) return 0;
throw exception("numeral does not fit in machine uint"); Z3_THROW(exception("numeral does not fit in machine uint"));
} }
return result; return result;
} }
@ -738,7 +744,7 @@ namespace z3 {
if (!is_numeral_i64(result)) { if (!is_numeral_i64(result)) {
assert(ctx().enable_exceptions()); assert(ctx().enable_exceptions());
if (!ctx().enable_exceptions()) return 0; if (!ctx().enable_exceptions()) return 0;
throw exception("numeral does not fit in machine __int64"); Z3_THROW(exception("numeral does not fit in machine __int64"));
} }
return result; return result;
} }
@ -755,7 +761,7 @@ namespace z3 {
if (!is_numeral_u64(result)) { if (!is_numeral_u64(result)) {
assert(ctx().enable_exceptions()); assert(ctx().enable_exceptions());
if (!ctx().enable_exceptions()) return 0; if (!ctx().enable_exceptions()) return 0;
throw exception("numeral does not fit in machine __uint64"); Z3_THROW(exception("numeral does not fit in machine __uint64"));
} }
return result; return result;
} }
@ -1709,7 +1715,7 @@ namespace z3 {
Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
check_error(); check_error();
if (status == Z3_FALSE && ctx().enable_exceptions()) if (status == Z3_FALSE && ctx().enable_exceptions())
throw exception("failed to evaluate expression"); Z3_THROW(exception("failed to evaluate expression"));
return expr(ctx(), r); return expr(ctx(), r);
} }
@ -2033,7 +2039,7 @@ namespace z3 {
} }
inline tactic par_or(unsigned n, tactic const* tactics) { inline tactic par_or(unsigned n, tactic const* tactics) {
if (n == 0) { if (n == 0) {
throw exception("a non-zero number of tactics need to be passed to par_or"); Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
} }
array<Z3_tactic> buffer(n); array<Z3_tactic> buffer(n);
for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i]; for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];

19
src/ast/rewriter/seq_rewriter.cpp
View file

@ -598,14 +598,25 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
return BR_FAILED; return BR_FAILED;
} }
/*
* (str.at s i), constants s/i, i < 0 or i >= |s| ==> (str.at s i) = ""
*/
br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
zstring c; zstring c;
rational r; rational r;
if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) { if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) {
unsigned j = r.get_unsigned(); if (r.is_neg()) {
if (j < c.length()) { result = m_util.str.mk_string(symbol(""));
result = m_util.str.mk_string(c.extract(j, 1));
return BR_DONE; return BR_DONE;
} else if (r.is_unsigned()) {
unsigned j = r.get_unsigned();
if (j < c.length()) {
result = m_util.str.mk_string(c.extract(j, 1));
return BR_DONE;
} else {
result = m_util.str.mk_string(symbol(""));
return BR_DONE;
}
} }
} }
return BR_FAILED; return BR_FAILED;