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

fix expr-app conversion

Browse source
This commit is contained in:
Murphy Berzish 2016-09-14 15:51:33 -04:00
parent 804009a757
commit e46fc7b0b6
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_str.cpp
View file

@ -1787,7 +1787,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) {
ctx.internalize(nn, false); ctx.internalize(nn, false);
std::string eq_strValue = m_strutil.get_string_constant_value(eq_str); std::string eq_strValue = m_strutil.get_string_constant_value(eq_str);
app * n_eqNode = nn; expr * n_eqNode = nn;
do { do {
enode * n_eq_enode = ctx.get_enode(n_eqNode); enode * n_eq_enode = ctx.get_enode(n_eqNode);
TRACE("t_str_detail", tout << "considering all parents of " << mk_ismt2_pp(n_eqNode, m) << std::endl TRACE("t_str_detail", tout << "considering all parents of " << mk_ismt2_pp(n_eqNode, m) << std::endl
@ -1872,7 +1872,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) {
assert_implication(implyL, implyR); assert_implication(implyL, implyR);
} }
} else if (is_concat(n_eqNode)) { } else if (is_concat(to_app(n_eqNode))) {
expr_ref simpleConcat(m); expr_ref simpleConcat(m);
simpleConcat = mk_concat(eq_str, arg1); simpleConcat = mk_concat(eq_str, arg1);
if (!in_same_eqc(a_parent, simpleConcat)) { if (!in_same_eqc(a_parent, simpleConcat)) {
@ -1943,7 +1943,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) {
assert_implication(implyL, implyR); assert_implication(implyL, implyR);
} }
} else if (is_concat(n_eqNode)) { } else if (is_concat(to_app(n_eqNode))) {
expr_ref simpleConcat(m); expr_ref simpleConcat(m);
simpleConcat = mk_concat(arg0, eq_str); simpleConcat = mk_concat(arg0, eq_str);
if (!in_same_eqc(a_parent, simpleConcat)) { if (!in_same_eqc(a_parent, simpleConcat)) {
@ -4198,9 +4198,9 @@ expr * theory_str::collect_eq_nodes(expr * n, expr_ref_vector & eqcSet) {
context & ctx = get_context(); context & ctx = get_context();
expr * constStrNode = NULL; expr * constStrNode = NULL;
app * ex = n; expr * ex = n;
do { do {
if (m_strutil.is_string(ex)) { if (m_strutil.is_string(to_app(ex))) {
constStrNode = ex; constStrNode = ex;
} }
eqcSet.push_back(ex); eqcSet.push_back(ex);
@ -5537,9 +5537,9 @@ bool theory_str::check_concat_len_in_eqc(expr * concat) {
bool no_assertions = true; bool no_assertions = true;
app * eqc_n = concat; expr * eqc_n = concat;
do { do {
if (is_concat(eqc_n)) { if (is_concat(to_app(eqc_n))) {
rational unused; rational unused;
bool status = infer_len_concat(eqc_n, unused); bool status = infer_len_concat(eqc_n, unused);
if (status) { if (status) {