New API to return the set of all reachable states as an AIG.

2 files changed, 97 insertions, 2 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f4c89526..4ee8245d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -33183,7 +33183,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Gia_Man_t * pTemp = NULL;
+    Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int nFrames = 10;
     int fSwitch = 0;
@@ -33204,6 +33204,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Gia_ManMuxProfiling( Gia_Man_t * p );
 //    extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia );
 //    extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p );
+    extern Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
@@ -33277,6 +33278,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_FrameUpdateGia( pAbc, pTemp );
 //    pTemp = Gia_ManInterTest( pAbc->pGia );
 //    Abc_FrameUpdateGia( pAbc, pTemp );
+    pTemp = Llb_ReachableStatesGia( pAbc->pGia );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index 6d5826a0..a9421358 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "llbInt.h"
+#include "base/abc/abc.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
  
@@ -888,8 +890,9 @@ printf( "Before = %d.  After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurr
     // report
     if ( !p->pPars->fSilent )
         printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    if ( !p->pPars->fSilent )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     p->pPars->iFrame = nIters - 1;
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return 1; // unreachable
 }
 
@@ -1084,6 +1087,95 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     return RetValue;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Takes an AIG and returns an AIG representing reachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Llb_ReachableStates( Aig_Man_t * pAig )
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    Vec_Int_t * vPermute;
+    Vec_Ptr_t * vNames;
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    DdManager * dd;
+    DdNode * bReached;
+    Llb_Mnx_t * pMnn;
+    Abc_Ntk_t * pNtk, * pNtkMuxes;
+    Aig_Obj_t * pObj;
+    int i, RetValue;
+    abctime clk = Abc_Clock();
+
+    // create parameters
+    Llb_ManSetDefaultParams( pPars );
+    pPars->fSkipOutCheck = 1;
+    pPars->fCluster      = 0;
+    pPars->fReorder      = 0;
+    pPars->fSilent       = 1;
+    pPars->nBddMax       = 100;
+    pPars->nClusterMax   = 500;
+
+    // run reachability
+    pMnn = Llb_MnxStart( pAig, pPars );
+    RetValue = Llb_Nonlin4Reachability( pMnn );
+    assert( RetValue == 1 );
+
+    // print BDD
+//    Extra_bddPrint( pMnn->dd, pMnn->bReached ); 
+//    Extra_bddPrintSupport( pMnn->dd, pMnn->bReached ); 
+//    printf( "\n" );
+
+    // collect flop output variables
+    vPermute = Vec_IntStartFull( Cudd_ReadSize(pMnn->dd) );
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntWriteEntry( vPermute, Llb_ObjBddVar(pMnn->vOrder, pObj), i );
+
+    // transfer the reached state BDD into the new manager
+    dd = Cudd_Init( Saig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    bReached = Extra_TransferPermute( pMnn->dd, dd, pMnn->bReached, Vec_IntArray(vPermute) );  Cudd_Ref( bReached );
+    Vec_IntFree( vPermute );
+    assert( Cudd_ReadSize(dd) == Saig_ManRegNum(pAig) );
+
+    // quit reachability engine
+    pMnn->timeTotal = Abc_Clock() - clk;
+    Llb_MnxStop( pMnn );
+
+    // derive the network
+    vNames = Abc_NodeGetFakeNames( Saig_ManRegNum(pAig) );
+    pNtk = Abc_NtkDeriveFromBdd( dd, bReached, "reached", vNames );
+    Abc_NodeFreeNames( vNames );
+    Cudd_RecursiveDeref( dd, bReached );
+    Cudd_Quit( dd );
+
+    // convert
+    pNtkMuxes = Abc_NtkBddToMuxes( pNtk );
+    Abc_NtkDelete( pNtk );
+    pNtk = Abc_NtkStrash( pNtkMuxes, 0, 1, 0 );
+    Abc_NtkDelete( pNtkMuxes );
+    pAig = Abc_NtkToDar( pNtk, 0, 0 );
+    Abc_NtkDelete( pNtk );
+    return pAig;
+}
+Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Aig_Man_t * pAig, * pReached;
+    pAig = Gia_ManToAigSimple( p );
+    pReached = Llb_ReachableStates( pAig );
+    Aig_ManStop( pAig );
+    pNew = Gia_ManFromAigSimple( pReached );
+    Aig_ManStop( pReached );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////