00001
00021 #include "cutInt.h"
00022
00023
00024
00025
00026
00027
00028
00032
00033 extern int nTotal = 0;
00034 extern int nGood = 0;
00035 extern int nEqual = 0;
00036
00040
00052 static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
00053 {
00054 unsigned uPhase = 0;
00055 int i, k;
00056 for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
00057 {
00058 if ( k == (int)pCut1->nLeaves )
00059 break;
00060 if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
00061 continue;
00062 assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
00063 uPhase |= (1 << i);
00064 k++;
00065 }
00066 return uPhase;
00067 }
00068
00081 void Cut_TruthNCanonicize( Cut_Cut_t * pCut )
00082 {
00083 unsigned uTruth;
00084 unsigned * uCanon2;
00085 char * pPhases2;
00086 assert( pCut->nVarsMax < 6 );
00087
00088
00089 uTruth = *Cut_CutReadTruth(pCut);
00090
00091
00092 Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
00093
00094
00095
00096 pCut->uCanon0 = uCanon2[0];
00097 pCut->Num0 = pPhases2[0];
00098
00099
00100 uTruth = ~*Cut_CutReadTruth(pCut);
00101
00102
00103 Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
00104
00105
00106
00107 pCut->uCanon1 = uCanon2[0];
00108 pCut->Num1 = pPhases2[0];
00109 }
00110
00122 void Cut_TruthComputeOld( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
00123 {
00124 static unsigned uTruth0[8], uTruth1[8];
00125 int nTruthWords = Cut_TruthWords( pCut->nVarsMax );
00126 unsigned * pTruthRes;
00127 int i, uPhase;
00128
00129
00130 uPhase = Cut_TruthPhase( pCut, pCut0 );
00131 Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut0), uPhase, uTruth0 );
00132 if ( fCompl0 )
00133 {
00134 for ( i = 0; i < nTruthWords; i++ )
00135 uTruth0[i] = ~uTruth0[i];
00136 }
00137
00138
00139 uPhase = Cut_TruthPhase( pCut, pCut1 );
00140 Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut1), uPhase, uTruth1 );
00141 if ( fCompl1 )
00142 {
00143 for ( i = 0; i < nTruthWords; i++ )
00144 uTruth1[i] = ~uTruth1[i];
00145 }
00146
00147
00148 pTruthRes = Cut_CutReadTruth(pCut);
00149
00150 if ( pCut->fCompl )
00151 {
00152 for ( i = 0; i < nTruthWords; i++ )
00153 pTruthRes[i] = ~(uTruth0[i] & uTruth1[i]);
00154 }
00155 else
00156 {
00157 for ( i = 0; i < nTruthWords; i++ )
00158 pTruthRes[i] = uTruth0[i] & uTruth1[i];
00159 }
00160 }
00161
00173 void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
00174 {
00175
00176 if ( fCompl0 )
00177 Extra_TruthNot( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
00178 else
00179 Extra_TruthCopy( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
00180 Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut0) );
00181
00182 if ( fCompl1 )
00183 Extra_TruthNot( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
00184 else
00185 Extra_TruthCopy( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
00186 Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut1) );
00187
00188 if ( pCut->fCompl )
00189 Extra_TruthNand( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
00190 else
00191 Extra_TruthAnd( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
00192
00193
00194
00195
00196 if ( !p->pParams->fFancy )
00197 return;
00198
00199 if ( pCut->nLeaves != 7 )
00200 return;
00201
00202
00203 nTotal++;
00204
00205
00206
00207
00208 if ( Extra_TruthMinCofSuppOverlap( Cut_CutReadTruth(pCut), pCut->nVarsMax, NULL ) <= 4 )
00209 nGood++;
00210
00211
00212
00213
00214
00215
00216
00217
00218 }
00219
00220
00221
00225
00226