From 6d17c656bd29ae7cd10b0ed991210302eeab92ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2020 10:32:38 -0700 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/smt/seq_eq_solver.cpp | 11 +++-------- src/smt/seq_skolem.cpp | 2 +- src/smt/seq_skolem.h | 14 ++++++-------- src/smt/theory_str_regex.cpp | 11 ++++------- 4 files changed, 14 insertions(+), 24 deletions(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index a6e3aaef3..4240dbcb5 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -939,14 +939,9 @@ bool theory_seq::branch_quat_variable() { * align_m(x1, x, _, _) - align_m(y1, x, _, _) = x1 - y1 */ literal theory_seq::mk_alignment(expr* e1, expr* e2) { - if (m_sk.is_align(e1) && m_sk.is_align(e2)) { - expr* x1 = to_app(e1)->get_arg(0); - expr* x2 = to_app(e1)->get_arg(1); - expr* y1 = to_app(e2)->get_arg(0); - expr* y2 = to_app(e2)->get_arg(1); - if (x2 == y2 && x1 != y1) { - return mk_alignment(x1, y1); - } + expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr; + if (m_sk.is_align(e1, x1, x2) && m_sk.is_align(e2, y1, y2) && x2 == y2 && x1 != y1) { + return mk_alignment(x1, y1); } return mk_simplified_literal(m_autil.mk_le(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(0))); } diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp index 843918e51..e110d41c7 100644 --- a/src/smt/seq_skolem.cpp +++ b/src/smt/seq_skolem.cpp @@ -70,7 +70,7 @@ bool seq_skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const { } -bool seq_skolem::is_skolem(symbol const& s, expr* e) const { +bool seq_skolem::is_skolem(symbol const& s, expr const* e) const { return seq.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s; } diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h index 1d26f2e16..77233266d 100644 --- a/src/smt/seq_skolem.h +++ b/src/smt/seq_skolem.h @@ -61,11 +61,8 @@ namespace smt { expr_ref mk_align_l(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.l", e1, e2, e3, e4); } expr_ref mk_align_r(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.r", e1, e2, e3, e4); } expr_ref mk_align_m(expr* e1, expr* e2, expr* e3, expr* e4) { - if (is_align(e1) && is_align(e2)) { - expr* x1 = to_app(e1)->get_arg(0); - expr* x2 = to_app(e1)->get_arg(1); - expr* y1 = to_app(e2)->get_arg(0); - expr* y2 = to_app(e2)->get_arg(1); + expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr; + if (is_align(e1, x1, x2) && is_align(e2, y1, y2)) { if (x2 == y2 && x1 != y1) return mk_align_m(x1, y1, e3, e4); } @@ -100,8 +97,8 @@ namespace smt { expr_ref mk_length_limit(expr* e, unsigned d); - bool is_skolem(symbol const& s, expr* e) const; - bool is_skolem(expr* e) const { return seq.is_skolem(e); } + bool is_skolem(symbol const& s, expr const* e) const; + bool is_skolem(expr const* e) const { return seq.is_skolem(e); } bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); } bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); } @@ -124,7 +121,8 @@ namespace smt { r = to_app(e)->get_arg(2), true) && a.is_unsigned(i, idx); } - bool is_align(expr* e) const { return is_skolem(symbol("seq.align.m"), e); } + bool is_align(expr const* e) const { return is_skolem(symbol("seq.align.m"), e); } + MATCH_BINARY(is_align); bool is_post(expr* e, expr*& s, expr*& start); bool is_pre(expr* e, expr*& s, expr*& i); bool is_eq(expr* e, expr*& a, expr*& b) const; diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index e27d79786..999c54e5d 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -36,14 +36,11 @@ namespace smt { if (a == UINT_MAX || b == UINT_MAX) { return UINT_MAX; } - if (a == 0 || b == 0) { - return 0; - } - unsigned result = a * b; - if (result < a || result < b) { + uint64_t result = static_cast(a) * static_cast(b); + if (result > UINT_MAX) { return UINT_MAX; } - return result; + return static_cast(result); } // Returns false if we need to give up solving, e.g. because we found symbolic expressions in an automaton. @@ -207,7 +204,7 @@ namespace smt { continue; } else { // fixed-length model construction handles path constraints on our behalf, and with a better reduction - return; + return false; } } else { // no automata available, or else all bounds assumptions are invalid