Version abc80919

1 files changed, 87 insertions, 97 deletions

diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index f5981439..be5377af 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -19,48 +19,21 @@
 ***********************************************************************/
 
 #include "bbr.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the initial state and sets up the variable map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
-{
-    DdNode ** pbVarsX, ** pbVarsY;
-    Aig_Obj_t * pLatch;
-    int i;
-
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsX = ALLOC( DdNode *, dd->size );
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Saig_ManForEachLo( p, pLatch, i )
-    {
-        pbVarsY[i] = dd->vars[ Saig_ManPiNum(p) + i ];
-        pbVarsX[i] = dd->vars[ Saig_ManCiNum(p) + i ];
-    }
-    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
-    FREE( pbVarsX );
-    FREE( pbVarsY );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
+  Synopsis    [Derives the counter-example using the set of reached states.]
 
   Description []
                
@@ -69,105 +42,122 @@ void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManComputeCountExample( Aig_Man_t * p, DdManager * dd, DdNode ** pbParts, Vec_Ptr_t * vCareSets, int nBddMax, int fVerbose, int fSilent )
+Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
+    int iOutput, int fVerbose, int fSilent )
 {
-/*
-    Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
-    DdNode * bCubeCs;
-    DdNode * bCurrent;
-    DdNode * bNext = NULL; // Suppress "might be used uninitialized"
-    DdNode * bTemp;
-    DdNode ** pbVarsY;
+    Ssw_Cex_t * pCex;
     Aig_Obj_t * pObj;
-    int i, nIters, nBddSize;
-    int nThreshold = 10000;
-    int * pCex;
+    Bbr_ImageTree_t * pTree;
+    DdNode * bCubeNs, * bState, * bImage;
+    DdNode * bTemp, * bVar, * bRing;
+    int i, v, RetValue, nPiOffset;
     char * pValues;
+    int clk = clock();
 
     // allocate room for the counter-example
-    pCex = ALLOC( int, Vec_PtrSize(vCareSets) );
+    pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
+    pCex->iFrame = Vec_PtrSize(vOnionRings);
+    pCex->iPo = iOutput;
+    nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);
+
+    // create the cube of NS variables
+    bCubeNs  = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) );    Cudd_Ref( bCubeNs );
+    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
+    Cudd_RecursiveDeref( dd, bCubeNs );
+    if ( pTree == NULL )
+    {
+        if ( !fSilent )
+            printf( "BDDs blew up during qualitification scheduling.  " );
+        return NULL;
+    }
 
     // allocate room for the cube
     pValues = ALLOC( char, dd->size );
 
-    // collect the NS variables
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Aig_ManForEachPi( p, pObj, i )
-        pbVarsY[i] = dd->vars[ i ];
+    // get the last cube
+    RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues );
+    assert( RetValue );
 
-    // create the initial state and the variable map
-    Aig_ManStateVarMap( dd, p, fVerbose );
+    // write PIs of counter-example
+    Saig_ManForEachPi( p, pObj, i )
+        if ( pValues[i] == 1 )
+            Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+    nPiOffset -= Saig_ManPiNum(p);
 
-    // start the image computation
-    bCubeCs  = Bbr_bddComputeRangeCube( dd, Aig_ManPiNum(p), 2*Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
-    pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
-    Cudd_RecursiveDeref( dd, bCubeCs );
-    free( pbVarsY );
-    if ( pTree == NULL )
+    // write state in terms of NS variables
+    bState = (dd)->one; Cudd_Ref( bState );
+    Saig_ManForEachLo( p, pObj, i )
     {
-        if ( !fSilent )
-            printf( "BDDs blew up during qualitification scheduling.  " );
-        return -1;
+        bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
+        bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
+        Cudd_RecursiveDeref( dd, bTemp ); 
     }
 
-    // create counter-example in terms of next state variables
-    // pNext = ...
-
-    // perform reachability analisys
-    Vec_PtrForEachEntryReverse( vCareSets, pCurrent, i )
+    // perform backward analysis
+    Vec_PtrForEachEntryReverse( vOnionRings, bRing, v )
     { 
         // compute the next states
-        bImage = Bbr_bddImageCompute( pTree, bCurrent );           
+        bImage = Bbr_bddImageCompute( pTree, bState );           
         if ( bImage == NULL )
         {
+            Cudd_RecursiveDeref( dd, bState );
             if ( !fSilent )
                 printf( "BDDs blew up during image computation.  " );
             Bbr_bddImageTreeDelete( pTree );
-            return -1;
+            free( pValues );
+            return NULL;
         }
         Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( dd, bState );
 
         // intersect with the previous set
-        bImage = Cudd_bddAnd( dd, pTemp = bImage, pCurrent );
-        Cudd_RecursiveDeref( dd, pTemp );
+        bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing );  Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( dd, bTemp );
 
         // find any assignment of the BDD
         RetValue = Cudd_bddPickOneCube( dd, bImage, pValues );
+        assert( RetValue );
+        Cudd_RecursiveDeref( dd, bImage );
 
-        // transform the assignment into the cube in terms of the next state vars
+        // write PIs of counter-example
+        Saig_ManForEachPi( p, pObj, i )
+            if ( pValues[i] == 1 )
+                Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+        nPiOffset -= Saig_ManPiNum(p);
 
-
-        
-        // pCurrent = ...
-
-        // save values of the PI variables
-
-
-        // check if there are any new states
-        if ( Cudd_bddLeq( dd, bNext, bReached ) )
-            break;
-        // check the BDD size
-        nBddSize = Cudd_DagSize(bNext);
-        if ( nBddSize > nBddMax )
+        // check that we get the init state
+        if ( v == 0 )
+        {
+            Saig_ManForEachLo( p, pObj, i )
+                assert( pValues[Saig_ManPiNum(p)+i] == 0 );
             break;
-        // check the result
-        for ( i = 0; i < Saig_ManPoNum(p); i++ )
+        }
+
+        // write state in terms of NS variables
+        bState = (dd)->one; Cudd_Ref( bState );
+        Saig_ManForEachLo( p, pObj, i )
         {
-            if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
-            {
-                if ( !fSilent )
-                    printf( "Output %d was asserted in frame %d.  ", i, nIters );
-                Cudd_RecursiveDeref( dd, bReached );
-                bReached = NULL;
-                break;
-            }
+            bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
+            bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
+            Cudd_RecursiveDeref( dd, bTemp ); 
         }
-        if ( i < Saig_ManPoNum(p) )
-            break;
-        // get the new states
-        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
-*/
+    }
+    // cleanup
+    Bbr_bddImageTreeDelete( pTree );
+    free( pValues );
+    // verify the counter example
+    if ( Vec_PtrSize(vOnionRings) < 1000 )
+    {
+    RetValue = Ssw_SmlRunCounterExample( p, pCex );
+    if ( RetValue == 0 && !fSilent )
+        printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
+    }
+    if ( fVerbose && !fSilent )
+    {
+    PRT( "Counter-example generation time", clock() - clk );
+    }
+    return pCex;
 }
 
 ////////////////////////////////////////////////////////////////////////