Searched refs:sumHashMap (Results 1 – 5 of 5) sorted by relevance
476 if (i == sumHashMap.end()) sumHashMap[newMul] = r; in canonCombineLikeTerms()490 if (i == sumHashMap.end()) sumHashMap[multExpr(rat(1), mul)] = 1; in canonCombineLikeTerms()504 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end(); in canonCombineLikeTerms()1100 ExprMap<Rational> sumHashMap; in canonComboLikeTerms() local1116 if(0 == sumHashMap.count((*i))) in canonComboLikeTerms()1117 sumHashMap[*i] = 1; in canonComboLikeTerms()1119 sumHashMap[*i] += 1; in canonComboLikeTerms()1122 if(0 == sumHashMap.count((*i)[1])) in canonComboLikeTerms()1125 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational(); in canonComboLikeTerms()1131 ExprMap<Rational>::iterator j = sumHashMap.begin(); in canonComboLikeTerms()[all …]
432 MonomMap sumHashMap; in canonCombineLikeTerms() local458 if (i == sumHashMap.end()) { in canonCombineLikeTerms()469 if (i == sumHashMap.end()) { in canonCombineLikeTerms()470 sumHashMap[mul] = 1; in canonCombineLikeTerms()482 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end(); in canonCombineLikeTerms()1087 ExprMap<Rational> sumHashMap; in canonComboLikeTerms() local1103 if(0 == sumHashMap.count((*i))) in canonComboLikeTerms()1104 sumHashMap[*i] = 1; in canonComboLikeTerms()1106 sumHashMap[*i] += 1; in canonComboLikeTerms()1112 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational(); in canonComboLikeTerms()[all …]
433 MonomMap sumHashMap; in canonCombineLikeTerms() local459 if (i == sumHashMap.end()) { in canonCombineLikeTerms()470 if (i == sumHashMap.end()) { in canonCombineLikeTerms()471 sumHashMap[mul] = 1; in canonCombineLikeTerms()483 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end(); in canonCombineLikeTerms()1137 ExprMap<Rational> sumHashMap; in canonComboLikeTerms() local1153 if(0 == sumHashMap.count((*i))) in canonComboLikeTerms()1154 sumHashMap[*i] = 1; in canonComboLikeTerms()1156 sumHashMap[*i] += 1; in canonComboLikeTerms()1162 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational(); in canonComboLikeTerms()[all …]
2255 ExprMap<Rational> sumHashMap; in rewriteBVSub() local4864 ExprMap<Rational> sumHashMap; in canonBVMult() local5074 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff; in getPlusTerms()5087 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff; in getPlusTerms()5099 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff; in getPlusTerms()5162 sumHashMap[ kid] = sumHashMap[ kid] + coeff; in getPlusTerms()5290 ExprMap<Rational> sumHashMap; in chopConcat() local5569 ExprMap<Rational> sumHashMap; in canonBVPlus() local5769 ExprMap<Rational> sumHashMap; in canonBVEQ() local5905 if (k == sumHashMap.end()) { in canonBVEQ()[all …]
82 void getPlusTerms(const Expr& e, Rational& known_term, ExprMap<Rational>& sumHashMap);83 Expr buildPlusTerm(int bv_size, Rational& known_term, ExprMap<Rational>& sumHashMap);