Home
last modified time | relevance | path

Searched refs:likeTerms (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.h58 ExprMap<Rational> & likeTerms,
66 ExprMap<Rational> & likeTerms,
72 const ExprMap<Rational> & likeTerms,
451 int sameKidCheck(const Expr& e, ExprMap<int>& likeTerms);
H A Dbitvector_theorem_producer.cpp2994 ExprMap<int> likeTerms; in bitwiseFlatten() local
3015 likeTerms.erase(t); in bitwiseFlatten()
3161 ExprMap<int>& likeTerms) { in sameKidCheck() argument
3169 if(it==likeTerms.end()) { in sameKidCheck()
3173 if(it0!=likeTerms.end()) in sameKidCheck()
3180 if(negIt!=likeTerms.end()) in sameKidCheck()
3699 if(it!=likeTerms.end()) in collectOneTermOfPlus()
3704 if (!likeTerms.empty()) { in collectOneTermOfPlus()
3708 if (it!= likeTerms.end()) { in collectOneTermOfPlus()
3726 likeTerms.clear(); in collectLikeTermsOfPlus()
[all …]