mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix build compiler warnings on OSX

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-12 09:36:01 -08:00
parent 01c3e02e99
commit db71563478
6 changed files with 153 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

164
src/ast/rewriter/seq_rewriter.cpp
View file

@ -53,6 +53,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr* e1, *e2;
scoped_ptr<eautomaton> 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<eautomaton> eps = eautomaton::mk_epsilon(m);
b = eautomaton::mk_epsilon(m);
while (hi > lo) {
scoped_ptr<eautomaton> 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<expr*>& 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<expr> 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<eautomaton> aut;
expr_ref_vector seq(m());
if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) {
expr_ref_vector trail(m());
u_map<expr*> 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<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map];
select_map = !select_map;
ch = seq[i].get();
next.reset();
u_map<expr*>::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<expr*> const& frontier = maps[select_map];
u_map<expr*>::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<expr*> 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<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map];
select_map = !select_map;
ch = seq[i].get();
next.reset();
u_map<expr*>::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<expr*> const& frontier = maps[select_map];
u_map<expr*>::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;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -75,6 +75,7 @@ class seq_rewriter {
void add_next(u_map<expr*>& 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:

44
src/ast/seq_decl_plugin.cpp
View file

@ -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, &paramA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);
parameter paramSA(seqA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramSA);
sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, &paramS);
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;
}
}

4
src/ast/seq_decl_plugin.h
View file

@ -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;

11
src/smt/theory_seq.cpp
View file

@ -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<expr> & 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<theory_mi_arith*>(th);

8
src/smt/theory_seq_empty.h
View file

@ -26,23 +26,19 @@ namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> 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<sort, expr*> 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()));
}
};