mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

theory_str refactor: check_contain_by_substr uses contain_pair_idx_map

Browse source
This commit is contained in:
Murphy Berzish 2017-02-14 16:09:45 -05:00
parent 52eaae9da0
commit 3e714075c4
1 changed files with 53 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

102
src/smt/theory_str.cpp
View file

@ -4977,67 +4977,71 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE
ast_manager & m = get_manager(); ast_manager & m = get_manager();
expr_ref_vector litems(m); expr_ref_vector litems(m);
// TODO refactor to use the new contain_pair_idx_map if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
expr * strAst = itor1->first;
expr * substrAst = itor1->second;
expr_ref_vector::iterator itor1 = contains_map.begin(); expr * boolVar;
for (; itor1 != contains_map.end(); ++itor1) { if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) {
expr * boolVar = *itor1; TRACE("t_str_detail", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;);
// boolVar is actually a Contains term }
app * containsApp = to_app(boolVar); // boolVar is actually a Contains term
expr * strAst = containsApp->get_arg(0); app * containsApp = to_app(boolVar);
expr * substrAst = containsApp->get_arg(1);
// we only want to inspect the Contains terms where either of strAst or substrAst // we only want to inspect the Contains terms where either of strAst or substrAst
// are equal to varNode. // are equal to varNode.
TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;);
if (varNode != strAst && varNode != substrAst) { if (varNode != strAst && varNode != substrAst) {
TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;);
continue; continue;
} }
TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;); TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;);
if (substrAst == varNode) { if (substrAst == varNode) {
bool strAstHasVal = false; bool strAstHasVal = false;
expr * strValue = get_eqc_value(strAst, strAstHasVal); expr * strValue = get_eqc_value(strAst, strAstHasVal);
if (strAstHasVal) { if (strAstHasVal) {
TRACE("t_str_detail", tout << mk_pp(strAst, m) << " has constant eqc value " << mk_pp(strValue, m) << std::endl;); TRACE("t_str_detail", tout << mk_pp(strAst, m) << " has constant eqc value " << mk_pp(strValue, m) << std::endl;);
if (strValue != strAst) { if (strValue != strAst) {
litems.push_back(ctx.mk_eq_atom(strAst, strValue)); litems.push_back(ctx.mk_eq_atom(strAst, strValue));
} }
std::string strConst = m_strutil.get_string_constant_value(strValue); std::string strConst = m_strutil.get_string_constant_value(strValue);
// iterate eqc (also eqc-to-be) of substr // iterate eqc (also eqc-to-be) of substr
for (expr_ref_vector::iterator itAst = willEqClass.begin(); itAst != willEqClass.end(); itAst++) { for (expr_ref_vector::iterator itAst = willEqClass.begin(); itAst != willEqClass.end(); itAst++) {
bool counterEgFound = false; bool counterEgFound = false;
if (is_concat(to_app(*itAst))) { if (is_concat(to_app(*itAst))) {
expr_ref_vector constList(m); expr_ref_vector constList(m);
// get constant strings in concat // get constant strings in concat
app * aConcat = to_app(*itAst); app * aConcat = to_app(*itAst);
get_const_str_asts_in_node(aConcat, constList); get_const_str_asts_in_node(aConcat, constList);
for (expr_ref_vector::iterator cstItor = constList.begin(); for (expr_ref_vector::iterator cstItor = constList.begin();
cstItor != constList.end(); cstItor++) { cstItor != constList.end(); cstItor++) {
std::string pieceStr = m_strutil.get_string_constant_value(*cstItor); std::string pieceStr = m_strutil.get_string_constant_value(*cstItor);
if (strConst.find(pieceStr) == std::string::npos) { if (strConst.find(pieceStr) == std::string::npos) {
TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;); TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;);
counterEgFound = true; counterEgFound = true;
if (aConcat != substrAst) { if (aConcat != substrAst) {
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
}
expr_ref implyLHS(mk_and(litems), m);
expr_ref implyR(m.mk_not(boolVar), m);
assert_implication(implyLHS, implyR);
break;
} }
expr_ref implyLHS(mk_and(litems), m);
expr_ref implyR(m.mk_not(boolVar), m);
assert_implication(implyLHS, implyR);
break;
} }
} }
} if (counterEgFound) {
if (counterEgFound) { break;
break; }
} }
} }
} }
} }
} } // varNode in contain_pair_idx_map
} }
bool theory_str::in_contain_idx_map(expr * n) { bool theory_str::in_contain_idx_map(expr * n) {