Searched refs:MSB1 (Results 1 – 6 of 6) sorted by relevance
1137 #define MSB1(u32) MSB1W(u32) //!< Most significant byte of 2nd rank of \a u32. macro
476 const Expr MSB1 = topBit1.getRHS(); in signBVLTRule() local490 if(MSB1.getKind() == BVCONST) b1 = d_theoryBitvector->computeBVConst(MSB1); in signBVLTRule()497 const Expr MSB1isZero = MSB1.eqExpr(bvZero()); in signBVLTRule()498 const Expr MSB1isOne = MSB1.eqExpr(bvOne()); in signBVLTRule()589 Expr k1 = MSB0.eqExpr(MSB1); in signBVLTRule()
1598 const Expr MSB1 = newBVExtractExpr(thm0RHS[1],bvlength-1,bvlength-1); in rewriteBV() local1602 const Theorem topBit1 = rewriteBV(MSB1, cache, 2); in rewriteBV()