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_arg

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

55
src/smt/theory_str.cpp
View file

@ -1756,6 +1756,61 @@ bool theory_str::infer_len_concat(expr * n, rational & nLen) {
}
}
void theory_str::infer_len_concat_arg(expr * n, rational len) {
if (len.is_neg()) {
return;
}
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);
expr_ref_vector l_items(m);
expr_ref axr(m);
axr.reset();
// if (mk_length(t, n) != mk_int(ctx, len)) {
{
l_items.push_back(ctx.mk_eq_atom(mk_strlen(n), mk_int(len)));
}
if (!arg0_len_exists && arg1_len_exists) {
//if (mk_length(t, arg1) != mk_int(ctx, arg1_len)) {
{
l_items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(arg1_len)));
}
rational arg0Len = len - arg1_len;
if (arg0Len.is_nonneg()) {
axr = ctx.mk_eq_atom(mk_strlen(arg0), mk_int(arg0Len));
} else {
// TODO negate?
}
} else if (arg0_len_exists && !arg1_len_exists) {
//if (mk_length(t, arg0) != mk_int(ctx, arg0_len)) {
{
l_items.push_back(ctx.mk_eq_atom(mk_strlen(arg0), mk_int(arg0_len)));
}
rational arg1Len = len - arg0_len;
if (arg1Len.is_nonneg()) {
axr = ctx.mk_eq_atom(mk_strlen(arg1), mk_int(arg1Len));
} else {
// TODO negate?
}
} else {
}
if (axr) {
expr_ref axl(m.mk_and(l_items.size(), l_items.c_ptr()), m);
assert_implication(axl, axr);
}
}
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

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