Version abc80919

3 files changed, 127 insertions, 111 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;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index 94d6dbfc..05f7ef55 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -24,6 +24,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern void * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, 
+    int iOutput, int fVerbose, int fSilent );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -212,25 +216,20 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     DdNode * bCurrent;
     DdNode * bNext = NULL; // Suppress "might be used uninitialized"
     DdNode * bTemp;
-    DdNode ** pbVarsY;
-    Aig_Obj_t * pLatch;
     int i, nIters, nBddSize;
     int nThreshold = 10000;
+    Vec_Ptr_t * vOnionRings;
 
-    // collect the NS variables
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Saig_ManForEachLo( p, pLatch, i )
-        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
+    // start the onion rings
+    vOnionRings = Vec_PtrAlloc( 1000 );
 
     // start the image computation
     bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
     if ( fPartition )
-        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
     else
-        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
     Cudd_RecursiveDeref( dd, bCubeCs );
-    free( pbVarsY );
     if ( pTree == NULL )
     {
         if ( !fSilent )
@@ -241,6 +240,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     // perform reachability analisys
     bCurrent = bInitial;   Cudd_Ref( bCurrent );
     bReached = bInitial;   Cudd_Ref( bReached );
+    Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
     for ( nIters = 1; nIters <= nIterMax; nIters++ )
     { 
         // compute the next states
@@ -275,8 +275,14 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
         {
             if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
             {
+                DdNode * bIntersect;
+                bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] );  Cudd_Ref( bIntersect );
+                assert( p->pSeqModel == NULL );
+                p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
+                    vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+                Cudd_RecursiveDeref( dd, bIntersect );
                 if ( !fSilent )
-                    printf( "Output %d was asserted in frame %d.  ", i, nIters );
+                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) );
                 Cudd_RecursiveDeref( dd, bReached );
                 bReached = NULL;
                 break;
@@ -286,6 +292,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             break;
         // get the new states
         bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
+        Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
         // minimize the new states with the reached states
 //        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
 //        Cudd_RecursiveDeref( dd, bTemp );
@@ -309,6 +316,10 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             fprintf( stdout, "\r" );
     }
     Cudd_RecursiveDeref( dd, bNext );
+    // free the onion rings
+    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Vec_PtrFree( vOnionRings );
     // undo the image tree
     if ( fPartition )
         Bbr_bddImageTreeDelete( pTree );
@@ -355,11 +366,15 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
 {
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
-    DdNode * bInitial;
+    DdNode * bInitial, * bTemp;
     int RetValue, i, clk = clock();
+    Vec_Ptr_t * vOnionRings;
 
     assert( Saig_ManRegNum(p) > 0 );
 
+    // start the onion rings
+    vOnionRings = Vec_PtrAlloc( 1000 );
+
     // compute the global BDDs of the latches
     dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );    
     if ( dd == NULL )
@@ -386,12 +401,22 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
     {
         if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
         {
+            DdNode * bIntersect;
+            bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] );  Cudd_Ref( bIntersect );
+            assert( p->pSeqModel == NULL );
+            p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
+                vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+            Cudd_RecursiveDeref( dd, bIntersect );
             if ( !fSilent )
-                printf( "The miter output %d is proved REACHABLE in the initial state.  ", i );
+                printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i );
             RetValue = 0;
             break;
         }
     }
+    // free the onion rings
+    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Vec_PtrFree( vOnionRings );
     // explore reachable states
     if ( RetValue == -1 )
         RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); 
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
index 07a05869..dce30a21 100644
--- a/src/aig/bbr/module.make
+++ b/src/aig/bbr/module.make
@@ -1,3 +1,4 @@
-SRC +=    src/aig/bbr/bbrImage.c \
+SRC +=    src/aig/bbr/bbrCex.c \
+    src/aig/bbr/bbrImage.c \
     src/aig/bbr/bbrNtbdd.c \
     src/aig/bbr/bbrReach.c