Version abc80719

abc.dsp

@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -3224,6 +3224,10 @@ SOURCE=.\src\aig\saig\saigScl.c
 
 SOURCE=.\src\aig\saig\saigTrans.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigUnique.c
+# End Source File
 # End Group
 # End Group
 # End Group

src/aig/cnf/cnf.h

@@ -136,6 +136,7 @@ extern Cnf_Dat_t *     Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses,
 extern Cnf_Dat_t *     Cnf_DataDup( Cnf_Dat_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
+extern void            Cnf_DataFlipLastLiteral( Cnf_Dat_t * p );
 extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );

src/aig/cnf/cnfMan.c

@@ -213,6 +213,22 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p )
+{
+    p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
 {
     FILE * pFile = stdout;

src/aig/fra/fraSec.c

@@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal );
 clk = clock();
     if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
-        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth );
+        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, 0, pParSec->fVeryVerbose, &Depth );
+        RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )

src/aig/saig/module.make

@@ -9,4 +9,5 @@ SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigRetMin.c \
     src/aig/saig/saigRetStep.c \
     src/aig/saig/saigScl.c \
-    src/aig/saig/saigTrans.c
+    src/aig/saig/saigTrans.c \
+    src/aig/saig/saigUnique.c

src/aig/saig/saig.h

@@ -85,7 +85,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/

src/aig/saig/saigInter.c

@@ -50,6 +50,7 @@ struct Saig_IntMan_t_
     Vec_Int_t *      vVarsAB;      // the variables participating in 
     // temporary place for the new interpolant
     Aig_Man_t *      pInterNew;
+    Vec_Ptr_t *      vInters;
     // parameters
     int              nFrames;      // the number of timeframes
     int              nConfCur;     // the current number of conflicts
@@ -65,7 +66,9 @@ struct Saig_IntMan_t_
     int              timeTotal;
 };
 
+#ifdef ABC_USE_LIBRARIES
 static int Saig_M144pPerformOneStep( Saig_IntMan_t * p );
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -328,7 +331,10 @@ sat_solver * Saig_DeriveSatSolver(
     for ( i = 0; i < pCnfFrames->nClauses; i++ )
     {
         if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
-            assert( 0 );
+        {
+            pSat->fSolved = 1;
+            break;
+        }
     }
     sat_solver_store_mark_roots( pSat );
     // return clauses to the original state
@@ -697,6 +703,26 @@ void Saig_ManagerClean( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Saig_ManagerFreeInters( Saig_IntMan_t * p )
+{
+    Aig_Man_t * pTemp;
+    int i;
+    Vec_PtrForEachEntry( p->vInters, pTemp, i )
+        Aig_ManStop( pTemp );
+    Vec_PtrClear( p->vInters );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Saig_ManagerFree( Saig_IntMan_t * p )
 {
     if ( p->fVerbose )
@@ -727,6 +753,8 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
         Aig_ManStop( p->pInter );
     if ( p->pInterNew )
         Aig_ManStop( p->pInterNew );
+    Saig_ManagerFreeInters( p );
+    Vec_PtrFree( p->vInters );
     free( p );
 }
 
@@ -743,7 +771,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
+int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld )
 {
     sat_solver * pSat;
     Aig_Man_t * pInterOld = p->pInter;
@@ -757,6 +785,9 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
 
     // start the solver
     pSat = sat_solver_new();
+    if ( fSubtractOld )
+        sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars + pCnfOld->nVars );
+    else
         sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars );
 
     // interpolant
@@ -803,21 +834,48 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
     }
 
     // complement the last literal
-    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
-    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
     // add clauses of B
+    Cnf_DataFlipLastLiteral( pCnfNew );
     for ( i = 0; i < pCnfNew->nClauses; i++ )
     {
         if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
-            assert( 0 );
+        {
+//            assert( 0 );
+            Cnf_DataFree( pCnfNew );
+            return 1;
         }
-    // complement the last literal
-    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
-    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
+    }
+    Cnf_DataFlipLastLiteral( pCnfNew );
 
     // return clauses to the original state
     Cnf_DataLift( pCnfTrans, -pCnfNew->nVars );
     Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars );
+    if ( fSubtractOld )
+    {
+        Cnf_DataLift( pCnfOld, 2 * pCnfNew->nVars + pCnfTrans->nVars );
+        // old interpolant clauses
+        Cnf_DataFlipLastLiteral( pCnfOld );
+        for ( i = 0; i < pCnfOld->nClauses; i++ )
+        {
+            if ( !sat_solver_addclause( pSat, pCnfOld->pClauses[i], pCnfOld->pClauses[i+1] ) )
+                assert( 0 );
+        }
+        Cnf_DataFlipLastLiteral( pCnfOld );
+        // connector clauses
+        Aig_ManForEachPi( pInterOld, pObj, i )
+        {
+            pObj2 = Aig_ManPi( pInterNew, i );
+            Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 1 );
+            Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+        Cnf_DataLift( pCnfOld, - 2 * pCnfNew->nVars - pCnfTrans->nVars );
+    }
     Cnf_DataFree( pCnfNew );
 
     // solve the problem
@@ -838,8 +896,9 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth )
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth )
 {
+    extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters );
     Saig_IntMan_t * p;
     Aig_Man_t * pAigTemp;
     int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
@@ -856,6 +915,7 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRew
     p->nFrames = 1;
     p->nConfLimit = nConfLimit;
     p->fVerbose = fVerbose;
+    p->vInters = Vec_PtrAlloc( 10 );
     // can perform SAT sweeping and/or rewriting of this AIG...
     p->pAig = pAig;      
     if ( fTransLoop )
@@ -878,9 +938,11 @@ p->timeCnf += clock() - clk;
     *pDepth = -1;
     for ( s = 0; ; s++ )
     {
+        Saig_ManagerFreeInters( p );
 clk2 = clock();
         // initial state
         p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) );
+        Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
 clk = clock();
         p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
 p->timeCnf += clock() - clk;    
@@ -919,10 +981,13 @@ p->timeCnf += clock() - clk;
             }
             // perform interplation
             clk = clock();
+#ifdef ABC_USE_LIBRARIES
             if ( fUseIp )
                 RetValue = Saig_M144pPerformOneStep( p );
             else
+#endif
                 RetValue = Saig_PerformOneStep( p, 0 );
+
             if ( fVerbose )
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
@@ -960,11 +1025,15 @@ clk = clock();
             p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
             Aig_ManStop( pAigTemp );
 p->timeRwr += clock() - clk;
+            // save the new interpolant
+            Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
             // check containment of interpolants
 clk = clock();
-            if ( fCheckInd )
-                Status = Saig_ManCheckInductiveContainment( p );
-            else
+            if ( fCheckKstep ) // k-step unique-state induction
+                Status = Saig_ManUniqueState( p->pAigTrans, p->vInters );
+            else if ( fCheckInd ) // simple induction
+                Status = Saig_ManCheckInductiveContainment( p, 1 );
+            else // combinational containment
                 Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
 p->timeEqu += clock() - clk;
             if ( Status ) // contained
@@ -1004,6 +1073,8 @@ p->timeCnf += clock() - clk;
 }
 
 
+#ifdef ABC_USE_LIBRARIES
+
 #include "m114p.h"
 
 /**Function*************************************************************
@@ -1134,10 +1205,14 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_
     Aig_Man_t * p;
     Aig_Obj_t * pInter, * pInter2, * pVar;
     Vec_Ptr_t * vInters;
+    Vec_Int_t * vASteps;
     int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, iVar;
+    int nLits, nVars, i, k, iVar, haveASteps;
+    int CountA, CountB, CountC, CountCsaved;
+
     assert( M114p_SolverProofIsReady(s) );
     vInters = Vec_PtrAlloc( 1000 );
+    vASteps = Vec_IntAlloc( 1000 );
     // process root clauses
     p = Aig_ManStart( 10000 );
     M114p_SolverForEachRoot( s, &pLits, nLits, i )
@@ -1157,26 +1232,50 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_
             }
         }
         Vec_PtrPush( vInters, pInter );
+        Vec_IntPush( vASteps, 0 );
     }
     assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
 
     // process learned clauses
+    CountA = CountB = CountC = CountCsaved = 0;
     M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
     {
         pInter = Vec_PtrEntry( vInters, pClauses[0] );
+        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
         for ( k = 0; k < nVars; k++ )
         {
             iVar = Vec_IntEntry( vMapVars, pVars[k] );
             pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
             if ( iVar == -1 ) // var of A
+            {
+                haveASteps = 1;
                 pInter = Aig_Or( p, pInter, pInter2 );
+            }
             else // var of B or C
                 pInter = Aig_And( p, pInter, pInter2 );
+
+            if ( iVar == -1 )
+                CountA++;
+            else if ( iVar == -2 )
+                CountB++;
+            else 
+            {
+                if ( haveASteps == 0 )
+                    CountCsaved++;
+                CountC++;
+            }
         }
         Vec_PtrPush( vInters, pInter );
+        Vec_IntPush( vASteps, haveASteps );
     }
+//    printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", 
+//        CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC );
+
     assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
     Vec_PtrFree( vInters );
+    Vec_IntFree( vASteps );
+
     Aig_ObjCreatePo( p, pInter );
     Aig_ManCleanup( p );
     return p;
@@ -1229,6 +1328,8 @@ p->timeInt += clock() - clk;
     return RetValue;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/saig/saigUnique.c

+/**CFile****************************************************************
+
+  FileName    [saigUnique.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Containment checking with unique state constraints.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigUnique.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for interpolation.]
+
+  Description [The resulting manager is combinational. The primary inputs
+  corresponding to register outputs are ordered first.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
+    Saig_ManForEachLo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+        Vec_PtrPush( *pvMapReg, pObj->pData );
+    }
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            Vec_PtrPush( *pvMapReg, pObjLo->pData );
+        }
+    }
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while mapping PIs into the given array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManPoNum(pOld) == 1 );
+    // create the PIs
+    Aig_ManCleanData( pOld );
+    Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( pOld, pObj, i )
+        pObj->pData = ppNewPis[i];
+    // duplicate internal nodes
+    Aig_ManForEachNode( pOld, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add one PO to new
+    pObj = Aig_ManPo( pOld, 0 );
+    Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters )
+{
+    Aig_Man_t * pFrames, * pInterNext, * pInterThis;
+    Aig_Obj_t ** ppNodes;
+    Vec_Ptr_t * vMapRegs;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    int f, nRegs, status;
+    nRegs = Saig_ManRegNum(pTrans);
+    assert( nRegs > 0 );
+    assert( Vec_PtrSize(vInters) > 1 );
+    // generate the timeframes
+    pFrames = Saig_ManFramesLatches( pTrans, Vec_PtrSize(vInters)-1, &vMapRegs );
+    assert( Vec_PtrSize(vMapRegs) == Vec_PtrSize(vInters) * nRegs );
+    // add main constraints to the timeframes
+    ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
+    Vec_PtrForEachEntryStop( vInters, pInterThis, f, Vec_PtrSize(vInters)-1 )
+    {
+        assert( nRegs == Aig_ManPiNum(pInterThis) );
+        pInterNext = Vec_PtrEntry( vInters, f+1 );
+        Saig_ManAppendCone( pInterNext, pFrames, ppNodes + f * nRegs, 0 );
+        Saig_ManAppendCone( pInterThis, pFrames, ppNodes + f * nRegs, 1 );
+    }
+    Saig_ManAppendCone( Vec_PtrEntryLast(vInters), pFrames, ppNodes + f * nRegs, 1 );
+    Aig_ManCleanup( pFrames );
+    Vec_PtrFree( vMapRegs );
+
+    // convert to CNF
+    pCnf = Cnf_Derive( pFrames, 0 ); 
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pFrames );
+
+    if ( pSat == NULL )
+        return 1;
+
+     // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    sat_solver_delete( pSat );
+    return status == l_False;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/abc.c

@@ -15348,9 +15348,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fTransLoop;
     int fUsePudlak;
     int fCheckInd;
+    int fCheckKstep;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15363,9 +15364,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     fTransLoop = 1;
     fUsePudlak = 0;
     fCheckInd  = 0;
+    fCheckKstep= 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15403,6 +15405,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fCheckInd ^= 1;
             break;
+        case 'k':
+            fCheckKstep ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -15432,18 +15437,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
     fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+//    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
+    fprintf( pErr, "\t-k     : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;

src/base/abci/abcDar.c

@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth );
+    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )

src/sat/bsat/satInterA.c

@@ -809,8 +809,12 @@ int Inta_ManProcessRoots( Inta_Man_t * p )
         if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
         {
             // detected root level conflict
-            printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
-            assert( 0 );
+//            printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+//            assert( 0 );
+            // detected root level conflict
+            Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+            if ( p->fVerbose )
+                printf( "Found root level conflict!\n" );
             return 0;
         }
     }

src/sat/bsat/satSolver.c

@@ -1061,7 +1061,8 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     begin = veci_begin( &s->temp_clause );
     end = begin + veci_size( &s->temp_clause );
 
-    if (begin == end) return false;
+    if (begin == end) 
+        return false;
 
     //printlits(begin,end); printf("\n");
     // insertion sort
@@ -1076,6 +1077,16 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     sat_solver_setnvars(s,maxvar+1);
 //    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
 
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
     //printlits(begin,end); printf("\n");
     values = s->assigns;
 
@@ -1095,16 +1106,6 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     if (j == begin)          // empty clause
         return false;
 
-    ///////////////////////////////////
-    // add clause to internal storage
-    if ( s->pStore )
-    {
-        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
-        assert( RetValue );
-    }
-    ///////////////////////////////////
-
     if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
@@ -1164,6 +1165,19 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
     lbool*  values        = s->assigns;
     lit*    i;
 
+    ////////////////////////////////////////////////
+    if ( s->fSolved )
+    {
+        if ( s->pStore )
+        {
+            extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+            int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+            assert( RetValue );
+        }
+        return l_False;
+    }
+    ////////////////////////////////////////////////
+
     // set the external limits
     s->nCalls++;
     s->nRestarts  = 0;

src/sat/bsat/satSolver.h

@@ -182,6 +182,7 @@ struct sat_solver_t
 
     // clause store
     void *   pStore;
+    int      fSolved;
 
     // trace recording
     FILE *   pFile;