mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
add theory_str::check_contain_by_eqc_val
This commit is contained in:
Murphy Berzish
parent
6612971049
commit
1f594b190a
2 changed files with 170 additions and 1 deletions
|
|
@ -4141,8 +4141,161 @@ expr * theory_str::collect_eq_nodes(expr * n, expr_ref_vector & eqcSet) {
|
|||
return constStrNode;
|
||||
}
|
||||
|
||||
/*
|
||||
* Collect constant strings (from left to right) in an AST node.
|
||||
*/
|
||||
void theory_str::get_const_str_asts_in_node(expr * node, expr_ref_vector & astList) {
|
||||
ast_manager & m = get_manager();
|
||||
if (m_strutil.is_string(node)) {
|
||||
astList.push_back(node);
|
||||
//} else if (getNodeType(t, node) == my_Z3_Func) {
|
||||
} else if (is_app(node)) {
|
||||
app * func_app = to_app(node);
|
||||
unsigned int argCount = func_app->get_num_args();
|
||||
for (unsigned int i = 0; i < argCount; i++) {
|
||||
expr * argAst = func_app->get_arg(i);
|
||||
get_const_str_asts_in_node(argAst, astList);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) {
|
||||
NOT_IMPLEMENTED_YET(); // TODO NEXT
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
TRACE("t_str_detail", tout << "varNode = " << mk_pp(varNode, m) << ", constNode = " << mk_pp(constNode, m) << std::endl;);
|
||||
|
||||
expr_ref_vector litems(m);
|
||||
|
||||
// Modification from Z3str:
|
||||
// since we don't track containPairIdxMap any more,
|
||||
// we check each element of contains_map to see whether
|
||||
// either of its arguments are equal to varNode.
|
||||
// This could possibly be made faster if we had a map class that
|
||||
// let us use an expr_ref as a key.
|
||||
|
||||
expr_ref_vector::iterator itor1 = contains_map.begin();
|
||||
for (; itor1 != contains_map.end(); ++itor1) {
|
||||
expr * boolVar = *itor1;
|
||||
// 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);
|
||||
bool subStrHasEqcValue = false;
|
||||
expr * substrValue = get_eqc_value(substrAst, subStrHasEqcValue);
|
||||
if (substrValue != substrAst) {
|
||||
litems.push_back(ctx.mk_eq_atom(substrAst, substrValue));
|
||||
}
|
||||
|
||||
if (subStrHasEqcValue) {
|
||||
// subStr has an eqc constant value
|
||||
std::string subStrConst = m_strutil.get_string_constant_value(substrValue);
|
||||
|
||||
TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << std::endl;);
|
||||
|
||||
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 {
|
||||
// ------------------------------------------------------------------------------------------------
|
||||
// subStr doesn't have an eqc contant value
|
||||
// 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;
|
||||
}
|
||||
}
|
||||
if (counterEgFound) {
|
||||
TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
// add assertion
|
||||
if (implyR != NULL) {
|
||||
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 != NULL) {
|
||||
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) {
|
||||
|
|
@ -7485,6 +7638,20 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe
|
|||
} // fVarLenCountMap.find(...)
|
||||
}
|
||||
|
||||
void theory_str::get_concats_in_eqc(expr * n, std::set<expr*> & concats) {
|
||||
context & ctx = get_context();
|
||||
|
||||
expr * eqcNode = n;
|
||||
do {
|
||||
if (is_concat(to_app(eqcNode))) {
|
||||
concats.insert(eqcNode);
|
||||
}
|
||||
enode * e_eqc = ctx.get_enode(eqcNode);
|
||||
eqcNode = e_eqc->get_next()->get_owner();
|
||||
// eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
|
||||
} while (eqcNode != n);
|
||||
}
|
||||
|
||||
void theory_str::get_var_in_eqc(expr * n, std::set<expr*> & varSet) {
|
||||
context & ctx = get_context();
|
||||
|
||||
|
|
|
|||
|
|
@ -379,6 +379,8 @@ namespace smt {
|
|||
expr * getMostLeftNodeInConcat(expr * node);
|
||||
expr * getMostRightNodeInConcat(expr * node);
|
||||
void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
|
||||
void get_concats_in_eqc(expr * n, std::set<expr*> & concats);
|
||||
void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
|
||||
expr * eval_concat(expr * n1, expr * n2);
|
||||
|
||||
// strRegex
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue