Experiments with recent ideas.

4 files changed, 156 insertions, 47 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a5858ca6..79578113 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -139,6 +139,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
     Vec_Int_t *    vGateClasses;  // classes of gates for abstraction
     Vec_Int_t *    vObjClasses;   // classes of objects for abstraction
+    Vec_Int_t *    vInitClasses;  // classes of flops for retiming/merging/etc
     Vec_Int_t *    vDoms;         // dominators
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 805ab4f9..e78cb849 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -95,6 +95,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vFlopClasses );
     Vec_IntFreeP( &p->vGateClasses );
     Vec_IntFreeP( &p->vObjClasses );
+    Vec_IntFreeP( &p->vInitClasses );
     Vec_IntFreeP( &p->vDoms );
     Vec_IntFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vTruths );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 76412726..8b8fab5e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -399,6 +399,7 @@ static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9FunFaTest          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Tulip              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -962,6 +963,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&funfatest",    Abc_CommandAbc9FunFaTest,    0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&tulip",        Abc_CommandAbc9Tulip,        0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -32747,6 +32749,98 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
+    Vec_Int_t * vTemp;
+    int c, nFrames = 5, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 )
+                goto usage;
+            break;
+        case 's':
+            fSim ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Tulip(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Tulip(): AIG is combinational.\n" );
+        return 0;
+    }
+    pAbc->pGia->vInitClasses = Gia_ManTulipTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
+    Vec_IntFreeP( &vTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &tulip [-FWT num] [-scdvh]\n" );
+    Abc_Print( -2, "\t         experimental prcedure for testing new ideas\n" );
+    Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
+    Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
+    Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
+    Abc_Print( -2, "\t-s     : toggles using ternary simulation [default = %s]\n",            fSim?     "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",        fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     return -1;
@@ -34054,7 +34148,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Agi_ManTest( Gia_Man_t * pGia );
 //    extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax );
 //    extern void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs );
-    extern void Gia_ManTulipTest( Gia_Man_t * p, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "WPFsvh" ) ) != EOF )
@@ -34158,7 +34251,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Jf_ManTestCnf( pAbc->pGia );
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
-    Gia_ManTulipTest( pAbc->pGia, nFrames, nWords, 0, fSwitch, fVerbose );
+    printf( "\nThis command is currently disabled.\n\n" );
 
     return 0;
 usage:
diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c
index 1d790522..29e8781f 100644
--- a/src/sat/bmc/bmcTulip.c
+++ b/src/sat/bmc/bmcTulip.c
@@ -70,7 +70,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars )
+Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -85,8 +85,21 @@ Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars )
     Gia_ManForEachRo( p, pObj, i )
         Gia_ManAppendCi( pNew );
     // build timeframes
+    assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
     Gia_ManForEachRo( p, pObj, i )
-        pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
+    {
+        if ( vInit == NULL ) // assume 2
+            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
+        else if ( Vec_IntEntry(vInit, i) == 0 )
+            pObj->Value = 0;
+        else if ( Vec_IntEntry(vInit, i) == 1 )
+            pObj->Value = 1;
+        else if ( Vec_IntEntry(vInit, i) == 2 )
+            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
+        else if ( Vec_IntEntry(vInit, i) == 3 )
+            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1;
+        else assert( 0 );
+    }
     for ( f = 0; f < nFrames; f++ )
     {
         Gia_ManForEachPi( p, pObj, i )
@@ -118,7 +131,7 @@ Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose )
+Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
 {
     int nIterMax = 1000000;
     int i, iLit, Iter, status;
@@ -128,13 +141,15 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
     Vec_Int_t * vLits, * vMap;
     sat_solver * pSat;
     Gia_Obj_t * pObj;
-    Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0 );
-    Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1 );
+    Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit );
+    Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit );
     Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
     Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
     Gia_ManStop( p0 );
     Gia_ManStop( p1 );
     assert( Gia_ManRegNum(p) > 0 );
+    if ( fVerbose )
+        printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
 
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, pCnf->nVars );
@@ -154,7 +169,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
     Gia_ManForEachPi( pM, pObj, i )
         if ( i == Gia_ManRegNum(p) )
             break;
-        else
+        else if ( vInit == NULL || (Vec_IntEntry(vInit, i) & 2) )
             Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
 
     if ( fVerbose )
@@ -163,7 +178,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
         printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
         printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
         printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
-        printf( "Subset =%6d  ",    Gia_ManRegNum(p) );
+        printf( "Subset =%6d  ",    Vec_IntSize(vLits) );
         Abc_PrintTime( 1, "Time", clkSat );
 //      ABC_PRTr( "Solver time", clkSat );
     }
@@ -214,13 +229,18 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
     vMap = Vec_IntStart( pCnf->nVars );
     Vec_IntForEachEntry( vLits, iLit, i )
         Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
+
     // create output
-    Vec_IntClear( vLits );
+    Vec_IntFree( vLits );
+    if ( vInit )
+        vLits = Vec_IntDup(vInit);
+    else
+        vLits = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vLits, Gia_ManRegNum(p), 2);
     Gia_ManForEachPi( pM, pObj, i )
         if ( i == Gia_ManRegNum(p) )
             break;
-        else if ( Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) )
-            Vec_IntPush( vLits, i );
+        else if ( (Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) )
+            Vec_IntWriteEntry( vLits, i, (Vec_IntEntry(vLits, i) & 1) );
     Vec_IntFree( vMap );
 
     // cleanup
@@ -243,7 +263,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit )
+void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit )
 {
     Gia_Obj_t * pObj;
     word * pData1, * pData0;
@@ -252,7 +272,7 @@ void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit )
     {
         pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
         pData1 = pData0 + p->iData;
-        if ( vInit == NULL ) // both X
+        if ( vInit == NULL ) // X
             for ( i = 0; i < p->iData; i++ )
                 pData0[i] = pData1[i] = 0;
         else if ( Vec_IntEntry(vInit, k) == 0 ) // 0
@@ -261,12 +281,12 @@ void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit )
         else if ( Vec_IntEntry(vInit, k) == 1 ) // 1
             for ( i = 0; i < p->iData; i++ )
                 pData0[i] = 0, pData1[i] = ~(word)0;
-        else // if ( Vec_IntEntry(vInit, k) == 2 )
+        else // if ( Vec_IntEntry(vInit, k) > 1 ) // X
             for ( i = 0; i < p->iData; i++ )
                 pData0[i] = pData1[i] = 0;
     }
 }
-void Bmc_RoseSimulateObj( Gia_Man_t * p, int Id )
+void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id )
 {
     Gia_Obj_t * pObj = Gia_ManObj( p, Id );
     word * pData0, * pDataA0, * pDataB0;
@@ -367,7 +387,7 @@ void Bmc_RoseSimulateObj( Gia_Man_t * p, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_RoseHighestScore( Gia_Man_t * p, int * pCost )
+int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost )
 {
     Gia_Obj_t * pObj;
     word * pData0, * pData1;
@@ -392,7 +412,7 @@ int Bmc_RoseHighestScore( Gia_Man_t * p, int * pCost )
     ABC_FREE( pCounts );
     return iPat;
 }
-void Bmc_RoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
+void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
 {
     Gia_Obj_t * pObj;
     word * pData0, * pData1;
@@ -424,30 +444,37 @@ void Bmc_RoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
+Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
 {
     Vec_Int_t * vInit;
     Gia_Obj_t * pObj;
-    int i, f, iPat, Cost;
+    int i, f, iPat, Cost, Cost0;
     abctime clk, clkTotal = Abc_Clock();
     Gia_ManRandomW( 1 );
     if ( fVerbose )
         printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
-    vInit = Vec_IntAlloc( Gia_ManRegNum(p) );
+    if ( vInit0 )
+        vInit = Vec_IntDup(vInit0);
+    else
+        vInit = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vInit, Gia_ManRegNum(p), 2);
+    assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
     Gia_ParTestAlloc( p, nWords );
-    Bmc_RoseSimulateInit( p, vInit0 );
+    Gia_ManRoseInit( p, vInit );
+    Cost0 = 0;
+    Vec_IntForEachEntry( vInit, iPat, i )
+        Cost0 += ((iPat >> 1) & 1);
     if ( fVerbose )
-        printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Gia_ManRegNum(p), Gia_ManRegNum(p) );
+        printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 );
     for ( f = 0; f < nFrames; f++ )
     {
         clk = Abc_Clock();
         Gia_ManForEachObj( p, pObj, i )
-            Bmc_RoseSimulateObj( p, i );
-        iPat = Bmc_RoseHighestScore( p, &Cost );
-        Bmc_RoseFindStarting( p, vInit, iPat );
-        Bmc_RoseSimulateInit( p, vInit );
+            Gia_ManRoseSimulateObj( p, i );
+        iPat = Gia_ManRoseHighestScore( p, &Cost );
+        Gia_ManRoseFindStarting( p, vInit, iPat );
+        Gia_ManRoseInit( p, vInit );
         if ( fVerbose )
-            printf( "Frame =%6d : Values =%6d (out of %6d)   ", f+1, Cost, Gia_ManRegNum(p) );
+            printf( "Frame =%6d : Values =%6d (out of %6d)   ", f+1, Cost, Cost0 );
         if ( fVerbose )
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
@@ -455,6 +482,8 @@ Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int
     printf( "After %d frames, found a sequence to produce %d x-values (out of %d).  ", f, Cost, Gia_ManRegNum(p) );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
 //    Vec_IntFreeP( &vInit );
+    Vec_IntFill(vInit, Vec_IntSize(vInit), 2);
+//    printf( "The resulting init state is invalid.\n" );
     return vInit;
 }
 
@@ -469,30 +498,15 @@ Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_RoseTest( Gia_Man_t * p, int nFrames, int nWords, int fVerbose )
-{
-    Bmc_RosePerform( p, NULL, nFrames, nWords, fVerbose );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManTulipTest( Gia_Man_t * p, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
+Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
 {
     Vec_Int_t * vRes;
     if ( fSim )
-        vRes = Bmc_RosePerform( p, NULL, nFrames, nWords, fVerbose );
+        vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose );
     else
-        vRes = Gia_ManTulip( p, nFrames, nTimeOut, fVerbose );
+        vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose );
     Vec_IntFreeP( &vRes );
+    return vRes;
 }