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

fix build warnings for theory_str

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-12 08:06:24 -07:00
parent 07474e4887
commit 169295c9ba
1 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str.cpp
View file

@ -5552,8 +5552,8 @@ namespace smt {
for (; arg1_grdItor != groundedMap[arg1DeAlias].end(); arg1_grdItor++) { for (; arg1_grdItor != groundedMap[arg1DeAlias].end(); arg1_grdItor++) {
std::vector<expr*> ndVec; std::vector<expr*> ndVec;
ndVec.insert(ndVec.end(), arg0_grdItor->first.begin(), arg0_grdItor->first.end()); ndVec.insert(ndVec.end(), arg0_grdItor->first.begin(), arg0_grdItor->first.end());
int arg0VecSize = arg0_grdItor->first.size(); size_t arg0VecSize = arg0_grdItor->first.size();
int arg1VecSize = arg1_grdItor->first.size(); size_t arg1VecSize = arg1_grdItor->first.size();
if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) { if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
ndVec.pop_back(); ndVec.pop_back();
ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0])); ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
@ -5645,8 +5645,8 @@ namespace smt {
} }
bool theory_str::is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec) { bool theory_str::is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec) {
int strCnt = strVec.size(); size_t strCnt = strVec.size();
int subStrCnt = subStrVec.size(); size_t subStrCnt = subStrVec.size();
if (strCnt == 0 || subStrCnt == 0) { if (strCnt == 0 || subStrCnt == 0) {
return false; return false;
@ -5717,7 +5717,7 @@ namespace smt {
} }
// tail nodes // tail nodes
int tailIdx = i + subStrCnt - 1; size_t tailIdx = i + subStrCnt - 1;
zstring subStrTailVal; zstring subStrTailVal;
if (u.str.is_string(subStrVec[subStrCnt - 1], subStrTailVal)) { if (u.str.is_string(subStrVec[subStrCnt - 1], subStrTailVal)) {
zstring strTailVal; zstring strTailVal;
@ -8251,7 +8251,7 @@ namespace smt {
} }
} }
if (lId == -1) if (lId == -1)
lId = mLMap.size(); lId = static_cast<int>(mLMap.size());
for (std::set<expr*>::iterator itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) { for (std::set<expr*>::iterator itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) {
bool itorHasEqcValue = false; bool itorHasEqcValue = false;
get_eqc_value(*itor2, itorHasEqcValue); get_eqc_value(*itor2, itorHasEqcValue);
@ -8290,7 +8290,7 @@ namespace smt {
} }
} }
if (rId == -1) if (rId == -1)
rId = mRMap.size(); rId = static_cast<int>(mRMap.size());
for (itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) { for (itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) {
bool rHasEqcValue = false; bool rHasEqcValue = false;
get_eqc_value(*itor2, rHasEqcValue); get_eqc_value(*itor2, rHasEqcValue);
@ -9182,7 +9182,7 @@ namespace smt {
// ---------------------------------------------------------------------------------------- // ----------------------------------------------------------------------------------------
int len = atoi(lenStr.encode().c_str()); int len = atoi(lenStr.encode().c_str());
bool coverAll = false; bool coverAll = false;
svector<int_vector> options; vector<int_vector, true, long long> options;
int_vector base; int_vector base;
TRACE("str", tout TRACE("str", tout
@ -9234,9 +9234,9 @@ namespace smt {
for (long long i = l; i < h; i++) { for (long long i = l; i < h; i++) {
orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) ));
if (m_params.m_AggressiveValueTesting) { if (m_params.m_AggressiveValueTesting) {
literal l = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false);
ctx.mark_as_relevant(l); ctx.mark_as_relevant(lit);
ctx.force_phase(l); ctx.force_phase(lit);
} }
zstring aStr = gen_val_string(len, options[i - l]); zstring aStr = gen_val_string(len, options[i - l]);