mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

theory_str refactor: check_contain_by_eqc_val uses contain_pair_idx_map

Browse source
This commit is contained in:
Murphy Berzish 2017-02-14 15:19:03 -05:00
parent 5ca4f2a1c8
commit 52eaae9da0
1 changed files with 113 additions and 111 deletions
Download patch file Download diff file Expand all files Collapse all files

224
src/smt/theory_str.cpp
View file

@ -4842,130 +4842,134 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) {
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);
expr * strAst = containsApp->get_arg(0);
expr * substrAst = containsApp->get_arg(1);
// we only want to inspect the Contains terms where either of strAst or substrAst
// are equal to varNode.
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) {
TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;);
continue;
}
TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;);
// varEqcNode is str
if (strAst == varNode) {
expr_ref implyR(m);
litems.reset();
if (strAst != constNode) {
litems.push_back(ctx.mk_eq_atom(strAst, constNode));
} }
std::string strConst = m_strutil.get_string_constant_value(constNode); // boolVar is actually a Contains term
bool subStrHasEqcValue = false; app * containsApp = to_app(boolVar);
expr * substrValue = get_eqc_value(substrAst, subStrHasEqcValue);
if (substrValue != substrAst) { // we only want to inspect the Contains terms where either of strAst or substrAst
litems.push_back(ctx.mk_eq_atom(substrAst, substrValue)); // are equal to varNode.
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) {
TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;);
continue;
} }
TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;);
if (subStrHasEqcValue) { // varEqcNode is str
// subStr has an eqc constant value if (strAst == varNode) {
std::string subStrConst = m_strutil.get_string_constant_value(substrValue); expr_ref implyR(m);
litems.reset();
TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << std::endl;); if (strAst != constNode) {
litems.push_back(ctx.mk_eq_atom(strAst, constNode));
if (strConst.find(subStrConst) != std::string::npos) {
//implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx));
implyR = boolVar;
} else {
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
implyR = m.mk_not(boolVar);
} }
} else { std::string strConst = m_strutil.get_string_constant_value(constNode);
// ------------------------------------------------------------------------------------------------ bool subStrHasEqcValue = false;
// subStr doesn't have an eqc contant value expr * substrValue = get_eqc_value(substrAst, subStrHasEqcValue);
// however, subStr equals to some concat(arg_1, arg_2, ..., arg_n) if (substrValue != substrAst) {
// if arg_j is a constant and is not a part of the strConst, it's sure that the contains is false litems.push_back(ctx.mk_eq_atom(substrAst, substrValue));
// ** This check is needed here because the "strConst" and "strAst" may not be in a same eqc yet }
// ------------------------------------------------------------------------------------------------
// collect eqc concat if (subStrHasEqcValue) {
std::set<expr*> eqcConcats; // subStr has an eqc constant value
get_concats_in_eqc(substrAst, eqcConcats); std::string subStrConst = m_strutil.get_string_constant_value(substrValue);
for (std::set<expr*>::iterator concatItor = eqcConcats.begin();
concatItor != eqcConcats.end(); concatItor++) { TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << std::endl;);
expr_ref_vector constList(m);
bool counterEgFound = false; if (strConst.find(subStrConst) != std::string::npos) {
// get constant strings in concat //implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx));
expr * aConcat = *concatItor; implyR = boolVar;
get_const_str_asts_in_node(aConcat, constList); } else {
for (expr_ref_vector::iterator cstItor = constList.begin(); //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
cstItor != constList.end(); cstItor++) { implyR = m.mk_not(boolVar);
std::string pieceStr = m_strutil.get_string_constant_value(*cstItor); }
if (strConst.find(pieceStr) == std::string::npos) { } else {
counterEgFound = true; // ------------------------------------------------------------------------------------------------
if (aConcat != substrAst) { // subStr doesn't have an eqc contant value
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); // however, subStr equals to some concat(arg_1, arg_2, ..., arg_n)
// if arg_j is a constant and is not a part of the strConst, it's sure that the contains is false
// ** This check is needed here because the "strConst" and "strAst" may not be in a same eqc yet
// ------------------------------------------------------------------------------------------------
// collect eqc concat
std::set<expr*> eqcConcats;
get_concats_in_eqc(substrAst, eqcConcats);
for (std::set<expr*>::iterator concatItor = eqcConcats.begin();
concatItor != eqcConcats.end(); concatItor++) {
expr_ref_vector constList(m);
bool counterEgFound = false;
// get constant strings in concat
expr * aConcat = *concatItor;
get_const_str_asts_in_node(aConcat, constList);
for (expr_ref_vector::iterator cstItor = constList.begin();
cstItor != constList.end(); cstItor++) {
std::string pieceStr = m_strutil.get_string_constant_value(*cstItor);
if (strConst.find(pieceStr) == std::string::npos) {
counterEgFound = true;
if (aConcat != substrAst) {
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
}
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
implyR = m.mk_not(boolVar);
break;
} }
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx)); }
implyR = m.mk_not(boolVar); if (counterEgFound) {
TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;);
break; break;
} }
} }
if (counterEgFound) { }
TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;); // add assertion
break; if (implyR) {
expr_ref implyLHS(mk_and(litems), m);
assert_implication(implyLHS, implyR);
}
}
// varEqcNode is subStr
else if (substrAst == varNode) {
expr_ref implyR(m);
litems.reset();
if (substrAst != constNode) {
litems.push_back(ctx.mk_eq_atom(substrAst, constNode));
}
bool strHasEqcValue = false;
expr * strValue = get_eqc_value(strAst, strHasEqcValue);
if (strValue != strAst) {
litems.push_back(ctx.mk_eq_atom(strAst, strValue));
}
if (strHasEqcValue) {
std::string strConst = m_strutil.get_string_constant_value(strValue);
std::string subStrConst = m_strutil.get_string_constant_value(constNode);
if (strConst.find(subStrConst) != std::string::npos) {
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_true(ctx));
implyR = boolVar;
} else {
// implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
implyR = m.mk_not(boolVar);
} }
} }
}
// add assertion
if (implyR) {
expr_ref implyLHS(mk_and(litems), m);
assert_implication(implyLHS, implyR);
}
}
// varEqcNode is subStr
else if (substrAst == varNode) {
expr_ref implyR(m);
litems.reset();
if (substrAst != constNode) { // add assertion
litems.push_back(ctx.mk_eq_atom(substrAst, constNode)); if (implyR) {
} expr_ref implyLHS(mk_and(litems), m);
bool strHasEqcValue = false; assert_implication(implyLHS, implyR);
expr * strValue = get_eqc_value(strAst, strHasEqcValue);
if (strValue != strAst) {
litems.push_back(ctx.mk_eq_atom(strAst, strValue));
}
if (strHasEqcValue) {
std::string strConst = m_strutil.get_string_constant_value(strValue);
std::string subStrConst = m_strutil.get_string_constant_value(constNode);
if (strConst.find(subStrConst) != std::string::npos) {
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_true(ctx));
implyR = boolVar;
} else {
// implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
implyR = m.mk_not(boolVar);
} }
} }
} // for (itor1 : contains_map)
// add assertion } // if varNode in contain_pair_idx_map
if (implyR) {
expr_ref implyLHS(mk_and(litems), m);
assert_implication(implyLHS, implyR);
}
}
} // for (itor1 : contains_map)
} }
void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass) { void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass) {
@ -5782,7 +5786,6 @@ void theory_str::compute_contains(std::map<expr*, expr*> & varAliasMap,
} }
bool theory_str::can_concat_eq_str(expr * concat, std::string str) { bool theory_str::can_concat_eq_str(expr * concat, std::string str) {
// TODO this method could use some traces and debugging info
int strLen = str.length(); int strLen = str.length();
if (is_concat(to_app(concat))) { if (is_concat(to_app(concat))) {
ptr_vector<expr> args; ptr_vector<expr> args;
@ -5834,7 +5837,6 @@ bool theory_str::can_concat_eq_str(expr * concat, std::string str) {
} }
bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) { bool theory_str::can_concat_eq_concat(expr * concat1, expr * concat2) {
// TODO this method could use some traces and debugging info
if (is_concat(to_app(concat1)) && is_concat(to_app(concat2))) { if (is_concat(to_app(concat1)) && is_concat(to_app(concat2))) {
{ {
// Suppose concat1 = (Concat X Y) and concat2 = (Concat M N). // Suppose concat1 = (Concat X Y) and concat2 = (Concat M N).