From 1f594b190a8a00a167dcb234c43caf3d684d9d1c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sun, 14 Aug 2016 14:55:29 -0400 Subject: [PATCH] add theory_str::check_contain_by_eqc_val --- src/smt/theory_str.cpp | 169 ++++++++++++++++++++++++++++++++++++++++- src/smt/theory_str.h | 2 + 2 files changed, 170 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index aed46e868..18157e4be 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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 eqcConcats; + get_concats_in_eqc(substrAst, eqcConcats); + for (std::set::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 & 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 & varSet) { context & ctx = get_context(); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 61eefece8..476519e5c 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -379,6 +379,8 @@ namespace smt { expr * getMostLeftNodeInConcat(expr * node); expr * getMostRightNodeInConcat(expr * node); void get_var_in_eqc(expr * n, std::set & varSet); + void get_concats_in_eqc(expr * n, std::set & concats); + void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList); expr * eval_concat(expr * n1, expr * n2); // strRegex