mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

add theory_str::can_concat_eq_str

Browse source
This commit is contained in:
Murphy Berzish 2016-07-27 15:15:01 -04:00
parent 1c518be61d
commit ceed3f3ff0
1 changed files with 46 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

89
src/smt/theory_str.cpp
View file

@ -4011,52 +4011,55 @@ bool theory_str::in_same_eqc(expr * n1, expr * n2) {
} }
bool theory_str::can_concat_eq_str(expr * concat, std::string str) { bool theory_str::can_concat_eq_str(expr * concat, std::string str) {
/* // TODO this method could use some traces and debugging info
int strLen = str.length(); int strLen = str.length();
if (isConcatFunc(t, concat)) { if (is_concat(to_app(concat))) {
std::vector<Z3_ast> args; ptr_vector<expr> args;
getNodesInConcat(t, concat, args); get_nodes_in_concat(concat, args);
Z3_ast ml_node = args[0]; expr * ml_node = args[0];
Z3_ast mr_node = args[args.size() - 1]; expr * mr_node = args[args.size() - 1];
if (isConstStr(t, ml_node)) { if (m_strutil.is_string(ml_node)) {
std::string ml_str = getConstStrValue(t, ml_node); std::string ml_str = m_strutil.get_string_constant_value(ml_node);
int ml_len = ml_str.length(); int ml_len = ml_str.length();
if (ml_len > strLen) if (ml_len > strLen) {
return 0; return false;
int cLen = ml_len; }
if (ml_str != str.substr(0, cLen)) int cLen = ml_len;
return 0; if (ml_str != str.substr(0, cLen)) {
} return false;
}
}
if (isConstStr(t, mr_node)) { if (m_strutil.is_string(mr_node)) {
std::string mr_str = getConstStrValue(t, mr_node); std::string mr_str = m_strutil.get_string_constant_value(mr_node);
int mr_len = mr_str.length(); int mr_len = mr_str.length();
if (mr_len > strLen) if (mr_len > strLen) {
return 0; return false;
int cLen = mr_len; }
if (mr_str != str.substr(strLen - cLen, cLen)) int cLen = mr_len;
return 0; if (mr_str != str.substr(strLen - cLen, cLen)) {
} return false;
}
}
int sumLen = 0; int sumLen = 0;
for (unsigned int i = 0; i < args.size(); i++) { for (unsigned int i = 0 ; i < args.size() ; i++) {
Z3_ast oneArg = args[i]; expr * oneArg = args[i];
if (isConstStr(t, oneArg)) { if (m_strutil.is_string(oneArg)) {
std::string arg_str = getConstStrValue(t, oneArg); std::string arg_str = m_strutil.get_string_constant_value(oneArg);
if (str.find(arg_str) == std::string::npos) { if (str.find(arg_str) == std::string::npos) {
return 0; return false;
} }
sumLen += getConstStrValue(t, oneArg).length(); sumLen += arg_str.length();
} }
} }
if (sumLen > strLen)
return 0; if (sumLen > strLen) {
} return false;
return 1; }
*/ }
// TODO NEXT return true;
NOT_IMPLEMENTED_YET(); return true;
} }
bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) { bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) {