diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 8c7399562..778890cb7 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -67,6 +67,7 @@ z3_add_component(smt theory_seq.cpp theory_special_relations.cpp theory_str.cpp + theory_str_mc.cpp theory_str_regex.cpp theory_utvpi.cpp theory_wmaxsat.cpp diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f20ec4d3c..76ee0ca7e 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7208,99 +7208,6 @@ namespace smt { } // (s == "yes") } - 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]; - expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); - TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (toAssert) { - assert_axiom(toAssert); - } - } - } - - void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { - ast_manager & m = get_manager(); (void)m; - - expr * fVar = valueTester_fvar_map[valTester]; - if (m_params.m_UseBinarySearch) { - if (!binary_search_len_tester_stack.contains(fVar) || binary_search_len_tester_stack[fVar].empty()) { - TRACE("str", tout << "WARNING: no active length testers for " << mk_pp(fVar, m) << std::endl;); - NOT_IMPLEMENTED_YET(); - } - expr * effectiveLenInd = binary_search_len_tester_stack[fVar].back(); - bool hasEqcValue; - expr * len_indicator_value = get_eqc_value(effectiveLenInd, hasEqcValue); - if (!hasEqcValue) { - TRACE("str", 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 - zstring effectiveLenIndiStr; - u.str.is_string(len_indicator_value, effectiveLenIndiStr); - if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { - TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); - UNREACHABLE(); - } - expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (valueAssert != nullptr) { - assert_axiom(valueAssert); - } - } - } else { - int lenTesterCount; - if (fvar_lenTester_map.contains(fVar)) { - lenTesterCount = fvar_lenTester_map[fVar].size(); - } else { - lenTesterCount = 0; - } - - expr * effectiveLenInd = nullptr; - 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) { - zstring len_pIndiStr; - u.str.is_string(len_indicator_value, len_pIndiStr); - if (len_pIndiStr != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = len_pIndiStr; - break; - } - } - } - expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (valueAssert != nullptr) { - assert_axiom(valueAssert); - } - } - } - - bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { - zstring nn2_str; - if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager()) - << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); - more_len_tests(nn1, nn2_str); - return true; - } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - if (nn2_str == "more") { - TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager()) - << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); - more_value_tests(nn1, nn2_str); - } - return true; - } else if (internal_unrollTest_vars.contains(nn1)) { - return true; - } else { - return false; - } - } - void theory_str::handle_equality(expr * lhs, expr * rhs) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -9527,1271 +9434,6 @@ namespace smt { return ss.str(); } - void theory_str::print_value_tester_list(svector > & testerList) { - TRACE("str", - int ss = testerList.size(); - tout << "valueTesterList = {"; - for (int i = 0; i < ss; ++i) { - if (i % 4 == 0) { - tout << std::endl; - } - tout << "(" << testerList[i].first << ", "; - tout << mk_pp(testerList[i].second, get_manager()); - tout << "), "; - } - tout << std::endl << "}" << std::endl; - ); - } - - zstring theory_str::gen_val_string(int len, int_vector & encoding) { - SASSERT(charSetSize > 0); - SASSERT(!char_set.empty()); - - std::string re(len, char_set[0]); - for (int i = 0; i < (int) encoding.size() - 1; i++) { - int idx = encoding[i]; - re[len - 1 - i] = char_set[idx]; - } - return zstring(re.c_str()); - } - - /* - * The return value indicates whether we covered the search space. - * - If the next encoding is valid, return false - * - Otherwise, return true - */ - bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { - SASSERT(charSetSize > 0); - - TRACE("str", tout << "base vector: [ "; - for (unsigned i = 0; i < base.size(); ++i) { - tout << base[i] << " "; - } - tout << "]" << std::endl; - ); - - int s = 0; - int carry = 0; - next.reset(); - - for (int i = 0; i < (int) base.size(); i++) { - if (i == 0) { - s = base[i] + 1; - carry = s / charSetSize; - s = s % charSetSize; - next.push_back(s); - } else { - s = base[i] + carry; - carry = s / charSetSize; - s = s % charSetSize; - next.push_back(s); - } - } - if (next[next.size() - 1] > 0) { - next.reset(); - return true; - } else { - return false; - } - } - - expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, - zstring lenStr, int tries) { - ast_manager & m = get_manager(); - context & ctx = get_context(); - - int distance = 32; - - // ---------------------------------------------------------------------------------------- - // generate value options encoding - // encoding is a vector of size (len + 1) - // e.g, len = 2, - // encoding {1, 2, 0} means the value option is "charSet[2]"."charSet[1]" - // the last item in the encoding indicates whether the whole space is covered - // for example, if the charSet = {a, b}. All valid encodings are - // {0, 0, 0}, {1, 0, 0}, {0, 1, 0}, {1, 1, 0} - // if add 1 to the last one, we get - // {0, 0, 1} - // the last item "1" shows this is not a valid encoding, and we have covered all space - // ---------------------------------------------------------------------------------------- - int len = atoi(lenStr.encode().c_str()); - bool coverAll = false; - vector options; - int_vector base; - - TRACE("str", tout - << "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 << "\n" - << "tries = " << tries << "\n"; - if (m_params.m_AggressiveValueTesting) { - tout << "note: aggressive value testing is enabled" << std::endl; - } - ); - - if (tries == 0) { - base = int_vector(len + 1, 0); - coverAll = false; - } else { - expr * lastestValIndi = fvar_valueTester_map[freeVar][len][tries - 1].second; - TRACE("str", tout << "last value tester = " << mk_ismt2_pp(lastestValIndi, m) << std::endl;); - coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); - } - - size_t l = (tries) * distance; - size_t h = l; - for (int i = 0; i < distance; i++) { - if (coverAll) - break; - options.push_back(base); - h++; - coverAll = get_next_val_encode(options[options.size() - 1], base); - } - val_range_map.insert(val_indicator, options[options.size() - 1]); - - TRACE("str", - tout << "value tester encoding " << "{" << std::endl; - int_vector vec = val_range_map[val_indicator]; - - for (int_vector::iterator it = vec.begin(); it != vec.end(); ++it) { - tout << *it << std::endl; - } - tout << "}" << std::endl; - ); - - // ---------------------------------------------------------------------------------------- - - expr_ref_vector orList(m), andList(m); - - for (size_t i = l; i < h; i++) { - orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); - if (m_params.m_AggressiveValueTesting) { - literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); - ctx.mark_as_relevant(lit); - ctx.force_phase(lit); - } - - zstring aStr = gen_val_string(len, options[i - l]); - expr * strAst; - if (m_params.m_UseFastValueTesterCache) { - if (!valueTesterCache.find(aStr, strAst)) { - strAst = mk_string(aStr); - valueTesterCache.insert(aStr, strAst); - m_trail.push_back(strAst); - } - } else { - strAst = mk_string(aStr); - } - andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); - } - if (!coverAll) { - orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); - if (m_params.m_AggressiveValueTesting) { - literal l = mk_eq(val_indicator, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - } - - andList.push_back(mk_or(orList)); - expr_ref valTestAssert = mk_and(andList); - - // --------------------------------------- - // If the new value tester is $$_val_x_16_i - // Should add ($$_len_x_j = 16) /\ ($$_val_x_16_i = "more") - // --------------------------------------- - andList.reset(); - 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) - andList.push_back(m.mk_eq(vTester, mk_string("more"))); - } - expr_ref assertL = mk_and(andList); - // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) - return m.mk_or(m.mk_not(assertL), valTestAssert); - } - - expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, - zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr) { - ast_manager & m = get_manager(); - - int len = atoi(len_valueStr.encode().c_str()); - - // check whether any value tester is actually in scope - TRACE("str", tout << "checking scope of previous value testers" << std::endl;); - bool map_effectively_empty = true; - if (fvar_valueTester_map.contains(freeVar) && - fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { - // there's *something* in the map, but check its scope - for (auto const& entry : fvar_valueTester_map[freeVar][len]) { - expr * aTester = entry.second; - if (!internal_variable_set.contains(aTester)) { - TRACE("str", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); - } else { - TRACE("str", tout << mk_pp(aTester, m) << " in scope" << std::endl;); - map_effectively_empty = false; - break; - } - } - } - - if (map_effectively_empty) { - TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;); - int tries = 0; - expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); - valueTester_fvar_map.insert(val_indicator, freeVar); - if (!fvar_valueTester_map.contains(freeVar)) { - fvar_valueTester_map.insert(freeVar, std::map > >()); - } - fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator)); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); - } else { - TRACE("str", tout << "checking previous value testers" << std::endl;); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - - // go through all previous value testers - // If some doesn't have an eqc value, add its assertion again. - int testerTotal = fvar_valueTester_map[freeVar][len].size(); - int i = 0; - for (; i < testerTotal; i++) { - expr * aTester = fvar_valueTester_map[freeVar][len][i].second; - - // it's probably worth checking scope here, actually - if (!internal_variable_set.contains(aTester)) { - TRACE("str", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); - continue; - } - - if (aTester == valTesterInCbEq) { - break; - } - - bool anEqcHasValue = false; - get_eqc_value(aTester, anEqcHasValue); - if (!anEqcHasValue) { - TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - << " doesn't have an equivalence class value." << std::endl;); - refresh_theory_var(aTester); - - expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); - - TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl - << mk_ismt2_pp(makeupAssert, m) << std::endl;); - assert_axiom(makeupAssert); - } else { - // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); - } - } - - if (valTesterValueStr == "more") { - expr * valTester = nullptr; - if (i + 1 < testerTotal) { - valTester = fvar_valueTester_map[freeVar][len][i + 1].second; - refresh_theory_var(valTester); - } else { - valTester = mk_internal_valTest_var(freeVar, len, i + 1); - valueTester_fvar_map.insert(valTester, freeVar); - fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - } - return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); - } - - return nullptr; - } - } - - void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - TRACE("str", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); - - app * regexFuncDecl = to_app(regex); - if (u.re.is_to_re(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in Str2Reg(s1) - // ==> - // var = s1 /\ length(var) = length(s1) - // --------------------------------------------------------- - expr * strInside = to_app(regex)->get_arg(0); - items.push_back(ctx.mk_eq_atom(var, strInside)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(strInside))); - return; - } - // RegexUnion - else if (u.re.is_union(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in RegexUnion(r1, r2) - // ==> - // (var = newVar1 \/ var = newVar2) - // (var = newVar1 --> length(var) = length(newVar1)) /\ (var = newVar2 --> length(var) = length(newVar2)) - // /\ (newVar1 \in r1) /\ (newVar2 \in r2) - // --------------------------------------------------------- - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - items.push_back(mgr.mk_or(ctx.mk_eq_atom(var, newVar1), ctx.mk_eq_atom(var, newVar2))); - items.push_back(mgr.mk_or( - mgr.mk_not(ctx.mk_eq_atom(var, newVar1)), - ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar1)))); - items.push_back(mgr.mk_or( - mgr.mk_not(ctx.mk_eq_atom(var, newVar2)), - ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar2)))); - - expr * regArg1 = to_app(regex)->get_arg(0); - reduce_virtual_regex_in(newVar1, regArg1, items); - - expr * regArg2 = to_app(regex)->get_arg(1); - reduce_virtual_regex_in(newVar2, regArg2, items); - - return; - } - // RegexConcat - else if (u.re.is_concat(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in RegexConcat(r1, r2) - // ==> - // (var = newVar1 . newVar2) /\ (length(var) = length(vewVar1 . newVar2) ) - // /\ (newVar1 \in r1) /\ (newVar2 \in r2) - // --------------------------------------------------------- - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); - items.push_back(ctx.mk_eq_atom(var, concatAst)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), - m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); - - expr * regArg1 = to_app(regex)->get_arg(0); - reduce_virtual_regex_in(newVar1, regArg1, items); - expr * regArg2 = to_app(regex)->get_arg(1); - reduce_virtual_regex_in(newVar2, regArg2, items); - return; - } - // Unroll - else if (u.re.is_star(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in Star(r1) - // ==> - // var = unroll(r1, t1) /\ |var| = |unroll(r1, t1)| - // --------------------------------------------------------- - expr * regArg = to_app(regex)->get_arg(0); - expr_ref unrollCnt(mk_unroll_bound_var(), mgr); - expr_ref unrollFunc(mk_unroll(regArg, unrollCnt), mgr); - items.push_back(ctx.mk_eq_atom(var, unrollFunc)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(unrollFunc))); - return; - } - // re.range - else if (u.re.is_range(regexFuncDecl)) { - // var in range("a", "z") - // ==> - // (var = "a" or var = "b" or ... or var = "z") - expr_ref lo(regexFuncDecl->get_arg(0), mgr); - expr_ref hi(regexFuncDecl->get_arg(1), mgr); - zstring str_lo, str_hi; - SASSERT(u.str.is_string(lo)); - SASSERT(u.str.is_string(hi)); - u.str.is_string(lo, str_lo); - u.str.is_string(hi, str_hi); - SASSERT(str_lo.length() == 1); - SASSERT(str_hi.length() == 1); - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange - unsigned int tmp = c1; - c1 = c2; - c2 = tmp; - } - expr_ref_vector range_cases(mgr); - for (unsigned int ch = c1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref rhs(ctx.mk_eq_atom(var, u.str.mk_string(s_ch)), mgr); - range_cases.push_back(rhs); - } - expr_ref rhs(mk_or(range_cases), mgr); - SASSERT(rhs); - assert_axiom(rhs); - return; - } else { - get_manager().raise_exception("unrecognized regex operator"); - UNREACHABLE(); - } - } - - void theory_str::gen_assign_unroll_reg(std::set & unrolls) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - expr_ref_vector items(mgr); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr * unrFunc = *itor; - TRACE("str", tout << "generating assignment for unroll " << mk_pp(unrFunc, mgr) << std::endl;); - - expr * regexInUnr = to_app(unrFunc)->get_arg(0); - expr * cntInUnr = to_app(unrFunc)->get_arg(1); - items.reset(); - - rational low, high; - bool low_exists = lower_bound(cntInUnr, low); (void)low_exists; - bool high_exists = upper_bound(cntInUnr, high); (void)high_exists; - - TRACE("str", - tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; - rational unrLenValue; - bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); - tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl; - rational cntInUnrValue; - bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue); - tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?") - << " low = " - << (low_exists ? low.to_string() : "?") - << " high = " - << (high_exists ? high.to_string() : "?") - << std::endl; - ); - - expr_ref toAssert(mgr); - if (low.is_neg()) { - toAssert = m_autil.mk_ge(cntInUnr, mk_int(0)); - } else { - if (!unroll_var_map.contains(unrFunc)) { - - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); - expr_ref newCnt(mk_unroll_bound_var(), mgr); - expr_ref newUnrollFunc(mk_unroll(regexInUnr, newCnt), mgr); - - // unroll(r1, t1) = newVar1 . newVar2 - items.push_back(ctx.mk_eq_atom(unrFunc, concatAst)); - items.push_back(ctx.mk_eq_atom(mk_strlen(unrFunc), m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); - // mk_strlen(unrFunc) >= mk_strlen(newVar{1,2}) - items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar1))), mk_int(0))); - items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar2))), mk_int(0))); - // newVar1 \in r1 - reduce_virtual_regex_in(newVar1, regexInUnr, items); - items.push_back(ctx.mk_eq_atom(cntInUnr, m_autil.mk_add(newCnt, mk_int(1)))); - items.push_back(ctx.mk_eq_atom(newVar2, newUnrollFunc)); - items.push_back(ctx.mk_eq_atom(mk_strlen(newVar2), mk_strlen(newUnrollFunc))); - toAssert = ctx.mk_eq_atom( - m_autil.mk_ge(cntInUnr, mk_int(1)), - mk_and(items)); - - // option 0 - expr_ref op0(ctx.mk_eq_atom(cntInUnr, mk_int(0)), mgr); - expr_ref ast1(ctx.mk_eq_atom(unrFunc, mk_string("")), mgr); - expr_ref ast2(ctx.mk_eq_atom(mk_strlen(unrFunc), mk_int(0)), mgr); - expr_ref and1(mgr.mk_and(ast1, ast2), mgr); - - // put together - toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert); - - unroll_var_map.insert(unrFunc, toAssert); - } - else { - toAssert = unroll_var_map[unrFunc]; - } - } - m_trail.push_back(toAssert); - assert_axiom(toAssert); - } - } - - static int computeGCD(int x, int y) { - if (x == 0) { - return y; - } - while (y != 0) { - if (x > y) { - x = x - y; - } else { - y = y - x; - } - } - return x; - } - - static int computeLCM(int a, int b) { - int temp = computeGCD(a, b); - return temp ? (a / temp * b) : 0; - } - - static zstring get_unrolled_string(zstring core, int count) { - zstring res(""); - for (int i = 0; i < count; i++) { - res = res + core; - } - return res; - } - - expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - int lcm = 1; - int coreValueCount = 0; - expr * oneUnroll = nullptr; - 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); - zstring coreStr; - u.str.is_string(coreVal, coreStr); - if (oneUnroll == nullptr) { - oneUnroll = *itor; - oneCoreStr = coreStr; - } - coreValueCount++; - int core1Len = coreStr.length(); - lcm = computeLCM(lcm, core1Len); - } - // - bool canHaveNonEmptyAssign = true; - expr_ref_vector litems(mgr); - 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); - 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; - } - litems.push_back(ctx.mk_eq_atom(n, *itor)); - } - - if (canHaveNonEmptyAssign) { - return gen_unroll_conditional_options(n, unrolls, lcmStr); - } else { - expr_ref implyL(mk_and(litems), mgr); - expr_ref implyR(ctx.mk_eq_atom(n, mk_string("")), mgr); - // want to return (implyL -> implyR) - expr * final_axiom = rewrite_implication(implyL, implyR); - return final_axiom; - } - } - - expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - int dist = opt_LCMUnrollStep; - expr_ref_vector litems(mgr); - expr_ref moreAst(mk_string("more"), mgr); - for (expr * e : unrolls) { - expr_ref item(ctx.mk_eq_atom(var, e), mgr); - TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); - litems.push_back(item); - } - - // handle out-of-scope entries in unroll_tries_map - - ptr_vector outOfScopeTesters; - - for (expr * tester : unroll_tries_map[var][unrolls]) { - bool inScope = internal_unrollTest_vars.contains(tester); - TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) - << (inScope ? " in scope" : " out of scope") - << std::endl;); - if (!inScope) { - outOfScopeTesters.push_back(tester); - } - } - - for (expr* e : outOfScopeTesters) { - unroll_tries_map[var][unrolls].erase(e); - } - - if (unroll_tries_map[var][unrolls].empty()) { - unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); - } - - int tries = unroll_tries_map[var][unrolls].size(); - for (int i = 0; i < tries; i++) { - expr * tester = unroll_tries_map[var][unrolls][i]; - // TESTING - refresh_theory_var(tester); - bool testerHasValue = false; - expr * testerVal = get_eqc_value(tester, testerHasValue); - if (!testerHasValue) { - // generate make-up assertion - int l = i * dist; - int h = (i + 1) * dist; - expr_ref lImp(mk_and(litems), mgr); - expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); - - SASSERT(lImp); - TRACE("str", tout << "lImp = " << mk_pp(lImp, mgr) << std::endl;); - SASSERT(rImp); - TRACE("str", tout << "rImp = " << mk_pp(rImp, mgr) << std::endl;); - - expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); - SASSERT(toAssert); - TRACE("str", tout << "Making up assignments for variable which is equal to unbounded Unroll" << std::endl;); - m_trail.push_back(toAssert); - return toAssert; - - // note: this is how the code looks in Z3str2's strRegex.cpp:genUnrollConditionalOptions. - // the return is in the same place - - // insert [tester = "more"] to litems so that the implyL for next tester is correct - litems.push_back(ctx.mk_eq_atom(tester, moreAst)); - } else { - zstring testerStr; - u.str.is_string(testerVal, testerStr); - TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); - if (testerStr == "more") { - litems.push_back(ctx.mk_eq_atom(tester, moreAst)); - } - } - } - expr * tester = mk_unroll_test_var(); - unroll_tries_map[var][unrolls].push_back(tester); - int l = tries * dist; - int h = (tries + 1) * dist; - expr_ref lImp(mk_and(litems), mgr); - expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); - SASSERT(lImp); - SASSERT(rImp); - expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); - SASSERT(toAssert); - TRACE("str", tout << "Generating assignment for variable which is equal to unbounded Unroll" << std::endl;); - m_trail.push_back(toAssert); - return toAssert; - } - - 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("str", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr - << ", l = " << l << ", h = " << h << "\n";); - - if (m_params.m_AggressiveUnrollTesting) { - TRACE("str", tout << "note: aggressive unroll testing is active" << std::endl;); - } - - expr_ref_vector orItems(mgr); - expr_ref_vector andItems(mgr); - - for (int i = l; i < h; i++) { - zstring iStr = int_to_string(i); - expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, mk_string(iStr)), mgr); - TRACE("str", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); - if (m_params.m_AggressiveUnrollTesting) { - literal l = mk_eq(testerVar, mk_string(iStr), false); - ctx.mark_as_relevant(l); - ctx.force_phase(l); - } - - orItems.push_back(testerEqAst); - 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("str", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); - andItems.push_back(x1); - - expr_ref x2(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(mk_strlen(var), mk_int(i * lcmStr.length()))), mgr); - TRACE("str", tout << "x2 = " << mk_pp(x2, mgr) << std::endl;); - andItems.push_back(x2); - } - expr_ref testerEqMore(ctx.mk_eq_atom(testerVar, mk_string("more")), mgr); - TRACE("str", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;); - if (m_params.m_AggressiveUnrollTesting) { - literal l = mk_eq(testerVar, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - - orItems.push_back(testerEqMore); - int nextLowerLenBound = h * lcmStr.length(); - expr_ref more2(ctx.mk_eq_atom(testerEqMore, - //Z3_mk_ge(mk_length(t, var), mk_int(ctx, nextLowerLenBound)) - m_autil.mk_ge(m_autil.mk_add(mk_strlen(var), mk_int(-1 * nextLowerLenBound)), mk_int(0)) - ), mgr); - TRACE("str", tout << "more2 = " << mk_pp(more2, mgr) << std::endl;); - andItems.push_back(more2); - - expr_ref finalOR(mgr.mk_or(orItems.size(), orItems.c_ptr()), mgr); - TRACE("str", tout << "finalOR = " << mk_pp(finalOR, mgr) << std::endl;); - andItems.push_back(mk_or(orItems)); - - expr_ref finalAND(mgr.mk_and(andItems.size(), andItems.c_ptr()), mgr); - TRACE("str", tout << "finalAND = " << mk_pp(finalAND, mgr) << std::endl;); - - // doing the following avoids a segmentation fault - m_trail.push_back(finalAND); - return finalAND; - } - - expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tries) { - ast_manager & m = get_manager(); - context & ctx = get_context(); - - expr_ref freeVarLen(mk_strlen(freeVar), m); - SASSERT(freeVarLen); - - { - rational freeVar_len_value; - if (get_len_value(freeVar, freeVar_len_value)) { - TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); - expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m); - expr_ref concreteValue(ctx.mk_eq_atom( - ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), - ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m); - expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m); - SASSERT(finalAxiom); - m_trail.push_back(finalAxiom); - return finalAxiom; - } - } - - expr_ref_vector orList(m); - expr_ref_vector andList(m); - - int distance = 3; - int l = (tries - 1) * distance; - int h = tries * distance; - - TRACE("str", - tout << "building andList and orList" << std::endl; - if (m_params.m_AggressiveLengthTesting) { - tout << "note: aggressive length testing is active" << std::endl; - } - ); - - // experimental theory-aware case split support - literal_vector case_split_literals; - - for (int i = l; i < h; ++i) { - expr_ref str_indicator(m); - if (m_params.m_UseFastLengthTesterCache) { - rational ri(i); - expr * lookup_val; - if(lengthTesterCache.find(ri, lookup_val)) { - str_indicator = expr_ref(lookup_val, m); - } else { - // no match; create and insert - 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 { - 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); - orList.push_back(or_expr); - - double priority; - // give high priority to small lengths if this is available - if (i <= 5) { - priority = 0.3; - } else { - // prioritize over "more" - priority = 0.2; - } - add_theory_aware_branching_info(or_expr, priority, l_true); - - if (m_params.m_AggressiveLengthTesting) { - literal l = mk_eq(indicator, str_indicator, false); - ctx.mark_as_relevant(l); - ctx.force_phase(l); - } - - case_split_literals.insert(mk_eq(freeVarLen, mk_int(i), false)); - - expr_ref and_expr(ctx.mk_eq_atom(orList.get(orList.size() - 1), m.mk_eq(freeVarLen, mk_int(i))), m); - andList.push_back(and_expr); - } - - expr_ref more_option(ctx.mk_eq_atom(indicator, mk_string("more")), m); - orList.push_back(more_option); - // decrease priority of this option - add_theory_aware_branching_info(more_option, -0.1, l_true); - if (m_params.m_AggressiveLengthTesting) { - literal l = mk_eq(indicator, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - - andList.push_back(ctx.mk_eq_atom(orList.get(orList.size() - 1), m_autil.mk_ge(freeVarLen, mk_int(h)))); - - /* - { // more experimental theory case split support - expr_ref tmp(m_autil.mk_ge(freeVarLen, mk_int(h)), m); - ctx.internalize(m_autil.mk_ge(freeVarLen, mk_int(h)), false); - case_split_literals.push_back(ctx.get_literal(tmp)); - ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - } - */ - - expr_ref_vector or_items(m); - expr_ref_vector and_items(m); - - for (unsigned i = 0; i < orList.size(); ++i) { - or_items.push_back(orList.get(i)); - } - - and_items.push_back(mk_or(or_items)); - for(unsigned i = 0; i < andList.size(); ++i) { - and_items.push_back(andList.get(i)); - } - - TRACE("str", tout << "check: " << mk_pp(mk_and(and_items), m) << std::endl;); - - expr_ref lenTestAssert = mk_and(and_items); - SASSERT(lenTestAssert); - TRACE("str", tout << "crash avoidance lenTestAssert: " << mk_pp(lenTestAssert, m) << std::endl;); - - int testerCount = tries - 1; - if (testerCount > 0) { - expr_ref_vector and_items_LHS(m); - expr_ref moreAst(mk_string("more"), m); - for (int i = 0; i < testerCount; ++i) { - expr * indicator = fvar_lenTester_map[freeVar][i]; - if (internal_variable_set.find(indicator) == internal_variable_set.end()) { - TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " out of scope; continuing" << std::endl;); - continue; - } else { - TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " in scope" << std::endl;); - and_items_LHS.push_back(ctx.mk_eq_atom(indicator, moreAst)); - } - } - expr_ref assertL(mk_and(and_items_LHS), m); - SASSERT(assertL); - expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get()); - SASSERT(finalAxiom != nullptr); - TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;); - return finalAxiom; - } else { - TRACE("str", tout << "crash avoidance lenTestAssert.get(): " << mk_pp(lenTestAssert.get(), m) << std::endl;); - m_trail.push_back(lenTestAssert.get()); - return lenTestAssert.get(); - } - } - - // Return an expression of the form - // (tester = "less" | tester = "N" | tester = "more") & - // (tester = "less" iff len(freeVar) < N) & (tester = "more" iff len(freeVar) > N) & (tester = "N" iff len(freeVar) = N)) - expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - rational N = bounds.midPoint; - rational N_minus_one = N - rational::one(); - rational N_plus_one = N + rational::one(); - expr_ref lenFreeVar(mk_strlen(freeVar), m); - - TRACE("str", tout << "create case split for free var " << mk_pp(freeVar, m) - << " over " << mk_pp(tester, m) << " with midpoint " << N << std::endl;); - - expr_ref_vector combinedCaseSplit(m); - expr_ref_vector testerCases(m); - - expr_ref caseLess(ctx.mk_eq_atom(tester, mk_string("less")), m); - testerCases.push_back(caseLess); - combinedCaseSplit.push_back(ctx.mk_eq_atom(caseLess, m_autil.mk_le(lenFreeVar, m_autil.mk_numeral(N_minus_one, true) ))); - - expr_ref caseMore(ctx.mk_eq_atom(tester, mk_string("more")), m); - 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().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)))); - - combinedCaseSplit.push_back(mk_or(testerCases)); - - // force internalization on all terms in testerCases so we can extract literals - for (unsigned i = 0; i < testerCases.size(); ++i) { - expr * testerCase = testerCases.get(i); - if (!ctx.b_internalized(testerCase)) { - ctx.internalize(testerCase, false); - } - literal l = ctx.get_literal(testerCase); - case_split.push_back(l); - } - - expr_ref final_term(mk_and(combinedCaseSplit), m); - SASSERT(final_term); - TRACE("str", tout << "final term: " << mk_pp(final_term, m) << std::endl;); - return final_term; - } - - expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue) { - ast_manager & m = get_manager(); - - if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) { - TRACE("str", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; - for (ptr_vector::const_iterator it = binary_search_len_tester_stack[freeVar].begin(); - it != binary_search_len_tester_stack[freeVar].end(); ++it) { - expr * tester = *it; - tout << mk_pp(tester, m) << ": "; - if (binary_search_len_tester_info.contains(tester)) { - binary_search_info & bounds = binary_search_len_tester_info[tester]; - tout << "[" << bounds.lowerBound << " | " << bounds.midPoint << " | " << bounds.upperBound << "]!" << bounds.windowSize; - } else { - tout << "[WARNING: no bounds info available]"; - } - bool hasEqcValue; - expr * testerEqcValue = get_eqc_value(tester, hasEqcValue); - if (hasEqcValue) { - tout << " = " << mk_pp(testerEqcValue, m); - } else { - tout << " [no eqc value]"; - } - tout << std::endl; - } - ); - expr * lastTester = binary_search_len_tester_stack[freeVar].back(); - bool lastTesterHasEqcValue; - expr * lastTesterValue = get_eqc_value(lastTester, lastTesterHasEqcValue); - zstring lastTesterConstant; - if (!lastTesterHasEqcValue) { - TRACE("str", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); - // check previousLenTester - if (previousLenTester == lastTester) { - lastTesterConstant = previousLenTesterValue; - TRACE("str", tout << "invoked with previousLenTester info matching top of stack" << std::endl;); - } else { - TRACE("str", tout << "WARNING: unexpected reordering of length testers!" << std::endl;); - UNREACHABLE(); return nullptr; - } - } else { - u.str.is_string(lastTesterValue, lastTesterConstant); - } - TRACE("str", 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; - if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { - // unexpected - TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); - UNREACHABLE(); - } - TRACE("str", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;); - binary_search_info newBounds; - expr * newTester = nullptr; - if (lastTesterConstant == "more") { - // special case: if the midpoint, upper bound, and window size are all equal, - // we double the window size and adjust the bounds - if (lastBounds.midPoint == lastBounds.upperBound && lastBounds.upperBound == lastBounds.windowSize) { - TRACE("str", tout << "search hit window size; expanding" << std::endl;); - newBounds.lowerBound = lastBounds.windowSize + rational::one(); - newBounds.windowSize = lastBounds.windowSize * rational(2); - newBounds.upperBound = newBounds.windowSize; - newBounds.calculate_midpoint(); - } else if (false) { - // handle the case where the midpoint can't be increased further - // (e.g. a window like [50 | 50 | 50]!64 and we don't answer "50") - } else { - // general case - newBounds.lowerBound = lastBounds.midPoint + rational::one(); - newBounds.windowSize = lastBounds.windowSize; - newBounds.upperBound = lastBounds.upperBound; - newBounds.calculate_midpoint(); - } - if (!binary_search_next_var_high.find(lastTester, newTester)) { - newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); - binary_search_next_var_high.insert(lastTester, newTester); - } - refresh_theory_var(newTester); - } else if (lastTesterConstant == "less") { - if (false) { - // handle the case where the midpoint can't be decreased further - // (e.g. a window like [0 | 0 | 0]!64 and we don't answer "0" - } else { - // general case - newBounds.upperBound = lastBounds.midPoint - rational::one(); - newBounds.windowSize = lastBounds.windowSize; - newBounds.lowerBound = lastBounds.lowerBound; - newBounds.calculate_midpoint(); - } - if (!binary_search_next_var_low.find(lastTester, newTester)) { - newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); - binary_search_next_var_low.insert(lastTester, newTester); - } - refresh_theory_var(newTester); - } - TRACE("str", tout << "new bounds are [" << newBounds.lowerBound << " | " << newBounds.midPoint << " | " << newBounds.upperBound << "]!" << newBounds.windowSize << std::endl;); - binary_search_len_tester_stack[freeVar].push_back(newTester); - m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); - binary_search_len_tester_info.insert(newTester, newBounds); - m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, newTester)); - - literal_vector case_split_literals; - expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals)); - m_trail.push_back(next_case_split); - // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - return next_case_split; - } else { // lastTesterConstant is a concrete value - TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); - // defensive check that this length did not converge on a negative value. - binary_search_info lastBounds; - if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { - // unexpected - TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); - UNREACHABLE(); - } - if (lastBounds.midPoint.is_neg()) { - TRACE("str", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;); - expr_ref axiom(m_autil.mk_ge(mk_strlen(freeVar), m_autil.mk_numeral(rational::zero(), true)), m); - return axiom; - } - // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, nullptr, zstring("")); - return valueAssert; - } - } else { - // no length testers yet - TRACE("str", tout << "no length testers for " << mk_pp(freeVar, m) << std::endl;); - binary_search_len_tester_stack.insert(freeVar, ptr_vector()); - - expr * firstTester; - rational lowerBound(0); - rational upperBound(m_params.m_BinarySearchInitialUpperBound); - rational windowSize(upperBound); - rational midPoint(floor(upperBound / rational(2))); - if (!binary_search_starting_len_tester.find(freeVar, firstTester)) { - firstTester = mk_internal_lenTest_var(freeVar, midPoint.get_int32()); - binary_search_starting_len_tester.insert(freeVar, firstTester); - } - refresh_theory_var(firstTester); - - { - rational freeVar_len_value; - if (get_len_value(freeVar, freeVar_len_value)) { - TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); - midPoint = freeVar_len_value; - upperBound = midPoint * 2; - windowSize = upperBound; - } - } - - binary_search_len_tester_stack[freeVar].push_back(firstTester); - m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); - binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize); - binary_search_len_tester_info.insert(firstTester, new_info); - m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, firstTester)); - - literal_vector case_split_literals; - expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals)); - m_trail.push_back(initial_case_split); - // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - return initial_case_split; - } - } - - // ----------------------------------------------------------------------------------------------------- - // True branch will be taken in final_check: - // - When we discover a variable is "free" for the first time - // lenTesterInCbEq = NULL - // lenTesterValue = "" - // False branch will be taken when invoked by new_eq_eh(). - // - After we set up length tester for a "free" var in final_check, - // when the tester is assigned to some value (e.g. "more" or "4"), - // lenTesterInCbEq != NULL, and its value will be passed by lenTesterValue - // The difference is that in new_eq_eh(), lenTesterInCbEq and its value have NOT been put into a same eqc - // ----------------------------------------------------------------------------------------------------- - expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { - - ast_manager & m = get_manager(); - - TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); - - if (m_params.m_UseBinarySearch) { - TRACE("str", tout << "using binary search heuristic" << std::endl;); - return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); - } else { - bool map_effectively_empty = false; - if (!fvar_len_count_map.contains(freeVar)) { - TRACE("str", tout << "fvar_len_count_map is empty" << std::endl;); - map_effectively_empty = true; - } - - if (!map_effectively_empty) { - // check whether any entries correspond to variables that went out of scope; - // if every entry is out of scope then the map counts as being empty - - // assume empty and find a counterexample - map_effectively_empty = true; - if (fvar_lenTester_map.contains(freeVar)) { - for (expr * indicator : fvar_lenTester_map[freeVar]) { - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { - TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) - << " in fvar_lenTester_map[freeVar]" << std::endl;); - map_effectively_empty = false; - break; - } - } - } - CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); - } - - if (map_effectively_empty) { - // no length assertions for this free variable have ever been added. - TRACE("str", tout << "no length assertions yet" << std::endl;); - - fvar_len_count_map.insert(freeVar, 1); - unsigned int testNum = fvar_len_count_map[freeVar]; - - expr_ref indicator(mk_internal_lenTest_var(freeVar, testNum), m); - SASSERT(indicator); - - // since the map is "effectively empty", we can remove those variables that have left scope... - if (!fvar_lenTester_map.contains(freeVar)) { - fvar_lenTester_map.insert(freeVar, ptr_vector()); - } - fvar_lenTester_map[freeVar].shrink(0); - fvar_lenTester_map[freeVar].push_back(indicator); - lenTester_fvar_map.insert(indicator, freeVar); - - expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); - SASSERT(lenTestAssert != nullptr); - return lenTestAssert; - } else { - TRACE("str", tout << "found previous in-scope length assertions" << std::endl;); - - expr * effectiveLenInd = nullptr; - zstring effectiveLenIndiStr(""); - int lenTesterCount; - if (fvar_lenTester_map.contains(freeVar)) { - lenTesterCount = fvar_lenTester_map[freeVar].size(); - } else { - lenTesterCount = 0; - } - - TRACE("str", - tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl; - for (int i = 0; i < lenTesterCount; ++i) { - expr * len_indicator = fvar_lenTester_map[freeVar][i]; - tout << mk_pp(len_indicator, m) << ": "; - bool effectiveInScope = (internal_variable_set.find(len_indicator) != internal_variable_set.end()); - tout << (effectiveInScope ? "in scope" : "NOT in scope"); - tout << std::endl; - } - ); - - int i = 0; - for (; i < lenTesterCount; ++i) { - expr * len_indicator_pre = fvar_lenTester_map[freeVar][i]; - // check whether this is in scope as well - if (internal_variable_set.find(len_indicator_pre) == internal_variable_set.end()) { - TRACE("str", tout << "length indicator " << mk_pp(len_indicator_pre, m) << " not in scope" << std::endl;); - continue; - } - - bool indicatorHasEqcValue = false; - expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); - TRACE("str", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << - " = " << mk_ismt2_pp(len_indicator_value, m) << std::endl;); - if (indicatorHasEqcValue) { - zstring len_pIndiStr; - u.str.is_string(len_indicator_value, len_pIndiStr); - if (len_pIndiStr != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = len_pIndiStr; - break; - } - } else { - if (lenTesterInCbEq != len_indicator_pre) { - TRACE("str", tout << "WARNING: length indicator " << mk_ismt2_pp(len_indicator_pre, m) - << " does not have an equivalence class value." - << " i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); - if (i > 0) { - effectiveLenInd = fvar_lenTester_map[freeVar][i - 1]; - bool effectiveHasEqcValue; - expr * effective_eqc_value = get_eqc_value(effectiveLenInd, effectiveHasEqcValue); - bool effectiveInScope = (internal_variable_set.find(effectiveLenInd) != internal_variable_set.end()); - TRACE("str", tout << "checking effective length indicator " << mk_pp(effectiveLenInd, m) << ": " - << (effectiveInScope ? "in scope" : "NOT in scope") << ", "; - if (effectiveHasEqcValue) { - tout << "~= " << mk_pp(effective_eqc_value, m); - } else { - tout << "no eqc string constant"; - } - tout << std::endl;); (void)effectiveInScope; - if (effectiveLenInd == lenTesterInCbEq) { - effectiveLenIndiStr = lenTesterValue; - } else { - if (effectiveHasEqcValue) { - u.str.is_string(effective_eqc_value, effectiveLenIndiStr); - } else { - NOT_IMPLEMENTED_YET(); - } - } - } - break; - } - // lenTesterInCbEq == len_indicator_pre - else { - if (lenTesterValue != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = lenTesterValue; - break; - } - } - } // !indicatorHasEqcValue - } // for (i : [0..lenTesterCount-1]) - if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "") { - TRACE("str", tout << "length is not fixed; generating length tester options for free var" << std::endl;); - expr_ref indicator(m); - unsigned int testNum = 0; - - TRACE("str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr - << ", i = " << i << ", lenTesterCount = " << lenTesterCount << "\n";); - - if (i == lenTesterCount) { - fvar_len_count_map[freeVar] = fvar_len_count_map[freeVar] + 1; - testNum = fvar_len_count_map[freeVar]; - indicator = mk_internal_lenTest_var(freeVar, testNum); - fvar_lenTester_map[freeVar].push_back(indicator); - lenTester_fvar_map.insert(indicator, freeVar); - } else { - indicator = fvar_lenTester_map[freeVar][i]; - refresh_theory_var(indicator); - testNum = i + 1; - } - expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); - SASSERT(lenTestAssert != nullptr); - return lenTestAssert; - } else { - // if we are performing automata-based reasoning and the term associated with - // this length tester is in any way constrained by regex terms, - // do not perform value testing -- this term is not a free variable. - if (m_params.m_RegexAutomata) { - std::map, expr*>::iterator it = regex_in_bool_map.begin(); - for (; it != regex_in_bool_map.end(); ++it) { - expr * re = it->second; - expr * re_str = to_app(re)->get_arg(0); - // recursive descent through all subterms of re_str to see if any of them are - // - the same as freeVar - // - in the same EQC as freeVar - if (term_appears_as_subterm(freeVar, re_str)) { - TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;); - return nullptr; - } - } - } - - TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); - // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, nullptr, zstring("")); - return valueAssert; - } - } // fVarLenCountMap.find(...) - - } // !UseBinarySearch - } void theory_str::get_concats_in_eqc(expr * n, std::set & concats) { @@ -10820,92 +9462,6 @@ namespace smt { return lhs_name.str() < rhs_name.str(); } - void theory_str::process_free_var(std::map & freeVar_map) { - context & ctx = get_context(); - - obj_hashtable eqcRepSet; - obj_hashtable leafVarSet; - std::map > aloneVars; - - for (auto const& kv : freeVar_map) { - expr * freeVar = kv.first; - // skip all regular expression vars - if (regex_variable_set.contains(freeVar)) { - continue; - } - - // Iterate the EQC of freeVar, its eqc variable should not be in the eqcRepSet. - // If found, have to filter it out - std::set eqVarSet; - get_var_in_eqc(freeVar, eqVarSet); - bool duplicated = false; - expr * dupVar = nullptr; - for (expr* eq : eqVarSet) { - if (eqcRepSet.contains(eq)) { - duplicated = true; - dupVar = eq; - break; - } - } - if (duplicated && dupVar != nullptr) { - TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) - << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;); - continue; - } else { - eqcRepSet.insert(freeVar); - } - } - - for (expr * freeVar : eqcRepSet) { - // has length constraint initially - bool standAlone = !input_var_in_len.contains(freeVar); - // iterate parents - if (standAlone) { - // I hope this works! - if (!ctx.e_internalized(freeVar)) { - ctx.internalize(freeVar, false); - } - enode * e_freeVar = ctx.get_enode(freeVar); - enode_vector::iterator it = e_freeVar->begin_parents(); - for (; it != e_freeVar->end_parents(); ++it) { - expr * parentAst = (*it)->get_owner(); - if (u.str.is_concat(to_app(parentAst))) { - standAlone = false; - break; - } - } - } - - if (standAlone) { - rational len_value; - bool len_value_exists = get_len_value(freeVar, len_value); - if (len_value_exists) { - leafVarSet.insert(freeVar); - } else { - aloneVars[-1].insert(freeVar); - } - } else { - leafVarSet.insert(freeVar); - } - } - - for (expr* lv : leafVarSet) { - expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, ""); - // gen_len_val_options_for_free_var() can legally return NULL, - // as methods that it calls may assert their own axioms instead. - if (toAssert) assert_axiom(toAssert); - - } - - for (auto const& kv : aloneVars) { - for (expr* av : kv.second) { - expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, ""); - // same deal with returning a NULL axiom here - if (toAssert) assert_axiom(toAssert); - } - } - } - /* * Collect all unroll functions * and constant string in eqc of node n diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp new file mode 100644 index 000000000..d2c978b8a --- /dev/null +++ b/src/smt/theory_str_mc.cpp @@ -0,0 +1,1493 @@ +/*++ + Module Name: + + theory_str_mc.cpp + + Abstract: + + Model Construction for String Theory Plugin + + Author: + + Murphy Berzish and Yunhui Zheng + + Revision History: + + --*/ +#include "ast/ast_smt2_pp.h" +#include "smt/smt_context.h" +#include "smt/theory_str.h" +#include "smt/smt_model_generator.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include +#include +#include "smt/theory_seq_empty.h" +#include "smt/theory_arith.h" +#include "ast/ast_util.h" +#include "ast/rewriter/seq_rewriter.h" +#include "smt_kernel.h" + +namespace smt { + + inline zstring int_to_string(int i) { + std::stringstream ss; + ss << i; + std::string str = ss.str(); + return zstring(str.c_str()); + } + + inline std::string longlong_to_string(long long i) { + std::stringstream ss; + ss << i; + return ss.str(); + } + + expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tries) { + ast_manager & m = get_manager(); + context & ctx = get_context(); + + expr_ref freeVarLen(mk_strlen(freeVar), m); + SASSERT(freeVarLen); + + { + rational freeVar_len_value; + if (get_len_value(freeVar, freeVar_len_value)) { + TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); + expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m); + expr_ref concreteValue(ctx.mk_eq_atom( + ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), + ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m); + expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m); + SASSERT(finalAxiom); + m_trail.push_back(finalAxiom); + return finalAxiom; + } + } + + expr_ref_vector orList(m); + expr_ref_vector andList(m); + + int distance = 3; + int l = (tries - 1) * distance; + int h = tries * distance; + + TRACE("str", + tout << "building andList and orList" << std::endl; + if (m_params.m_AggressiveLengthTesting) { + tout << "note: aggressive length testing is active" << std::endl; + } + ); + + // experimental theory-aware case split support + literal_vector case_split_literals; + + for (int i = l; i < h; ++i) { + expr_ref str_indicator(m); + if (m_params.m_UseFastLengthTesterCache) { + rational ri(i); + expr * lookup_val; + if(lengthTesterCache.find(ri, lookup_val)) { + str_indicator = expr_ref(lookup_val, m); + } else { + // no match; create and insert + 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 { + 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); + orList.push_back(or_expr); + + double priority; + // give high priority to small lengths if this is available + if (i <= 5) { + priority = 0.3; + } else { + // prioritize over "more" + priority = 0.2; + } + add_theory_aware_branching_info(or_expr, priority, l_true); + + if (m_params.m_AggressiveLengthTesting) { + literal l = mk_eq(indicator, str_indicator, false); + ctx.mark_as_relevant(l); + ctx.force_phase(l); + } + + case_split_literals.insert(mk_eq(freeVarLen, mk_int(i), false)); + + expr_ref and_expr(ctx.mk_eq_atom(orList.get(orList.size() - 1), m.mk_eq(freeVarLen, mk_int(i))), m); + andList.push_back(and_expr); + } + + expr_ref more_option(ctx.mk_eq_atom(indicator, mk_string("more")), m); + orList.push_back(more_option); + // decrease priority of this option + add_theory_aware_branching_info(more_option, -0.1, l_true); + if (m_params.m_AggressiveLengthTesting) { + literal l = mk_eq(indicator, mk_string("more"), false); + ctx.mark_as_relevant(l); + ctx.force_phase(~l); + } + + andList.push_back(ctx.mk_eq_atom(orList.get(orList.size() - 1), m_autil.mk_ge(freeVarLen, mk_int(h)))); + + /* + { // more experimental theory case split support + expr_ref tmp(m_autil.mk_ge(freeVarLen, mk_int(h)), m); + ctx.internalize(m_autil.mk_ge(freeVarLen, mk_int(h)), false); + case_split_literals.push_back(ctx.get_literal(tmp)); + ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); + } + */ + + expr_ref_vector or_items(m); + expr_ref_vector and_items(m); + + for (unsigned i = 0; i < orList.size(); ++i) { + or_items.push_back(orList.get(i)); + } + + and_items.push_back(mk_or(or_items)); + for(unsigned i = 0; i < andList.size(); ++i) { + and_items.push_back(andList.get(i)); + } + + TRACE("str", tout << "check: " << mk_pp(mk_and(and_items), m) << std::endl;); + + expr_ref lenTestAssert = mk_and(and_items); + SASSERT(lenTestAssert); + TRACE("str", tout << "crash avoidance lenTestAssert: " << mk_pp(lenTestAssert, m) << std::endl;); + + int testerCount = tries - 1; + if (testerCount > 0) { + expr_ref_vector and_items_LHS(m); + expr_ref moreAst(mk_string("more"), m); + for (int i = 0; i < testerCount; ++i) { + expr * indicator = fvar_lenTester_map[freeVar][i]; + if (internal_variable_set.find(indicator) == internal_variable_set.end()) { + TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " out of scope; continuing" << std::endl;); + continue; + } else { + TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " in scope" << std::endl;); + and_items_LHS.push_back(ctx.mk_eq_atom(indicator, moreAst)); + } + } + expr_ref assertL(mk_and(and_items_LHS), m); + SASSERT(assertL); + expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get()); + SASSERT(finalAxiom != nullptr); + TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;); + return finalAxiom; + } else { + TRACE("str", tout << "crash avoidance lenTestAssert.get(): " << mk_pp(lenTestAssert.get(), m) << std::endl;); + m_trail.push_back(lenTestAssert.get()); + return lenTestAssert.get(); + } + } + + /* + * The return value indicates whether we covered the search space. + * - If the next encoding is valid, return false + * - Otherwise, return true + */ + bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { + SASSERT(charSetSize > 0); + + TRACE("str", tout << "base vector: [ "; + for (unsigned i = 0; i < base.size(); ++i) { + tout << base[i] << " "; + } + tout << "]" << std::endl; + ); + + int s = 0; + int carry = 0; + next.reset(); + + for (int i = 0; i < (int) base.size(); i++) { + if (i == 0) { + s = base[i] + 1; + carry = s / charSetSize; + s = s % charSetSize; + next.push_back(s); + } else { + s = base[i] + carry; + carry = s / charSetSize; + s = s % charSetSize; + next.push_back(s); + } + } + if (next[next.size() - 1] > 0) { + next.reset(); + return true; + } else { + return false; + } + } + + expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + zstring lenStr, int tries) { + ast_manager & m = get_manager(); + context & ctx = get_context(); + + int distance = 32; + + // ---------------------------------------------------------------------------------------- + // generate value options encoding + // encoding is a vector of size (len + 1) + // e.g, len = 2, + // encoding {1, 2, 0} means the value option is "charSet[2]"."charSet[1]" + // the last item in the encoding indicates whether the whole space is covered + // for example, if the charSet = {a, b}. All valid encodings are + // {0, 0, 0}, {1, 0, 0}, {0, 1, 0}, {1, 1, 0} + // if add 1 to the last one, we get + // {0, 0, 1} + // the last item "1" shows this is not a valid encoding, and we have covered all space + // ---------------------------------------------------------------------------------------- + int len = atoi(lenStr.encode().c_str()); + bool coverAll = false; + vector options; + int_vector base; + + TRACE("str", tout + << "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 << "\n" + << "tries = " << tries << "\n"; + if (m_params.m_AggressiveValueTesting) { + tout << "note: aggressive value testing is enabled" << std::endl; + } + ); + + if (tries == 0) { + base = int_vector(len + 1, 0); + coverAll = false; + } else { + expr * lastestValIndi = fvar_valueTester_map[freeVar][len][tries - 1].second; + TRACE("str", tout << "last value tester = " << mk_ismt2_pp(lastestValIndi, m) << std::endl;); + coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); + } + + size_t l = (tries) * distance; + size_t h = l; + for (int i = 0; i < distance; i++) { + if (coverAll) + break; + options.push_back(base); + h++; + coverAll = get_next_val_encode(options[options.size() - 1], base); + } + val_range_map.insert(val_indicator, options[options.size() - 1]); + + TRACE("str", + tout << "value tester encoding " << "{" << std::endl; + int_vector vec = val_range_map[val_indicator]; + + for (int_vector::iterator it = vec.begin(); it != vec.end(); ++it) { + tout << *it << std::endl; + } + tout << "}" << std::endl; + ); + + // ---------------------------------------------------------------------------------------- + + expr_ref_vector orList(m), andList(m); + + for (size_t i = l; i < h; i++) { + orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); + if (m_params.m_AggressiveValueTesting) { + literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); + ctx.mark_as_relevant(lit); + ctx.force_phase(lit); + } + + zstring aStr = gen_val_string(len, options[i - l]); + expr * strAst; + if (m_params.m_UseFastValueTesterCache) { + if (!valueTesterCache.find(aStr, strAst)) { + strAst = mk_string(aStr); + valueTesterCache.insert(aStr, strAst); + m_trail.push_back(strAst); + } + } else { + strAst = mk_string(aStr); + } + andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); + } + if (!coverAll) { + orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); + if (m_params.m_AggressiveValueTesting) { + literal l = mk_eq(val_indicator, mk_string("more"), false); + ctx.mark_as_relevant(l); + ctx.force_phase(~l); + } + } + + andList.push_back(mk_or(orList)); + expr_ref valTestAssert = mk_and(andList); + + // --------------------------------------- + // If the new value tester is $$_val_x_16_i + // Should add ($$_len_x_j = 16) /\ ($$_val_x_16_i = "more") + // --------------------------------------- + andList.reset(); + 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) + andList.push_back(m.mk_eq(vTester, mk_string("more"))); + } + expr_ref assertL = mk_and(andList); + // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) + return m.mk_or(m.mk_not(assertL), valTestAssert); + } + + // ----------------------------------------------------------------------------------------------------- + // True branch will be taken in final_check: + // - When we discover a variable is "free" for the first time + // lenTesterInCbEq = NULL + // lenTesterValue = "" + // False branch will be taken when invoked by new_eq_eh(). + // - After we set up length tester for a "free" var in final_check, + // when the tester is assigned to some value (e.g. "more" or "4"), + // lenTesterInCbEq != NULL, and its value will be passed by lenTesterValue + // The difference is that in new_eq_eh(), lenTesterInCbEq and its value have NOT been put into a same eqc + // ----------------------------------------------------------------------------------------------------- + expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { + + ast_manager & m = get_manager(); + + TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); + + if (m_params.m_UseBinarySearch) { + TRACE("str", tout << "using binary search heuristic" << std::endl;); + return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); + } else { + bool map_effectively_empty = false; + if (!fvar_len_count_map.contains(freeVar)) { + TRACE("str", tout << "fvar_len_count_map is empty" << std::endl;); + map_effectively_empty = true; + } + + if (!map_effectively_empty) { + // check whether any entries correspond to variables that went out of scope; + // if every entry is out of scope then the map counts as being empty + + // assume empty and find a counterexample + map_effectively_empty = true; + if (fvar_lenTester_map.contains(freeVar)) { + for (expr * indicator : fvar_lenTester_map[freeVar]) { + if (internal_variable_set.find(indicator) != internal_variable_set.end()) { + TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) + << " in fvar_lenTester_map[freeVar]" << std::endl;); + map_effectively_empty = false; + break; + } + } + } + CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); + } + + if (map_effectively_empty) { + // no length assertions for this free variable have ever been added. + TRACE("str", tout << "no length assertions yet" << std::endl;); + + fvar_len_count_map.insert(freeVar, 1); + unsigned int testNum = fvar_len_count_map[freeVar]; + + expr_ref indicator(mk_internal_lenTest_var(freeVar, testNum), m); + SASSERT(indicator); + + // since the map is "effectively empty", we can remove those variables that have left scope... + if (!fvar_lenTester_map.contains(freeVar)) { + fvar_lenTester_map.insert(freeVar, ptr_vector()); + } + fvar_lenTester_map[freeVar].shrink(0); + fvar_lenTester_map[freeVar].push_back(indicator); + lenTester_fvar_map.insert(indicator, freeVar); + + expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); + SASSERT(lenTestAssert != nullptr); + return lenTestAssert; + } else { + TRACE("str", tout << "found previous in-scope length assertions" << std::endl;); + + expr * effectiveLenInd = nullptr; + zstring effectiveLenIndiStr(""); + int lenTesterCount; + if (fvar_lenTester_map.contains(freeVar)) { + lenTesterCount = fvar_lenTester_map[freeVar].size(); + } else { + lenTesterCount = 0; + } + + TRACE("str", + tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl; + for (int i = 0; i < lenTesterCount; ++i) { + expr * len_indicator = fvar_lenTester_map[freeVar][i]; + tout << mk_pp(len_indicator, m) << ": "; + bool effectiveInScope = (internal_variable_set.find(len_indicator) != internal_variable_set.end()); + tout << (effectiveInScope ? "in scope" : "NOT in scope"); + tout << std::endl; + } + ); + + int i = 0; + for (; i < lenTesterCount; ++i) { + expr * len_indicator_pre = fvar_lenTester_map[freeVar][i]; + // check whether this is in scope as well + if (internal_variable_set.find(len_indicator_pre) == internal_variable_set.end()) { + TRACE("str", tout << "length indicator " << mk_pp(len_indicator_pre, m) << " not in scope" << std::endl;); + continue; + } + + bool indicatorHasEqcValue = false; + expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); + TRACE("str", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << + " = " << mk_ismt2_pp(len_indicator_value, m) << std::endl;); + if (indicatorHasEqcValue) { + zstring len_pIndiStr; + u.str.is_string(len_indicator_value, len_pIndiStr); + if (len_pIndiStr != "more") { + effectiveLenInd = len_indicator_pre; + effectiveLenIndiStr = len_pIndiStr; + break; + } + } else { + if (lenTesterInCbEq != len_indicator_pre) { + TRACE("str", tout << "WARNING: length indicator " << mk_ismt2_pp(len_indicator_pre, m) + << " does not have an equivalence class value." + << " i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); + if (i > 0) { + effectiveLenInd = fvar_lenTester_map[freeVar][i - 1]; + bool effectiveHasEqcValue; + expr * effective_eqc_value = get_eqc_value(effectiveLenInd, effectiveHasEqcValue); + bool effectiveInScope = (internal_variable_set.find(effectiveLenInd) != internal_variable_set.end()); + TRACE("str", tout << "checking effective length indicator " << mk_pp(effectiveLenInd, m) << ": " + << (effectiveInScope ? "in scope" : "NOT in scope") << ", "; + if (effectiveHasEqcValue) { + tout << "~= " << mk_pp(effective_eqc_value, m); + } else { + tout << "no eqc string constant"; + } + tout << std::endl;); (void)effectiveInScope; + if (effectiveLenInd == lenTesterInCbEq) { + effectiveLenIndiStr = lenTesterValue; + } else { + if (effectiveHasEqcValue) { + u.str.is_string(effective_eqc_value, effectiveLenIndiStr); + } else { + NOT_IMPLEMENTED_YET(); + } + } + } + break; + } + // lenTesterInCbEq == len_indicator_pre + else { + if (lenTesterValue != "more") { + effectiveLenInd = len_indicator_pre; + effectiveLenIndiStr = lenTesterValue; + break; + } + } + } // !indicatorHasEqcValue + } // for (i : [0..lenTesterCount-1]) + if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "") { + TRACE("str", tout << "length is not fixed; generating length tester options for free var" << std::endl;); + expr_ref indicator(m); + unsigned int testNum = 0; + + TRACE("str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr + << ", i = " << i << ", lenTesterCount = " << lenTesterCount << "\n";); + + if (i == lenTesterCount) { + fvar_len_count_map[freeVar] = fvar_len_count_map[freeVar] + 1; + testNum = fvar_len_count_map[freeVar]; + indicator = mk_internal_lenTest_var(freeVar, testNum); + fvar_lenTester_map[freeVar].push_back(indicator); + lenTester_fvar_map.insert(indicator, freeVar); + } else { + indicator = fvar_lenTester_map[freeVar][i]; + refresh_theory_var(indicator); + testNum = i + 1; + } + expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); + SASSERT(lenTestAssert != nullptr); + return lenTestAssert; + } else { + // if we are performing automata-based reasoning and the term associated with + // this length tester is in any way constrained by regex terms, + // do not perform value testing -- this term is not a free variable. + if (m_params.m_RegexAutomata) { + std::map, expr*>::iterator it = regex_in_bool_map.begin(); + for (; it != regex_in_bool_map.end(); ++it) { + expr * re = it->second; + expr * re_str = to_app(re)->get_arg(0); + // recursive descent through all subterms of re_str to see if any of them are + // - the same as freeVar + // - in the same EQC as freeVar + if (term_appears_as_subterm(freeVar, re_str)) { + TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;); + return nullptr; + } + } + } + + TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); + // length is fixed + expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, nullptr, zstring("")); + return valueAssert; + } + } // fVarLenCountMap.find(...) + + } // !UseBinarySearch + } + + expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, + zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr) { + ast_manager & m = get_manager(); + + int len = atoi(len_valueStr.encode().c_str()); + + // check whether any value tester is actually in scope + TRACE("str", tout << "checking scope of previous value testers" << std::endl;); + bool map_effectively_empty = true; + if (fvar_valueTester_map.contains(freeVar) && + fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { + // there's *something* in the map, but check its scope + for (auto const& entry : fvar_valueTester_map[freeVar][len]) { + expr * aTester = entry.second; + if (!internal_variable_set.contains(aTester)) { + TRACE("str", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); + } else { + TRACE("str", tout << mk_pp(aTester, m) << " in scope" << std::endl;); + map_effectively_empty = false; + break; + } + } + } + + if (map_effectively_empty) { + TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;); + int tries = 0; + expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); + valueTester_fvar_map.insert(val_indicator, freeVar); + if (!fvar_valueTester_map.contains(freeVar)) { + fvar_valueTester_map.insert(freeVar, std::map > >()); + } + fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator)); + print_value_tester_list(fvar_valueTester_map[freeVar][len]); + return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); + } else { + TRACE("str", tout << "checking previous value testers" << std::endl;); + print_value_tester_list(fvar_valueTester_map[freeVar][len]); + + // go through all previous value testers + // If some doesn't have an eqc value, add its assertion again. + int testerTotal = fvar_valueTester_map[freeVar][len].size(); + int i = 0; + for (; i < testerTotal; i++) { + expr * aTester = fvar_valueTester_map[freeVar][len][i].second; + + // it's probably worth checking scope here, actually + if (!internal_variable_set.contains(aTester)) { + TRACE("str", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); + continue; + } + + if (aTester == valTesterInCbEq) { + break; + } + + bool anEqcHasValue = false; + get_eqc_value(aTester, anEqcHasValue); + if (!anEqcHasValue) { + TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) + << " doesn't have an equivalence class value." << std::endl;); + refresh_theory_var(aTester); + + expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); + + TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl + << mk_ismt2_pp(makeupAssert, m) << std::endl;); + assert_axiom(makeupAssert); + } else { + // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) + // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); + } + } + + if (valTesterValueStr == "more") { + expr * valTester = nullptr; + if (i + 1 < testerTotal) { + valTester = fvar_valueTester_map[freeVar][len][i + 1].second; + refresh_theory_var(valTester); + } else { + valTester = mk_internal_valTest_var(freeVar, len, i + 1); + valueTester_fvar_map.insert(valTester, freeVar); + fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); + print_value_tester_list(fvar_valueTester_map[freeVar][len]); + } + return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); + } + + return nullptr; + } + } + + void theory_str::process_free_var(std::map & freeVar_map) { + context & ctx = get_context(); + + obj_hashtable eqcRepSet; + obj_hashtable leafVarSet; + std::map > aloneVars; + + for (auto const& kv : freeVar_map) { + expr * freeVar = kv.first; + // skip all regular expression vars + if (regex_variable_set.contains(freeVar)) { + continue; + } + + // Iterate the EQC of freeVar, its eqc variable should not be in the eqcRepSet. + // If found, have to filter it out + std::set eqVarSet; + get_var_in_eqc(freeVar, eqVarSet); + bool duplicated = false; + expr * dupVar = nullptr; + for (expr* eq : eqVarSet) { + if (eqcRepSet.contains(eq)) { + duplicated = true; + dupVar = eq; + break; + } + } + if (duplicated && dupVar != nullptr) { + TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) + << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;); + continue; + } else { + eqcRepSet.insert(freeVar); + } + } + + for (expr * freeVar : eqcRepSet) { + // has length constraint initially + bool standAlone = !input_var_in_len.contains(freeVar); + // iterate parents + if (standAlone) { + // I hope this works! + if (!ctx.e_internalized(freeVar)) { + ctx.internalize(freeVar, false); + } + enode * e_freeVar = ctx.get_enode(freeVar); + enode_vector::iterator it = e_freeVar->begin_parents(); + for (; it != e_freeVar->end_parents(); ++it) { + expr * parentAst = (*it)->get_owner(); + if (u.str.is_concat(to_app(parentAst))) { + standAlone = false; + break; + } + } + } + + if (standAlone) { + rational len_value; + bool len_value_exists = get_len_value(freeVar, len_value); + if (len_value_exists) { + leafVarSet.insert(freeVar); + } else { + aloneVars[-1].insert(freeVar); + } + } else { + leafVarSet.insert(freeVar); + } + } + + for (expr* lv : leafVarSet) { + expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, ""); + // gen_len_val_options_for_free_var() can legally return NULL, + // as methods that it calls may assert their own axioms instead. + if (toAssert) assert_axiom(toAssert); + + } + + for (auto const& kv : aloneVars) { + for (expr* av : kv.second) { + expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, ""); + // same deal with returning a NULL axiom here + if (toAssert) assert_axiom(toAssert); + } + } + } + + bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { + zstring nn2_str; + if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { + TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); + more_len_tests(nn1, nn2_str); + return true; + } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { + if (nn2_str == "more") { + TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); + more_value_tests(nn1, nn2_str); + } + return true; + } else if (internal_unrollTest_vars.contains(nn1)) { + return true; + } else { + return false; + } + } + + 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]; + expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); + TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + if (toAssert) { + assert_axiom(toAssert); + } + } + } + + void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { + ast_manager & m = get_manager(); (void)m; + + expr * fVar = valueTester_fvar_map[valTester]; + if (m_params.m_UseBinarySearch) { + if (!binary_search_len_tester_stack.contains(fVar) || binary_search_len_tester_stack[fVar].empty()) { + TRACE("str", tout << "WARNING: no active length testers for " << mk_pp(fVar, m) << std::endl;); + NOT_IMPLEMENTED_YET(); + } + expr * effectiveLenInd = binary_search_len_tester_stack[fVar].back(); + bool hasEqcValue; + expr * len_indicator_value = get_eqc_value(effectiveLenInd, hasEqcValue); + if (!hasEqcValue) { + TRACE("str", 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 + zstring effectiveLenIndiStr; + u.str.is_string(len_indicator_value, effectiveLenIndiStr); + if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { + TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); + UNREACHABLE(); + } + expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); + TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + if (valueAssert != nullptr) { + assert_axiom(valueAssert); + } + } + } else { + int lenTesterCount; + if (fvar_lenTester_map.contains(fVar)) { + lenTesterCount = fvar_lenTester_map[fVar].size(); + } else { + lenTesterCount = 0; + } + + expr * effectiveLenInd = nullptr; + 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) { + zstring len_pIndiStr; + u.str.is_string(len_indicator_value, len_pIndiStr); + if (len_pIndiStr != "more") { + effectiveLenInd = len_indicator_pre; + effectiveLenIndiStr = len_pIndiStr; + break; + } + } + } + expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); + TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + if (valueAssert != nullptr) { + assert_axiom(valueAssert); + } + } + } + + + // Return an expression of the form + // (tester = "less" | tester = "N" | tester = "more") & + // (tester = "less" iff len(freeVar) < N) & (tester = "more" iff len(freeVar) > N) & (tester = "N" iff len(freeVar) = N)) + expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + rational N = bounds.midPoint; + rational N_minus_one = N - rational::one(); + rational N_plus_one = N + rational::one(); + expr_ref lenFreeVar(mk_strlen(freeVar), m); + + TRACE("str", tout << "create case split for free var " << mk_pp(freeVar, m) + << " over " << mk_pp(tester, m) << " with midpoint " << N << std::endl;); + + expr_ref_vector combinedCaseSplit(m); + expr_ref_vector testerCases(m); + + expr_ref caseLess(ctx.mk_eq_atom(tester, mk_string("less")), m); + testerCases.push_back(caseLess); + combinedCaseSplit.push_back(ctx.mk_eq_atom(caseLess, m_autil.mk_le(lenFreeVar, m_autil.mk_numeral(N_minus_one, true) ))); + + expr_ref caseMore(ctx.mk_eq_atom(tester, mk_string("more")), m); + 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().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)))); + + combinedCaseSplit.push_back(mk_or(testerCases)); + + // force internalization on all terms in testerCases so we can extract literals + for (unsigned i = 0; i < testerCases.size(); ++i) { + expr * testerCase = testerCases.get(i); + if (!ctx.b_internalized(testerCase)) { + ctx.internalize(testerCase, false); + } + literal l = ctx.get_literal(testerCase); + case_split.push_back(l); + } + + expr_ref final_term(mk_and(combinedCaseSplit), m); + SASSERT(final_term); + TRACE("str", tout << "final term: " << mk_pp(final_term, m) << std::endl;); + return final_term; + } + + expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue) { + ast_manager & m = get_manager(); + + if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) { + TRACE("str", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; + for (ptr_vector::const_iterator it = binary_search_len_tester_stack[freeVar].begin(); + it != binary_search_len_tester_stack[freeVar].end(); ++it) { + expr * tester = *it; + tout << mk_pp(tester, m) << ": "; + if (binary_search_len_tester_info.contains(tester)) { + binary_search_info & bounds = binary_search_len_tester_info[tester]; + tout << "[" << bounds.lowerBound << " | " << bounds.midPoint << " | " << bounds.upperBound << "]!" << bounds.windowSize; + } else { + tout << "[WARNING: no bounds info available]"; + } + bool hasEqcValue; + expr * testerEqcValue = get_eqc_value(tester, hasEqcValue); + if (hasEqcValue) { + tout << " = " << mk_pp(testerEqcValue, m); + } else { + tout << " [no eqc value]"; + } + tout << std::endl; + } + ); + expr * lastTester = binary_search_len_tester_stack[freeVar].back(); + bool lastTesterHasEqcValue; + expr * lastTesterValue = get_eqc_value(lastTester, lastTesterHasEqcValue); + zstring lastTesterConstant; + if (!lastTesterHasEqcValue) { + TRACE("str", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); + // check previousLenTester + if (previousLenTester == lastTester) { + lastTesterConstant = previousLenTesterValue; + TRACE("str", tout << "invoked with previousLenTester info matching top of stack" << std::endl;); + } else { + TRACE("str", tout << "WARNING: unexpected reordering of length testers!" << std::endl;); + UNREACHABLE(); return nullptr; + } + } else { + u.str.is_string(lastTesterValue, lastTesterConstant); + } + TRACE("str", 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; + if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { + // unexpected + TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); + UNREACHABLE(); + } + TRACE("str", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;); + binary_search_info newBounds; + expr * newTester = nullptr; + if (lastTesterConstant == "more") { + // special case: if the midpoint, upper bound, and window size are all equal, + // we double the window size and adjust the bounds + if (lastBounds.midPoint == lastBounds.upperBound && lastBounds.upperBound == lastBounds.windowSize) { + TRACE("str", tout << "search hit window size; expanding" << std::endl;); + newBounds.lowerBound = lastBounds.windowSize + rational::one(); + newBounds.windowSize = lastBounds.windowSize * rational(2); + newBounds.upperBound = newBounds.windowSize; + newBounds.calculate_midpoint(); + } else if (false) { + // handle the case where the midpoint can't be increased further + // (e.g. a window like [50 | 50 | 50]!64 and we don't answer "50") + } else { + // general case + newBounds.lowerBound = lastBounds.midPoint + rational::one(); + newBounds.windowSize = lastBounds.windowSize; + newBounds.upperBound = lastBounds.upperBound; + newBounds.calculate_midpoint(); + } + if (!binary_search_next_var_high.find(lastTester, newTester)) { + newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); + binary_search_next_var_high.insert(lastTester, newTester); + } + refresh_theory_var(newTester); + } else if (lastTesterConstant == "less") { + if (false) { + // handle the case where the midpoint can't be decreased further + // (e.g. a window like [0 | 0 | 0]!64 and we don't answer "0" + } else { + // general case + newBounds.upperBound = lastBounds.midPoint - rational::one(); + newBounds.windowSize = lastBounds.windowSize; + newBounds.lowerBound = lastBounds.lowerBound; + newBounds.calculate_midpoint(); + } + if (!binary_search_next_var_low.find(lastTester, newTester)) { + newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); + binary_search_next_var_low.insert(lastTester, newTester); + } + refresh_theory_var(newTester); + } + TRACE("str", tout << "new bounds are [" << newBounds.lowerBound << " | " << newBounds.midPoint << " | " << newBounds.upperBound << "]!" << newBounds.windowSize << std::endl;); + binary_search_len_tester_stack[freeVar].push_back(newTester); + m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); + binary_search_len_tester_info.insert(newTester, newBounds); + m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, newTester)); + + literal_vector case_split_literals; + expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals)); + m_trail.push_back(next_case_split); + // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); + return next_case_split; + } else { // lastTesterConstant is a concrete value + TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); + // defensive check that this length did not converge on a negative value. + binary_search_info lastBounds; + if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { + // unexpected + TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); + UNREACHABLE(); + } + if (lastBounds.midPoint.is_neg()) { + TRACE("str", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;); + expr_ref axiom(m_autil.mk_ge(mk_strlen(freeVar), m_autil.mk_numeral(rational::zero(), true)), m); + return axiom; + } + // length is fixed + expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, nullptr, zstring("")); + return valueAssert; + } + } else { + // no length testers yet + TRACE("str", tout << "no length testers for " << mk_pp(freeVar, m) << std::endl;); + binary_search_len_tester_stack.insert(freeVar, ptr_vector()); + + expr * firstTester; + rational lowerBound(0); + rational upperBound(m_params.m_BinarySearchInitialUpperBound); + rational windowSize(upperBound); + rational midPoint(floor(upperBound / rational(2))); + if (!binary_search_starting_len_tester.find(freeVar, firstTester)) { + firstTester = mk_internal_lenTest_var(freeVar, midPoint.get_int32()); + binary_search_starting_len_tester.insert(freeVar, firstTester); + } + refresh_theory_var(firstTester); + + { + rational freeVar_len_value; + if (get_len_value(freeVar, freeVar_len_value)) { + TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); + midPoint = freeVar_len_value; + upperBound = midPoint * 2; + windowSize = upperBound; + } + } + + binary_search_len_tester_stack[freeVar].push_back(firstTester); + m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); + binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize); + binary_search_len_tester_info.insert(firstTester, new_info); + m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, firstTester)); + + literal_vector case_split_literals; + expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals)); + m_trail.push_back(initial_case_split); + // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); + return initial_case_split; + } + } + + static int computeGCD(int x, int y) { + if (x == 0) { + return y; + } + while (y != 0) { + if (x > y) { + x = x - y; + } else { + y = y - x; + } + } + return x; + } + + static int computeLCM(int a, int b) { + int temp = computeGCD(a, b); + return temp ? (a / temp * b) : 0; + } + + static zstring get_unrolled_string(zstring core, int count) { + zstring res(""); + for (int i = 0; i < count; i++) { + res = res + core; + } + return res; + } + + expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls) { + context & ctx = get_context(); + ast_manager & mgr = get_manager(); + + int lcm = 1; + int coreValueCount = 0; + expr * oneUnroll = nullptr; + 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); + zstring coreStr; + u.str.is_string(coreVal, coreStr); + if (oneUnroll == nullptr) { + oneUnroll = *itor; + oneCoreStr = coreStr; + } + coreValueCount++; + int core1Len = coreStr.length(); + lcm = computeLCM(lcm, core1Len); + } + // + bool canHaveNonEmptyAssign = true; + expr_ref_vector litems(mgr); + 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); + 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; + } + litems.push_back(ctx.mk_eq_atom(n, *itor)); + } + + if (canHaveNonEmptyAssign) { + return gen_unroll_conditional_options(n, unrolls, lcmStr); + } else { + expr_ref implyL(mk_and(litems), mgr); + expr_ref implyR(ctx.mk_eq_atom(n, mk_string("")), mgr); + // want to return (implyL -> implyR) + expr * final_axiom = rewrite_implication(implyL, implyR); + return final_axiom; + } + } + + expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr) { + context & ctx = get_context(); + ast_manager & mgr = get_manager(); + + int dist = opt_LCMUnrollStep; + expr_ref_vector litems(mgr); + expr_ref moreAst(mk_string("more"), mgr); + for (expr * e : unrolls) { + expr_ref item(ctx.mk_eq_atom(var, e), mgr); + TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); + litems.push_back(item); + } + + // handle out-of-scope entries in unroll_tries_map + + ptr_vector outOfScopeTesters; + + for (expr * tester : unroll_tries_map[var][unrolls]) { + bool inScope = internal_unrollTest_vars.contains(tester); + TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) + << (inScope ? " in scope" : " out of scope") + << std::endl;); + if (!inScope) { + outOfScopeTesters.push_back(tester); + } + } + + for (expr* e : outOfScopeTesters) { + unroll_tries_map[var][unrolls].erase(e); + } + + if (unroll_tries_map[var][unrolls].empty()) { + unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); + } + + int tries = unroll_tries_map[var][unrolls].size(); + for (int i = 0; i < tries; i++) { + expr * tester = unroll_tries_map[var][unrolls][i]; + // TESTING + refresh_theory_var(tester); + bool testerHasValue = false; + expr * testerVal = get_eqc_value(tester, testerHasValue); + if (!testerHasValue) { + // generate make-up assertion + int l = i * dist; + int h = (i + 1) * dist; + expr_ref lImp(mk_and(litems), mgr); + expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); + + SASSERT(lImp); + TRACE("str", tout << "lImp = " << mk_pp(lImp, mgr) << std::endl;); + SASSERT(rImp); + TRACE("str", tout << "rImp = " << mk_pp(rImp, mgr) << std::endl;); + + expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); + SASSERT(toAssert); + TRACE("str", tout << "Making up assignments for variable which is equal to unbounded Unroll" << std::endl;); + m_trail.push_back(toAssert); + return toAssert; + + // note: this is how the code looks in Z3str2's strRegex.cpp:genUnrollConditionalOptions. + // the return is in the same place + + // insert [tester = "more"] to litems so that the implyL for next tester is correct + litems.push_back(ctx.mk_eq_atom(tester, moreAst)); + } else { + zstring testerStr; + u.str.is_string(testerVal, testerStr); + TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); + if (testerStr == "more") { + litems.push_back(ctx.mk_eq_atom(tester, moreAst)); + } + } + } + expr * tester = mk_unroll_test_var(); + unroll_tries_map[var][unrolls].push_back(tester); + int l = tries * dist; + int h = (tries + 1) * dist; + expr_ref lImp(mk_and(litems), mgr); + expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); + SASSERT(lImp); + SASSERT(rImp); + expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); + SASSERT(toAssert); + TRACE("str", tout << "Generating assignment for variable which is equal to unbounded Unroll" << std::endl;); + m_trail.push_back(toAssert); + return toAssert; + } + + 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("str", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr + << ", l = " << l << ", h = " << h << "\n";); + + if (m_params.m_AggressiveUnrollTesting) { + TRACE("str", tout << "note: aggressive unroll testing is active" << std::endl;); + } + + expr_ref_vector orItems(mgr); + expr_ref_vector andItems(mgr); + + for (int i = l; i < h; i++) { + zstring iStr = int_to_string(i); + expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, mk_string(iStr)), mgr); + TRACE("str", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); + if (m_params.m_AggressiveUnrollTesting) { + literal l = mk_eq(testerVar, mk_string(iStr), false); + ctx.mark_as_relevant(l); + ctx.force_phase(l); + } + + orItems.push_back(testerEqAst); + 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("str", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); + andItems.push_back(x1); + + expr_ref x2(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(mk_strlen(var), mk_int(i * lcmStr.length()))), mgr); + TRACE("str", tout << "x2 = " << mk_pp(x2, mgr) << std::endl;); + andItems.push_back(x2); + } + expr_ref testerEqMore(ctx.mk_eq_atom(testerVar, mk_string("more")), mgr); + TRACE("str", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;); + if (m_params.m_AggressiveUnrollTesting) { + literal l = mk_eq(testerVar, mk_string("more"), false); + ctx.mark_as_relevant(l); + ctx.force_phase(~l); + } + + orItems.push_back(testerEqMore); + int nextLowerLenBound = h * lcmStr.length(); + expr_ref more2(ctx.mk_eq_atom(testerEqMore, + //Z3_mk_ge(mk_length(t, var), mk_int(ctx, nextLowerLenBound)) + m_autil.mk_ge(m_autil.mk_add(mk_strlen(var), mk_int(-1 * nextLowerLenBound)), mk_int(0)) + ), mgr); + TRACE("str", tout << "more2 = " << mk_pp(more2, mgr) << std::endl;); + andItems.push_back(more2); + + expr_ref finalOR(mgr.mk_or(orItems.size(), orItems.c_ptr()), mgr); + TRACE("str", tout << "finalOR = " << mk_pp(finalOR, mgr) << std::endl;); + andItems.push_back(mk_or(orItems)); + + expr_ref finalAND(mgr.mk_and(andItems.size(), andItems.c_ptr()), mgr); + TRACE("str", tout << "finalAND = " << mk_pp(finalAND, mgr) << std::endl;); + + // doing the following avoids a segmentation fault + m_trail.push_back(finalAND); + return finalAND; + } + + void theory_str::print_value_tester_list(svector > & testerList) { + TRACE("str", + int ss = testerList.size(); + tout << "valueTesterList = {"; + for (int i = 0; i < ss; ++i) { + if (i % 4 == 0) { + tout << std::endl; + } + tout << "(" << testerList[i].first << ", "; + tout << mk_pp(testerList[i].second, get_manager()); + tout << "), "; + } + tout << std::endl << "}" << std::endl; + ); + } + + zstring theory_str::gen_val_string(int len, int_vector & encoding) { + SASSERT(charSetSize > 0); + SASSERT(!char_set.empty()); + + std::string re(len, char_set[0]); + for (int i = 0; i < (int) encoding.size() - 1; i++) { + int idx = encoding[i]; + re[len - 1 - i] = char_set[idx]; + } + return zstring(re.c_str()); + } + + void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items) { + context & ctx = get_context(); + ast_manager & mgr = get_manager(); + + TRACE("str", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); + + app * regexFuncDecl = to_app(regex); + if (u.re.is_to_re(regexFuncDecl)) { + // --------------------------------------------------------- + // var \in Str2Reg(s1) + // ==> + // var = s1 /\ length(var) = length(s1) + // --------------------------------------------------------- + expr * strInside = to_app(regex)->get_arg(0); + items.push_back(ctx.mk_eq_atom(var, strInside)); + items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(strInside))); + return; + } + // RegexUnion + else if (u.re.is_union(regexFuncDecl)) { + // --------------------------------------------------------- + // var \in RegexUnion(r1, r2) + // ==> + // (var = newVar1 \/ var = newVar2) + // (var = newVar1 --> length(var) = length(newVar1)) /\ (var = newVar2 --> length(var) = length(newVar2)) + // /\ (newVar1 \in r1) /\ (newVar2 \in r2) + // --------------------------------------------------------- + expr_ref newVar1(mk_regex_rep_var(), mgr); + expr_ref newVar2(mk_regex_rep_var(), mgr); + items.push_back(mgr.mk_or(ctx.mk_eq_atom(var, newVar1), ctx.mk_eq_atom(var, newVar2))); + items.push_back(mgr.mk_or( + mgr.mk_not(ctx.mk_eq_atom(var, newVar1)), + ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar1)))); + items.push_back(mgr.mk_or( + mgr.mk_not(ctx.mk_eq_atom(var, newVar2)), + ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar2)))); + + expr * regArg1 = to_app(regex)->get_arg(0); + reduce_virtual_regex_in(newVar1, regArg1, items); + + expr * regArg2 = to_app(regex)->get_arg(1); + reduce_virtual_regex_in(newVar2, regArg2, items); + + return; + } + // RegexConcat + else if (u.re.is_concat(regexFuncDecl)) { + // --------------------------------------------------------- + // var \in RegexConcat(r1, r2) + // ==> + // (var = newVar1 . newVar2) /\ (length(var) = length(vewVar1 . newVar2) ) + // /\ (newVar1 \in r1) /\ (newVar2 \in r2) + // --------------------------------------------------------- + expr_ref newVar1(mk_regex_rep_var(), mgr); + expr_ref newVar2(mk_regex_rep_var(), mgr); + expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); + items.push_back(ctx.mk_eq_atom(var, concatAst)); + items.push_back(ctx.mk_eq_atom(mk_strlen(var), + m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); + + expr * regArg1 = to_app(regex)->get_arg(0); + reduce_virtual_regex_in(newVar1, regArg1, items); + expr * regArg2 = to_app(regex)->get_arg(1); + reduce_virtual_regex_in(newVar2, regArg2, items); + return; + } + // Unroll + else if (u.re.is_star(regexFuncDecl)) { + // --------------------------------------------------------- + // var \in Star(r1) + // ==> + // var = unroll(r1, t1) /\ |var| = |unroll(r1, t1)| + // --------------------------------------------------------- + expr * regArg = to_app(regex)->get_arg(0); + expr_ref unrollCnt(mk_unroll_bound_var(), mgr); + expr_ref unrollFunc(mk_unroll(regArg, unrollCnt), mgr); + items.push_back(ctx.mk_eq_atom(var, unrollFunc)); + items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(unrollFunc))); + return; + } + // re.range + else if (u.re.is_range(regexFuncDecl)) { + // var in range("a", "z") + // ==> + // (var = "a" or var = "b" or ... or var = "z") + expr_ref lo(regexFuncDecl->get_arg(0), mgr); + expr_ref hi(regexFuncDecl->get_arg(1), mgr); + zstring str_lo, str_hi; + SASSERT(u.str.is_string(lo)); + SASSERT(u.str.is_string(hi)); + u.str.is_string(lo, str_lo); + u.str.is_string(hi, str_hi); + SASSERT(str_lo.length() == 1); + SASSERT(str_hi.length() == 1); + unsigned int c1 = str_lo[0]; + unsigned int c2 = str_hi[0]; + if (c1 > c2) { + // exchange + unsigned int tmp = c1; + c1 = c2; + c2 = tmp; + } + expr_ref_vector range_cases(mgr); + for (unsigned int ch = c1; ch <= c2; ++ch) { + zstring s_ch(ch); + expr_ref rhs(ctx.mk_eq_atom(var, u.str.mk_string(s_ch)), mgr); + range_cases.push_back(rhs); + } + expr_ref rhs(mk_or(range_cases), mgr); + SASSERT(rhs); + assert_axiom(rhs); + return; + } else { + get_manager().raise_exception("unrecognized regex operator"); + UNREACHABLE(); + } + } + + void theory_str::gen_assign_unroll_reg(std::set & unrolls) { + context & ctx = get_context(); + ast_manager & mgr = get_manager(); + + expr_ref_vector items(mgr); + for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { + expr * unrFunc = *itor; + TRACE("str", tout << "generating assignment for unroll " << mk_pp(unrFunc, mgr) << std::endl;); + + expr * regexInUnr = to_app(unrFunc)->get_arg(0); + expr * cntInUnr = to_app(unrFunc)->get_arg(1); + items.reset(); + + rational low, high; + bool low_exists = lower_bound(cntInUnr, low); (void)low_exists; + bool high_exists = upper_bound(cntInUnr, high); (void)high_exists; + + TRACE("str", + tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; + rational unrLenValue; + bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); + tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl; + rational cntInUnrValue; + bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue); + tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?") + << " low = " + << (low_exists ? low.to_string() : "?") + << " high = " + << (high_exists ? high.to_string() : "?") + << std::endl; + ); + + expr_ref toAssert(mgr); + if (low.is_neg()) { + toAssert = m_autil.mk_ge(cntInUnr, mk_int(0)); + } else { + if (!unroll_var_map.contains(unrFunc)) { + + expr_ref newVar1(mk_regex_rep_var(), mgr); + expr_ref newVar2(mk_regex_rep_var(), mgr); + expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); + expr_ref newCnt(mk_unroll_bound_var(), mgr); + expr_ref newUnrollFunc(mk_unroll(regexInUnr, newCnt), mgr); + + // unroll(r1, t1) = newVar1 . newVar2 + items.push_back(ctx.mk_eq_atom(unrFunc, concatAst)); + items.push_back(ctx.mk_eq_atom(mk_strlen(unrFunc), m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); + // mk_strlen(unrFunc) >= mk_strlen(newVar{1,2}) + items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar1))), mk_int(0))); + items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar2))), mk_int(0))); + // newVar1 \in r1 + reduce_virtual_regex_in(newVar1, regexInUnr, items); + items.push_back(ctx.mk_eq_atom(cntInUnr, m_autil.mk_add(newCnt, mk_int(1)))); + items.push_back(ctx.mk_eq_atom(newVar2, newUnrollFunc)); + items.push_back(ctx.mk_eq_atom(mk_strlen(newVar2), mk_strlen(newUnrollFunc))); + toAssert = ctx.mk_eq_atom( + m_autil.mk_ge(cntInUnr, mk_int(1)), + mk_and(items)); + + // option 0 + expr_ref op0(ctx.mk_eq_atom(cntInUnr, mk_int(0)), mgr); + expr_ref ast1(ctx.mk_eq_atom(unrFunc, mk_string("")), mgr); + expr_ref ast2(ctx.mk_eq_atom(mk_strlen(unrFunc), mk_int(0)), mgr); + expr_ref and1(mgr.mk_and(ast1, ast2), mgr); + + // put together + toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert); + + unroll_var_map.insert(unrFunc, toAssert); + } + else { + toAssert = unroll_var_map[unrFunc]; + } + } + m_trail.push_back(toAssert); + assert_axiom(toAssert); + } + } + + +}; // namespace smt