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

z3str3: small refactoring to previous commit

Browse source
This commit is contained in:
Murphy Berzish 2020-02-17 15:55:15 -05:00 • committed by Nikolaj Bjorner
parent b4acd44d5e
commit 698e2ffb0b
1 changed files with 18 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/smt/theory_str_mc.cpp
View file

@ -105,10 +105,8 @@ namespace smt {
ptr_vector<expr> full_chars, suff_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, suff_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, suff_chars, cex)) {
return false;
}
@ -169,10 +167,8 @@ namespace smt {
expr_ref needle(suff, m);
ptr_vector<expr> full_chars, suff_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, suff_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, suff_chars, cex)) {
return false;
}
@ -226,10 +222,8 @@ namespace smt {
expr_ref needle(pref, m);
ptr_vector<expr> full_chars, pref_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, pref_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, pref_chars, cex)) {
return false;
}
@ -290,10 +284,8 @@ namespace smt {
expr_ref needle(pref, m);
ptr_vector<expr> full_chars, pref_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, pref_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, full_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, pref_chars, cex)) {
return false;
}
@ -347,10 +339,8 @@ namespace smt {
expr_ref needle(small, m);
ptr_vector<expr> haystack_chars, needle_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, haystack_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, needle_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, haystack_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, needle_chars, cex)) {
return false;
}
@ -416,10 +406,8 @@ namespace smt {
expr_ref needle(small, m);
ptr_vector<expr> haystack_chars, needle_chars;
if (!fixed_length_reduce_string_term(subsolver, haystack, haystack_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, needle, needle_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, haystack, haystack_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, needle, needle_chars, cex)) {
return false;
}
@ -663,10 +651,8 @@ namespace smt {
expr_ref first(arg0, sub_m);
expr_ref second(arg1, sub_m);
ptr_vector<expr> chars0, chars1;
if (!fixed_length_reduce_string_term(subsolver, first, chars0, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, second, chars1, cex)) {
if (!fixed_length_reduce_string_term(subsolver, first, chars0, cex)
|| !fixed_length_reduce_string_term(subsolver, second, chars1, cex)) {
return false;
}
eqc_chars.append(chars0);
@ -739,10 +725,8 @@ namespace smt {
ptr_vector<expr> lhs_chars, rhs_chars;
if (!fixed_length_reduce_string_term(subsolver, lhs, lhs_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, rhs, rhs_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, lhs, lhs_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, rhs, rhs_chars, cex)) {
return false;
}
@ -787,10 +771,8 @@ namespace smt {
}
ptr_vector<expr> lhs_chars, rhs_chars;
if (!fixed_length_reduce_string_term(subsolver, lhs, lhs_chars, cex)) {
return false;
}
if (!fixed_length_reduce_string_term(subsolver, rhs, rhs_chars, cex)) {
if (!fixed_length_reduce_string_term(subsolver, lhs, lhs_chars, cex)
|| !fixed_length_reduce_string_term(subsolver, rhs, rhs_chars, cex)) {
return false;
}