From ab71dea82d574aba85811d858a674f97820c5f0c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 28 Feb 2017 17:47:55 -0500 Subject: [PATCH] theory_str refactoring --- src/api/z3_api.h | 148 ------------------------------- src/ast/ast_smt2_pp.cpp | 55 ------------ src/ast/ast_smt2_pp.h | 3 +- src/ast/rewriter/th_rewriter.cpp | 8 -- src/ast/seq_decl_plugin.cpp | 50 ++++++++++- src/ast/seq_decl_plugin.h | 6 +- src/model/model_evaluator.cpp | 7 -- src/smt/theory_str.cpp | 76 +++++----------- src/smt/theory_str.h | 10 ++- 9 files changed, 83 insertions(+), 280 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0b8351190..87c48f3d2 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3173,154 +3173,6 @@ extern "C" { /*@}*/ - /** @name Strings and regular expressions (Z3str2 implementation) */ - /*@{*/ - - /** - \brief Create a string sort for 8-bit ASCII strings. - - This function creates a sort for ASCII strings. - Each character is 8 bits. - - def_API('Z3_mk_str_sort', SORT, (_in(CONTEXT), )) - */ - Z3_sort Z3_API Z3_mk_str_sort(Z3_context c); - - /** - \brief Check if \c s is a string sort. - - def_API('Z3_is_str_sort', BOOL, (_in(CONTEXT), _in(SORT))) - */ - - Z3_bool Z3_API Z3_is_str_sort(Z3_context c, Z3_sort s); - - /** - \brief Determine if \c s is a string constant. - - def_API('Z3_is_str', BOOL, (_in(CONTEXT), _in(AST))) - */ - - Z3_bool Z3_API Z3_is_str(Z3_context c, Z3_ast s); - - /** - \brief Retrieve the string constant stored in \c s. - - \pre Z3_is_str(c, s) - - def_API('Z3_get_str', STRING, (_in(CONTEXT), _in(AST))) - */ - - Z3_string Z3_API Z3_get_str(Z3_context c, Z3_ast s); - - /** - \brief Create a string constant. - - \param c logical context. - \param str The ASCII representation of the string constant. - - def_API('Z3_mk_str', AST, (_in(CONTEXT), _in(STRING))) - */ - Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str); - - /** - \brief Create a string concatenation term. - def_API('Z3_mk_str_concat', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_concat(Z3_context c, Z3_ast s1, Z3_ast s2); - - /** - \brief Create a string length term. (Integer representation) - def_API('Z3_mk_str_length', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_length(Z3_context c, Z3_ast s); - - /** - \brief Create 'character at index' term. - def_API('Z3_mk_str_at', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_at(Z3_context c, Z3_ast s, Z3_ast idx); - - /** - \brief Create 'str.prefixof' term. - def_API('Z3_mk_str_prefixof', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full); - - /** - \brief Create 'str.suffixof' term. - def_API('Z3_mk_str_suffixof', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_suffixof(Z3_context c, Z3_ast suf, Z3_ast full); - - /** - \brief Create 'str.contains' term. - def_API('Z3_mk_str_contains', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_contains(Z3_context c, Z3_ast needle, Z3_ast haystack); - - /** - \brief Create 'str.indexof' term. - def_API('Z3_mk_str_indexof', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_indexof(Z3_context c, Z3_ast haystack, Z3_ast needle, Z3_ast start); - - /** - \brief Create 'str.substr' term. - def_API('Z3_mk_str_substr', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_substr(Z3_context c, Z3_ast s, Z3_ast start, Z3_ast count); - - /** - \brief Create 'str.replace' term. - def_API('Z3_mk_str_replace', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_replace(Z3_context c, Z3_ast base, Z3_ast target, Z3_ast replacement); - - - /** - \brief Create a regular expression that matches the given string constant. - def_API('Z3_mk_str_to_regex', AST, (_in(CONTEXT), _in(STRING))) - */ - Z3_ast Z3_API Z3_mk_str_to_regex(Z3_context c, Z3_string str); - - /** - \brief Create a regular expression membership predicate. - def_API('Z3_mk_str_in_regex', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_str_in_regex(Z3_context c, Z3_ast str, Z3_ast regex); - - /** - \brief Create a regex concatenation term. - def_API('Z3_mk_regex_concat', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_regex_concat(Z3_context c, Z3_ast r1, Z3_ast r2); - - /** - \brief Create a regex union term. - def_API('Z3_mk_regex_union', AST, (_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_regex_union(Z3_context c, Z3_ast r1, Z3_ast r2); - - /** - \brief Create a regex Kleene star term. - def_API('Z3_mk_regex_star', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_regex_star(Z3_context c, Z3_ast r); - - /** - \brief Create a regex plus term. - def_API('Z3_mk_regex_plus', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_regex_plus(Z3_context c, Z3_ast r); - - /** - \brief Create a regex character range term. - def_API('Z3_mk_regex_range', AST, (_in(CONTEXT), _in(STRING), _in(STRING))) - */ - Z3_ast Z3_API Z3_mk_regex_range(Z3_context c, Z3_string start, Z3_string end); - - /*@}*/ - /** @name Sequences and regular expressions */ /*@{*/ diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 023773f62..98c3b7962 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -304,58 +304,6 @@ format * smt2_pp_environment::mk_float(rational const & val) const { return mk_string(get_manager(), s.c_str()); } -format * smt2_pp_environment::pp_str_literal(app * t) { - ast_manager & m = get_manager(); - str_util & u = get_strutil(); - TRACE("parse_string", tout << "pp_str_literal\n";); - - SASSERT(u.is_string(t)); - std::string strVal = u.get_string_constant_value(t); - string_buffer<> buf; - buf << "\""; - - // we want to scan strVal and escape every non-printable character - for (unsigned int i = 0; i < strVal.length(); ++i) { - char c = strVal.at(i); - if (c == '"') { - // SMT-LIB 2.5 string escape - buf << "\"\""; - } else if (isprint(c)) { - buf << c; - } else if (c == '\a') { - buf << "\\a"; - } else if (c == '\b') { - buf << "\\b"; - } else if (c == '\e') { - buf << "\\e"; - } else if (c == '\f') { - buf << "\\f"; - } else if (c == '\n') { - buf << "\\n"; - } else if (c == '\r') { - buf << "\\r"; - } else if (c == '\t') { - buf << "\\t"; - } else if (c == '\v') { - buf << "\\v"; - } else if (c == '\\') { - buf << "\\" << "\\"; - } else { - // general hex escape - buf << "\\x"; - unsigned int cVal = ((unsigned int)c) & 0x000000FF; - const char convtable[16] = {'0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'}; - unsigned int highPart = cVal / 16; - unsigned int lowPart = cVal % 16; - SASSERT(highPart < 16); SASSERT(lowPart < 16); - buf << convtable[highPart] << convtable[lowPart]; - } - } - - buf << "\""; - return mk_string(m, buf.c_str()); -} - format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned decimal_prec) { arith_util & u = get_autil(); SASSERT(u.is_numeral(t) || u.is_irrational_algebraic_numeral(t)); @@ -666,9 +614,6 @@ class smt2_printer { else if (m_env.get_dlutil().is_numeral(c)) { f = m_env.pp_datalog_literal(c); } - else if (m_env.get_strutil().is_string(c)) { - f = m_env.pp_str_literal(c); - } else { buffer names; if (m().is_label_lit(c, names)) { diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index b1bdf52bd..2f79ebaec 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -56,9 +56,8 @@ public: virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg); virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec); virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits); - virtual format_ns::format * pp_str_literal(app * t); - virtual format_ns::format * pp_datalog_literal(app * t); virtual format_ns::format * pp_string_literal(app * t); + virtual format_ns::format * pp_datalog_literal(app * t); virtual format_ns::format * pp_sort(sort * s); virtual format_ns::format * pp_fdecl_ref(func_decl * f); format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 86772cdb4..0c57ea609 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -27,7 +27,6 @@ Notes: #include"dl_rewriter.h" #include"pb_rewriter.h" #include"seq_rewriter.h" -#include"str_rewriter.h" #include"rewriter_def.h" #include"expr_substitution.h" #include"ast_smt2_pp.h" @@ -46,7 +45,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { dl_rewriter m_dl_rw; pb_rewriter m_pb_rw; seq_rewriter m_seq_rw; - str_rewriter m_str_rw; arith_util m_a_util; bv_util m_bv_util; unsigned long long m_max_memory; // in bytes @@ -81,7 +79,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_ar_rw.updt_params(p); m_f_rw.updt_params(p); m_seq_rw.updt_params(p); - m_str_rw.updt_params(p); updt_local_params(p); } @@ -182,8 +179,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_ar_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); - else if (s_fid == m_str_rw.get_fid()) - st = m_str_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; @@ -220,8 +215,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return m_pb_rw.mk_app_core(f, num, args, result); if (fid == m_seq_rw.get_fid()) return m_seq_rw.mk_app_core(f, num, args, result); - if (fid == m_str_rw.get_fid()) - return m_str_rw.mk_app_core(f, num, args, result); return BR_FAILED; } @@ -680,7 +673,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_dl_rw(m), m_pb_rw(m), m_seq_rw(m), - m_str_rw(m), m_a_util(m), m_bv_util(m), m_used_dependencies(m), diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5022c57a6..059fe9674 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -284,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const { return result; } -std::ostream& zstring::operator<<(std::ostream& out) const { - return out << encode(); +bool zstring::operator==(const zstring& other) const { + // two strings are equal iff they have the same length and characters + if (length() != other.length()) { + return false; + } + for (unsigned i = 0; i < length(); ++i) { + unsigned Xi = m_buffer[i]; + unsigned Yi = other[i]; + if (Xi != Yi) { + return false; + } + } + + return true; +} + +bool zstring::operator!=(const zstring& other) const { + return !(*this == other); +} + +std::ostream& operator<<(std::ostream &os, const zstring &str) { + return os << str.encode(); +} + +bool operator<(const zstring& lhs, const zstring& rhs) { + // This has the same semantics as strcmp() + unsigned len = lhs.length(); + if (rhs.length() < len) { + len = rhs.length(); + } + for (unsigned i = 0; i < len; ++i) { + unsigned Li = lhs[i]; + unsigned Ri = rhs[i]; + if (Li < Ri) { + return true; + } else if (Li > Ri) { + return false; + } else { + continue; + } + } + // at this point, all compared characters are equal, + // so decide based on the relative lengths + if (lhs.length() < rhs.length()) { + return true; + } else { + return false; + } } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index b07e4d307..a7e534bbb 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -114,7 +114,11 @@ public: int indexof(zstring const& other, int offset) const; zstring extract(int lo, int hi) const; zstring operator+(zstring const& other) const; - std::ostream& operator<<(std::ostream& out) const; + bool operator==(const zstring& other) const; + bool operator!=(const zstring& other) const; + + friend std::ostream& operator<<(std::ostream &os, const zstring &str); + friend bool operator<(const zstring& lhs, const zstring& rhs); }; class seq_decl_plugin : public decl_plugin { diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 06bbceb43..af2253801 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -28,7 +28,6 @@ Revision History: #include"datatype_rewriter.h" #include"array_rewriter.h" #include"fpa_rewriter.h" -#include"str_rewriter.h" #include"rewriter_def.h" #include"cooperate.h" #include"ast_pp.h" @@ -46,7 +45,6 @@ struct evaluator_cfg : public default_rewriter_cfg { pb_rewriter m_pb_rw; fpa_rewriter m_f_rw; seq_rewriter m_seq_rw; - str_rewriter m_str_rw; array_util m_ar; unsigned long long m_max_memory; unsigned m_max_steps; @@ -66,7 +64,6 @@ struct evaluator_cfg : public default_rewriter_cfg { m_pb_rw(m), m_f_rw(m), m_seq_rw(m), - m_str_rw(m), m_ar(m) { bool flat = true; m_b_rw.set_flat(flat); @@ -158,8 +155,6 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); - else if (s_fid == m_str_rw.get_fid()) - st = m_str_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_ar_rw.get_fid()) st = mk_array_eq(args[0], args[1], result); if (st != BR_FAILED) @@ -182,8 +177,6 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_app_core(f, num, args, result); else if (fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_app_core(f, num, args, result); - else if (fid == m_str_rw.get_fid()) - st = m_str_rw.mk_app_core(f, num, args, result); else if (fid == m().get_label_family_id() && num == 1) { result = args[0]; st = BR_DONE; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d81bb9471..79b6efb8b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -887,7 +887,7 @@ void theory_str::try_eval_concat(enode * cat) { app * evalArg = worklist.top(); worklist.pop(); zstring nextStr; if (u.str.is_string(evalArg, nextStr)) { - flattenedString += nextStr; + flattenedString = flattenedString + nextStr; } else if (u.str.is_concat(evalArg)) { app * arg0 = to_app(evalArg->get_arg(0)); app * arg1 = to_app(evalArg->get_arg(1)); @@ -1643,9 +1643,10 @@ static zstring str2RegexStr(zstring str) { // 12 special chars if (nc == '\\' || nc == '^' || nc == '$' || nc == '.' || nc == '|' || nc == '?' || nc == '*' || nc == '+' || nc == '(' || nc == ')' || nc == '[' || nc == '{') { - res += zstring("\\"); + res = res + zstring("\\"); } - res += zstring(1, (unsigned)str[i]); + char tmp[1] = {(char)str[i]}; + res = res + zstring(tmp); } return res; } @@ -2783,11 +2784,9 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { // case 2: concat(x, y) = concat(m, "str") //************************************************************* if (is_concat_eq_type2(new_nn1, new_nn2)) { - expr * x = NULL; - expr * y = NULL; - expr * strAst = NULL; - expr * m = NULL; + expr * y = NULL; + expr * m = NULL; expr * v1_arg0 = to_app(new_nn1)->get_arg(0); expr * v1_arg1 = to_app(new_nn1)->get_arg(1); expr * v2_arg0 = to_app(new_nn2)->get_arg(0); @@ -2795,13 +2794,9 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { if (u.str.is_string(v1_arg1) && !u.str.is_string(v2_arg1)) { m = v1_arg0; - strAst = v1_arg1; - x = v2_arg0; y = v2_arg1; } else { m = v2_arg0; - strAst = v2_arg1; - x = v1_arg0; y = v1_arg1; } @@ -2823,20 +2818,14 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * v2_arg1 = to_app(new_nn2)->get_arg(1); expr * x = NULL; - expr * y = NULL; - expr * strAst = NULL; expr * n = NULL; if (u.str.is_string(v1_arg0) && !u.str.is_string(v2_arg0)) { - strAst = v1_arg0; n = v1_arg1; x = v2_arg0; - y = v2_arg1; } else { - strAst = v2_arg0; n = v2_arg1; x = v1_arg0; - y = v1_arg1; } if (has_self_cut(x, n)) { TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(x, tout); print_cut_var(n, tout);); @@ -2870,21 +2859,15 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * v2_arg0 = to_app(new_nn2)->get_arg(0); expr * v2_arg1 = to_app(new_nn2)->get_arg(1); - expr * str1Ast = NULL; expr * y = NULL; expr * m = NULL; - expr * str2Ast = NULL; if (u.str.is_string(v1_arg0)) { - str1Ast = v1_arg0; y = v1_arg1; m = v2_arg0; - str2Ast = v2_arg1; } else { - str1Ast = v2_arg0; y = v2_arg1; m = v1_arg0; - str2Ast = v1_arg1; } if (has_self_cut(m, y)) { TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); @@ -3160,9 +3143,6 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { // This vector will eventually contain one term for each possible arrangement we explore. expr_ref_vector arrangement_disjunction(mgr); - int option = 0; - int pos = 1; - // break option 1: m cuts y // len(x) < len(m) || len(y) > len(n) if (!avoidLoopCut || !has_self_cut(m, y)) { @@ -3508,16 +3488,13 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { // | m | str | rational lenDelta; expr_ref_vector l_items(mgr); - int l_count = 0; l_items.push_back(ctx.mk_eq_atom(concatAst1, concatAst2)); if (x_len_exists && m_len_exists) { l_items.push_back(ctx.mk_eq_atom(mk_strlen(x), mk_int(x_len))); l_items.push_back(ctx.mk_eq_atom(mk_strlen(m), mk_int(m_len))); - l_count = 3; lenDelta = x_len - m_len; } else { l_items.push_back(ctx.mk_eq_atom(mk_strlen(y), mk_int(y_len))); - l_count = 2; lenDelta = str_len - y_len; } TRACE("t_str", @@ -3562,12 +3539,8 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } } else { // Split type -1: no idea about the length... - int optionTotal = 2 + strValue.length(); expr_ref_vector arrangement_disjunction(mgr); - int option = 0; - int pos = 1; - expr_ref temp1_strAst(mk_concat(temp1, strAst), mgr); // m cuts y @@ -3904,7 +3877,6 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { // Split type -1. We know nothing about the length... expr_ref_vector arrangement_disjunction(mgr); - unsigned option = 0; int pos = 1; for (unsigned int i = 0; i <= strValue.length(); i++) { @@ -4336,7 +4308,6 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { } expr_ref_vector arrangement_disjunction(mgr); - int option = 0; int pos = 1; if (!avoidLoopCut || !has_self_cut(m, y)) { @@ -5602,7 +5573,7 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector & strVec if (subStrCnt == 1) { zstring subStrVal; - if (u.str.is_string(subStrVec[0]), subStrVal) { + if (u.str.is_string(subStrVec[0], subStrVal)) { for (int i = 0; i < strCnt; i++) { zstring strVal; if (u.str.is_string(strVec[i], strVal)) { @@ -5630,7 +5601,7 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector & strVec zstring strHeadVal; if (u.str.is_string(strVec[i], strHeadVal)) { if (strHeadVal.length() >= subStrHeadVal.length()) { - std::string suffix = strHeadVal.extract(strHeadVal.length() - subStrHeadVal.length(), subStrHeadVal.length()); + zstring suffix = strHeadVal.extract(strHeadVal.length() - subStrHeadVal.length(), subStrHeadVal.length()); if (suffix != subStrHeadVal) { firstNodesOK = false; } @@ -5758,7 +5729,7 @@ void theory_str::compute_contains(std::map & varAliasMap, } bool theory_str::can_concat_eq_str(expr * concat, zstring& str) { - int strLen = str.length(); + unsigned int strLen = str.length(); if (u.str.is_concat(to_app(concat))) { ptr_vector args; get_nodes_in_concat(concat, args); @@ -6244,7 +6215,7 @@ bool nfa::matches(zstring input) { std::set current_states; epsilon_closure(m_start_state, current_states); for (unsigned i = 0; i < input.length(); ++i) { - char A = input.at(i); + char A = (char)input[i]; std::set next_states; for (std::set::iterator it = current_states.begin(); it != current_states.end(); ++it) { @@ -6288,12 +6259,12 @@ void theory_str::check_regex_in(expr * nn1, expr * nn2) { expr_ref_vector::iterator itor = eqNodeSet.begin(); for (; itor != eqNodeSet.end(); itor++) { if (regex_in_var_reg_str_map.find(*itor) != regex_in_var_reg_str_map.end()) { - std::set::iterator strItor = regex_in_var_reg_str_map[*itor].begin(); + std::set::iterator strItor = regex_in_var_reg_str_map[*itor].begin(); for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) { - std::string regStr = *strItor; + zstring regStr = *strItor; zstring constStrValue; u.str.is_string(constStr, constStrValue); - std::pair key1 = std::make_pair(*itor, regStr); + std::pair key1 = std::make_pair(*itor, regStr); if (regex_in_bool_map.find(key1) != regex_in_bool_map.end()) { expr * boolVar = regex_in_bool_map[key1]; // actually the RegexIn term app * a_regexIn = to_app(boolVar); @@ -6403,7 +6374,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { // Inconsistency TRACE("t_str", tout << "inconsistency detected: \"" << arg1_str << "\" + \"" << arg2_str << - "\" != \"" << const_str << "\"\n"); + "\" != \"" << const_str << "\"" << "\n";); expr_ref equality(ctx.mk_eq_atom(concat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6421,7 +6392,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { TRACE("t_str", tout << "inconsistency detected: \"" << arg2_str << "\" is longer than \"" << const_str << "\"," - << " so cannot be concatenated with anything to form it\n"); + << " so cannot be concatenated with anything to form it" << "\n";); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6435,7 +6406,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { TRACE("t_str", tout << "inconsistency detected: " << "suffix of concatenation result expected \"" << secondPart << "\", " << "actually \"" << arg2_str << "\"" - << "\n"); + << "\n";); expr_ref equality(ctx.mk_eq_atom(newConcat, str), m); expr_ref diseq(m.mk_not(equality), m); assert_axiom(diseq); @@ -6620,7 +6591,6 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } int concatStrLen = const_str.length(); - int xor_pos = 0; int and_count = 1; expr_ref_vector arrangement_disjunction(m); @@ -6701,8 +6671,8 @@ expr_ref theory_str::set_up_finite_model_test(expr * lhs, expr * rhs) { } // make things easy for the core wrt. testvar - expr_ref t1(ctx.mk_eq_atom(testvar, u.str.mk_string("")), m); - expr_ref t_yes(ctx.mk_eq_atom(testvar, u.str.mk_string("yes")), m); + expr_ref t1(ctx.mk_eq_atom(testvar, mk_string("")), m); + expr_ref t_yes(ctx.mk_eq_atom(testvar, mk_string("yes")), m); expr_ref testvaraxiom(m.mk_or(t1, t_yes), m); assert_axiom(testvaraxiom); @@ -6812,8 +6782,8 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { expr_ref_vector andList(m); for (rational l = v_lower_bound; l <= v_upper_bound; l += rational::one()) { - std::string lStr = l.to_string(); - expr_ref str_indicator(u.str.mk_string(lStr), m); + zstring lStr = zstring(l.to_string().c_str()); + expr_ref str_indicator(mk_string(lStr), m); expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); orList.push_back(or_expr); expr_ref and_expr(ctx.mk_eq_atom(or_expr, ctx.mk_eq_atom(vLengthExpr, m_autil.mk_numeral(l, true))), m); @@ -9006,12 +8976,12 @@ zstring theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); SASSERT(char_set != NULL); - zstring re(len, (int) char_set[0]); + 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 re; + return zstring(re.c_str()); } /* @@ -9474,7 +9444,7 @@ static int computeLCM(int a, int b) { static zstring get_unrolled_string(zstring core, int count) { zstring res(""); for (int i = 0; i < count; i++) { - res += core; + res = res + core; } return res; } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 499bb23f8..fc238acbd 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -33,6 +33,8 @@ Revision History: namespace smt { + typedef hashtable symbol_set; + class str_value_factory : public value_factory { seq_util u; symbol_set m_strings; @@ -44,11 +46,11 @@ namespace smt { u(m), delim("!"), m_next(0) {} virtual ~str_value_factory() {} virtual expr * get_some_value(sort * s) { - return u.str.mk_string("some value"); + return u.str.mk_string(symbol("some value")); } virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { - v1 = u.str.mk_string("value 1"); - v2 = u.str.mk_string("value 2"); + v1 = u.str.mk_string(symbol("value 1")); + v2 = u.str.mk_string(symbol("value 2")); return true; } virtual expr * get_fresh_value(sort * s) { @@ -256,7 +258,7 @@ namespace smt { expr_ref_vector m_trail; // trail for generated terms - seq_factory * m_factory; + str_value_factory * m_factory; // terms we couldn't go through set_up_axioms() with because they weren't internalized expr_ref_vector m_delayed_axiom_setup_terms;