diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1d56c43a4..6585bd7f2 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -23,6 +23,7 @@ Revision History: #include #include #include +#include"theory_seq_empty.h" #include "../ast/ast.h" #include"theory_arith.h" @@ -832,11 +833,12 @@ void theory_str::propagate() { } else if (is_LastIndexof(e)) { instantiate_axiom_LastIndexof(e); */ - } else if (u.str.is_substr(a)) { + } else if (u.str.is_extract(a)) { + // TODO check semantics of substr vs. extract instantiate_axiom_Substr(e); - } else if (is_Replace(e)) { + } else if (u.str.is_replace(a)) { instantiate_axiom_Replace(e); - } else if (is_RegexIn(e)) { + } else if (u.str.is_in_re(a)) { instantiate_axiom_RegexIn(e); } else { TRACE("t_str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); @@ -861,8 +863,8 @@ void theory_str::propagate() { */ void theory_str::try_eval_concat(enode * cat) { - SASSERT(is_concat(cat)); app * a_cat = cat->get_owner(); + SASSERT(u.str.is_concat(a_cat)); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -870,7 +872,7 @@ void theory_str::try_eval_concat(enode * cat) { TRACE("t_str_detail", tout << "attempting to flatten " << mk_pp(a_cat, m) << std::endl;); std::stack worklist; - std::string flattenedString(""); + zstring flattenedString(""); bool constOK = true; { @@ -883,10 +885,10 @@ void theory_str::try_eval_concat(enode * cat) { while (constOK && !worklist.empty()) { app * evalArg = worklist.top(); worklist.pop(); - if (m_strutil.is_string(evalArg)) { - std::string nextStr = m_strutil.get_string_constant_value(evalArg); - flattenedString.append(nextStr); - } else if (is_concat(evalArg)) { + zstring nextStr; + if (u.str.is_string(evalArg, nextStr)) { + flattenedString += nextStr; + } else if (u.str.is_concat(evalArg)) { app * arg0 = to_app(evalArg->get_arg(0)); app * arg1 = to_app(evalArg->get_arg(1)); @@ -899,7 +901,7 @@ void theory_str::try_eval_concat(enode * cat) { } } if (constOK) { - TRACE("t_str_detail", tout << "flattened to \"" << flattenedString << "\"" << std::endl;); + TRACE("t_str_detail", tout << "flattened to \"" << flattenedString.encode().c_str() << "\"" << std::endl;); expr_ref constStr(mk_string(flattenedString), m); expr_ref axiom(ctx.mk_eq_atom(a_cat, constStr), m); assert_axiom(axiom); @@ -911,8 +913,8 @@ void theory_str::try_eval_concat(enode * cat) { * Length(Concat(x, y)) = Length(x) + Length(y) */ void theory_str::instantiate_concat_axiom(enode * cat) { - SASSERT(is_concat(cat)); app * a_cat = cat->get_owner(); + SASSERT(u.str.is_concat(a_cat)); ast_manager & m = get_manager(); @@ -969,15 +971,15 @@ void theory_str::instantiate_basic_string_axioms(enode * str) { // generate a stronger axiom for constant strings app * a_str = str->get_owner(); - if (m_strutil.is_string(str->get_owner())) { + if (u.str.is_string(a_str)) { expr_ref len_str(m); len_str = mk_strlen(a_str); SASSERT(len_str); - const char * strconst = 0; - m_strutil.is_string(str->get_owner(), & strconst); - TRACE("t_str_detail", tout << "instantiating constant string axioms for \"" << strconst << "\"" << std::endl;); - int l = strlen(strconst); + zstring strconst; + u.str.is_string(str->get_owner(), strconst); + TRACE("t_str_detail", tout << "instantiating constant string axioms for \"" << strconst.encode().c_str() << "\"" << std::endl;); + unsigned int l = strconst.length(); expr_ref len(m_autil.mk_numeral(rational(l), true), m); literal lit(mk_eq(len_str, len, false)); @@ -1186,12 +1188,11 @@ void theory_str::instantiate_axiom_Contains(enode * e) { axiomatized_terms.insert(ex); // quick path, because this is necessary due to rewriter behaviour - // (at minimum it should fix z3str/concat-006.smt2 - if (m_strutil.is_string(ex->get_arg(0)) && m_strutil.is_string(ex->get_arg(1))) { + // at minimum it should fix z3str/concat-006.smt2 + zstring haystackStr, needleStr; + if (u.str.is_string(ex->get_arg(0), haystackStr) && u.str.is_string(ex->get_arg(1), needleStr)) { TRACE("t_str_detail", tout << "eval constant Contains term " << mk_pp(ex, m) << std::endl;); - std::string haystackStr = m_strutil.get_string_constant_value(ex->get_arg(0)); - std::string needleStr = m_strutil.get_string_constant_value(ex->get_arg(1)); - if (haystackStr.find(needleStr) != std::string::npos) { + if (haystackStr.contains(needleStr)) { assert_axiom(ex); } else { assert_axiom(m.mk_not(ex)); @@ -1378,8 +1379,8 @@ void theory_str::instantiate_axiom_LastIndexof(enode * e) { thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1))); bool canSkip = false; - if (m_strutil.is_string(expr->get_arg(1))) { - std::string arg1Str = m_strutil.get_string_constant_value(expr->get_arg(1)); + zstring arg1Str; + if (u.str.is_string(expr->get_arg(1), arg1Str)) { if (arg1Str.length() == 1) { canSkip = true; } @@ -1503,30 +1504,6 @@ void theory_str::instantiate_axiom_Substr(enode * e) { expr_ref finalAxiom(m.mk_and(case1, case2, case3), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); - - /* - expr_ref ts0(mk_str_var("ts0"), m); - expr_ref ts1(mk_str_var("ts1"), m); - expr_ref ts2(mk_str_var("ts2"), m); - - expr_ref ts0_contains_ts1(mk_contains(expr->get_arg(0), ts1), m); - - expr_ref_vector and_item(m); - //and_item.push_back(ts0_contains_ts1); - and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2)))); - and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0))); - and_item.push_back(ctx.mk_eq_atom(expr->get_arg(2), mk_strlen(ts1))); - - expr_ref breakdownAssert(m.mk_and(and_item.size(), and_item.c_ptr()), m); - SASSERT(breakdownAssert); - - expr_ref reduceToVar(ctx.mk_eq_atom(expr, ts1), m); - SASSERT(reduceToVar); - - expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToVar), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - */ } void theory_str::instantiate_axiom_Replace(enode * e) { @@ -1651,14 +1628,58 @@ void theory_str::instantiate_axiom_int_to_str(enode * e) { } expr * theory_str::mk_RegexIn(expr * str, expr * regexp) { - expr * args[2] = {str, regexp}; - app * regexIn = get_manager().mk_app(get_id(), OP_RE_REGEXIN, 0, 0, 2, args); + app * regexIn = u.re.mk_in_re(str, regexp); // immediately force internalization so that axiom setup does not fail get_context().internalize(regexIn, false); set_up_axioms(regexIn); return regexIn; } +static zstring str2RegexStr(zstring str) { + zstring res(""); + int len = str.length(); + for (int i = 0; i < len; i++) { + char nc = str[i]; + // 12 special chars + if (nc == '\\' || nc == '^' || nc == '$' || nc == '.' || nc == '|' || nc == '?' + || nc == '*' || nc == '+' || nc == '(' || nc == ')' || nc == '[' || nc == '{') { + res += zstring("\\"); + } + res += zstring(1, (unsigned)str[i]); + } + return res; +} + +zstring theory_str::get_std_regex_str(expr * regex) { + app * a_regex = to_app(regex); + if (u.re.is_to_re(a_regex)) { + expr * regAst = a_regex->get_arg(0); + zstring regAstVal; + u.str.is_string(regAst, regAstVal); + zstring regStr = str2RegexStr(regAstVal); + return regStr; + } else if (u.re.is_concat(a_regex)) { + expr * reg1Ast = a_regex->get_arg(0); + expr * reg2Ast = a_regex->get_arg(1); + zstring reg1Str = get_std_regex_str(reg1Ast); + zstring reg2Str = get_std_regex_str(reg2Ast); + return zstring("(") + reg1Str + zstring(")(") + reg2Str + zstring(")"); + } else if (u.re.is_union(a_regex)) { + expr * reg1Ast = a_regex->get_arg(0); + expr * reg2Ast = a_regex->get_arg(1); + zstring reg1Str = get_std_regex_str(reg1Ast); + zstring reg2Str = get_std_regex_str(reg2Ast); + return zstring("(") + reg1Str + zstring(")|(") + reg2Str + zstring(")"); + } else if (u.re.is_star(a_regex)) { + expr * reg1Ast = a_regex->get_arg(0); + zstring reg1Str = get_std_regex_str(reg1Ast); + return zstring("(") + reg1Str + zstring(")*"); + } else { + TRACE("t_str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); + UNREACHABLE(); return zstring(""); + } +} + void theory_str::instantiate_axiom_RegexIn(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); @@ -1673,8 +1694,8 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { TRACE("t_str_detail", tout << "instantiate RegexIn axiom for " << mk_pp(ex, m) << std::endl;); { - std::string regexStr = m_strutil.get_std_regex_str(ex->get_arg(1)); - std::pair key1(ex->get_arg(0), regexStr); + zstring regexStr = get_std_regex_str(ex->get_arg(1)); + std::pair key1(ex->get_arg(0), regexStr); // skip Z3str's map check, because we already check if we set up axioms on this term regex_in_bool_map[key1] = ex; regex_in_var_reg_str_map[ex->get_arg(0)].insert(regexStr); @@ -1683,7 +1704,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { expr_ref str(ex->get_arg(0), m); app * regex = to_app(ex->get_arg(1)); - if (is_Str2Reg(regex)) { + if (u.re.is_to_re(regex)) { expr_ref rxStr(regex->get_arg(0), m); // want to assert 'expr IFF (str == rxStr)' expr_ref rhs(ctx.mk_eq_atom(str, rxStr), m); @@ -1691,7 +1712,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { SASSERT(finalAxiom); assert_axiom(finalAxiom); TRACE("t_str", tout << "set up Str2Reg: (RegexIn " << mk_pp(str, m) << " " << mk_pp(regex, m) << ")" << std::endl;); - } else if (is_RegexConcat(regex)) { + } else if (u.re.is_concat(regex)) { expr_ref var1(mk_regex_rep_var(), m); expr_ref var2(mk_regex_rep_var(), m); expr_ref rhs(mk_concat(var1, var2), m); @@ -1708,7 +1729,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { expr_ref finalAxiom(mk_and(items), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); - } else if (is_RegexUnion(regex)) { + } else if (u.re.is_union(regex)) { expr_ref var1(mk_regex_rep_var(), m); expr_ref var2(mk_regex_rep_var(), m); expr_ref orVar(m.mk_or(ctx.mk_eq_atom(str, var1), ctx.mk_eq_atom(str, var2)), m); @@ -1721,7 +1742,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { items.push_back(var2InRegex2); items.push_back(ctx.mk_eq_atom(ex, orVar)); assert_axiom(mk_and(items)); - } else if (is_RegexStar(regex)) { + } else if (u.re.is_star(regex)) { // slightly more complex due to the unrolling step. expr_ref regex1(regex->get_arg(0), m); expr_ref unrollCount(mk_unroll_bound_var(), m); @@ -1852,13 +1873,13 @@ void theory_str::group_terms_by_eqc(expr * n, std::set & concats, std::se expr * eqcNode = n; do { app * ast = to_app(eqcNode); - if (is_concat(ast)) { + if (u.str.is_concat(ast)) { expr * simConcat = simplify_concat(ast); if (simConcat != ast) { - if (is_concat(to_app(simConcat))) { + if (u.str.is_concat(to_app(simConcat))) { concats.insert(simConcat); } else { - if (m_strutil.is_string(simConcat)) { + if (u.str.is_string(simConcat)) { consts.insert(simConcat); } else { vars.insert(simConcat); @@ -1867,7 +1888,7 @@ void theory_str::group_terms_by_eqc(expr * n, std::set & concats, std::se } else { concats.insert(simConcat); } - } else if (is_string(ast)) { + } else if (u.str.is_string(ast)) { consts.insert(ast); } else { vars.insert(ast); @@ -1878,7 +1899,7 @@ void theory_str::group_terms_by_eqc(expr * n, std::set & concats, std::se void theory_str::get_nodes_in_concat(expr * node, ptr_vector & nodeList) { app * a_node = to_app(node); - if (!is_concat(a_node)) { + if (!u.str.is_concat(a_node)) { nodeList.push_back(node); return; } else { @@ -1901,16 +1922,21 @@ expr * theory_str::eval_concat(expr * n1, expr * n2) { expr * v1 = get_eqc_value(n1, n1HasEqcValue); expr * v2 = get_eqc_value(n2, n2HasEqcValue); if (n1HasEqcValue && n2HasEqcValue) { - std::string n1_str = m_strutil.get_string_constant_value(v1); - std::string n2_str = m_strutil.get_string_constant_value(v2); - std::string result = n1_str + n2_str; + zstring n1_str, n2_str; + u.str.is_string(v1, n1_str); + u.str.is_string(v2, n2_str); + zstring result = n1_str + n2_str; return mk_string(result); } else if (n1HasEqcValue && !n2HasEqcValue) { - if (m_strutil.get_string_constant_value(v1) == "") { + zstring v1_str; + u.str.is_string(v1, v1_str); + if (v1_str.empty()) { return n2; } } else if (n2HasEqcValue && !n1HasEqcValue) { - if (m_strutil.get_string_constant_value(v2) == "") { + zstring v2_str; + u.str.is_string(v2, v2_str); + if (v2_str.empty()) { return n1; } } @@ -1943,7 +1969,8 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { ctx.internalize(nn, false); - std::string eq_strValue = m_strutil.get_string_constant_value(eq_str); + zstring eq_strValue; + u.str.is_string(eq_str, eq_strValue); expr * n_eqNode = nn; do { enode * n_eq_enode = ctx.get_enode(n_eqNode); @@ -1966,7 +1993,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { app * a_parent = e_parent->get_owner(); TRACE("t_str_detail", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;); - if (is_concat(a_parent)) { + if (u.str.is_concat(a_parent)) { expr * arg0 = a_parent->get_arg(0); expr * arg1 = a_parent->get_arg(1); @@ -2028,7 +2055,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { assert_implication(implyL, implyR); } - } else if (is_concat(to_app(n_eqNode))) { + } else if (u.str.is_concat(to_app(n_eqNode))) { expr_ref simpleConcat(m); simpleConcat = mk_concat(eq_str, arg1); if (!in_same_eqc(a_parent, simpleConcat)) { @@ -2097,7 +2124,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { assert_implication(implyL, implyR); } - } else if (is_concat(to_app(n_eqNode))) { + } else if (u.str.is_concat(to_app(n_eqNode))) { expr_ref simpleConcat(m); simpleConcat = mk_concat(arg0, eq_str); if (!in_same_eqc(a_parent, simpleConcat)) { @@ -2116,11 +2143,11 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { //--------------------------------------------------------- // Case (2-1) begin: (Concat n_eqNode (Concat str var)) - if (arg0 == n_eqNode && is_concat(to_app(arg1))) { + if (arg0 == n_eqNode && u.str.is_concat(to_app(arg1))) { app * a_arg1 = to_app(arg1); TRACE("t_str_detail", tout << "simplify_parent #3" << std::endl;); expr * r_concat_arg0 = a_arg1->get_arg(0); - if (m_strutil.is_string(r_concat_arg0)) { + if (u.str.is_string(r_concat_arg0)) { expr * combined_str = eval_concat(eq_str, r_concat_arg0); SASSERT(combined_str); expr * r_concat_arg1 = a_arg1->get_arg(1); @@ -2140,11 +2167,11 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { //--------------------------------------------------------- // Case (2-2) begin: (Concat (Concat var str) n_eqNode) - if (is_concat(to_app(arg0)) && arg1 == n_eqNode) { + if (u.str.is_concat(to_app(arg0)) && arg1 == n_eqNode) { app * a_arg0 = to_app(arg0); TRACE("t_str_detail", tout << "simplify_parent #4" << std::endl;); expr * l_concat_arg1 = a_arg0->get_arg(1); - if (m_strutil.is_string(l_concat_arg1)) { + if (u.str.is_string(l_concat_arg1)) { expr * combined_str = eval_concat(l_concat_arg1, eq_str); SASSERT(combined_str); expr * l_concat_arg0 = a_arg0->get_arg(0); @@ -2169,10 +2196,10 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { concat_parent_it != e_parent->end_parents(); concat_parent_it++) { enode * e_concat_parent = *concat_parent_it; app * concat_parent = e_concat_parent->get_owner(); - if (is_concat(concat_parent)) { + if (u.str.is_concat(concat_parent)) { expr * concat_parent_arg0 = concat_parent->get_arg(0); expr * concat_parent_arg1 = concat_parent->get_arg(1); - if (concat_parent_arg0 == a_parent && m_strutil.is_string(concat_parent_arg1)) { + if (concat_parent_arg0 == a_parent && u.str.is_string(concat_parent_arg1)) { TRACE("t_str_detail", tout << "simplify_parent #5" << std::endl;); expr * combinedStr = eval_concat(eq_str, concat_parent_arg1); SASSERT(combinedStr); @@ -2195,10 +2222,10 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { concat_parent_it != e_parent->end_parents(); concat_parent_it++) { enode * e_concat_parent = *concat_parent_it; app * concat_parent = e_concat_parent->get_owner(); - if (is_concat(concat_parent)) { + if (u.str.is_concat(concat_parent)) { expr * concat_parent_arg0 = concat_parent->get_arg(0); expr * concat_parent_arg1 = concat_parent->get_arg(1); - if (concat_parent_arg1 == a_parent && m_strutil.is_string(concat_parent_arg0)) { + if (concat_parent_arg1 == a_parent && u.str.is_string(concat_parent_arg0)) { TRACE("t_str_detail", tout << "simplify_parent #6" << std::endl;); expr * combinedStr = eval_concat(concat_parent_arg0, eq_str); SASSERT(combinedStr); @@ -2376,7 +2403,7 @@ void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) { // Known: a1_arg0 and a1_arg1 // Unknown: nn1 - if (is_concat(to_app(nn1))) { + if (u.str.is_concat(to_app(nn1))) { rational nn1ConcatLen; bool nn1ConcatLen_exists = infer_len_concat(nn1, nn1ConcatLen); if (nnLen_exists && nn1ConcatLen_exists) { @@ -2388,7 +2415,7 @@ void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) { // Known: a1_arg0 and a1_arg1 // Unknown: nn1 - if (is_concat(to_app(nn2))) { + if (u.str.is_concat(to_app(nn2))) { rational nn2ConcatLen; bool nn2ConcatLen_exists = infer_len_concat(nn2, nn2ConcatLen); if (nnLen_exists && nn2ConcatLen_exists) { @@ -2397,10 +2424,10 @@ void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) { } if (nnLen_exists) { - if (is_concat(to_app(nn1))) { + if (u.str.is_concat(to_app(nn1))) { infer_len_concat_arg(nn1, nnLen); } - if (is_concat(to_app(nn2))) { + if (u.str.is_concat(to_app(nn2))) { infer_len_concat_arg(nn2, nnLen); } } @@ -2604,17 +2631,17 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { // check whether new_nn1 and new_nn2 are still concats - bool n1IsConcat = is_concat(a_new_nn1); - bool n2IsConcat = is_concat(a_new_nn2); + bool n1IsConcat = u.str.is_concat(a_new_nn1); + bool n2IsConcat = u.str.is_concat(a_new_nn2); if (!n1IsConcat && n2IsConcat) { TRACE("t_str_detail", tout << "nn1_new is not a concat" << std::endl;); - if (is_string(a_new_nn1)) { + if (u.str.is_string(a_new_nn1)) { simplify_parent(new_nn2, new_nn1); } return; } else if (n1IsConcat && !n2IsConcat) { TRACE("t_str_detail", tout << "nn2_new is not a concat" << std::endl;); - if (is_string(a_new_nn2)) { + if (u.str.is_string(a_new_nn2)) { simplify_parent(new_nn1, new_nn2); } return; @@ -2712,8 +2739,8 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { app * a_new_nn1 = to_app(new_nn1); app * a_new_nn2 = to_app(new_nn2); - bool n1IsConcat = is_concat(a_new_nn1); - bool n2IsConcat = is_concat(a_new_nn2); + bool n1IsConcat = u.str.is_concat(a_new_nn1); + bool n2IsConcat = u.str.is_concat(a_new_nn2); if (!n1IsConcat && !n2IsConcat) { // we simplified both sides to non-concat expressions... return false; @@ -2766,7 +2793,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * v2_arg0 = to_app(new_nn2)->get_arg(0); expr * v2_arg1 = to_app(new_nn2)->get_arg(1); - if (m_strutil.is_string(v1_arg1) && !m_strutil.is_string(v2_arg1)) { + if (u.str.is_string(v1_arg1) && !u.str.is_string(v2_arg1)) { m = v1_arg0; strAst = v1_arg1; x = v2_arg0; @@ -2800,7 +2827,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * strAst = NULL; expr * n = NULL; - if (m_strutil.is_string(v1_arg0) && !m_strutil.is_string(v2_arg0)) { + if (u.str.is_string(v1_arg0) && !u.str.is_string(v2_arg0)) { strAst = v1_arg0; n = v1_arg1; x = v2_arg0; @@ -2848,7 +2875,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * m = NULL; expr * str2Ast = NULL; - if (m_strutil.is_string(v1_arg0)) { + if (u.str.is_string(v1_arg0)) { str1Ast = v1_arg0; y = v1_arg1; m = v2_arg0; @@ -2881,7 +2908,7 @@ bool theory_str::is_concat_eq_type1(expr * concatAst1, expr * concatAst2) { expr * m = to_app(concatAst2)->get_arg(0); expr * n = to_app(concatAst2)->get_arg(1); - if (!m_strutil.is_string(x) && !m_strutil.is_string(y) && !m_strutil.is_string(m) && !m_strutil.is_string(n)) { + if (!u.str.is_string(x) && !u.str.is_string(y) && !u.str.is_string(m) && !u.str.is_string(n)) { return true; } else { return false; @@ -2896,11 +2923,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -3268,11 +3295,11 @@ bool theory_str::is_concat_eq_type2(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if ((!m_strutil.is_string(v1_arg0)) && m_strutil.is_string(v1_arg1) - && (!m_strutil.is_string(v2_arg0)) && (!m_strutil.is_string(v2_arg1))) { + if ((!u.str.is_string(v1_arg0)) && u.str.is_string(v1_arg1) + && (!u.str.is_string(v2_arg0)) && (!u.str.is_string(v2_arg1))) { return true; - } else if ((!m_strutil.is_string(v2_arg0)) && m_strutil.is_string(v2_arg1) - && (!m_strutil.is_string(v1_arg0)) && (!m_strutil.is_string(v1_arg1))) { + } else if ((!u.str.is_string(v2_arg0)) && u.str.is_string(v2_arg1) + && (!u.str.is_string(v1_arg0)) && (!u.str.is_string(v1_arg1))) { return true; } else { return false; @@ -3287,11 +3314,11 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -3306,7 +3333,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if (m_strutil.is_string(v1_arg1) && !m_strutil.is_string(v2_arg1)) { + if (u.str.is_string(v1_arg1) && !u.str.is_string(v2_arg1)) { m = v1_arg0; strAst = v1_arg1; x = v2_arg0; @@ -3318,14 +3345,15 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { y = v1_arg1; } - std::string strValue = m_strutil.get_string_constant_value(strAst); + zstring strValue; + u.str.is_string(strAst, strValue); rational x_len, y_len, m_len, str_len; bool x_len_exists = get_len_value(x, x_len); bool y_len_exists = get_len_value(y, y_len); bool m_len_exists = get_len_value(m, m_len); bool str_len_exists = true; - str_len = rational((unsigned)(strValue.length())); + str_len = rational(strValue.length()); // setup @@ -3502,12 +3530,12 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { << "mLen = " << m_len.to_string() << std::endl << "strLen = " << str_len.to_string() << std::endl << "lenDelta = " << lenDelta.to_string() << std::endl - << "strValue = \"" << strValue << "\" (len=" << strValue.length() << ")" << std::endl + << "strValue = \"" << strValue << "\" (len=" << strValue.length() << ")" << "\n" ; ); - std::string part1Str = strValue.substr(0, lenDelta.get_unsigned()); - std::string part2Str = strValue.substr(lenDelta.get_unsigned(), strValue.length() - lenDelta.get_unsigned()); + zstring part1Str = strValue.extract(0, lenDelta.get_unsigned()); + zstring part2Str = strValue.extract(lenDelta.get_unsigned(), strValue.length() - lenDelta.get_unsigned()); expr_ref prefixStr(mk_string(part1Str), mgr); expr_ref x_concat(mk_concat(m, prefixStr), mgr); @@ -3573,9 +3601,9 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } } - for (int i = 0; i <= (int)strValue.size(); ++i) { - std::string part1Str = strValue.substr(0, i); - std::string part2Str = strValue.substr(i, strValue.size() - i); + for (unsigned int i = 0; i <= strValue.length(); ++i) { + zstring part1Str = strValue.extract(0, i); + zstring part2Str = strValue.extract(i, strValue.length() - i); expr_ref prefixStr(mk_string(part1Str), mgr); expr_ref x_concat(mk_concat(m, prefixStr), mgr); expr_ref cropStr(mk_string(part2Str), mgr); @@ -3624,11 +3652,11 @@ bool theory_str::is_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if (m_strutil.is_string(v1_arg0) && (!m_strutil.is_string(v1_arg1)) - && (!m_strutil.is_string(v2_arg0)) && (!m_strutil.is_string(v2_arg1))) { + if (u.str.is_string(v1_arg0) && (!u.str.is_string(v1_arg1)) + && (!u.str.is_string(v2_arg0)) && (!u.str.is_string(v2_arg1))) { return true; - } else if (m_strutil.is_string(v2_arg0) && (!m_strutil.is_string(v2_arg1)) - && (!m_strutil.is_string(v1_arg0)) && (!m_strutil.is_string(v1_arg1))) { + } else if (u.str.is_string(v2_arg0) && (!u.str.is_string(v2_arg1)) + && (!u.str.is_string(v1_arg0)) && (!u.str.is_string(v1_arg1))) { return true; } else { return false; @@ -3643,11 +3671,11 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -3662,7 +3690,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr * strAst = NULL; expr * n = NULL; - if (m_strutil.is_string(v1_arg0) && !m_strutil.is_string(v2_arg0)) { + if (u.str.is_string(v1_arg0) && !u.str.is_string(v2_arg0)) { strAst = v1_arg0; n = v1_arg1; x = v2_arg0; @@ -3674,7 +3702,8 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { y = v1_arg1; } - std::string strValue = m_strutil.get_string_constant_value(strAst); + zstring strValue; + u.str.is_string(strAst, strValue); rational x_len, y_len, str_len, n_len; bool x_len_exists = get_len_value(x, x_len); @@ -3776,9 +3805,9 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { prefixLen = x_len; litems.push_back(ctx.mk_eq_atom(mk_strlen(x), mk_int(x_len))); } - std::string prefixStr = strValue.substr(0, prefixLen.get_unsigned()); + zstring prefixStr = strValue.extract(0, prefixLen.get_unsigned()); rational str_sub_prefix = str_len - prefixLen; - std::string suffixStr = strValue.substr(prefixLen.get_unsigned(), str_sub_prefix.get_unsigned()); + zstring suffixStr = strValue.extract(prefixLen.get_unsigned(), str_sub_prefix.get_unsigned()); expr_ref prefixAst(mk_string(prefixStr), mgr); expr_ref suffixAst(mk_string(suffixStr), mgr); expr_ref ax_l(mgr.mk_and(litems.size(), litems.c_ptr()), mgr); @@ -3878,9 +3907,9 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { unsigned option = 0; int pos = 1; - for (int i = 0; i <= (int) strValue.size(); i++) { - std::string part1Str = strValue.substr(0, i); - std::string part2Str = strValue.substr(i, strValue.size() - i); + for (unsigned int i = 0; i <= strValue.length(); i++) { + zstring part1Str = strValue.extract(0, i); + zstring part2Str = strValue.extract(i, strValue.length() - i); expr_ref cropStr(mk_string(part1Str), mgr); expr_ref suffixStr(mk_string(part2Str), mgr); expr_ref y_concat(mk_concat(suffixStr, n), mgr); @@ -3900,7 +3929,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr_ref option1(mk_and(and_item), mgr); arrangement_disjunction.push_back(option1); double priority; - if (i == (int)strValue.size()) { + if (i == strValue.length()) { priority = 0.5; } else { priority = 0.1; @@ -3974,8 +4003,8 @@ bool theory_str::is_concat_eq_type4(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if (m_strutil.is_string(v1_arg0) && (!m_strutil.is_string(v1_arg1)) - && m_strutil.is_string(v2_arg0) && (!m_strutil.is_string(v2_arg1))) { + if (u.str.is_string(v1_arg0) && (!u.str.is_string(v1_arg1)) + && u.str.is_string(v2_arg0) && (!u.str.is_string(v2_arg1))) { return true; } else { return false; @@ -3990,11 +4019,11 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4009,17 +4038,15 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { expr * str2Ast = v2_arg0; expr * n = v2_arg1; - const char *tmp = 0; - m_strutil.is_string(str1Ast, &tmp); - std::string str1Value(tmp); - m_strutil.is_string(str2Ast, &tmp); - std::string str2Value(tmp); + zstring str1Value, str2Value; + u.str.is_string(str1Ast, str1Value); + u.str.is_string(str2Ast, str2Value); - int str1Len = str1Value.length(); - int str2Len = str2Value.length(); + unsigned int str1Len = str1Value.length(); + unsigned int str2Len = str2Value.length(); int commonLen = (str1Len > str2Len) ? str2Len : str1Len; - if (str1Value.substr(0, commonLen) != str2Value.substr(0, commonLen)) { + if (str1Value.extract(0, commonLen) != str2Value.extract(0, commonLen)) { TRACE("t_str_detail", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) << " has no common prefix with " << mk_ismt2_pp(concatAst2, mgr) << std::endl;); expr_ref toNegate(mgr.mk_not(ctx.mk_eq_atom(concatAst1, concatAst2)), mgr); @@ -4027,7 +4054,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { return; } else { if (str1Len > str2Len) { - std::string deltaStr = str1Value.substr(str2Len, str1Len - str2Len); + zstring deltaStr = str1Value.extract(str2Len, str1Len - str2Len); expr_ref tmpAst(mk_concat(mk_string(deltaStr), y), mgr); if (!in_same_eqc(tmpAst, n)) { // break down option 4-1 @@ -4052,7 +4079,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { } } } else { - std::string deltaStr = str2Value.substr(str1Len, str2Len - str1Len); + zstring deltaStr = str2Value.extract(str1Len, str2Len - str1Len); expr_ref tmpAst(mk_concat(mk_string(deltaStr), n), mgr); if (!in_same_eqc(y, tmpAst)) { //break down option 4-3 @@ -4077,8 +4104,8 @@ bool theory_str::is_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if ((!m_strutil.is_string(v1_arg0)) && m_strutil.is_string(v1_arg1) - && (!m_strutil.is_string(v2_arg0)) && m_strutil.is_string(v2_arg1)) { + if ((!u.str.is_string(v1_arg0)) && u.str.is_string(v1_arg1) + && (!u.str.is_string(v2_arg0)) && u.str.is_string(v2_arg1)) { return true; } else { return false; @@ -4093,11 +4120,11 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4112,17 +4139,15 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr * m = v2_arg0; expr * str2Ast = v2_arg1; - const char *tmp = 0; - m_strutil.is_string(str1Ast, &tmp); - std::string str1Value(tmp); - m_strutil.is_string(str2Ast, &tmp); - std::string str2Value(tmp); + zstring str1Value, str2Value; + u.str.is_string(str1Ast, str1Value); + u.str.is_string(str2Ast, str2Value); - int str1Len = str1Value.length(); - int str2Len = str2Value.length(); + unsigned int str1Len = str1Value.length(); + unsigned int str2Len = str2Value.length(); int cLen = (str1Len > str2Len) ? str2Len : str1Len; - if (str1Value.substr(str1Len - cLen, cLen) != str2Value.substr(str2Len - cLen, cLen)) { + if (str1Value.extract(str1Len - cLen, cLen) != str2Value.extract(str2Len - cLen, cLen)) { TRACE("t_str_detail", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) << " has no common suffix with " << mk_ismt2_pp(concatAst2, mgr) << std::endl;); expr_ref toNegate(mgr.mk_not(ctx.mk_eq_atom(concatAst1, concatAst2)), mgr); @@ -4130,7 +4155,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { return; } else { if (str1Len > str2Len) { - std::string deltaStr = str1Value.substr(0, str1Len - str2Len); + zstring deltaStr = str1Value.extract(0, str1Len - str2Len); expr_ref x_deltaStr(mk_concat(x, mk_string(deltaStr)), mgr); if (!in_same_eqc(m, x_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr); @@ -4153,7 +4178,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { } } } else { - std::string deltaStr = str2Value.substr(0, str2Len - str1Len); + zstring deltaStr = str2Value.extract(0, str2Len - str1Len); expr_ref m_deltaStr(mk_concat(m, mk_string(deltaStr)), mgr); if (!in_same_eqc(x, m_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr); @@ -4177,11 +4202,11 @@ bool theory_str::is_concat_eq_type6(expr * concatAst1, expr * concatAst2) { expr * v2_arg0 = to_app(concatAst2)->get_arg(0); expr * v2_arg1 = to_app(concatAst2)->get_arg(1); - if (m_strutil.is_string(v1_arg0) && (!m_strutil.is_string(v1_arg1)) - && (!m_strutil.is_string(v2_arg0)) && m_strutil.is_string(v2_arg1)) { + if (u.str.is_string(v1_arg0) && (!u.str.is_string(v1_arg1)) + && (!u.str.is_string(v2_arg0)) && u.str.is_string(v2_arg1)) { return true; - } else if (m_strutil.is_string(v2_arg0) && (!m_strutil.is_string(v2_arg1)) - && (!m_strutil.is_string(v1_arg0)) && m_strutil.is_string(v1_arg1)) { + } else if (u.str.is_string(v2_arg0) && (!u.str.is_string(v2_arg1)) + && (!u.str.is_string(v1_arg0)) && u.str.is_string(v1_arg1)) { return true; } else { return false; @@ -4196,11 +4221,11 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); - if (!is_concat(to_app(concatAst1))) { + if (!u.str.is_concat(to_app(concatAst1))) { TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); return; } - if (!is_concat(to_app(concatAst2))) { + if (!u.str.is_concat(to_app(concatAst2))) { TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4216,7 +4241,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { expr * m = NULL; expr * str2Ast = NULL; - if (m_strutil.is_string(v1_arg0)) { + if (u.str.is_string(v1_arg0)) { str1Ast = v1_arg0; y = v1_arg1; m = v2_arg0; @@ -4228,14 +4253,12 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { str2Ast = v1_arg1; } - const char *tmp = 0; - m_strutil.is_string(str1Ast, &tmp); - std::string str1Value(tmp); - m_strutil.is_string(str2Ast, &tmp); - std::string str2Value(tmp); + zstring str1Value, str2Value; + u.str.is_string(str1Ast, str1Value); + u.str.is_string(str2Ast, str2Value); - int str1Len = str1Value.length(); - int str2Len = str2Value.length(); + unsigned int str1Len = str1Value.length(); + unsigned int str2Len = str2Value.length(); //---------------------------------------- //(a) |---str1---|----y----| @@ -4248,11 +4271,11 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { // |------m------|-str2-| //---------------------------------------- - std::list overlapLen; + std::list overlapLen; overlapLen.push_back(0); - for (int i = 1; i <= str1Len && i <= str2Len; i++) { - if (str1Value.substr(str1Len - i, i) == str2Value.substr(0, i)) + for (unsigned int i = 1; i <= str1Len && i <= str2Len; i++) { + if (str1Value.extract(str1Len - i, i) == str2Value.extract(0, i)) overlapLen.push_back(i); } @@ -4351,10 +4374,10 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { } } - for (std::list::iterator itor = overlapLen.begin(); itor != overlapLen.end(); itor++) { - int overLen = *itor; - std::string prefix = str1Value.substr(0, str1Len - overLen); - std::string suffix = str2Value.substr(overLen, str2Len - overLen); + for (std::list::iterator itor = overlapLen.begin(); itor != overlapLen.end(); itor++) { + unsigned int overLen = *itor; + zstring prefix = str1Value.extract(0, str1Len - overLen); + zstring suffix = str2Value.extract(overLen, str2Len - overLen); expr_ref_vector and_item(mgr); @@ -4408,12 +4431,13 @@ void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) if (!is_Unroll(to_app(unrollFunc))) { return; } - if (!m_strutil.is_string(constStr)) { + if (!u.str.is_string(constStr)) { return; } expr * funcInUnroll = to_app(unrollFunc)->get_arg(0); - std::string strValue = m_strutil.get_string_constant_value(constStr); + zstring strValue; + u.str.is_string(constStr, strValue); TRACE("t_str_detail", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl << "constStr: " << mk_pp(constStr, m) << std::endl;); @@ -4422,7 +4446,7 @@ void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) return; } - if (is_Str2Reg(to_app(funcInUnroll))) { + if (u.re.is_to_re(to_app(funcInUnroll))) { unroll_str2reg_constStr(unrollFunc, constStr); return; } @@ -4504,12 +4528,14 @@ void theory_str::unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr) { expr * strInStr2RegFunc = to_app(str2RegFunc)->get_arg(0); expr * oriCnt = to_app(unrollFunc)->get_arg(1); - std::string strValue = m_strutil.get_string_constant_value(eqConstStr); - std::string regStrValue = m_strutil.get_string_constant_value(strInStr2RegFunc); - int strLen = strValue.length(); - int regStrLen = regStrValue.length(); + zstring strValue; + u.str.is_string(eqConstStr, strValue); + zstring regStrValue; + u.str.is_string(strInStr2RegFunc, regStrValue); + unsigned int strLen = strValue.length(); + unsigned int regStrLen = regStrValue.length(); SASSERT(regStrLen != 0); // this should never occur -- the case for empty string is handled elsewhere - int cnt = strLen / regStrLen; + unsigned int cnt = strLen / regStrLen; expr_ref implyL(ctx.mk_eq_atom(unrollFunc, eqConstStr), m); expr_ref implyR1(ctx.mk_eq_atom(oriCnt, mk_int(cnt)), m); @@ -4537,7 +4563,7 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { expr * curr = n; do { - if (m_strutil.is_string(curr)) { + if (u.str.is_string(curr)) { hasEqcValue = true; return curr; } @@ -4649,14 +4675,16 @@ bool theory_str::get_len_value(expr* e, rational& val) { while (!todo.empty()) { expr* c = todo.back(); todo.pop_back(); - if (is_concat(to_app(c))) { + if (u.str.is_concat(to_app(c))) { e1 = to_app(c)->get_arg(0); e2 = to_app(c)->get_arg(1); todo.push_back(e1); todo.push_back(e2); } - else if (is_string(to_app(c))) { - int sl = m_strutil.get_string_constant_value(c).length(); + else if (u.str.is_string(to_app(c))) { + zstring tmp; + u.str.is_string(to_app(c), tmp); + unsigned int sl = tmp.length(); val += rational(sl); } else { @@ -4738,7 +4766,7 @@ expr * theory_str::collect_eq_nodes(expr * n, expr_ref_vector & eqcSet) { expr * ex = n; do { - if (m_strutil.is_string(to_app(ex))) { + if (u.str.is_string(to_app(ex))) { constStrNode = ex; } eqcSet.push_back(ex); @@ -4753,7 +4781,7 @@ expr * theory_str::collect_eq_nodes(expr * n, expr_ref_vector & eqcSet) { */ void theory_str::get_const_str_asts_in_node(expr * node, expr_ref_vector & astList) { ast_manager & m = get_manager(); - if (m_strutil.is_string(node)) { + if (u.str.is_string(node)) { astList.push_back(node); //} else if (getNodeType(t, node) == my_Z3_Func) { } else if (is_app(node)) { @@ -4806,7 +4834,8 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { if (strAst != constNode) { litems.push_back(ctx.mk_eq_atom(strAst, constNode)); } - std::string strConst = m_strutil.get_string_constant_value(constNode); + zstring strConst; + u.str.is_string(constNode, strConst); bool subStrHasEqcValue = false; expr * substrValue = get_eqc_value(substrAst, subStrHasEqcValue); if (substrValue != substrAst) { @@ -4815,11 +4844,12 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { if (subStrHasEqcValue) { // subStr has an eqc constant value - std::string subStrConst = m_strutil.get_string_constant_value(substrValue); + zstring subStrConst; + u.str.is_string(substrValue, subStrConst); - TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << std::endl;); + TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << "\n";); - if (strConst.find(subStrConst) != std::string::npos) { + if (strConst.contains(subStrConst)) { //implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx)); implyR = boolVar; } else { @@ -4845,8 +4875,9 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { get_const_str_asts_in_node(aConcat, constList); for (expr_ref_vector::iterator cstItor = constList.begin(); cstItor != constList.end(); cstItor++) { - std::string pieceStr = m_strutil.get_string_constant_value(*cstItor); - if (strConst.find(pieceStr) == std::string::npos) { + zstring pieceStr; + u.str.is_string(*cstItor, pieceStr); + if (strConst.contains(pieceStr)) { counterEgFound = true; if (aConcat != substrAst) { litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); @@ -4883,9 +4914,10 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { } if (strHasEqcValue) { - std::string strConst = m_strutil.get_string_constant_value(strValue); - std::string subStrConst = m_strutil.get_string_constant_value(constNode); - if (strConst.find(subStrConst) != std::string::npos) { + zstring strConst, subStrConst; + u.str.is_string(strValue, strConst); + u.str.is_string(constNode, subStrConst); + if (strConst.contains(subStrConst)) { //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_true(ctx)); implyR = boolVar; } else { @@ -4941,19 +4973,21 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE if (strValue != strAst) { litems.push_back(ctx.mk_eq_atom(strAst, strValue)); } - std::string strConst = m_strutil.get_string_constant_value(strValue); + zstring strConst; + u.str.is_string(strValue, strConst); // iterate eqc (also eqc-to-be) of substr for (expr_ref_vector::iterator itAst = willEqClass.begin(); itAst != willEqClass.end(); itAst++) { bool counterEgFound = false; - if (is_concat(to_app(*itAst))) { + if (u.str.is_concat(to_app(*itAst))) { expr_ref_vector constList(m); // get constant strings in concat app * aConcat = to_app(*itAst); get_const_str_asts_in_node(aConcat, constList); for (expr_ref_vector::iterator cstItor = constList.begin(); cstItor != constList.end(); cstItor++) { - std::string pieceStr = m_strutil.get_string_constant_value(*cstItor); - if (strConst.find(pieceStr) == std::string::npos) { + zstring pieceStr; + u.str.is_string(*cstItor, pieceStr); + if (!strConst.contains(pieceStr)) { TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;); counterEgFound = true; if (aConcat != substrAst) { @@ -5045,18 +5079,19 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { litems1.push_back(ctx.mk_eq_atom(subAst2, subValue2)); } - std::string subConst1 = m_strutil.get_string_constant_value(subValue1); - std::string subConst2 = m_strutil.get_string_constant_value(subValue2); + zstring subConst1, subConst2; + u.str.is_string(subValue1, subConst1); + u.str.is_string(subValue2, subConst2); expr_ref implyR(m); if (subConst1 == subConst2) { // key1.first = key2.first /\ key1.second = key2.second // ==> (containPairBoolMap[key1] = containPairBoolMap[key2]) implyR = ctx.mk_eq_atom(contain_pair_bool_map[key1], contain_pair_bool_map[key2]); - } else if (subConst1.find(subConst2) != std::string::npos) { + } else if (subConst1.contains(subConst2)) { // key1.first = key2.first /\ Contains(key1.second, key2.second) // ==> (containPairBoolMap[key1] --> containPairBoolMap[key2]) implyR = rewrite_implication(contain_pair_bool_map[key1], contain_pair_bool_map[key2]); - } else if (subConst2.find(subConst1) != std::string::npos) { + } else if (subConst2.contains(subConst1)) { // key1.first = key2.first /\ Contains(key2.second, key1.second) // ==> (containPairBoolMap[key2] --> containPairBoolMap[key1]) implyR = rewrite_implication(contain_pair_bool_map[key2], contain_pair_bool_map[key1]); @@ -5191,19 +5226,20 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { litems1.push_back(ctx.mk_eq_atom(str2, strVal2)); } - std::string const1 = m_strutil.get_string_constant_value(strVal1); - std::string const2 = m_strutil.get_string_constant_value(strVal2); + zstring const1, const2; + u.str.is_string(strVal1, const1); + u.str.is_string(strVal2, const2); expr_ref implyR(m); if (const1 == const2) { // key1.second = key2.second /\ key1.first = key2.first // ==> (containPairBoolMap[key1] = containPairBoolMap[key2]) implyR = ctx.mk_eq_atom(contain_pair_bool_map[key1], contain_pair_bool_map[key2]); - } else if (const1.find(const2) != std::string::npos) { + } else if (const1.contains(const2)) { // key1.second = key2.second /\ Contains(key1.first, key2.first) // ==> (containPairBoolMap[key2] --> containPairBoolMap[key1]) implyR = rewrite_implication(contain_pair_bool_map[key2], contain_pair_bool_map[key1]); - } else if (const2.find(const1) != std::string::npos) { + } else if (const2.contains(const1)) { // key1.first = key2.first /\ Contains(key2.first, key1.first) // ==> (containPairBoolMap[key1] --> containPairBoolMap[key2]) implyR = rewrite_implication(contain_pair_bool_map[key1], contain_pair_bool_map[key2]); @@ -5398,7 +5434,7 @@ void theory_str::check_contain_in_new_eq(expr * n1, expr * n2) { expr * theory_str::dealias_node(expr * node, std::map & varAliasMap, std::map & concatAliasMap) { if (variable_set.find(node) != variable_set.end()) { return get_alias_index_ast(varAliasMap, node); - } else if (is_concat(to_app(node))) { + } else if (u.str.is_concat(to_app(node))) { return get_alias_index_ast(concatAliasMap, node); } return node; @@ -5427,13 +5463,13 @@ void theory_str::get_grounded_concats(expr* node, std::map & varAl ast_manager & m = get_manager(); // const strings: node is de-aliased - if (m_strutil.is_string(node)) { + if (u.str.is_string(node)) { std::vector concatNodes; concatNodes.push_back(node); groundedMap[node][concatNodes].clear(); // no condition } // Concat functions - else if (is_concat(to_app(node))) { + else if (u.str.is_concat(to_app(node))) { // if "node" equals to a constant string, thenjust push the constant into the concat vector // Again "node" has been de-aliased at the very beginning if (concatConstMap.find(node) != concatConstMap.end()) { @@ -5461,7 +5497,7 @@ void theory_str::get_grounded_concats(expr* node, std::map & varAl ndVec.insert(ndVec.end(), arg0_grdItor->first.begin(), arg0_grdItor->first.end()); int arg0VecSize = arg0_grdItor->first.size(); int arg1VecSize = arg1_grdItor->first.size(); - if (arg0VecSize > 0 && arg1VecSize > 0 && m_strutil.is_string(arg0_grdItor->first[arg0VecSize - 1]) && m_strutil.is_string(arg1_grdItor->first[0])) { + if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) { ndVec.pop_back(); ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0])); for (int i = 1; i < arg1VecSize; i++) { @@ -5565,11 +5601,11 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector & strVec } if (subStrCnt == 1) { - if (m_strutil.is_string(subStrVec[0])) { - std::string subStrVal = m_strutil.get_string_constant_value(subStrVec[0]); + zstring subStrVal; + if (u.str.is_string(subStrVec[0]), subStrVal) { for (int i = 0; i < strCnt; i++) { - if (m_strutil.is_string(strVec[i])) { - std::string strVal = m_strutil.get_string_constant_value(strVec[i]); + zstring strVal; + if (u.str.is_string(strVec[i], strVal)) { if (strVal.find(subStrVal) != std::string::npos) { return true; } @@ -5589,12 +5625,12 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector & strVec // * constant: a suffix of a note in strVec[i] // * variable: bool firstNodesOK = true; - if (m_strutil.is_string(subStrVec[0])) { - std::string subStrHeadVal = m_strutil.get_string_constant_value(subStrVec[0]); - if (m_strutil.is_string(strVec[i])) { - std::string strHeadVal = m_strutil.get_string_constant_value(strVec[i]); - if (strHeadVal.size() >= subStrHeadVal.size()) { - std::string suffix = strHeadVal.substr(strHeadVal.size() - subStrHeadVal.size(), subStrHeadVal.size()); + zstring subStrHeadVal; + if (u.str.is_string(subStrVec[0], subStrHeadVal)) { + zstring strHeadVal; + if (u.str.is_string(strVec[i], strHeadVal)) { + if (strHeadVal.length() >= subStrHeadVal.length()) { + std::string suffix = strHeadVal.extract(strHeadVal.length() - subStrHeadVal.length(), subStrHeadVal.length()); if (suffix != subStrHeadVal) { firstNodesOK = false; } @@ -5625,12 +5661,12 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector & strVec // tail nodes int tailIdx = i + subStrCnt - 1; - if (m_strutil.is_string(subStrVec[subStrCnt - 1])) { - std::string subStrTailVal = m_strutil.get_string_constant_value(subStrVec[subStrCnt - 1]); - if (m_strutil.is_string(strVec[tailIdx])) { - std::string strTailVal = m_strutil.get_string_constant_value(strVec[tailIdx]); - if (strTailVal.size() >= subStrTailVal.size()) { - std::string prefix = strTailVal.substr(0, subStrTailVal.size()); + zstring subStrTailVal; + if (u.str.is_string(subStrVec[subStrCnt - 1], subStrTailVal)) { + zstring strTailVal; + if (u.str.is_string(strVec[tailIdx], strTailVal)) { + if (strTailVal.length() >= subStrTailVal.length()) { + zstring prefix = strTailVal.extract(0, subStrTailVal.length()); if (prefix == subStrTailVal) { return true; } else { @@ -5721,44 +5757,44 @@ void theory_str::compute_contains(std::map & varAliasMap, } } -bool theory_str::can_concat_eq_str(expr * concat, std::string str) { +bool theory_str::can_concat_eq_str(expr * concat, zstring& str) { int strLen = str.length(); - if (is_concat(to_app(concat))) { + if (u.str.is_concat(to_app(concat))) { ptr_vector args; get_nodes_in_concat(concat, args); expr * ml_node = args[0]; expr * mr_node = args[args.size() - 1]; - if (m_strutil.is_string(ml_node)) { - std::string ml_str = m_strutil.get_string_constant_value(ml_node); - int ml_len = ml_str.length(); + zstring ml_str; + if (u.str.is_string(ml_node, ml_str)) { + unsigned int ml_len = ml_str.length(); if (ml_len > strLen) { return false; } - int cLen = ml_len; - if (ml_str != str.substr(0, cLen)) { + unsigned int cLen = ml_len; + if (ml_str != str.extract(0, cLen)) { return false; } } - if (m_strutil.is_string(mr_node)) { - std::string mr_str = m_strutil.get_string_constant_value(mr_node); - int mr_len = mr_str.length(); + zstring mr_str; + if (u.str.is_string(mr_node, mr_str)) { + unsigned int mr_len = mr_str.length(); if (mr_len > strLen) { return false; } - int cLen = mr_len; - if (mr_str != str.substr(strLen - cLen, cLen)) { + unsigned int cLen = mr_len; + if (mr_str != str.extract(strLen - cLen, cLen)) { return false; } } - int sumLen = 0; + unsigned int sumLen = 0; for (unsigned int i = 0 ; i < args.size() ; i++) { expr * oneArg = args[i]; - if (m_strutil.is_string(oneArg)) { - std::string arg_str = m_strutil.get_string_constant_value(oneArg); - if (str.find(arg_str) == std::string::npos) { + zstring arg_str; + if (u.str.is_string(oneArg, arg_str)) { + if (str.contains(arg_str)) { return false; } sumLen += arg_str.length(); @@ -5773,17 +5809,16 @@ bool theory_str::can_concat_eq_str(expr * concat, std::string str) { } bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) { - if (is_concat(to_app(concat1)) && is_concat(to_app(concat2))) { + if (u.str.is_concat(to_app(concat1)) && u.str.is_concat(to_app(concat2))) { { // Suppose concat1 = (Concat X Y) and concat2 = (Concat M N). expr * concat1_mostL = getMostLeftNodeInConcat(concat1); expr * concat2_mostL = getMostLeftNodeInConcat(concat2); // if both X and M are constant strings, check whether they have the same prefix - if (m_strutil.is_string(concat1_mostL) && m_strutil.is_string(concat2_mostL)) { - std::string concat1_mostL_str = m_strutil.get_string_constant_value(concat1_mostL); - std::string concat2_mostL_str = m_strutil.get_string_constant_value(concat2_mostL); - int cLen = std::min(concat1_mostL_str.length(), concat2_mostL_str.length()); - if (concat1_mostL_str.substr(0, cLen) != concat2_mostL_str.substr(0, cLen)) { + zstring concat1_mostL_str, concat2_mostL_str; + if (u.str.is_string(concat1_mostL, concat1_mostL_str) && u.str.is_string(concat2_mostL, concat2_mostL_str)) { + unsigned int cLen = std::min(concat1_mostL_str.length(), concat2_mostL_str.length()); + if (concat1_mostL_str.extract(0, cLen) != concat2_mostL_str.extract(0, cLen)) { return false; } } @@ -5793,12 +5828,11 @@ bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) { // Similarly, if both Y and N are constant strings, check whether they have the same suffix expr * concat1_mostR = getMostRightNodeInConcat(concat1); expr * concat2_mostR = getMostRightNodeInConcat(concat2); - if (m_strutil.is_string(concat1_mostR) && m_strutil.is_string(concat2_mostR)) { - std::string concat1_mostR_str = m_strutil.get_string_constant_value(concat1_mostR); - std::string concat2_mostR_str = m_strutil.get_string_constant_value(concat2_mostR); - int cLen = std::min(concat1_mostR_str.length(), concat2_mostR_str.length()); - if (concat1_mostR_str.substr(concat1_mostR_str.length() - cLen, cLen) != - concat2_mostR_str.substr(concat2_mostR_str.length() - cLen, cLen)) { + zstring concat1_mostR_str, concat2_mostR_str; + if (u.str.is_string(concat1_mostR, concat1_mostR_str) && u.str.is_string(concat2_mostR, concat2_mostR_str)) { + unsigned int cLen = std::min(concat1_mostR_str.length(), concat2_mostR_str.length()); + if (concat1_mostR_str.extract(concat1_mostR_str.length() - cLen, cLen) != + concat2_mostR_str.extract(concat2_mostR_str.length() - cLen, cLen)) { return false; } } @@ -5817,31 +5851,29 @@ bool theory_str::can_two_nodes_eq(expr * n1, expr * n2) { app * n2_curr = to_app(n2); // case 0: n1_curr is const string, n2_curr is const string - if (is_string(n1_curr) && is_string(n2_curr)) { + if (u.str.is_string(n1_curr) && u.str.is_string(n2_curr)) { if (n1_curr != n2_curr) { return false; } } // case 1: n1_curr is concat, n2_curr is const string - else if (is_concat(n1_curr) && is_string(n2_curr)) { - const char * tmp = 0; - m_strutil.is_string(n2_curr, & tmp); - std::string n2_curr_str(tmp); + else if (u.str.is_concat(n1_curr) && u.str.is_string(n2_curr)) { + zstring n2_curr_str; + u.str.is_string(n2_curr, n2_curr_str); if (!can_concat_eq_str(n1_curr, n2_curr_str)) { return false; } } // case 2: n2_curr is concat, n1_curr is const string - else if (is_concat(n2_curr) && is_string(n1_curr)) { - const char * tmp = 0; - m_strutil.is_string(n1_curr, & tmp); - std::string n1_curr_str(tmp); + else if (u.str.is_concat(n2_curr) && u.str.is_string(n1_curr)) { + zstring n1_curr_str; + u.str.is_string(n1_curr, n1_curr_str); if (!can_concat_eq_str(n2_curr, n1_curr_str)) { return false; } } // case 3: both are concats - else if (is_concat(n1_curr) && is_concat(n2_curr)) { + else if (u.str.is_concat(n1_curr) && u.str.is_concat(n2_curr)) { if (!can_concat_eq_concat(n1_curr, n2_curr)) { return false; } @@ -5857,9 +5889,11 @@ bool theory_str::check_length_const_string(expr * n1, expr * constStr) { ast_manager & mgr = get_manager(); context & ctx = get_context(); - rational strLen((unsigned) (m_strutil.get_string_constant_value(constStr).length())); + zstring tmp; + u.str.is_string(constStr, tmp); + rational strLen(tmp.length()); - if (is_concat(to_app(n1))) { + if (u.str.is_concat(to_app(n1))) { ptr_vector args; expr_ref_vector items(mgr); @@ -5870,7 +5904,7 @@ bool theory_str::check_length_const_string(expr * n1, expr * constStr) { rational argLen; bool argLen_exists = get_len_value(args[i], argLen); if (argLen_exists) { - if (!m_strutil.is_string(args[i])) { + if (!u.str.is_string(args[i])) { items.push_back(ctx.mk_eq_atom(mk_strlen(args[i]), mk_int(argLen))); } TRACE("t_str_detail", tout << "concat arg: " << mk_pp(args[i], mgr) << " has len = " << argLen.to_string() << std::endl;); @@ -5926,7 +5960,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) { bool argLen_exists = get_len_value(oneArg, argLen); if (argLen_exists) { sum1 += argLen; - if (!m_strutil.is_string(oneArg)) { + if (!u.str.is_string(oneArg)) { items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen))); } } else { @@ -5940,7 +5974,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) { bool argLen_exists = get_len_value(oneArg, argLen); if (argLen_exists) { sum2 += argLen; - if (!m_strutil.is_string(oneArg)) { + if (!u.str.is_string(oneArg)) { items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen))); } } else { @@ -5993,7 +6027,7 @@ bool theory_str::check_length_concat_var(expr * concat, expr * var) { rational argLen; bool argLen_exists = get_len_value(oneArg, argLen); if (argLen_exists) { - if (!m_strutil.is_string(oneArg) && !argLen.is_zero()) { + if (!u.str.is_string(oneArg) && !argLen.is_zero()) { items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen))); } sumLen += argLen; @@ -6036,8 +6070,8 @@ bool theory_str::check_length_var_var(expr * var1, expr * var2) { // - note that these are different from the semantics in Z3str2 bool theory_str::check_length_eq_var_concat(expr * n1, expr * n2) { // n1 and n2 are not const string: either variable or concat - bool n1Concat = is_concat(to_app(n1)); - bool n2Concat = is_concat(to_app(n2)); + bool n1Concat = u.str.is_concat(to_app(n1)); + bool n2Concat = u.str.is_concat(to_app(n2)); if (n1Concat && n2Concat) { return check_length_concat_concat(n1, n2); } @@ -6059,12 +6093,12 @@ bool theory_str::check_length_eq_var_concat(expr * n1, expr * n2) { // returns false if an inconsistency is detected, or true if no inconsistencies were found // - note that these are different from the semantics of checkLengConsistency() in Z3str2 bool theory_str::check_length_consistency(expr * n1, expr * n2) { - if (m_strutil.is_string(n1) && m_strutil.is_string(n2)) { + if (u.str.is_string(n1) && u.str.is_string(n2)) { // consistency has already been checked in can_two_nodes_eq(). return true; - } else if (m_strutil.is_string(n1) && (!m_strutil.is_string(n2))) { + } else if (u.str.is_string(n1) && (!u.str.is_string(n2))) { return check_length_const_string(n2, n1); - } else if (m_strutil.is_string(n2) && (!m_strutil.is_string(n1))) { + } else if (u.str.is_string(n2) && (!u.str.is_string(n1))) { return check_length_const_string(n1, n2); } else { // n1 and n2 are vars or concats @@ -6082,7 +6116,7 @@ bool theory_str::check_concat_len_in_eqc(expr * concat) { expr * eqc_n = concat; do { - if (is_concat(to_app(eqc_n))) { + if (u.str.is_concat(to_app(eqc_n))) { rational unused; bool status = infer_len_concat(eqc_n, unused); if (status) { @@ -6114,13 +6148,15 @@ void theory_str::check_regex_in(expr * nn1, expr * nn2) { std::set::iterator strItor = regex_in_var_reg_str_map[*itor].begin(); for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) { std::string regStr = *strItor; - std::string constStrValue = m_strutil.get_string_constant_value(constStr); + zstring constStrValue; + u.str.is_string(constStr, constStrValue); std::pair key1 = std::make_pair(*itor, regStr); if (regex_in_bool_map.find(key1) != regex_in_bool_map.end()) { expr * boolVar = regex_in_bool_map[key1]; // actually the RegexIn term app * a_regexIn = to_app(boolVar); expr * regexTerm = a_regexIn->get_arg(1); + // TODO figure out regex NFA stuff if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) { TRACE("t_str_detail", tout << "regex_nfa_cache: cache miss" << std::endl;); regex_nfa_cache[regexTerm] = nfa(m_strutil, regexTerm); @@ -6159,16 +6195,14 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { TRACE("t_str_detail", tout << mk_ismt2_pp(concat, m) << " == " << mk_ismt2_pp(str, m) << std::endl;); - if (is_concat(to_app(concat)) && is_string(to_app(str))) { - const char * tmp = 0; - m_strutil.is_string(str, & tmp); - std::string const_str(tmp); + zstring const_str; + if (u.str.is_concat(to_app(concat)) && u.str.is_string(to_app(str), const_str)) { app * a_concat = to_app(concat); SASSERT(a_concat->get_num_args() == 2); expr * a1 = a_concat->get_arg(0); expr * a2 = a_concat->get_arg(1); - if (const_str == "") { + if (const_str.empty()) { TRACE("t_str", tout << "quick path: concat == \"\"" << std::endl;); // assert the following axiom: // ( (Concat a1 a2) == "" ) -> ( (a1 == "") AND (a2 == "") ) @@ -6211,26 +6245,22 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { if (newConcat == str) { return; } - if (!is_concat(to_app(newConcat))) { + if (!u.str.is_concat(to_app(newConcat))) { return; } if (arg1_has_eqc_value && arg2_has_eqc_value) { // Case 1: Concat(const, const) == const TRACE("t_str", tout << "Case 1: Concat(const, const) == const" << std::endl;); - const char * str1; - m_strutil.is_string(arg1, & str1); - std::string arg1_str(str1); + zstring arg1_str, arg2_str; + u.str.is_string(arg1, arg1_str); + u.str.is_string(arg2, arg2_str); - const char * str2; - m_strutil.is_string(arg2, & str2); - std::string arg2_str(str2); - - std::string result_str = arg1_str + arg2_str; + zstring result_str = arg1_str + arg2_str; if (result_str != const_str) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: \"" << arg1_str << "\" + \"" << arg2_str << - "\" != \"" << const_str << "\"" << std::endl;); + "\" != \"" << const_str << "\"\n"); expr_ref equality(ctx.mk_eq_atom(concat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6239,31 +6269,30 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } else if (!arg1_has_eqc_value && arg2_has_eqc_value) { // Case 2: Concat(var, const) == const TRACE("t_str", tout << "Case 2: Concat(var, const) == const" << std::endl;); - const char * str2; - m_strutil.is_string(arg2, & str2); - std::string arg2_str(str2); - int resultStrLen = const_str.length(); - int arg2StrLen = arg2_str.length(); + zstring arg2_str; + u.str.is_string(arg2, arg2_str); + unsigned int resultStrLen = const_str.length(); + unsigned int arg2StrLen = arg2_str.length(); if (resultStrLen < arg2StrLen) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: \"" << arg2_str << "\" is longer than \"" << const_str << "\"," - << " so cannot be concatenated with anything to form it" << std::endl;); + << " so cannot be concatenated with anything to form it\n"); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); return; } else { int varStrLen = resultStrLen - arg2StrLen; - std::string firstPart = const_str.substr(0, varStrLen); - std::string secondPart = const_str.substr(varStrLen, arg2StrLen); + zstring firstPart = const_str.extract(0, varStrLen); + zstring secondPart = const_str.extract(varStrLen, arg2StrLen); if (arg2_str != secondPart) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: " << "suffix of concatenation result expected \"" << secondPart << "\", " << "actually \"" << arg2_str << "\"" - << std::endl;); + << "\n"); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6279,31 +6308,30 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } else if (arg1_has_eqc_value && !arg2_has_eqc_value) { // Case 3: Concat(const, var) == const TRACE("t_str", tout << "Case 3: Concat(const, var) == const" << std::endl;); - const char * str1; - m_strutil.is_string(arg1, & str1); - std::string arg1_str(str1); - int resultStrLen = const_str.length(); - int arg1StrLen = arg1_str.length(); + zstring arg1_str; + u.str.is_string(arg1, arg1_str); + unsigned int resultStrLen = const_str.length(); + unsigned int arg1StrLen = arg1_str.length(); if (resultStrLen < arg1StrLen) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: \"" << arg1_str << "\" is longer than \"" << const_str << "\"," - << " so cannot be concatenated with anything to form it" << std::endl;); + << " so cannot be concatenated with anything to form it" << "\n";); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); return; } else { int varStrLen = resultStrLen - arg1StrLen; - std::string firstPart = const_str.substr(0, arg1StrLen); - std::string secondPart = const_str.substr(arg1StrLen, varStrLen); + zstring firstPart = const_str.extract(0, arg1StrLen); + zstring secondPart = const_str.extract(arg1StrLen, varStrLen); if (arg1_str != firstPart) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: " << "prefix of concatenation result expected \"" << secondPart << "\", " << "actually \"" << arg1_str << "\"" - << std::endl;); + << "\n";); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6327,7 +6355,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { if (arg1Len_exists || arg2Len_exists) { expr_ref ax_l1(ctx.mk_eq_atom(concat, str), m); expr_ref ax_l2(m); - std::string prefixStr, suffixStr; + zstring prefixStr, suffixStr; if (arg1Len_exists) { if (arg1Len.is_neg()) { TRACE("t_str_detail", tout << "length conflict: arg1Len = " << arg1Len << ", concatStrLen = " << concatStrLen << std::endl;); @@ -6341,9 +6369,9 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { return; } - prefixStr = const_str.substr(0, arg1Len.get_unsigned()); + prefixStr = const_str.extract(0, arg1Len.get_unsigned()); rational concat_minus_arg1 = concatStrLen - arg1Len; - suffixStr = const_str.substr(arg1Len.get_unsigned(), concat_minus_arg1.get_unsigned()); + suffixStr = const_str.extract(arg1Len.get_unsigned(), concat_minus_arg1.get_unsigned()); ax_l2 = ctx.mk_eq_atom(mk_strlen(arg1), mk_int(arg1Len)); } else { // arg2's length is available @@ -6360,17 +6388,17 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } rational concat_minus_arg2 = concatStrLen - arg2Len; - prefixStr = const_str.substr(0, concat_minus_arg2.get_unsigned()); - suffixStr = const_str.substr(concat_minus_arg2.get_unsigned(), arg2Len.get_unsigned()); + prefixStr = const_str.extract(0, concat_minus_arg2.get_unsigned()); + suffixStr = const_str.extract(concat_minus_arg2.get_unsigned(), arg2Len.get_unsigned()); ax_l2 = ctx.mk_eq_atom(mk_strlen(arg2), mk_int(arg2Len)); } // consistency check - if (is_concat(to_app(arg1)) && !can_concat_eq_str(arg1, prefixStr)) { + if (u.str.is_concat(to_app(arg1)) && !can_concat_eq_str(arg1, prefixStr)) { expr_ref ax_r(m.mk_not(ax_l2), m); assert_implication(ax_l1, ax_r); return; } - if (is_concat(to_app(arg2)) && !can_concat_eq_str(arg2, suffixStr)) { + if (u.str.is_concat(to_app(arg2)) && !can_concat_eq_str(arg2, suffixStr)) { expr_ref ax_r(m.mk_not(ax_l2), m); assert_implication(ax_l1, ax_r); return; @@ -6379,10 +6407,10 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { r_items.push_back(ctx.mk_eq_atom(arg1, mk_string(prefixStr))); r_items.push_back(ctx.mk_eq_atom(arg2, mk_string(suffixStr))); if (!arg1Len_exists) { - r_items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(prefixStr.size()))); + r_items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(prefixStr.length()))); } if (!arg2Len_exists) { - r_items.push_back(ctx.mk_eq_atom(mk_strlen(arg2), mk_int(suffixStr.size()))); + r_items.push_back(ctx.mk_eq_atom(mk_strlen(arg2), mk_int(suffixStr.length()))); } expr_ref lhs(m.mk_and(ax_l1, ax_l2), m); expr_ref rhs(mk_and(r_items), m); @@ -6456,13 +6484,13 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { for (int i = 0; i < concatStrLen + 1; ++i) { expr_ref_vector and_items(m); - std::string prefixStr = const_str.substr(0, i); - std::string suffixStr = const_str.substr(i, concatStrLen - i); + zstring prefixStr = const_str.extract(0, i); + zstring suffixStr = const_str.extract(i, concatStrLen - i); // skip invalid options - if (is_concat(to_app(arg1)) && !can_concat_eq_str(arg1, prefixStr)) { + if (u.str.is_concat(to_app(arg1)) && !can_concat_eq_str(arg1, prefixStr)) { continue; } - if (is_concat(to_app(arg2)) && !can_concat_eq_str(arg2, suffixStr)) { + if (u.str.is_concat(to_app(arg2)) && !can_concat_eq_str(arg2, suffixStr)) { continue; } @@ -6530,8 +6558,8 @@ expr_ref theory_str::set_up_finite_model_test(expr * lhs, expr * rhs) { } // make things easy for the core wrt. testvar - expr_ref t1(ctx.mk_eq_atom(testvar, m_strutil.mk_string("")), m); - expr_ref t_yes(ctx.mk_eq_atom(testvar, m_strutil.mk_string("yes")), m); + expr_ref t1(ctx.mk_eq_atom(testvar, u.str.mk_string("")), m); + expr_ref t_yes(ctx.mk_eq_atom(testvar, u.str.mk_string("yes")), m); expr_ref testvaraxiom(m.mk_or(t1, t_yes), m); assert_axiom(testvaraxiom); @@ -6544,8 +6572,8 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { context & ctx = get_context(); ast_manager & m = get_manager(); - if (!m_strutil.is_string(str)) return; - std::string s = m_strutil.get_string_constant_value(str); + zstring s; + if (!u.str.is_string(str, s)) return; if (s == "yes") { TRACE("t_str", tout << "start finite model test for " << mk_pp(testvar, m) << std::endl;); ptr_vector & vars = finite_model_test_varlists[testvar]; @@ -6642,7 +6670,7 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { for (rational l = v_lower_bound; l <= v_upper_bound; l += rational::one()) { std::string lStr = l.to_string(); - expr_ref str_indicator(m_strutil.mk_string(lStr), m); + expr_ref str_indicator(u.str.mk_string(lStr), m); expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); orList.push_back(or_expr); expr_ref and_expr(ctx.mk_eq_atom(or_expr, ctx.mk_eq_atom(vLengthExpr, m_autil.mk_numeral(l, true))), m); @@ -6661,7 +6689,7 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { } // (s == "yes") } -void theory_str::more_len_tests(expr * lenTester, std::string lenTesterValue) { +void theory_str::more_len_tests(expr * lenTester, zstring lenTesterValue) { ast_manager & m = get_manager(); if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; @@ -6673,7 +6701,7 @@ void theory_str::more_len_tests(expr * lenTester, std::string lenTesterValue) { } } -void theory_str::more_value_tests(expr * valTester, std::string valTesterValue) { +void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { ast_manager & m = get_manager(); expr * fVar = valueTester_fvar_map[valTester]; @@ -6689,7 +6717,8 @@ void theory_str::more_value_tests(expr * valTester, std::string valTesterValue) TRACE("t_str_binary_search", tout << "WARNING: length tester " << mk_pp(effectiveLenInd, m) << " at top of stack for " << mk_pp(fVar, m) << " has no EQC value" << std::endl;); } else { // safety check - std::string effectiveLenIndiStr = m_strutil.get_string_constant_value(len_indicator_value); + zstring effectiveLenIndiStr; + u.str.is_string(len_indicator_value, effectiveLenIndiStr); if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { TRACE("t_str_binary_search", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); UNREACHABLE(); @@ -6704,13 +6733,14 @@ void theory_str::more_value_tests(expr * valTester, std::string valTesterValue) int lenTesterCount = fvar_lenTester_map[fVar].size(); expr * effectiveLenInd = NULL; - std::string effectiveLenIndiStr = ""; + zstring effectiveLenIndiStr = ""; for (int i = 0; i < lenTesterCount; ++i) { expr * len_indicator_pre = fvar_lenTester_map[fVar][i]; bool indicatorHasEqcValue = false; expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); if (indicatorHasEqcValue) { - std::string len_pIndiStr = m_strutil.get_string_constant_value(len_indicator_value); + zstring len_pIndiStr; + u.str.is_string(len_indicator_value, len_pIndiStr); if (len_pIndiStr != "more") { effectiveLenInd = len_indicator_pre; effectiveLenIndiStr = len_pIndiStr; @@ -6728,14 +6758,13 @@ void theory_str::more_value_tests(expr * valTester, std::string valTesterValue) bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { ast_manager & m = get_manager(); - - if (internal_lenTest_vars.contains(nn1) && m_strutil.is_string(nn2)) { + zstring nn2_str; + if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { TRACE("t_str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m) << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); - more_len_tests(nn1, m_strutil.get_string_constant_value(nn2)); + more_len_tests(nn1, nn2_str); return true; - } else if (internal_valTest_vars.contains(nn1) && m_strutil.is_string(nn2)) { - std::string nn2_str = m_strutil.get_string_constant_value(nn2); + } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { if (nn2_str == "more") { TRACE("t_str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m) << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); @@ -6755,7 +6784,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { // both terms must be of sort String sort * lhs_sort = m.get_sort(lhs); sort * rhs_sort = m.get_sort(rhs); - sort * str_sort = m.mk_sort(get_family_id(), STRING_SORT); + sort * str_sort = u.str.mk_string_sort(); if (lhs_sort != str_sort || rhs_sort != str_sort) { TRACE("t_str_detail", tout << "skip equality: not String sort" << std::endl;); @@ -6776,7 +6805,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { return; } - if (is_concat(to_app(lhs)) && is_concat(to_app(rhs))) { + if (u.str.is_concat(to_app(lhs)) && u.str.is_concat(to_app(rhs))) { bool nn1HasEqcValue = false; bool nn2HasEqcValue = false; expr * nn1_value = get_eqc_value(lhs, nn1HasEqcValue); @@ -6993,7 +7022,7 @@ void theory_str::set_up_axioms(expr * ex) { context & ctx = get_context(); sort * ex_sort = m.get_sort(ex); - sort * str_sort = m.mk_sort(get_family_id(), STRING_SORT); + sort * str_sort = u.str.mk_string_sort(); sort * bool_sort = m.mk_bool_sort(); family_id m_arith_fid = m.mk_family_id("arith"); @@ -7011,23 +7040,23 @@ void theory_str::set_up_axioms(expr * ex) { if (is_app(ex)) { app * ap = to_app(ex); - if (is_concat(ap)) { + if (u.str.is_concat(ap)) { // if ex is a concat, set up concat axioms later m_concat_axiom_todo.push_back(n); // we also want to check whether we can eval this concat, // in case the rewriter did not totally finish with this term m_concat_eval_todo.push_back(n); - } else if (is_strlen(ap)) { + } else if (u.str.is_length(ap)) { // if the argument is a variable, // keep track of this for later, we'll need it during model gen expr * var = ap->get_arg(0); app * aVar = to_app(var); - if (aVar->get_num_args() == 0 && !is_string(aVar)) { + if (aVar->get_num_args() == 0 && !u.str.is_string(aVar)) { input_var_in_len.insert(var); } - } else if (is_CharAt(ap) || is_Substr(ap) || is_Replace(ap)) { + } else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) { m_library_aware_axiom_todo.push_back(n); - } else if (ap->get_num_args() == 0 && !is_string(ap)) { + } else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) { // if ex is a variable, add it to our list of variables TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); variable_set.insert(ex); @@ -7049,7 +7078,7 @@ void theory_str::set_up_axioms(expr * ex) { if (is_app(ex)) { app * ap = to_app(ex); - if (is_StartsWith(ap) || is_EndsWith(ap) || is_Contains(ap) || is_RegexIn(ap)) { + if (u.str.is_prefix(ap) || u.str.is_suffix(ap) || u.str.is_contains(ap) || u.str.is_in_re(ap)) { m_library_aware_axiom_todo.push_back(n); } } @@ -7068,9 +7097,10 @@ void theory_str::set_up_axioms(expr * ex) { if (is_app(ex)) { app * ap = to_app(ex); - if (is_Indexof(ap) || is_Indexof2(ap) || is_LastIndexof(ap)) { + // TODO indexof2/lastindexof + if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) { m_library_aware_axiom_todo.push_back(n); - } else if (is_str_to_int(ap) || is_int_to_str(ap)) { + } else if (u.str.is_stoi(ap) || u.str.is_itos(ap)) { string_int_conversion_terms.push_back(ap); m_library_aware_axiom_todo.push_back(n); } @@ -7200,12 +7230,12 @@ void theory_str::recursive_check_variable_scope(expr * ex) { if (a->get_num_args() == 0) { // we only care about string variables sort * s = m.get_sort(ex); - sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT); + sort * string_sort = u.str.mk_string_sort(); if (s != string_sort) { return; } // base case: string constant / var - if (m_strutil.is_string(a)) { + if (u.str.is_string(a)) { return; } else { // assume var @@ -7331,10 +7361,10 @@ void theory_str::classify_ast_by_type(expr * node, std::map & varMap // check whether the node is a function that we want to inspect else if (is_app(node)) { app * aNode = to_app(node); - if (is_strlen(aNode)) { + if (u.str.is_length(aNode)) { // Length return; - } else if (is_concat(aNode)) { + } else if (u.str.is_concat(aNode)) { expr * arg0 = aNode->get_arg(0); expr * arg1 = aNode->get_arg(1); bool arg0HasEq = false; @@ -7343,10 +7373,13 @@ void theory_str::classify_ast_by_type(expr * node, std::map & varMap expr * arg1Val = get_eqc_value(arg1, arg1HasEq); int canskip = 0; - if (arg0HasEq && m_strutil.get_string_constant_value(arg0Val).empty()) { + zstring tmp; + u.str.is_string(arg0Val, tmp); + if (arg0HasEq && tmp.empty()) { canskip = 1; } - if (canskip == 0 && arg1HasEq && m_strutil.get_string_constant_value(arg1Val).empty()) { + u.str.is_string(arg1Val, tmp); + if (canskip == 0 && arg1HasEq && tmp.empty()) { canskip = 1; } if (canskip == 0 && concatMap.find(node) == concatMap.end()) { @@ -7402,7 +7435,7 @@ inline expr * theory_str::get_alias_index_ast(std::map & aliasInde inline expr * theory_str::getMostLeftNodeInConcat(expr * node) { app * aNode = to_app(node); - if (!is_concat(aNode)) { + if (!u.str.is_concat(aNode)) { return node; } else { expr * concatArgL = aNode->get_arg(0); @@ -7412,7 +7445,7 @@ inline expr * theory_str::getMostLeftNodeInConcat(expr * node) { inline expr * theory_str::getMostRightNodeInConcat(expr * node) { app * aNode = to_app(node); - if (!is_concat(aNode)) { + if (!u.str.is_concat(aNode)) { return node; } else { expr * concatArgR = aNode->get_arg(1); @@ -7556,7 +7589,7 @@ void theory_str::trace_ctx_dep(std::ofstream & tout, enode * e_curr_end = e_curr; do { app * curr = e_curr->get_owner(); - if (is_concat(curr)) { + if (u.str.is_concat(curr)) { tout << " >>> " << mk_pp(curr, mgr) << std::endl; } e_curr = e_curr->get_next(); @@ -7691,7 +7724,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::mapget_arg(0); expr * arg1 = aCurr->get_arg(1); bool arg0HasEqcValue = false; @@ -7701,18 +7734,18 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map & strVarMap, std::mapfirst; do { - if (is_concat(to_app(curr))) { + if (u.str.is_concat(to_app(curr))) { if (aRoot == NULL) { aRoot = curr; } else { @@ -7780,7 +7813,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map & strVarMap, std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); itor1++) { expr * concatNode = itor1->first; expr * mLNode = getMostLeftNodeInConcat(concatNode); - const char * strval; - if (m_strutil.is_string(to_app(mLNode), & strval)) { - if (mLConst == NULL && strcmp(strval, "") != 0) { + zstring strval; + if (u.str.is_string(to_app(mLNode), strval)) { + if (mLConst == NULL && strval.empty()) { mLConst = mLNode; } } else { @@ -7913,8 +7946,8 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map integer value < 0 if (Sval.empty()) { // ignore this. we should already assert the axiom for what happens when the string is "" @@ -8228,7 +8262,7 @@ bool theory_str::finalcheck_int2str(app * a) { rational ten(10); bool conversionOK = true; for (unsigned i = 0; i < Sval.length(); ++i) { - char digit = Sval.at(i); + char digit = (int)Sval[i]; if (isdigit((int)digit)) { std::string sDigit(1, digit); int val = atoi(sDigit.c_str()); @@ -8272,11 +8306,11 @@ void theory_str::collect_var_concat(expr * node, std::set & varSet, std:: } else if (is_app(node)) { app * aNode = to_app(node); - if (is_strlen(aNode)) { + if (u.str.is_length(aNode)) { // Length return; } - if (is_concat(aNode)) { + if (u.str.is_concat(aNode)) { expr * arg0 = aNode->get_arg(0); expr * arg1 = aNode->get_arg(1); if (concatSet.find(node) == concatSet.end()) { @@ -8406,7 +8440,7 @@ bool theory_str::propagate_length(std::set & varSet, std::set & co void theory_str::get_unique_non_concat_nodes(expr * node, std::set & argSet) { app * a_node = to_app(node); - if (!is_concat(a_node)) { + if (!u.str.is_concat(a_node)) { argSet.insert(node); return; } else { @@ -8447,7 +8481,7 @@ final_check_status theory_str::final_check_eh() { for (std::set::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) { enode * e = *it; app * a = e->get_owner(); - if (!(is_sort_of(m.get_sort(a), m_strutil.get_fid(), STRING_SORT))) { + if (!(m.get_sort(a) == u.str.mk_string_sort())) { TRACE("t_str_detail", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;); } else { TRACE("t_str_detail", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;); @@ -8516,9 +8550,10 @@ final_check_status theory_str::final_check_eh() { if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) { TRACE("t_str_detail", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;); - std::string lhsString = m_strutil.get_string_constant_value(concat_lhs_str); - std::string rhsString = m_strutil.get_string_constant_value(concat_rhs_str); - std::string concatString = lhsString + rhsString; + zstring lhsString, rhsString; + u.str.is_string(concat_lhs_str, lhsString); + u.str.is_string(concat_rhs_str, rhsString); + zstring concatString = lhsString + rhsString; expr_ref lhs1(ctx.mk_eq_atom(concat_lhs, concat_lhs_str), m); expr_ref lhs2(ctx.mk_eq_atom(concat_rhs, concat_rhs_str), m); expr_ref lhs(m.mk_and(lhs1, lhs2), m); @@ -8584,12 +8619,12 @@ final_check_status theory_str::final_check_eh() { bool addedStrIntAxioms = false; for (unsigned i = 0; i < string_int_conversion_terms.size(); ++i) { app * ex = to_app(string_int_conversion_terms[i].get()); - if (is_str_to_int(ex)) { + if (u.str.is_stoi(ex)) { bool axiomAdd = finalcheck_str2int(ex); if (axiomAdd) { addedStrIntAxioms = true; } - } else if (is_int_to_str(ex)) { + } else if (u.str.is_itos(ex)) { bool axiomAdd = finalcheck_int2str(ex); if (axiomAdd) { addedStrIntAxioms = true; @@ -8664,7 +8699,7 @@ final_check_status theory_str::final_check_eh() { expr * unroll = urItor->first; expr * curr = unroll; do { - if (is_concat(to_app(curr))) { + if (u.str.is_concat(to_app(curr))) { concatEqUnrollsMap[curr].insert(unroll); concatEqUnrollsMap[curr].insert(unrollGroup_map[unroll].begin(), unrollGroup_map[unroll].end()); } @@ -8690,7 +8725,7 @@ final_check_status theory_str::final_check_eh() { } else { fvUnrollSet.insert(concatArg1); } - } else if (is_concat(to_app(concatArg1))) { + } else if (u.str.is_concat(to_app(concatArg1))) { if (concatEqUnrollsMap.find(concatArg1) == concatEqUnrollsMap.end()) { arg1Bounded = true; } @@ -8702,7 +8737,7 @@ final_check_status theory_str::final_check_eh() { } else { fvUnrollSet.insert(concatArg2); } - } else if (is_concat(to_app(concatArg2))) { + } else if (u.str.is_concat(to_app(concatArg2))) { if (concatEqUnrollsMap.find(concatArg2) == concatEqUnrollsMap.end()) { arg2Bounded = true; } @@ -8794,10 +8829,11 @@ final_check_status theory_str::final_check_eh() { return FC_CONTINUE; // since by this point we've added axioms } -inline std::string int_to_string(int i) { +inline zstring int_to_string(int i) { std::stringstream ss; ss << i; - return ss.str(); + std::string str = ss.str(); + return zstring(str.c_str()); } inline std::string longlong_to_string(long long i) { @@ -8823,11 +8859,11 @@ void theory_str::print_value_tester_list(svector > & teste ); } -std::string theory_str::gen_val_string(int len, int_vector & encoding) { +zstring theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); SASSERT(char_set != NULL); - std::string re = std::string(len, char_set[0]); + zstring re(len, (int) char_set[0]); for (int i = 0; i < (int) encoding.size() - 1; i++) { int idx = encoding[i]; re[len - 1 - i] = char_set[idx]; @@ -8876,7 +8912,7 @@ bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { } expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, - std::string lenStr, int tries) { + zstring lenStr, int tries) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -8894,7 +8930,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * // {0, 0, 1} // the last item "1" shows this is not a valid encoding, and we have covered all space // ---------------------------------------------------------------------------------------- - int len = atoi(lenStr.c_str()); + int len = atoi(lenStr.encode().c_str()); bool coverAll = false; svector options; int_vector base; @@ -8903,8 +8939,8 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * << "freeVar = " << mk_ismt2_pp(freeVar, m) << std::endl << "len_indicator = " << mk_ismt2_pp(len_indicator, m) << std::endl << "val_indicator = " << mk_ismt2_pp(val_indicator, m) << std::endl - << "lenstr = " << lenStr << std::endl - << "tries = " << tries << std::endl; + << "lenstr = " << lenStr << "\n" + << "tries = " << tries << "\n"; if (m_params.m_AggressiveValueTesting) { tout << "note: aggressive value testing is enabled" << std::endl; } @@ -8953,7 +8989,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * ctx.force_phase(l); } - std::string aStr = gen_val_string(len, options[i - l]); + zstring aStr = gen_val_string(len, options[i - l]); expr * strAst; if (m_params.m_UseFastValueTesterCache) { if (!valueTesterCache.find(aStr, strAst)) { @@ -8996,7 +9032,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * // Should add ($$_len_x_j = 16) /\ ($$_val_x_16_i = "more") // --------------------------------------- andList.reset(); - andList.push_back(m.mk_eq(len_indicator, mk_string(lenStr.c_str()))); + andList.push_back(m.mk_eq(len_indicator, mk_string(lenStr))); for (int i = 0; i < tries; i++) { expr * vTester = fvar_valueTester_map[freeVar][len][i].second; if (vTester != val_indicator) @@ -9019,10 +9055,10 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * } expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, - std::string len_valueStr, expr * valTesterInCbEq, std::string valTesterValueStr) { + zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr) { ast_manager & m = get_manager(); - int len = atoi(len_valueStr.c_str()); + int len = atoi(len_valueStr.encode().c_str()); // check whether any value tester is actually in scope TRACE("t_str_detail", tout << "checking scope of previous value testers" << std::endl;); @@ -9117,7 +9153,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect TRACE("t_str_detail", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); app * regexFuncDecl = to_app(regex); - if (is_Str2Reg(regexFuncDecl)) { + if (u.re.is_to_re(regexFuncDecl)) { // --------------------------------------------------------- // var \in Str2Reg(s1) // ==> @@ -9129,7 +9165,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect return; } // RegexUnion - else if (is_RegexUnion(regexFuncDecl)) { + else if (u.re.is_union(regexFuncDecl)) { // --------------------------------------------------------- // var \in RegexUnion(r1, r2) // ==> @@ -9156,7 +9192,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect return; } // RegexConcat - else if (is_RegexConcat(regexFuncDecl)) { + else if (u.re.is_concat(regexFuncDecl)) { // --------------------------------------------------------- // var \in RegexConcat(r1, r2) // ==> @@ -9177,7 +9213,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect return; } // Unroll - else if (is_RegexStar(regexFuncDecl)) { + else if (u.re.is_star(regexFuncDecl)) { // --------------------------------------------------------- // var \in Star(r1) // ==> @@ -9190,6 +9226,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(unrollFunc))); return; } else { + get_manager().raise_exception("unrecognized regex operator"); UNREACHABLE(); } } @@ -9291,8 +9328,8 @@ static int computeLCM(int a, int b) { return temp ? (a / temp * b) : 0; } -static std::string get_unrolled_string(std::string core, int count) { - std::string res = ""; +static zstring get_unrolled_string(zstring core, int count) { + zstring res(""); for (int i = 0; i < count; i++) { res += core; } @@ -9306,11 +9343,12 @@ expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls int lcm = 1; int coreValueCount = 0; expr * oneUnroll = NULL; - std::string oneCoreStr = ""; + zstring oneCoreStr(""); for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { expr * str2RegFunc = to_app(*itor)->get_arg(0); expr * coreVal = to_app(str2RegFunc)->get_arg(0); - std::string coreStr = m_strutil.get_string_constant_value(coreVal); + zstring coreStr; + u.str.is_string(coreVal, coreStr); if (oneUnroll == NULL) { oneUnroll = *itor; oneCoreStr = coreStr; @@ -9322,13 +9360,14 @@ expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls // bool canHaveNonEmptyAssign = true; expr_ref_vector litems(mgr); - std::string lcmStr = get_unrolled_string(oneCoreStr, (lcm / oneCoreStr.length())); + zstring lcmStr = get_unrolled_string(oneCoreStr, (lcm / oneCoreStr.length())); for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { expr * str2RegFunc = to_app(*itor)->get_arg(0); expr * coreVal = to_app(str2RegFunc)->get_arg(0); - std::string coreStr = m_strutil.get_string_constant_value(coreVal); - int core1Len = coreStr.length(); - std::string uStr = get_unrolled_string(coreStr, (lcm / core1Len)); + zstring coreStr; + u.str.is_string(coreVal, coreStr); + unsigned int core1Len = coreStr.length(); + zstring uStr = get_unrolled_string(coreStr, (lcm / core1Len)); if (uStr != lcmStr) { canHaveNonEmptyAssign = false; } @@ -9346,7 +9385,7 @@ expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls } } -expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & unrolls, std::string lcmStr) { +expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr) { context & ctx = get_context(); ast_manager & mgr = get_manager(); @@ -9416,8 +9455,9 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & // insert [tester = "more"] to litems so that the implyL for next tester is correct litems.push_back(ctx.mk_eq_atom(tester, moreAst)); } else { - std::string testerStr = m_strutil.get_string_constant_value(testerVal); - TRACE("t_str_detail", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << std::endl;); + zstring testerStr; + u.str.is_string(testerVal, testerStr); + TRACE("t_str_detail", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); if (testerStr == "more") { litems.push_back(ctx.mk_eq_atom(tester, moreAst)); } @@ -9438,12 +9478,12 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & return toAssert; } -expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * testerVar, int l, int h) { +expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h) { context & ctx = get_context(); ast_manager & mgr = get_manager(); TRACE("t_str_detail", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr - << ", l = " << l << ", h = " << h << std::endl;); + << ", l = " << l << ", h = " << h << "\n";); if (m_params.m_AggressiveUnrollTesting) { TRACE("t_str_detail", tout << "note: aggressive unroll testing is active" << std::endl;); @@ -9453,7 +9493,7 @@ expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * test expr_ref_vector andItems(mgr); for (int i = l; i < h; i++) { - std::string iStr = int_to_string(i); + zstring iStr = int_to_string(i); expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, mk_string(iStr)), mgr); TRACE("t_str_detail", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); if (m_params.m_AggressiveUnrollTesting) { @@ -9463,7 +9503,7 @@ expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * test } orItems.push_back(testerEqAst); - std::string unrollStrInstance = get_unrolled_string(lcmStr, i); + zstring unrollStrInstance = get_unrolled_string(lcmStr, i); expr_ref x1(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(var, mk_string(unrollStrInstance))), mgr); TRACE("t_str_detail", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); @@ -9535,14 +9575,14 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr str_indicator = expr_ref(lookup_val, m); } else { // no match; create and insert - std::string i_str = int_to_string(i); + zstring i_str = int_to_string(i); expr_ref new_val(mk_string(i_str), m); lengthTesterCache.insert(ri, new_val); m_trail.push_back(new_val); str_indicator = expr_ref(new_val, m); } } else { - std::string i_str = int_to_string(i); + zstring i_str = int_to_string(i); str_indicator = expr_ref(mk_string(i_str), m); } expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); @@ -9661,7 +9701,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin testerCases.push_back(caseMore); combinedCaseSplit.push_back(ctx.mk_eq_atom(caseMore, m_autil.mk_ge(lenFreeVar, m_autil.mk_numeral(N_plus_one, true) ))); - expr_ref caseEq(ctx.mk_eq_atom(tester, mk_string(N.to_string())), m); + expr_ref caseEq(ctx.mk_eq_atom(tester, mk_string(N.to_string().c_str())), m); testerCases.push_back(caseEq); combinedCaseSplit.push_back(ctx.mk_eq_atom(caseEq, ctx.mk_eq_atom(lenFreeVar, m_autil.mk_numeral(N, true)))); @@ -9712,7 +9752,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT expr * lastTester = binary_search_len_tester_stack[freeVar].back(); bool lastTesterHasEqcValue; expr * lastTesterValue = get_eqc_value(lastTester, lastTesterHasEqcValue); - std::string lastTesterConstant; + zstring lastTesterConstant; if (!lastTesterHasEqcValue) { TRACE("t_str_binary_search", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); // check previousLenTester @@ -9724,9 +9764,9 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT UNREACHABLE(); return NULL; } } else { - lastTesterConstant = m_strutil.get_string_constant_value(lastTesterValue); + u.str.is_string(lastTesterValue, lastTesterConstant); } - TRACE("t_str_binary_search", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << std::endl;); + TRACE("t_str_binary_search", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";); if (lastTesterConstant == "more" || lastTesterConstant == "less") { // use the previous bounds info to generate a new midpoint binary_search_info lastBounds; @@ -9805,7 +9845,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT return axiom; } // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, NULL, ""); + expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, NULL, zstring("")); return valueAssert; } } else { @@ -9906,7 +9946,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe TRACE("t_str_detail", tout << "found previous in-scope length assertions" << std::endl;); expr * effectiveLenInd = NULL; - std::string effectiveLenIndiStr = ""; + zstring effectiveLenIndiStr(""); int lenTesterCount = (int) fvar_lenTester_map[freeVar].size(); TRACE("t_str_detail", @@ -9934,9 +9974,8 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe TRACE("t_str_detail", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << " = " << mk_ismt2_pp(len_indicator_value, m) << std::endl;); if (indicatorHasEqcValue) { - const char * val = 0; - m_strutil.is_string(len_indicator_value, & val); - std::string len_pIndiStr(val); + zstring len_pIndiStr; + u.str.is_string(len_indicator_value, len_pIndiStr); if (len_pIndiStr != "more") { effectiveLenInd = len_indicator_pre; effectiveLenIndiStr = len_pIndiStr; @@ -9964,7 +10003,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe effectiveLenIndiStr = lenTesterValue; } else { if (effectiveHasEqcValue) { - effectiveLenIndiStr = m_strutil.get_string_constant_value(effective_eqc_value); + u.str.is_string(effective_eqc_value, effectiveLenIndiStr); } else { NOT_IMPLEMENTED_YET(); } @@ -9988,7 +10027,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe unsigned int testNum = 0; TRACE("t_str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr - << ", i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); + << ", i = " << i << ", lenTesterCount = " << lenTesterCount << "\n";); if (i == lenTesterCount) { fvar_len_count_map[freeVar] = fvar_len_count_map[freeVar] + 1; @@ -10007,7 +10046,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe } else { TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;); // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, NULL, ""); + expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, NULL, zstring("")); return valueAssert; } } // fVarLenCountMap.find(...) @@ -10020,7 +10059,7 @@ void theory_str::get_concats_in_eqc(expr * n, std::set & concats) { expr * eqcNode = n; do { - if (is_concat(to_app(eqcNode))) { + if (u.str.is_concat(to_app(eqcNode))) { concats.insert(eqcNode); } eqcNode = get_eqc_next(eqcNode); @@ -10096,7 +10135,7 @@ void theory_str::process_free_var(std::map & freeVar_map) { enode_vector::iterator it = e_freeVar->begin_parents(); for (; it != e_freeVar->end_parents(); ++it) { expr * parentAst = (*it)->get_owner(); - if (is_concat(to_app(parentAst))) { + if (u.str.is_concat(to_app(parentAst))) { standAlone = false; break; } @@ -10150,7 +10189,7 @@ void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set & expr * curr = n; do { - if (is_string(to_app(curr))) { + if (u.str.is_string(to_app(curr))) { constStr = curr; } else if (is_Unroll(to_app(curr))) { if (unrollFuncSet.find(curr) == unrollFuncSet.end()) { @@ -10169,11 +10208,11 @@ void theory_str::get_eqc_simpleUnroll(expr * n, expr * &constStr, std::setget_arg(0); - if (is_Str2Reg(to_app(core))) { + if (u.re.is_to_re(to_app(core))) { if (unrollFuncSet.find(curr) == unrollFuncSet.end()) { unrollFuncSet.insert(curr); } @@ -10200,9 +10239,9 @@ void theory_str::init_model(model_generator & mg) { * or else returns NULL if no concrete value was derived. */ app * theory_str::mk_value_helper(app * n) { - if (m_strutil.is_string(n)) { + if (u.str.is_string(n)) { return n; - } else if (is_concat(n)) { + } else if (u.str.is_concat(n)) { // recursively call this function on each argument SASSERT(n->get_num_args() == 2); expr * a0 = n->get_arg(0); @@ -10212,15 +10251,10 @@ app * theory_str::mk_value_helper(app * n) { app * a1_conststr = mk_value_helper(to_app(a1)); if (a0_conststr != NULL && a1_conststr != NULL) { - const char * a0_str = 0; - m_strutil.is_string(a0_conststr, &a0_str); - - const char * a1_str = 0; - m_strutil.is_string(a1_conststr, &a1_str); - - std::string a0_s(a0_str); - std::string a1_s(a1_str); - std::string result = a0_s + a1_s; + zstring a0_s, a1_s; + u.str.is_string(a0_conststr, a0_s); + u.str.is_string(a1_conststr, a1_s); + zstring result = a0_s + a1_s; return to_app(mk_string(result)); } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 63f5d3cfc..3be852cf4 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -30,10 +30,44 @@ Revision History: #include #include"seq_decl_plugin.h" #include"union_find.h" -#include"theory_seq_empty.h" namespace smt { + class str_value_factory : public value_factory { + seq_util u; + symbol_set m_strings; + std::string delim; + unsigned m_next; + public: + str_value_factory(ast_manager & m, family_id fid) : + value_factory(m, fid), + u(m), delim("!"), m_next(0) {} + virtual ~str_value_factory() {} + virtual expr * get_some_value(sort * s) { + return u.str.mk_string("some value"); + } + virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { + v1 = u.str.mk_string("value 1"); + v2 = u.str.mk_string("value 2"); + return true; + } + virtual expr * get_fresh_value(sort * s) { + if (u.is_string(s)) { + while (true) { + std::ostringstream strm; + strm << delim << std::hex << (m_next++) << std::dec << delim; + symbol sym(strm.str().c_str()); + if (m_strings.contains(sym)) continue; + m_strings.insert(sym); + return u.str.mk_string(sym); + } + } else { + UNREACHABLE(); return NULL; + } + } + virtual void register_value(expr * n) { /* Ignore */ } + }; + // rather than modify obj_pair_map I inherit from it and add my own helper methods class theory_str_contain_pair_bool_map_t : public obj_pair_map { public: @@ -237,8 +271,8 @@ namespace smt { //obj_map > contain_pair_idx_map; std::map > > contain_pair_idx_map; - std::map, expr*> regex_in_bool_map; - std::map > regex_in_var_reg_str_map; + std::map, expr*> regex_in_bool_map; + std::map > regex_in_var_reg_str_map; // std::map regex_nfa_cache; // Regex term --> NFA @@ -380,7 +414,7 @@ namespace smt { bool upper_bound(expr* _e, rational& hi); bool can_two_nodes_eq(expr * n1, expr * n2); - bool can_concat_eq_str(expr * concat, std::string str); + bool can_concat_eq_str(expr * concat, zstring& str); bool can_concat_eq_concat(expr * concat1, expr * concat2); bool check_concat_len_in_eqc(expr * concat); bool check_length_consistency(expr * n1, expr * n2); @@ -462,20 +496,20 @@ namespace smt { void process_free_var(std::map & freeVar_map); expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); expr * gen_free_var_options(expr * freeVar, expr * len_indicator, - std::string len_valueStr, expr * valTesterInCbEq, std::string valTesterValueStr); + zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr); expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, - std::string lenStr, int tries); + zstring lenStr, int tries); void print_value_tester_list(svector > & testerList); bool get_next_val_encode(int_vector & base, int_vector & next); - std::string gen_val_string(int len, int_vector & encoding); + zstring gen_val_string(int len, int_vector & encoding); // binary search heuristic expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue); expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits); bool free_var_attempt(expr * nn1, expr * nn2); - void more_len_tests(expr * lenTester, std::string lenTesterValue); - void more_value_tests(expr * valTester, std::string valTesterValue); + void more_len_tests(expr * lenTester, zstring lenTesterValue); + void more_value_tests(expr * valTester, zstring valTesterValue); expr * get_alias_index_ast(std::map & aliasIndexMap, expr * node); expr * getMostLeftNodeInConcat(expr * node); @@ -494,10 +528,11 @@ namespace smt { void get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set & unrollFuncSet); void gen_assign_unroll_reg(std::set & unrolls); expr * gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls); - expr * gen_unroll_conditional_options(expr * var, std::set & unrolls, std::string lcmStr); - expr * gen_unroll_assign(expr * var, std::string lcmStr, expr * testerVar, int l, int h); + expr * gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr); + expr * gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h); void reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items); void check_regex_in(expr * nn1, expr * nn2); + zstring get_std_regex_str(expr * r); void dump_assignments(); void initialize_charset();