fraImp.c 23.3 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [fraImp.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [New FRAIG package.]

  Synopsis    [Detecting and proving implications.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 30, 2007.]

  Revision    [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]

***********************************************************************/

#include "fra.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Counts the number of 1s in each siminfo of each node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
{
    unsigned * pSim;
    int k, Counter = 0;
    pSim = Fra_ObjSim( p, Node );
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        Counter += Aig_WordCountOnes( pSim[k] );
    return Counter;
}

/**Function*************************************************************

  Synopsis    [Counts the number of 1s in each siminfo of each node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
66
static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
Alan Mishchenko committed
67 68
{
    Aig_Obj_t * pObj;
Alan Mishchenko committed
69
    int i, * pnBits; 
Alan Mishchenko committed
70
    pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
Alan Mishchenko committed
71
    memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Alan Mishchenko committed
72
    Aig_ManForEachObj( p->pAig, pObj, i )
Alan Mishchenko committed
73
        pnBits[i] = Fra_SmlCountOnesOne( p, i );
Alan Mishchenko committed
74 75 76 77 78
    return pnBits;
}

/**Function*************************************************************

Alan Mishchenko committed
79
  Synopsis    [Returns 1 if implications holds.]
Alan Mishchenko committed
80 81 82 83 84 85 86 87

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
88
static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
Alan Mishchenko committed
89 90
{
    unsigned * pSimL, * pSimR;
Alan Mishchenko committed
91
    int k;
Alan Mishchenko committed
92 93
    pSimL = Fra_ObjSim( p, Left );
    pSimR = Fra_ObjSim( p, Right );
Alan Mishchenko committed
94 95 96 97
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        if ( pSimL[k] & ~pSimR[k] )
            return 0;
    return 1;
Alan Mishchenko committed
98 99 100 101
}

/**Function*************************************************************

Alan Mishchenko committed
102
  Synopsis    [Counts the number of 1s in the complement of the implication.]
Alan Mishchenko committed
103 104 105 106 107 108 109 110

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
111
static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
Alan Mishchenko committed
112 113
{
    unsigned * pSimL, * pSimR;
Alan Mishchenko committed
114
    int k, Counter = 0;
Alan Mishchenko committed
115 116
    pSimL = Fra_ObjSim( p, Left );
    pSimR = Fra_ObjSim( p, Right );
Alan Mishchenko committed
117 118 119
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
    return Counter;
Alan Mishchenko committed
120 121 122 123
}

/**Function*************************************************************

Alan Mishchenko committed
124
  Synopsis    [Computes the complement of the implication.]
Alan Mishchenko committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
{
    unsigned * pSimL, * pSimR;
    int k;
    pSimL = Fra_ObjSim( p, Left );
    pSimR = Fra_ObjSim( p, Right );
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        pResult[k] |= pSimL[k] & ~pSimR[k];
}

/**Function*************************************************************

Alan Mishchenko committed
145 146 147 148 149 150 151 152 153
  Synopsis    [Returns the array of nodes sorted by the number of 1s.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
154
Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
Alan Mishchenko committed
155 156 157 158
{
    Aig_Obj_t * pObj;
    Vec_Ptr_t * vNodes;
    int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
Alan Mishchenko committed
159
    assert( p->nWordsTotal > 0 );
Alan Mishchenko committed
160
    // count 1s in each node's siminfo
Alan Mishchenko committed
161
    pnBits = Fra_SmlCountOnes( p );
Alan Mishchenko committed
162 163
    // count number of nodes having that many 1s
    nNodes = 0;
Alan Mishchenko committed
164
    nBits = p->nWordsTotal * 32;
Alan Mishchenko committed
165
    pnNodes = ABC_ALLOC( int, nBits + 1 );
Alan Mishchenko committed
166
    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
Alan Mishchenko committed
167 168 169
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( i == 0 ) continue;
Alan Mishchenko committed
170 171 172
        // skip non-PI and non-internal nodes
        if ( fLatchCorr )
        {
173
            if ( !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
174 175 176 177
                continue;
        }
        else
        {
178
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
179 180 181 182 183 184
                continue;
        }
        // skip nodes participating in the classes
//        if ( Fra_ClassObjRepr(pObj) )
//            continue;
        assert( pnBits[i] <= nBits ); // "<" because of normalized info
Alan Mishchenko committed
185 186 187 188
        pnNodes[pnBits[i]]++;
        nNodes++;
    }
    // allocate memory for all the nodes
Alan Mishchenko committed
189
    pMemory = ABC_ALLOC( int, nNodes + nBits + 1 );  
Alan Mishchenko committed
190
    // markup the memory for each node
Alan Mishchenko committed
191
    vNodes = Vec_PtrAlloc( nBits + 1 );
Alan Mishchenko committed
192
    Vec_PtrPush( vNodes, pMemory );
Alan Mishchenko committed
193
    for ( i = 1; i <= nBits; i++ )
Alan Mishchenko committed
194
    {
Alan Mishchenko committed
195
        pMemory += pnNodes[i-1] + 1;
Alan Mishchenko committed
196 197 198
        Vec_PtrPush( vNodes, pMemory );
    }
    // add the nodes
Alan Mishchenko committed
199
    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
Alan Mishchenko committed
200 201 202
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( i == 0 ) continue;
Alan Mishchenko committed
203 204 205
        // skip non-PI and non-internal nodes
        if ( fLatchCorr )
        {
206
            if ( !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
207 208 209 210
                continue;
        }
        else
        {
211
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
212 213 214 215 216
                continue;
        }
        // skip nodes participating in the classes
//        if ( Fra_ClassObjRepr(pObj) )
//            continue;
217
        pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] );
Alan Mishchenko committed
218 219 220 221
        pMemory[ pnNodes[pnBits[i]]++ ] = i;
    }
    // add 0s in the end
    nTotal = 0;
222
    Vec_PtrForEachEntry( int *, vNodes, pMemory, i )
Alan Mishchenko committed
223 224 225 226
    {
        pMemory[ pnNodes[i]++ ] = 0;
        nTotal += pnNodes[i];
    }
Alan Mishchenko committed
227
    assert( nTotal == nNodes + nBits + 1 );
Alan Mishchenko committed
228 229
    ABC_FREE( pnNodes );
    ABC_FREE( pnBits );
Alan Mishchenko committed
230 231 232 233 234
    return vNodes;
}

/**Function*************************************************************

Alan Mishchenko committed
235
  Synopsis    [Returns the array of implications with the highest cost.]
Alan Mishchenko committed
236 237 238 239 240 241 242 243

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
244
Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
Alan Mishchenko committed
245
{
Alan Mishchenko committed
246 247 248 249
    Vec_Int_t * vImpsNew;
    int * pCostCount, nImpCount, Imp, i, c;
    assert( Vec_IntSize(vImps) >= nImpLimit );
    // count how many implications have each cost
Alan Mishchenko committed
250
    pCostCount = ABC_ALLOC( int, nCostMax + 1 );
Alan Mishchenko committed
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
    memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
    for ( i = 0; i < Vec_IntSize(vImps); i++ )
    {
        assert( pCosts[i] <= nCostMax );
        pCostCount[ pCosts[i] ]++;
    }
    assert( pCostCount[0] == 0 );
    // select the bound on the cost (above this bound, implication will be included)
    nImpCount = 0;
    for ( c = nCostMax; c > 0; c-- )
    {
        nImpCount += pCostCount[c];
        if ( nImpCount >= nImpLimit )
            break;
    }
//    printf( "Cost range >= %d.\n", c );
    // collect implications with the given costs
    vImpsNew = Vec_IntAlloc( nImpLimit );
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        if ( pCosts[i] < c )
            continue;
        Vec_IntPush( vImpsNew, Imp );
        if ( Vec_IntSize( vImpsNew ) == nImpLimit )
            break;
    }
Alan Mishchenko committed
277
    ABC_FREE( pCostCount );
Alan Mishchenko committed
278 279
    if ( pCostRange )
        *pCostRange = c;
Alan Mishchenko committed
280
    return vImpsNew;
Alan Mishchenko committed
281 282 283 284 285 286 287 288 289 290 291 292 293 294 295
}

/**Function*************************************************************

  Synopsis    [Compares two implications using their largest ID.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
{
296 297
    int Max1 = Abc_MaxInt( pImp1[0], pImp1[1] );
    int Max2 = Abc_MaxInt( pImp2[0], pImp2[1] );
Alan Mishchenko committed
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
    if ( Max1 < Max2 )
        return -1;
    if ( Max1 > Max2  )
        return 1;
    return 0; 
}

/**Function*************************************************************

  Synopsis    [Derives implication candidates.]

  Description [Implication candidates have the property that 
  (1) they hold using sequential simulation information
  (2) they do not hold using combinational simulation information
  (3) they have as high expressive power as possible (heuristically)
Alan Mishchenko committed
313 314
      that is, they are easy to disprove combinationally
      meaning they cover relatively larger sequential subspace.]
Alan Mishchenko committed
315
               
Alan Mishchenko committed
316
  SideEffects []
Alan Mishchenko committed
317 318 319 320

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
321
Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
Alan Mishchenko committed
322
{
Alan Mishchenko committed
323 324
    int nSimWords = 64;
    Fra_Sml_t * pSeq, * pComb;
Alan Mishchenko committed
325 326
    Vec_Int_t * vImps, * vTemp;
    Vec_Ptr_t * vNodes;
Alan Mishchenko committed
327 328
    int * pImpCosts, * pNodesI, * pNodesK;
    int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
Alan Mishchenko committed
329
    int CostMin = ABC_INFINITY, CostMax = 0;
330
    int i, k, Imp, CostRange;
331
    abctime clk = Abc_Clock();
Alan Mishchenko committed
332
    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
Alan Mishchenko committed
333 334
    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
    // normalize both managers
335 336
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
Alan Mishchenko committed
337
    // get the nodes sorted by the number of 1s
Alan Mishchenko committed
338 339 340 341
    vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
    // count the total number of implications
    for ( k = nSimWords * 32; k > 0; k-- )
    for ( i = k - 1; i > 0; i-- )
342 343
    for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
    for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
Alan Mishchenko committed
344 345
        nImpsTotal++;

Alan Mishchenko committed
346
    // compute implications and their costs
Alan Mishchenko committed
347
    pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
Alan Mishchenko committed
348
    vImps = Vec_IntAlloc( nImpMaxLimit );
Alan Mishchenko committed
349 350
    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
        for ( i = k - 1; i > 0; i-- )
Alan Mishchenko committed
351
        {
Alan Mishchenko committed
352 353
            // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)

354 355
            for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
            for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
Alan Mishchenko committed
356
            {
Alan Mishchenko committed
357 358
                nImpsTried++;
                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
Alan Mishchenko committed
359
                {
Alan Mishchenko committed
360 361
                    nImpsNonSeq++;
                    continue;
Alan Mishchenko committed
362
                }
Alan Mishchenko committed
363 364 365 366 367 368
                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
                {
                    nImpsComb++;
                    continue;
                }
                nImpsCollected++;
Alan Mishchenko committed
369
                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
Alan Mishchenko committed
370
                pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
371 372
                CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
                CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
Alan Mishchenko committed
373
                Vec_IntPush( vImps, Imp );
Alan Mishchenko committed
374 375
                if ( Vec_IntSize(vImps) == nImpMaxLimit )
                    goto finish;
Alan Mishchenko committed
376
            } 
Alan Mishchenko committed
377 378
        }
finish:
Alan Mishchenko committed
379 380 381 382
    Fra_SmlStop( pComb );
    Fra_SmlStop( pSeq );

    // select implications with the highest cost
Alan Mishchenko committed
383
    CostRange = CostMin;
Alan Mishchenko committed
384 385
    if ( Vec_IntSize(vImps) > nImpUseLimit )
    {
Alan Mishchenko committed
386
        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
Alan Mishchenko committed
387 388
        Vec_IntFree( vTemp );  
    }
Alan Mishchenko committed
389 390

    // dealloc
Alan Mishchenko committed
391 392 393 394 395
    ABC_FREE( pImpCosts ); 
    {
    void * pTemp = Vec_PtrEntry(vNodes, 0);
    ABC_FREE( pTemp );
    }
Alan Mishchenko committed
396
    Vec_PtrFree( vNodes );
Alan Mishchenko committed
397
    // reorder implications topologically
Alan Mishchenko committed
398 399
    qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
            (int (*)(const void *, const void *)) Sml_CompareMaxId );
Alan Mishchenko committed
400 401
if ( p->pPars->fVerbose )
{
Alan Mishchenko committed
402 403 404 405
printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
       CostMin, CostRange, CostMax );
406
ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
407
}
Alan Mishchenko committed
408 409 410
    return vImps;
}

Alan Mishchenko committed
411

Alan Mishchenko committed
412 413 414 415 416 417 418
// the following three procedures are called to 
// - add implications to the SAT solver
// - check implications using the SAT solver
// - refine implications using after a cex is generated

/**Function*************************************************************

Alan Mishchenko committed
419
  Synopsis    [Add implication clauses to the SAT solver.]
Alan Mishchenko committed
420

Alan Mishchenko committed
421
  Description [Note that implications should be checked in the first frame!]
Alan Mishchenko committed
422 423 424 425 426 427
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
428
void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
Alan Mishchenko committed
429 430 431 432 433
{
    sat_solver * pSat = p->pSat;
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftF, * pRightF;
    int pLits[2], Imp, Left, Right, i, f, status;
Alan Mishchenko committed
434
    int fComplL, fComplR;
Alan Mishchenko committed
435 436 437
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        // get the corresponding nodes
Alan Mishchenko committed
438 439
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
Alan Mishchenko committed
440 441 442 443 444 445 446 447 448 449 450
        // check if all the nodes are present
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
            {
                Vec_IntWriteEntry( vImps, i, 0 );
                break;
            }
451
        } 
Alan Mishchenko committed
452 453
        if ( f < p->pPars->nFramesK )
            continue;
Alan Mishchenko committed
454 455 456 457 458 459 460
        // add constraints in each timeframe
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            // get the corresponding SAT numbers
Alan Mishchenko committed
461 462
            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
Alan Mishchenko committed
463 464
            assert( Left > 0  && Left < p->nSatVars );
            assert( Right > 0 && Right < p->nSatVars );
Alan Mishchenko committed
465 466 467
            // get the complemented attributes
            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
Alan Mishchenko committed
468
            // get the constraint
Alan Mishchenko committed
469 470 471
            // L => R      L' v R     (complement = L & R')
            pLits[0] = 2 * Left  + !fComplL;
            pLits[1] = 2 * Right +  fComplR;
472
            // add constraint to solver
Alan Mishchenko committed
473 474 475 476 477 478 479 480 481 482 483 484 485 486
            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
            {
                sat_solver_delete( pSat );
                p->pSat = NULL;
                return;
            }
        }
    }
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
        p->pSat = NULL;
    }
Alan Mishchenko committed
487 488 489
//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
    Fra_ImpCompactArray( vImps );
//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
Alan Mishchenko committed
490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505
}

/**Function*************************************************************

  Synopsis    [Check implications for the node (if they are present).]

  Description [Returns the new position in the array.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
{
    Aig_Obj_t * pLeft, * pRight;
Alan Mishchenko committed
506
    Aig_Obj_t * pLeftF, * pRightF;
Alan Mishchenko committed
507
    int i, Imp, Left, Right, Max, RetValue;
Alan Mishchenko committed
508
    int fComplL, fComplR;
Alan Mishchenko committed
509 510
    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
    {
Alan Mishchenko committed
511 512
        if ( Imp == 0 )
            continue;
Alan Mishchenko committed
513 514
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
515
        Max = Abc_MaxInt( Left, Right );
Alan Mishchenko committed
516 517 518 519
        assert( Max >= pNode->Id );
        if ( Max > pNode->Id )
            return i;
        // get the corresponding nodes
Alan Mishchenko committed
520
        pLeft  = Aig_ManObj( p->pManAig, Left );
Alan Mishchenko committed
521
        pRight = Aig_ManObj( p->pManAig, Right );
Alan Mishchenko committed
522 523 524 525 526 527 528 529 530
        // get the corresponding FRAIG nodes
        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
        // get the complemented attributes
        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
        // check equality
        if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
        {
Alan Mishchenko committed
531 532 533 534 535 536 537 538 539 540 541 542 543
            if ( fComplL == fComplR ) // x => x  - always true
                continue;
            assert( fComplL != fComplR );
            // consider 4 possibilities:
            // NOT(1) => 1    or   0 => 1  - always true
            // 1 => NOT(1)    or   1 => 0  - never true
            // NOT(x) => x    or   x       - not always true
            // x => NOT(x)    or   NOT(x)  - not always true
            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
                continue;
            // disproved implication
            p->pCla->fRefinement = 1;
            Vec_IntWriteEntry( vImps, i, 0 );
Alan Mishchenko committed
544 545
            continue;
        }
Alan Mishchenko committed
546 547 548 549
        // check the implication 
        // - if true, a clause is added
        // - if false, a cex is simulated
        // make sure the implication is refined
Alan Mishchenko committed
550 551
        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
        if ( RetValue != 1 )
Alan Mishchenko committed
552
        {
Alan Mishchenko committed
553
            p->pCla->fRefinement = 1;
Alan Mishchenko committed
554 555
            if ( RetValue == 0 )
                Fra_SmlResimulate( p );
Alan Mishchenko committed
556 557 558 559
            if ( Vec_IntEntry(vImps, i) != 0 )
                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
            assert( Vec_IntEntry(vImps, i) == 0 );
        }
Alan Mishchenko committed
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583
    }
    return i;
}

/**Function*************************************************************

  Synopsis    [Removes those implications that no longer hold.]

  Description [Returns 1 if refinement has happened.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
{
    Aig_Obj_t * pLeft, * pRight;
    int Imp, i, RetValue = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        if ( Imp == 0 )
            continue;
        // get the corresponding nodes
Alan Mishchenko committed
584 585
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
Alan Mishchenko committed
586
        // check if implication holds using this simulation info
Alan Mishchenko committed
587
        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
Alan Mishchenko committed
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
        {
            Vec_IntWriteEntry( vImps, i, 0 );
            RetValue = 1;
        }
    }
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Removes empty implications.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fra_ImpCompactArray( Vec_Int_t * vImps )
{
    int i, k, Imp;
    k = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
        if ( Imp )
            Vec_IntWriteEntry( vImps, k++, Imp );
    Vec_IntShrink( vImps, k );
}

Alan Mishchenko committed
617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
/**Function*************************************************************

  Synopsis    [Determines the ratio of the state space by computed implications.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
{
    int nSimWords = 64;
    Fra_Sml_t * pComb;
    unsigned * pResult;
    double Ratio = 0.0;
    int Left, Right, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return Ratio;
    // simulate the AIG manager with combinational patterns
638
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
Alan Mishchenko committed
639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666
    // go through the implications and collect where they do not hold
    pResult = Fra_ObjSim( pComb, 0 );
    assert( pResult[0] == 0 );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
    }
    // count the number of ones in this area
    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
    Fra_SmlStop( pComb );
    return Ratio;
}

/**Function*************************************************************

  Synopsis    [Returns the number of failed implications.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
{
Alan Mishchenko committed
667 668
    int nFrames = 2000;
    int nSimWords = 8;
Alan Mishchenko committed
669 670 671 672 673 674
    Fra_Sml_t * pSeq;
    char * pfFails;
    int Left, Right, Imp, i, Counter;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return 0;
    // simulate the AIG manager with combinational patterns
Alan Mishchenko committed
675
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1  );
Alan Mishchenko committed
676
    // go through the implications and check how many of them do not hold
Alan Mishchenko committed
677
    pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
Alan Mishchenko committed
678 679 680 681 682 683 684 685 686 687 688
    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
    }
    // count how many has failed
    Counter = 0;
    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
        Counter += pfFails[i];
Alan Mishchenko committed
689
    ABC_FREE( pfFails );
Alan Mishchenko committed
690
    Fra_SmlStop( pSeq );
Alan Mishchenko committed
691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711
    return Counter;
}

/**Function*************************************************************

  Synopsis    [Record proven implications in the AIG manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
{
    Aig_Obj_t * pLeft, * pRight, * pMiter;
    int nPosOld, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return;
    // go through the implication
712
    nPosOld = Aig_ManCoNum(pNew);
Alan Mishchenko committed
713 714 715 716 717 718
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // record the implication: L' + R
        pMiter = Aig_Or( pNew, 
719 720
            Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), 
            Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
721
        Aig_ObjCreateCo( pNew, pMiter );
Alan Mishchenko committed
722
    }
723
    pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
Alan Mishchenko committed
724 725
}

Alan Mishchenko committed
726 727 728 729 730
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


731 732
ABC_NAMESPACE_IMPL_END