Adding new switch to &genqfb to use output as an enable in the miter.

2 files changed, 24 insertions, 8 deletions

diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
index 247c3dad..f32db0a4 100644
--- a/src/aig/gia/giaQbf.c
+++ b/src/aig/gia/giaQbf.c
@@ -132,11 +132,11 @@ Vec_Int_t * Gia_GenCreateMuxes( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vFl
     }
     return vLits;
 }
-Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSize, char * pStr, int fVerbose )
+Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSize, char * pStr, int fUseOut, int fVerbose )
 {
     Gia_Obj_t * pObj; 
     Gia_Man_t * pTemp, * pNew;
-    int i, iMiter, nPars = nLutNum * (1 << nLutSize);
+    int i, iMiter, iLut0, iLut1, nPars = nLutNum * (1 << nLutSize);
     Vec_Int_t * vLits0, * vLits1, * vParLits;
     Vec_Int_t * vFlops = Gia_GenCollectFlopIndexes( pStr, nLutNum, nLutSize, Gia_ManRegNum(p) );
     // collect parameter literals (data vars)
@@ -160,7 +160,18 @@ Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSi
     vLits0 = Gia_GenCreateMuxes( p, pNew, vFlops, nLutNum, nLutSize, vParLits, 0 );
     vLits1 = Gia_GenCreateMuxes( p, pNew, vFlops, nLutNum, nLutSize, vParLits, 1 );
     // create miter output
-    iMiter = Gia_ManHashAnd( pNew, Vec_IntEntry(vLits0, 0), Abc_LitNot(Vec_IntEntry(vLits1, 0)) );
+    //iMiter = Gia_ManHashAnd( pNew, Vec_IntEntry(vLits0, 0), Abc_LitNot(Vec_IntEntry(vLits1, 0)) );
+    ///////////////////////////////////////////////////////////////////////////
+    iLut0 = Vec_IntEntry(vLits0, 0);
+    iLut1 = Vec_IntEntry(vLits1, 0);
+    if ( fUseOut )
+    {
+        Gia_Obj_t * pObjPoLast = Gia_ManPo( p, Gia_ManPoNum(p)-1 );
+        int iOut = Abc_LitNotCond( Gia_ObjFanin0Copy(pObjPoLast), 0 );
+        iLut1 = Gia_ManHashAnd( pNew, iLut1, Abc_LitNot(iOut) );
+    }
+    iMiter = Gia_ManHashAnd( pNew, iLut0, Abc_LitNot(iLut1) );
+    ///////////////////////////////////////////////////////////////////////////
     iMiter = Gia_ManHashAnd( pNew, Abc_LitNot(iMiter), Abc_Var2Lit(1, 0) );
     Gia_ManAppendCo( pNew, iMiter );
     // cleanup
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ad7257f0..a5251c7a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -42761,16 +42761,17 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * pGia, int nFrames, int nLutNum, int nLutSize, char * pStr, int fVerbose );
+    extern Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * pGia, int nFrames, int nLutNum, int nLutSize, char * pStr, int fUseOut, int fVerbose );
     int nFrames   =    1;
     int nLutNum   =    1;
     int nLutSize  =    6;
     char * pStr   = NULL;
+    int fUseOut   =    0;
     int fVerbose  =    0;
     int c;
     Gia_Man_t * pTemp;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FKNSvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FKNSovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -42810,7 +42811,7 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'S':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by a string.\n" );
                 goto usage;
             }
             pStr = Abc_UtilStrsav(argv[globalUtilOptind]);
@@ -42818,6 +42819,9 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pStr == NULL )
                 goto usage;
             break;
+        case 'o':
+            fUseOut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -42847,17 +42851,18 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Currently this commands works for one frame and one LUT.\n" );
         return 1;
     }
-    pTemp = Gia_GenQbfMiter( pAbc->pGia, nFrames, nLutNum, nLutSize, pStr, fVerbose );
+    pTemp = Gia_GenQbfMiter( pAbc->pGia, nFrames, nLutNum, nLutSize, pStr, fUseOut, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     ABC_FREE( pStr );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &genqbf [-FKN num] [-vh]\n" );
+    Abc_Print( -2, "usage: &genqbf [-FKN num] [-ovh]\n" );
     Abc_Print( -2, "\t         generates QBF miter for computing an inductive invariant\n" );
     Abc_Print( -2, "\t-F num : the number of time frames for induction [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", nLutSize );
     Abc_Print( -2, "\t-N num : the number of LUTs [default = %d]\n", nLutNum );
+    Abc_Print( -2, "\t-o     : toggle using the last output [default = %s]\n", fUseOut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;