mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
parent
780346c7ca
commit
e63992c8bd
|
@ -679,6 +679,7 @@ namespace datatype {
|
|||
bool util::is_recursive_core(sort* s) const {
|
||||
obj_map<sort, status> already_found;
|
||||
ptr_vector<sort> todo, subsorts;
|
||||
sort* s0 = s;
|
||||
todo.push_back(s);
|
||||
status st;
|
||||
while (!todo.empty()) {
|
||||
|
@ -700,7 +701,8 @@ namespace datatype {
|
|||
if (is_datatype(s2)) {
|
||||
if (already_found.find(s2, st)) {
|
||||
// type is recursive
|
||||
if (st == GRAY) return true;
|
||||
if (st == GRAY && s0 == s2)
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
todo.push_back(s2);
|
||||
|
|
|
@ -1285,13 +1285,18 @@ unsigned seq_util::str::min_length(expr* s) const {
|
|||
unsigned seq_util::str::max_length(expr* s) const {
|
||||
SASSERT(u.is_seq(s));
|
||||
unsigned result = 0;
|
||||
expr* s1 = nullptr, *s2 = nullptr;
|
||||
expr* s1 = nullptr, *s2 = nullptr, *s3 = nullptr;
|
||||
unsigned n = 0;
|
||||
zstring st;
|
||||
auto get_length = [&](expr* s1) {
|
||||
if (is_empty(s1))
|
||||
return 0u;
|
||||
else if (is_unit(s1))
|
||||
return 1u;
|
||||
else if (is_at(s1))
|
||||
return 1u;
|
||||
else if (is_extract(s1, s1, s2, s3))
|
||||
return (arith_util(m).is_unsigned(s3, n)) ? n : UINT_MAX;
|
||||
else if (is_string(s1, st))
|
||||
return st.length();
|
||||
else
|
||||
|
|
|
@ -252,10 +252,14 @@ void seq_axioms::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
|
|||
s = "" or !contains(x*s1, s)
|
||||
*/
|
||||
void seq_axioms::tightest_prefix(expr* s, expr* x) {
|
||||
literal s_eq_emp = mk_eq_empty(s);
|
||||
if (seq.str.max_length(s) <= 1) {
|
||||
add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(x, s)));
|
||||
return;
|
||||
}
|
||||
expr_ref s1 = m_sk.mk_first(s);
|
||||
expr_ref c = m_sk.mk_last(s);
|
||||
expr_ref s1c = mk_concat(s1, seq.str.mk_unit(c));
|
||||
literal s_eq_emp = mk_eq_empty(s);
|
||||
add_axiom(s_eq_emp, mk_seq_eq(s, s1c));
|
||||
add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(mk_concat(x, s1), s)));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue