mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix weird Contains rewriter behaviour in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-08-18 19:14:50 -04:00
parent 3c8b833eeb
commit 8598a48e3b
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str.cpp
View file

@ -1130,6 +1130,22 @@ void theory_str::instantiate_axiom_Contains(enode * e) {
return;
}
axiomatized_terms.insert(ex);
// quick path, because this is necessary due to rewriter behaviour
// (at minimum it should fix z3str/concat-006.smt2
// TODO: see if it's necessary for other such terms
if (m_strutil.is_string(ex->get_arg(0)) && m_strutil.is_string(ex->get_arg(1))) {
TRACE("t_str_detail", tout << "eval constant Contains term " << mk_pp(ex, m) << std::endl;);
std::string haystackStr = m_strutil.get_string_constant_value(ex->get_arg(0));
std::string needleStr = m_strutil.get_string_constant_value(ex->get_arg(1));
if (haystackStr.find(needleStr) != std::string::npos) {
assert_axiom(ex);
} else {
assert_axiom(m.mk_not(ex));
}
return;
}
{ // register Contains()
expr * str = ex->get_arg(0);
expr * substr = ex->get_arg(1);