Experiments with recent ideas.

1 files changed, 345 insertions, 0 deletions

diff --git a/src/sat/bmc/bmcInse.c b/src/sat/bmc/bmcInse.c
new file mode 100644
index 00000000..00cd3df3
--- /dev/null
+++ b/src/sat/bmc/bmcInse.c
@@ -0,0 +1,345 @@
+/**CFile****************************************************************
+
+  FileName    [bmcInse.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline void   Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, 2*nWords*Gia_ManObjNum(p)); p->iData = nWords; }
+static inline void   Gia_ParTestFree( Gia_Man_t * p )              { ABC_FREE( p->pData ); p->iData = 0;             }
+static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id )       { return (word *)p->pData + Id*(p->iData << 1);   }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManInseInit( Gia_Man_t * p, Vec_Int_t * vInit )
+{
+    Gia_Obj_t * pObj;
+    word * pData1, * pData0;
+    int i, k;
+    Gia_ManForEachRi( p, pObj, k )
+    {
+        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
+        pData1 = pData0 + p->iData;
+        if ( Vec_IntEntry(vInit, k) == 0 ) // 0
+            for ( i = 0; i < p->iData; i++ )
+                pData0[i] = ~(word)0, pData1[i] = 0;
+        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) > 1 ) // X
+            for ( i = 0; i < p->iData; i++ )
+                pData0[i] = pData1[i] = 0;
+    }
+}
+void Gia_ManInseSimulateObj( Gia_Man_t * p, int Id )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, Id );
+    word * pData0, * pDataA0, * pDataB0;
+    word * pData1, * pDataA1, * pDataB1;
+    int i;
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        pData0  = Gia_ParTestObj( p, Id );
+        pData1  = pData0 + p->iData;
+        if ( Gia_ObjFaninC0(pObj) )
+        {
+            pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
+            pDataA0 = pDataA1 + p->iData;
+            if ( Gia_ObjFaninC1(pObj) )
+            {
+                pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
+                pDataB0 = pDataB1 + p->iData;
+            }
+            else 
+            {
+                pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
+                pDataB1 = pDataB0 + p->iData;
+            }
+        }
+        else 
+        {
+            pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
+            pDataA1 = pDataA0 + p->iData;
+            if ( Gia_ObjFaninC1(pObj) )
+            {
+                pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
+                pDataB0 = pDataB1 + p->iData;
+            }
+            else 
+            {
+                pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
+                pDataB1 = pDataB0 + p->iData;
+            }
+        }
+        for ( i = 0; i < p->iData; i++ )
+            pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i];
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+    {
+        pData0  = Gia_ParTestObj( p, Id );
+        pData1  = pData0 + p->iData;
+        if ( Gia_ObjFaninC0(pObj) )
+        {
+            pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
+            pDataA0 = pDataA1 + p->iData;
+        }
+        else 
+        {
+            pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
+            pDataA1 = pDataA0 + p->iData;
+        }
+        for ( i = 0; i < p->iData; i++ )
+            pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
+    }
+    else if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( Gia_ObjIsPi(p, pObj) )
+        {
+            pData0  = Gia_ParTestObj( p, Id );
+            pData1  = pData0 + p->iData;
+            for ( i = 0; i < p->iData; i++ )
+                pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i];
+        }
+        else
+        {
+            int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj));
+            pData0  = Gia_ParTestObj( p, Id );
+            pData1  = pData0 + p->iData;
+            pDataA0 = Gia_ParTestObj( p, Id2 );
+            pDataA1 = pDataA0 + p->iData;
+            for ( i = 0; i < p->iData; i++ )
+                pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
+        }
+    }
+    else if ( Gia_ObjIsConst0(pObj) )
+    {
+        pData0  = Gia_ParTestObj( p, Id );
+        pData1  = pData0 + p->iData;
+        for ( i = 0; i < p->iData; i++ )
+            pData0[i] = ~(word)0, pData1[i] = 0;
+    }
+    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManInseHighestScore( Gia_Man_t * p, int * pCost )
+{
+    Gia_Obj_t * pObj;
+    word * pData0, * pData1;
+    int * pCounts, CountBest;
+    int i, k, b, nPats, iPat;
+    nPats = 64 * p->iData;
+    pCounts = ABC_CALLOC( int, nPats );
+    Gia_ManForEachRi( p, pObj, k )
+    {
+        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
+        pData1 = pData0 + p->iData;
+        for ( i = 0; i < p->iData; i++ )
+            for ( b = 0; b < 64; b++ )
+                pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary
+    }
+    iPat = 0;
+    CountBest = pCounts[0]; 
+    for ( k = 1; k < nPats; k++ )
+        if ( CountBest < pCounts[k] )
+            CountBest = pCounts[k], iPat = k;
+    *pCost = Gia_ManRegNum(p) - CountBest; // ternary
+    ABC_FREE( pCounts );
+    return iPat;
+}
+void Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs )
+{
+    Gia_Obj_t * pObj;
+    word * pData0, * pData1;
+    int i, k;
+    Vec_IntClear( vInit );
+    Gia_ManForEachRi( p, pObj, k )
+    {
+        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
+        pData1 = pData0 + p->iData;
+        for ( i = 0; i < p->iData; i++ )
+            assert( (pData0[i] & pData1[i]) == 0 );
+        if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
+            Vec_IntPush( vInit, 0 );
+        else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
+            Vec_IntPush( vInit, 1 );
+        else 
+            Vec_IntPush( vInit, 2 );
+    }
+    Gia_ManForEachPi( p, pObj, k )
+    {
+        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
+        pData1 = pData0 + p->iData;
+        for ( i = 0; i < p->iData; i++ )
+            assert( (pData0[i] & pData1[i]) == 0 );
+        if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
+            Vec_IntPush( vInputs, 0 );
+        else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
+            Vec_IntPush( vInputs, 1 );
+        else 
+            Vec_IntPush( vInputs, 2 );
+    }
+}
+Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit )
+{
+    Vec_Int_t * vRes;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
+    int i, f, iBit = 0;
+    assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
+    assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
+    assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
+    Gia_ManConst0(p)->fMark0 = 0;
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->fMark0 = Vec_IntEntry(vInit0, i);
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachRi( p, pObj, i )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == Vec_IntSize(vInputs) );
+    vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+        assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
+    Gia_ManForEachRo( p, pObj, i )
+        Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = 0;
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
+{
+    Vec_Int_t * vRes, * vInit, * vInputs;
+    Gia_Obj_t * pObj;
+    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(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
+    vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
+    Gia_ParTestAlloc( p, nWords );
+    Gia_ManInseInit( 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, Cost0, Cost0 );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        clk = Abc_Clock();
+        Gia_ManForEachObj( p, pObj, i )
+            Gia_ManInseSimulateObj( p, i );
+        iPat = Gia_ManInseHighestScore( p, &Cost );
+        Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
+        Gia_ManInseInit( p, vInit );
+        if ( fVerbose )
+            printf( "Frame =%6d : Values =%6d (out of %6d)   ", f+1, Cost, Cost0 );
+        if ( fVerbose )
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
+    Gia_ParTestFree( p );
+    vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
+    Vec_IntFreeP( &vInit );
+    Vec_IntFreeP( &vInputs );
+    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 );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
+{
+    Vec_Int_t * vRes, * vInit;
+    vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
+    vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
+    if ( vInit != vInit0 )
+        Vec_IntFree( vInit );
+    return vRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+