mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix int-to-str terms in theory_str not being picked up

Browse source
This commit is contained in:
Murphy Berzish 2017-03-10 13:53:55 -05:00
parent c198bc5863
commit b459d17624
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_str.cpp
View file

@ -7169,6 +7169,10 @@ void theory_str::set_up_axioms(expr * ex) {
} }
} else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) { } else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) {
m_library_aware_axiom_todo.push_back(n); m_library_aware_axiom_todo.push_back(n);
} else if (u.str.is_itos(ap)) {
TRACE("t_str_detail", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n);
} else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) { } else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) {
// if ex is a variable, add it to our list of variables // if ex is a variable, add it to our list of variables
TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
@ -7213,7 +7217,8 @@ void theory_str::set_up_axioms(expr * ex) {
// TODO indexof2/lastindexof // TODO indexof2/lastindexof
if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) { if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) {
m_library_aware_axiom_todo.push_back(n); m_library_aware_axiom_todo.push_back(n);
} else if (u.str.is_stoi(ap) || u.str.is_itos(ap)) { } else if (u.str.is_stoi(ap)) {
TRACE("t_str_detail", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap); string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n); m_library_aware_axiom_todo.push_back(n);
} }