Specialized inductive check.

3 files changed, 159 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0ac0b7cf..c9159d3f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32686,9 +32686,9 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fVerbose = 0;
+    int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fDump = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MTevh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32717,6 +32717,15 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'e':
             fEmpty ^= 1;
             break;
+        case 's':
+            fSearch ^= 1;
+            break;
+        case 'r':
+            fReverse ^= 1;
+            break;
+        case 'd':
+            fDump ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -32736,15 +32745,21 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9ICheck(): The AIG is combinational.\n" );
         return 0;
     }
-    Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
+    if ( fSearch )
+        Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
+    else
+        Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &icheck [-MT num] [-evh]\n" );
+    Abc_Print( -2, "usage: &icheck [-MT num] [-esrdvh]\n" );
     Abc_Print( -2, "\t         performs specialized induction check\n" );
     Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n",    nFramesMax );
     Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n",    nTimeOut );
     Abc_Print( -2, "\t-e     : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle searching for a minimal subset [default = %s]\n",          fSearch? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle searching in the reverse order [default = %s]\n",          fReverse? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle printing out the resulting set [default = %s]\n",          fDump? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",            fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0cfc9b37..2f7af2ba 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -132,6 +132,7 @@ extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
+extern void              Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
 /*=== bmcUnroll.c ==========================================================*/
 extern Unr_Man_t *       Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
 extern Gia_Man_t *       Unr_ManUnrollFrame( Unr_Man_t * p, int f );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index 17408e78..13ab1038 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -293,6 +293,145 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
     Vec_IntFree( vUsed );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t * vLits )
+{
+    int fUseOldCnf = 0;
+    Gia_Man_t * pMiter, * pTemp;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+//    Vec_Int_t * vLits;
+    int i, Iter, status;
+    int nLitsUsed;
+    abctime clkStart = Abc_Clock();
+    assert( nFramesMax > 0 );
+    assert( Gia_ManRegNum(p) > 0 );
+
+    // create miter
+    pTemp = Gia_ManDup( p );
+    pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
+    Gia_ManStop( pTemp );
+    assert( Gia_ManPoNum(pMiter)  == 2 * Gia_ManPoNum(p) );
+    assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
+    // derive CNF
+    if ( fUseOldCnf )
+        pCnf = Cnf_DeriveGiaRemapped( pMiter );
+    else
+    {
+        pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
+        Gia_ManStop( pTemp );
+        pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
+    }
+/*
+    // collect positive literals
+    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+*/
+    // derive SAT solver        
+    pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
+    status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( status == l_True )
+    {
+        printf( "I = %4d :  ", nFramesMax );
+        printf( "Problem is satisfiable.\n" );
+        sat_solver_delete( pSat );
+        Cnf_DataFree( pCnf );
+        Gia_ManStop( pMiter );
+        return;
+    }
+    assert( status == l_False );
+
+    // count the number of positive literals
+    nLitsUsed = 0;
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+            nLitsUsed++;
+
+    // try removing variables
+    for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
+    {
+        i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
+        if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+            continue;
+        Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        if ( status == l_Undef )
+        {
+            printf( "Timeout reached after %d seconds.\n", nTimeOut );
+            break;
+        }
+        if ( status == l_True )
+            Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
+        else if ( status == l_False )
+            nLitsUsed--;
+        else assert( 0 );
+        // report the results
+        //printf( "Round %d:  ", o );
+        printf( "I = %4d :  AIG =%8d.  SAT vars =%8d.  SAT conf =%8d.  S =%6d. (%6.2f %%)  ",
+            i, (nFramesMax+1) * Gia_ManAndNum(pMiter), 
+            Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), 
+            sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
+        ABC_PRTr( "Time", Abc_Clock() - clkStart );
+        fflush( stdout );
+    }
+    // report the results
+    //printf( "Round %d:  ", o );
+    printf( "M = %4d :  AIG =%8d.  SAT vars =%8d.  SAT conf =%8d.  S =%6d. (%6.2f %%)  ",
+        nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), 
+        Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), 
+        sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+    fflush( stdout );
+
+    // cleanup
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pMiter );
+//    Vec_IntFree( vLits );
+}
+void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
+{
+    Vec_Int_t * vLits;
+    int i, f;
+    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
+        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
+    fflush( stdout );
+
+    // collect positive literals
+    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+
+    for ( f = 1; f < nFramesMax; f++ )
+        Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits );
+
+    // dump the numbers of the flops
+    if ( fDump )
+    {
+        int nLitsUsed = 0;
+        for ( i = 0; i < Gia_ManRegNum(p); i++ )
+            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+                nLitsUsed++;
+        printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
+        for ( i = 0; i < Gia_ManRegNum(p); i++ )
+            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+                printf( "%d ", i );
+        printf( "\n" );
+    }       
+    Vec_IntFree( vLits );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////