Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.h504 const std::vector<Theorem>& t2BitExtractThms,
H A Dbitvector_theorem_producer.cpp1257 const std::vector<Theorem>& t2BitExtractThms, in bitExtractBVPlus() argument
1266 …CHECK_SOUND(bitPos+1 == (int)t1BitExtractThms.size() && bitPos+1 == (int)t2BitExtractThms.size(), … in bitExtractBVPlus()
1271 std::vector<Theorem>::const_iterator j = t2BitExtractThms.begin(); in bitExtractBVPlus()
1281 const Expr& t2_iBit = (t2BitExtractThms[bitPos]).getRHS(); in bitExtractBVPlus()
1283 const Expr carry_iBit = computeCarry(t1BitExtractThms, t2BitExtractThms, bitPos); in bitExtractBVPlus()
1306 const std::vector<Theorem>& t2BitExtractThms, in computeCarry() argument
1314 const Expr& t2Thm = t2BitExtractThms[bitPos].getRHS(); in computeCarry()
1319 const Expr& t2Thm = t2BitExtractThms[bitPos-1].getRHS(); in computeCarry()
1324 computeCarry(t1BitExtractThms,t2BitExtractThms,bitPos-1); in computeCarry()