mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

z3str3: loop and trace cleanup

Browse source
This commit is contained in:
Murphy Berzish 2020-02-10 15:07:18 -05:00 • committed by Nikolaj Bjorner
parent b1e6031230
commit 8d3ed19981
1 changed files with 21 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/smt/theory_str_mc.cpp
View file

@ -471,8 +471,7 @@ namespace smt {
} else { } else {
unsigned_vector eps_states; unsigned_vector eps_states;
aut->get_epsilon_closure(initial_state, eps_states); aut->get_epsilon_closure(initial_state, eps_states);
for (unsigned_vector::iterator it = eps_states.begin(); it != eps_states.end(); ++it) { for (unsigned state : eps_states) {
unsigned state = *it;
if (aut->is_final_state(state)) { if (aut->is_final_state(state)) {
zero_solution = true; zero_solution = true;
break; break;
@ -494,16 +493,15 @@ namespace smt {
expr_ref_vector trail(m); expr_ref_vector trail(m);
u_map<expr*> maps[2]; u_map<expr*> maps[2];
bool select_map = false; bool select_map = false;
expr_ref ch(m), cond(m); expr_ref cond(m);
eautomaton::moves mvs; eautomaton::moves mvs;
maps[0].insert(aut->init(), m.mk_true()); maps[0].insert(aut->init(), m.mk_true());
// is_accepted(a, aut) & some state in frontier is final. // is_accepted(a, aut) & some state in frontier is final.
for (unsigned i = 0; i < str_chars.size(); ++i) { for (auto& ch : str_chars) {
u_map<expr*>& frontier = maps[select_map]; u_map<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map]; u_map<expr*>& next = maps[!select_map];
select_map = !select_map; select_map = !select_map;
ch = str_chars.get(i);
next.reset(); next.reset();
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end(); u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -511,8 +509,7 @@ namespace smt {
unsigned state = it->m_key; unsigned state = it->m_key;
expr* acc = it->m_value; expr* acc = it->m_value;
aut->get_moves_from(state, mvs, false); aut->get_moves_from(state, mvs, false);
for (unsigned j = 0; j < mvs.size(); ++j) { for (eautomaton::move& mv : mvs) {
eautomaton::move const& mv = mvs[j];
SASSERT(mv.t()); SASSERT(mv.t());
if (mv.t()->is_char() && m.is_value(mv.t()->get_char()) && m.is_value(ch)) { if (mv.t()->is_char() && m.is_value(mv.t()->get_char()) && m.is_value(ch)) {
if (mv.t()->get_char() == ch) { if (mv.t()->get_char() == ch) {
@ -772,17 +769,15 @@ namespace smt {
} }
} }
if (is_trace_enabled("str")) { TRACE("str",
TRACE_CODE( ast_manager & m = get_manager();
ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
tout << "dumping all formulas:" << std::endl; tout << "dumping all formulas:" << std::endl;
for (expr_ref_vector::iterator i = formulas.begin(); i != formulas.end(); ++i) { for (expr_ref_vector::iterator i = formulas.begin(); i != formulas.end(); ++i) {
expr * ex = *i; expr * ex = *i;
tout << mk_pp(ex, m) << (ctx.is_relevant(ex) ? "" : " (NOT REL)") << std::endl; tout << mk_pp(ex, m) << (ctx.is_relevant(ex) ? "" : " (NOT REL)") << std::endl;
} }
); );
}
fixed_length_subterm_trail.reset(); fixed_length_subterm_trail.reset();
fixed_length_used_len_terms.reset(); fixed_length_used_len_terms.reset();
@ -955,20 +950,18 @@ namespace smt {
precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value()))); precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value())));
} }
TRACE_CODE( TRACE("str_fl",
if(is_trace_enabled("str_fl")) { tout << "formulas asserted to bitvector subsolver:" << std::endl;
tout << "formulas asserted to bitvector subsolver:" << std::endl; for (auto e : fixed_length_assumptions) {
for (auto e : fixed_length_assumptions) { tout << mk_pp(e, subsolver.m()) << std::endl;
tout << mk_pp(e, subsolver.m()) << std::endl; }
} tout << "variable to character mappings:" << std::endl;
tout << "variable to character mappings:" << std::endl; for (auto &entry : var_to_char_subterm_map) {
for (auto &entry : var_to_char_subterm_map) { tout << mk_pp(entry.m_key, get_manager()) << ":";
tout << mk_pp(entry.m_key, get_manager()) << ":"; for (auto e : entry.m_value) {
for (auto e : entry.m_value) { tout << " " << mk_pp(e, subsolver.m());
tout << " " << mk_pp(e, subsolver.m());
}
tout << std::endl;
} }
tout << std::endl;
} }
); );
@ -1002,11 +995,9 @@ namespace smt {
model.insert(var, strValue); model.insert(var, strValue);
subst.insert(var, mk_string(strValue)); subst.insert(var, mk_string(strValue));
} }
TRACE_CODE( TRACE("str_fl",
if (is_trace_enabled("str_fl")) { for (auto entry : model) {
for (auto entry : model) { tout << mk_pp(entry.m_key, m) << " = " << entry.m_value << std::endl;
tout << mk_pp(entry.m_key, m) << " = " << entry.m_value << std::endl;
}
} }
); );
for (auto entry : uninterpreted_to_char_subterm_map) { for (auto entry : uninterpreted_to_char_subterm_map) {