mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-28 10:32:38 -07:00
parent 4aa1e60daa
commit 6d17c656bd
4 changed files with 14 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/seq_eq_solver.cpp
View file

@ -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)));
}

2
src/smt/seq_skolem.cpp
View file

@ -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;
}

14
src/smt/seq_skolem.h
View file

@ -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;

11
src/smt/theory_str_regex.cpp
View file

@ -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<uint64_t>(a) * static_cast<uint64_t>(b);
if (result > UINT_MAX) {
return UINT_MAX;
}
return result;
return static_cast<unsigned>(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