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

theory_str infer_len_concat

Browse source
This commit is contained in:
Murphy Berzish 2016-06-21 17:25:28 -04:00
parent ba42478f9b
commit 1e46782392
2 changed files with 41 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/smt/theory_str.cpp
View file

@ -1716,6 +1716,46 @@ expr * theory_str::simplify_concat(expr * node) {
}
// Modified signature of Z3str2's inferLenConcat().
// Returns true iff nLen can be inferred by this method
// (i.e. the equivalent of a len_exists flag in get_len_value()).
bool theory_str::infer_len_concat(expr * n, rational & nLen) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr * arg0 = to_app(n)->get_arg(0);
expr * arg1 = to_app(n)->get_arg(1);
rational arg0_len, arg1_len;
bool arg0_len_exists = get_len_value(arg0, arg0_len);
bool arg1_len_exists = get_len_value(arg1, arg1_len);
rational tmp_len;
bool nLen_exists = get_len_value(n, tmp_len);
if (arg0_len_exists && arg1_len_exists && !nLen_exists) {
expr_ref_vector l_items(m);
// if (mk_strlen(arg0) != mk_int(arg0_len)) {
{
l_items.push_back(ctx.mk_eq_atom(mk_strlen(arg0), mk_int(arg0_len)));
}
// if (mk_strlen(arg1) != mk_int(arg1_len)) {
{
l_items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(arg1_len)));
}
expr_ref axl(m.mk_and(l_items.size(), l_items.c_ptr()), m);
rational nnLen = arg0_len + arg1_len;
expr_ref axr(ctx.mk_eq_atom(mk_strlen(n), mk_int(nnLen)), m);
TRACE("t_str_detail", tout << "inferred (Length " << mk_pp(n, m) << ") = " << nnLen << std::endl;);
assert_implication(axl, axr);
nLen = nnLen;
return true;
} else {
return false;
}
}
void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) {
rational nnLen;
bool nnLen_exists = get_len_value(nn1, nnLen);

1
src/smt/theory_str.h
View file

@ -245,6 +245,7 @@ namespace smt {
void solve_concat_eq_str(expr * concat, expr * str);
void infer_len_concat_equality(expr * nn1, expr * nn2);
bool infer_len_concat(expr * n, rational & nLen);
bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);