Home
last modified time | relevance | path

Searched refs:sumHashMap (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Darith_theorem_producer.cpp476 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() local
1116 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 …]
H A Darith_theorem_producer3.cpp432 MonomMap sumHashMap; in canonCombineLikeTerms() local
458 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() local
1103 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 …]
H A Darith_theorem_producer_old.cpp433 MonomMap sumHashMap; in canonCombineLikeTerms() local
459 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() local
1153 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 …]
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.cpp2255 ExprMap<Rational> sumHashMap; in rewriteBVSub() local
4864 ExprMap<Rational> sumHashMap; in canonBVMult() local
5074 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() local
5569 ExprMap<Rational> sumHashMap; in canonBVPlus() local
5769 ExprMap<Rational> sumHashMap; in canonBVEQ() local
5905 if (k == sumHashMap.end()) { in canonBVEQ()
[all …]
H A Dbitvector_theorem_producer.h82 void getPlusTerms(const Expr& e, Rational& known_term, ExprMap<Rational>& sumHashMap);
83 Expr buildPlusTerm(int bv_size, Rational& known_term, ExprMap<Rational>& sumHashMap);