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

theory_str cleanup

Browse source
This commit is contained in:
Murphy Berzish 2017-02-13 17:15:13 -05:00
parent e699f25889
commit 5ca4f2a1c8
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -4576,7 +4576,8 @@ void theory_str::unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr) {
std::string regStrValue = m_strutil.get_string_constant_value(strInStr2RegFunc); std::string regStrValue = m_strutil.get_string_constant_value(strInStr2RegFunc);
int strLen = strValue.length(); int strLen = strValue.length();
int regStrLen = regStrValue.length(); int regStrLen = regStrValue.length();
int cnt = strLen / regStrLen; // TODO prevent DIV/0 on regStrLen SASSERT(regStrLen != 0); // this should never occur -- the case for empty string is handled elsewhere
int cnt = strLen / regStrLen;
expr_ref implyL(ctx.mk_eq_atom(unrollFunc, eqConstStr), m); expr_ref implyL(ctx.mk_eq_atom(unrollFunc, eqConstStr), m);
expr_ref implyR1(ctx.mk_eq_atom(oriCnt, mk_int(cnt)), m); expr_ref implyR1(ctx.mk_eq_atom(oriCnt, mk_int(cnt)), m);
@ -7446,7 +7447,7 @@ void theory_str::classify_ast_by_type(expr * node, std::map<expr*, int> & varMap
varMap[node] = 1; varMap[node] = 1;
} }
// check whether the node is a function that we want to inspect // check whether the node is a function that we want to inspect
else if (is_app(node)) { // TODO else if (is_app(node)) {
app * aNode = to_app(node); app * aNode = to_app(node);
if (is_strlen(aNode)) { if (is_strlen(aNode)) {
// Length // Length