From db715634785fcb74c3578ddb8f33be9fcd703154 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 09:36:01 -0800 Subject: [PATCH] fix build compiler warnings on OSX Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 164 +++++++++++++++++++----------- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 44 ++++++-- src/ast/seq_decl_plugin.h | 4 +- src/smt/theory_seq.cpp | 11 +- src/smt/theory_seq_empty.h | 8 +- 6 files changed, 153 insertions(+), 79 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d94e54935..8a6515f00 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -53,6 +53,7 @@ eautomaton* re2automaton::re2aut(expr* e) { SASSERT(u.is_re(e)); expr* e1, *e2; scoped_ptr a, b; + unsigned lo, hi; if (u.re.is_to_re(e, e1)) { return seq2aut(e1); } @@ -77,10 +78,21 @@ eautomaton* re2automaton::re2aut(expr* e) { return a.detach(); } else if (u.re.is_range(e)) { - + // TBD } - else if (u.re.is_loop(e)) { - + else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) { + scoped_ptr eps = eautomaton::mk_epsilon(m); + b = eautomaton::mk_epsilon(m); + while (hi > lo) { + scoped_ptr c = eautomaton::mk_concat(*a, *b); + b = eautomaton::mk_union(*eps, *c); + --hi; + } + while (lo > 0) { + b = eautomaton::mk_concat(*a, *b); + --lo; + } + return b.detach(); } #if 0 else if (u.re.is_intersect(e, e1, e2)) { @@ -210,8 +222,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STRING_STOI: SASSERT(num_args == 1); return mk_str_stoi(args[0], result); - case OP_REGEXP_LOOP: - return BR_FAILED; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -653,6 +663,31 @@ void seq_rewriter::add_next(u_map& next, unsigned idx, expr* cond) { } } +bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { + unsigned state = aut.init(); + uint_set visited; + eautomaton::moves mvs; + aut.get_moves_from(state, mvs, true); + while (!aut.is_final_state(state)) { + if (mvs.size() != 1) { + return false; + } + if (visited.contains(state)) { + return false; + } + visited.insert(state); + expr* t = mvs[0].t(); + if (!t) { + return false; + } + seq.push_back(m_util.str.mk_unit(t)); + state = mvs[0].dst(); + mvs.reset(); + aut.get_moves_from(state, mvs, true); + } + return mvs.empty(); +} + bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { zstring s; ptr_vector todo; @@ -688,63 +723,78 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { scoped_ptr aut; expr_ref_vector seq(m()); - if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) { - expr_ref_vector trail(m()); - u_map maps[2]; - bool select_map = false; - expr_ref ch(m()), cond(m()); - eautomaton::moves mvs; - maps[0].insert(aut->init(), m().mk_true()); - // is_accepted(a, aut) & some state in frontier is final. + if (!(aut = re2automaton(m())(b))) { + return BR_FAILED; + } - for (unsigned i = 0; i < seq.size(); ++i) { - u_map& frontier = maps[select_map]; - u_map& next = maps[!select_map]; - select_map = !select_map; - ch = seq[i].get(); - next.reset(); - u_map::iterator it = frontier.begin(), end = frontier.end(); - for (; it != end; ++it) { - mvs.reset(); - unsigned state = it->m_key; - expr* acc = it->m_value; - aut->get_moves_from(state, mvs, false); - for (unsigned j = 0; j < mvs.size(); ++j) { - eautomaton::move const& mv = mvs[j]; - if (m().is_value(mv.t()) && m().is_value(ch)) { - if (mv.t() == ch) { - add_next(next, mv.dst(), acc); - } - else { - continue; - } - } - else { - cond = m().mk_eq(mv.t(), ch); - if (!m().is_true(acc)) cond = m().mk_and(acc, cond); - add_next(next, mv.dst(), cond); - } - } - } + if (is_sequence(*aut, seq)) { + if (seq.empty()) { + result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a))); } - u_map const& frontier = maps[select_map]; - u_map::iterator it = frontier.begin(), end = frontier.end(); - expr_ref_vector ors(m()); - for (; it != end; ++it) { - unsigned_vector states; - bool has_final = false; - aut->get_epsilon_closure(it->m_key, states); - for (unsigned i = 0; i < states.size() && !has_final; ++i) { - has_final = aut->is_final_state(states[i]); - } - if (has_final) { - ors.push_back(it->m_value); - } + else { + result = m().mk_eq(a, m_util.str.mk_concat(seq)); } - result = mk_or(ors); return BR_REWRITE_FULL; } - return BR_FAILED; + + if (!is_sequence(a, seq)) { + return BR_FAILED; + } + + expr_ref_vector trail(m()); + u_map maps[2]; + bool select_map = false; + expr_ref ch(m()), cond(m()); + eautomaton::moves mvs; + maps[0].insert(aut->init(), m().mk_true()); + // is_accepted(a, aut) & some state in frontier is final. + + for (unsigned i = 0; i < seq.size(); ++i) { + u_map& frontier = maps[select_map]; + u_map& next = maps[!select_map]; + select_map = !select_map; + ch = seq[i].get(); + next.reset(); + u_map::iterator it = frontier.begin(), end = frontier.end(); + for (; it != end; ++it) { + mvs.reset(); + unsigned state = it->m_key; + expr* acc = it->m_value; + aut->get_moves_from(state, mvs, false); + for (unsigned j = 0; j < mvs.size(); ++j) { + eautomaton::move const& mv = mvs[j]; + if (m().is_value(mv.t()) && m().is_value(ch)) { + if (mv.t() == ch) { + add_next(next, mv.dst(), acc); + } + else { + continue; + } + } + else { + cond = m().mk_eq(mv.t(), ch); + if (!m().is_true(acc)) cond = m().mk_and(acc, cond); + add_next(next, mv.dst(), cond); + } + } + } + } + u_map const& frontier = maps[select_map]; + u_map::iterator it = frontier.begin(), end = frontier.end(); + expr_ref_vector ors(m()); + for (; it != end; ++it) { + unsigned_vector states; + bool has_final = false; + aut->get_epsilon_closure(it->m_key, states); + for (unsigned i = 0; i < states.size() && !has_final; ++i) { + has_final = aut->is_final_state(states[i]); + } + if (has_final) { + ors.push_back(it->m_value); + } + } + result = mk_or(ors); + return BR_REWRITE_FULL; } br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { return BR_FAILED; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index b9d3460aa..5d6c40fa1 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -75,6 +75,7 @@ class seq_rewriter { void add_next(u_map& next, unsigned idx, expr* cond); bool is_sequence(expr* e, expr_ref_vector& seq); + bool is_sequence(eautomaton& aut, expr_ref_vector& seq); bool is_epsilon(expr* e) const; public: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 165e24eac..e31b168b8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -250,7 +250,13 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do if (!is_match) { std::ostringstream strm; strm << "Sort of function '" << sig.m_name << "' "; - strm << "does not match the declared type"; + strm << "does not match the declared type. Given domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(dom[i], m) << " "; + } + if (range) { + strm << " and range: " << mk_pp(range, m); + } m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); @@ -277,7 +283,19 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran if (!is_match) { std::ostringstream strm; strm << "Sort of polymorphic function '" << sig.m_name << "' "; - strm << "does not match the declared type"; + strm << "does not match the declared type. "; + strm << "\nGiven domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(dom[i], m) << " "; + } + if (range) { + strm << " and range: " << mk_pp(range, m); + } + strm << "\nExpected domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(sig.m_dom[i].get(), m) << " "; + } + m.raise_exception(strm.str().c_str()); } if (!range && dsz == 0) { @@ -319,7 +337,8 @@ void seq_decl_plugin::init() { parameter paramA(A); parameter paramS(strT); sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, ¶mA); - sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mA); + parameter paramSA(seqA); + sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mSA); sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, ¶mS); sort* boolT = m.mk_bool_sort(); sort* intT = arith_util(m).mk_int(); @@ -356,7 +375,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA); m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA); - m_sigs[OP_RE_LOOP] = alloc(psig, m, "re-loop", 1, 1, &reA, reA); + m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re-empty-set", 1, 0, 0, reA); m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re-full-set", 1, 0, 0, reA); m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA); @@ -367,7 +386,6 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); - m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments. m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT); m_sigs[_OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT); m_sigs[_OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT); @@ -472,7 +490,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_OF_PRED: case OP_STRING_ITOS: case OP_STRING_STOI: - case OP_REGEXP_LOOP: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); @@ -670,3 +687,18 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { es.push_back(e); } } + +bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) { + if (is_loop(n)) { + app const* a = to_app(n); + SASSERT(a->get_num_args() == 1); + SASSERT(a->get_decl()->get_num_parameters() == 2); + body = a->get_arg(0); + lo = a->get_decl()->get_parameter(0).get_int(); + hi = a->get_decl()->get_parameter(1).get_int(); + return true; + } + else { + return false; + } +} diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 00ada9e86..4a94ef18f 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -63,7 +63,6 @@ enum seq_op_kind { OP_STRING_CONST, OP_STRING_ITOS, OP_STRING_STOI, - OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments? // internal only operators. Converted to SEQ variants. _OP_STRING_STRREPL, _OP_STRING_CONCAT, @@ -304,7 +303,7 @@ public: bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } - bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); } + bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); @@ -313,6 +312,7 @@ public: MATCH_UNARY(is_star); MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); + bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); }; str str; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c1083ea25..6c27dc104 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -165,9 +165,9 @@ theory_seq::theory_seq(ast_manager& m): m_util(m), m_autil(m), m_trail_stack(*this), - m_atoms_qhead(0), m_ls(m), m_rs(m), m_lhs(m), m_rhs(m), + m_atoms_qhead(0), m_new_solution(false), m_new_propagation(false) { m_prefix = "seq.prefix.suffix"; @@ -194,7 +194,6 @@ theory_seq::~theory_seq() { final_check_status theory_seq::final_check_eh() { - context & ctx = get_context(); TRACE("seq", display(tout);); if (simplify_and_solve_eqs()) { ++m_stats.m_solve_eqs; @@ -760,7 +759,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) { if (l == r) { return false; } - context& ctx = get_context(); TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";); m_new_solution = true; m_rep.update(l, r, deps); @@ -933,7 +931,6 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons } bool theory_seq::solve_nqs(unsigned i) { - bool change = false; context & ctx = get_context(); for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) { if (solve_ne(i)) { @@ -1262,7 +1259,7 @@ void theory_seq::init_model(expr_ref_vector const& es) { } void theory_seq::init_model(model_generator & mg) { - m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); + m_factory = alloc(seq_factory, get_manager(), get_family_id()); mg.register_factory(m_factory); for (unsigned j = 0; j < m_nqs.size(); ++j) { ne const& n = m_nqs[j]; @@ -1288,7 +1285,6 @@ public: } virtual app * mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == m_dependencies.size()); - ast_manager& m = mg.get_manager(); if (values.empty()) { return th.mk_value(n); } @@ -1362,7 +1358,7 @@ app* theory_seq::mk_value(app* e) { unsigned sz; if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) { unsigned v = val.get_unsigned(); - if ((0 <= v && v < 7) || (14 <= v && v < 32) || v == 127) { + if ((v < 7) || (14 <= v && v < 32) || v == 127) { result = m_util.str.mk_unit(result); } else { @@ -1817,7 +1813,6 @@ enode* theory_seq::ensure_enode(expr* e) { } static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { - ast_manager& m = ctx.get_manager(); theory* th = ctx.get_theory(afid); if (th && ctx.e_internalized(e)) { return dynamic_cast(th); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 9c8f15a7a..69f8b54b7 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -26,23 +26,19 @@ namespace smt { class seq_factory : public value_factory { typedef hashtable symbol_set; ast_manager& m; - proto_model& m_model; seq_util u; symbol_set m_strings; unsigned m_next; - char m_char; std::string m_unique_delim; obj_map m_unique_sequences; expr_ref_vector m_trail; public: - seq_factory(ast_manager & m, family_id fid, proto_model & md): + seq_factory(ast_manager & m, family_id fid): value_factory(m, fid), m(m), - m_model(md), u(m), m_next(0), - m_char(0), m_unique_delim("!"), m_trail(m) { @@ -129,7 +125,7 @@ namespace smt { public: theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {} virtual void init_model(model_generator & mg) { - mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); + mg.register_factory(alloc(seq_factory, get_manager(), get_family_id())); } };