Lines Matching refs:bFR
565 DdNode * bFR, * bGR; in extraBddSpaceFromFunction() local
567 bFR = Cudd_Regular( bF ); in extraBddSpaceFromFunction()
569 if ( cuddIsConstant(bFR) ) in extraBddSpaceFromFunction()
596 LevelF = dd->perm[bFR->index]; in extraBddSpaceFromFunction()
601 if ( bFR != bF ) in extraBddSpaceFromFunction()
603 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceFromFunction()
604 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceFromFunction()
608 bF0 = cuddE(bFR); in extraBddSpaceFromFunction()
609 bF1 = cuddT(bFR); in extraBddSpaceFromFunction()
740 DdNode * bRes, * bFR; in extraBddSpaceFromFunctionPos() local
743 bFR = Cudd_Regular(bF); in extraBddSpaceFromFunctionPos()
744 if ( cuddIsConstant(bFR) ) in extraBddSpaceFromFunctionPos()
756 if ( bFR != bF ) // bF is complemented in extraBddSpaceFromFunctionPos()
758 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceFromFunctionPos()
759 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceFromFunctionPos()
763 bF0 = cuddE(bFR); in extraBddSpaceFromFunctionPos()
764 bF1 = cuddT(bFR); in extraBddSpaceFromFunctionPos()
829 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); in extraBddSpaceFromFunctionPos()
840 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); in extraBddSpaceFromFunctionPos()
871 DdNode * bRes, * bFR; in extraBddSpaceFromFunctionNeg() local
874 bFR = Cudd_Regular(bF); in extraBddSpaceFromFunctionNeg()
875 if ( cuddIsConstant(bFR) ) in extraBddSpaceFromFunctionNeg()
887 if ( bFR != bF ) // bF is complemented in extraBddSpaceFromFunctionNeg()
889 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceFromFunctionNeg()
890 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceFromFunctionNeg()
894 bF0 = cuddE(bFR); in extraBddSpaceFromFunctionNeg()
895 bF1 = cuddT(bFR); in extraBddSpaceFromFunctionNeg()
960 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); in extraBddSpaceFromFunctionNeg()
971 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); in extraBddSpaceFromFunctionNeg()
1002 DdNode * bRes, * bFR; in extraBddSpaceCanonVars() local
1005 bFR = Cudd_Regular(bF); in extraBddSpaceCanonVars()
1006 if ( cuddIsConstant(bFR) ) in extraBddSpaceCanonVars()
1016 if ( bFR != bF ) // bF is complemented in extraBddSpaceCanonVars()
1018 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceCanonVars()
1019 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceCanonVars()
1023 bF0 = cuddE(bFR); in extraBddSpaceCanonVars()
1024 bF1 = cuddT(bFR); in extraBddSpaceCanonVars()
1046 bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); in extraBddSpaceCanonVars()
1085 DdNode * bFR, * bF0, * bF1; in extraBddSpaceEquationsPos() local
1089 bFR = Cudd_Regular(bF); in extraBddSpaceEquationsPos()
1090 if ( bFR != bF ) // bF is complemented in extraBddSpaceEquationsPos()
1092 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceEquationsPos()
1093 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceEquationsPos()
1097 bF0 = cuddE(bFR); in extraBddSpaceEquationsPos()
1098 bF1 = cuddT(bFR); in extraBddSpaceEquationsPos()
1109 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); in extraBddSpaceEquationsPos()
1173 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); in extraBddSpaceEquationsPos()
1215 DdNode * bFR, * bF0, * bF1; in extraBddSpaceEquationsNeg() local
1219 bFR = Cudd_Regular(bF); in extraBddSpaceEquationsNeg()
1220 if ( bFR != bF ) // bF is complemented in extraBddSpaceEquationsNeg()
1222 bF0 = Cudd_Not( cuddE(bFR) ); in extraBddSpaceEquationsNeg()
1223 bF1 = Cudd_Not( cuddT(bFR) ); in extraBddSpaceEquationsNeg()
1227 bF0 = cuddE(bFR); in extraBddSpaceEquationsNeg()
1228 bF1 = cuddT(bFR); in extraBddSpaceEquationsNeg()
1245 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); in extraBddSpaceEquationsNeg()
1303 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); in extraBddSpaceEquationsNeg()