mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

string-integer wip

Browse source
This commit is contained in:
Murphy Berzish 2016-06-20 20:02:22 -04:00
parent 89a337ba7e
commit ba42478f9b
2 changed files with 61 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

60
src/smt/theory_str.cpp
View file

@ -1716,6 +1716,64 @@ expr * theory_str::simplify_concat(expr * node) {
} }
void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) {
rational nnLen;
bool nnLen_exists = get_len_value(nn1, nnLen);
if (!nnLen_exists) {
nnLen_exists = get_len_value(nn2, nnLen);
}
// case 1:
// Known: a1_arg0 and a1_arg1
// Unknown: nn1
if (is_concat(to_app(nn1))) {
rational nn1ConcatLen;
bool nn1ConcatLen_exists = infer_len_concat(nn1, nn1ConcatLen);
if (nnLen_exists && nn1ConcatLen_exists) {
nnLen = nn1ConcatLen;
}
}
// case 2:
// Known: a1_arg0 and a1_arg1
// Unknown: nn1
if (is_concat(to_app(nn2))) {
rational nn2ConcatLen;
bool nn2ConcatLen_exists = infer_len_concat(nn2, nn2ConcatLen);
if (nnLen_exists && nn2ConcatLen_exists) {
nnLen = nn2ConcatLen;
}
}
if (nnLen_exists) {
if (is_concat(to_app(nn1))) {
infer_len_concat_arg(nn1, nnLen);
}
if (is_concat(to_app(nn2))) {
infer_len_concat_arg(nn2, nnLen);
}
}
/*
if (isConcatFunc(t, nn2)) {
int nn2ConcatLen = inferLenConcat(t, nn2);
if (nnLen == -1 && nn2ConcatLen != -1)
nnLen = nn2ConcatLen;
}
if (nnLen != -1) {
if (isConcatFunc(t, nn1)) {
inferLenConcatArg(t, nn1, nnLen);
}
if (isConcatFunc(t, nn2)) {
inferLenConcatArg(t, nn2, nnLen);
}
}
*/
}
/* /*
* Handle two equivalent Concats. * Handle two equivalent Concats.
*/ */
@ -1743,7 +1801,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) {
TRACE("t_str", tout << "nn1 = " << mk_ismt2_pp(nn1, m) << std::endl TRACE("t_str", tout << "nn1 = " << mk_ismt2_pp(nn1, m) << std::endl
<< "nn2 = " << mk_ismt2_pp(nn2, m) << std::endl;); << "nn2 = " << mk_ismt2_pp(nn2, m) << std::endl;);
// TODO inferLenConcatEq(nn1, nn2); infer_len_concat_equality(nn1, nn2);
if (a1_arg0 == a2_arg0) { if (a1_arg0 == a2_arg0) {
if (!in_same_eqc(a1_arg1, a2_arg1)) { if (!in_same_eqc(a1_arg1, a2_arg1)) {

2
src/smt/theory_str.h
View file

@ -244,6 +244,8 @@ namespace smt {
void simplify_concat_equality(expr * lhs, expr * rhs); void simplify_concat_equality(expr * lhs, expr * rhs);
void solve_concat_eq_str(expr * concat, expr * str); void solve_concat_eq_str(expr * concat, expr * str);
void infer_len_concat_equality(expr * nn1, expr * nn2);
bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2); bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2); bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2); bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);