SAT sweeping under constraints.

1 files changed, 245 insertions, 0 deletions

diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
new file mode 100644
index 00000000..a6d2b5e3
--- /dev/null
+++ b/src/proof/ssc/sscClass.c
@@ -0,0 +1,245 @@
+/**CFile****************************************************************
+
+  FileName    [sscClass.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [Equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash key of the simuation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ssc_GiaSimHashKey( Gia_Man_t * p, int iObj, int nTableSize )
+{
+    static int s_Primes[16] = { 
+        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
+        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+    word * pSim = Gia_ObjSim( p, iObj );
+    unsigned uHash = 0;
+    int i, nWords = Gia_ObjSimWords(p);
+    if ( pSim[0] & 1 )
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
+    else
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= pSim[i] * s_Primes[i & 0xf];
+    return (int)(uHash % nTableSize);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if sim patterns are equal up to the complement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ssc_GiaSimIsConst0( Gia_Man_t * p, int iObj0 )
+{
+    int w, nWords = Gia_ObjSimWords(p);
+    word * pSim = Gia_ObjSim( p, iObj0 );
+    if ( pSim[0] & 1 )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pSim[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim[w] )
+                return 0;
+    }
+    return 1;
+}
+static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
+{
+    int w, nWords = Gia_ObjSimWords(p);
+    word * pSim0 = Gia_ObjSim( p, iObj0 );
+    word * pSim1 = Gia_ObjSim( p, iObj1 );
+    if ( (pSim0[0] & 1) != (pSim1[0] & 1) )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim0[w] != ~pSim1[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim0[w] != pSim1[w] )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
+{
+    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
+    assert( Vec_IntSize(vClass) > 0 );
+    Vec_IntForEachEntry( vClass, Ent, i )
+    {
+        if ( i == 0 )
+        {
+            Repr = Ent;
+            Gia_ObjSetRepr( p, Ent, GIA_VOID );
+            EntPrev = Ent;
+        }
+        else
+        {
+            assert( Repr < Ent );
+            Gia_ObjSetRepr( p, Ent, Repr );
+            Gia_ObjSetNext( p, EntPrev, Ent );
+            EntPrev = Ent;
+        }
+    }
+    Gia_ObjSetNext( p, EntPrev, 0 );
+}
+int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
+{
+    Gia_Obj_t * pObj;
+    int Ent;
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Vec_IntPush( p->vClassOld, i );
+    pObj = Gia_ManObj(p, i);
+    Gia_ClassForEachObj1( p, i, Ent )
+    {
+        if ( Ssc_GiaSimAreEqual( p, i, Ent ) )
+            Vec_IntPush( p->vClassOld, Ent );
+        else
+            Vec_IntPush( p->vClassNew, Ent );
+    }
+    if ( Vec_IntSize( p->vClassNew ) == 0 )
+        return 0;
+    Ssc_GiaSimClassCreate( p, p->vClassOld );
+    Ssc_GiaSimClassCreate( p, p->vClassNew );
+    if ( Vec_IntSize(p->vClassNew) > 1 )
+        return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
+    return 1;
+}
+void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
+{
+    int * pTable, nTableSize, i, k, Key;
+    if ( Vec_IntSize(vRefined) == 0 )
+        return;
+    nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    Vec_IntForEachEntry( vRefined, i, k )
+    {
+        assert( !Ssc_GiaSimIsConst0( p, i ) );
+        Key = Ssc_GiaSimHashKey( p, i, nTableSize );
+        if ( pTable[Key] == 0 )
+        {
+            assert( Gia_ObjRepr(p, i) == 0 );
+            assert( Gia_ObjNext(p, i) == 0 );
+            Gia_ObjSetRepr( p, i, GIA_VOID );
+        }
+        else
+        {
+            Gia_ObjSetNext( p, pTable[Key], i );
+            Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) );
+            if ( Gia_ObjRepr(p, i) == GIA_VOID )
+                Gia_ObjSetRepr( p, i, pTable[Key] );
+            assert( Gia_ObjRepr(p, i) > 0 );
+        }
+        pTable[Key] = i;
+    }
+    Vec_IntForEachEntry( vRefined, i, k )
+        if ( Gia_ObjIsHead( p, i ) )
+            Ssc_GiaSimClassRefineOne( p, i );
+    ABC_FREE( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_GiaClassesRefine( Gia_Man_t * p )
+{
+    Vec_Int_t * vRefinedC;
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->pReprs == NULL )
+    {
+        assert( p->pReprs == NULL );
+        p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+        p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+        Gia_ManForEachObj( p, pObj, i )
+            Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
+        if ( p->vClassOld == NULL )
+            p->vClassOld = Vec_IntAlloc( 100 );
+        if ( p->vClassNew == NULL )
+            p->vClassNew = Vec_IntAlloc( 100 );
+    }
+    vRefinedC = Vec_IntAlloc( 100 );
+    Gia_ManForEachCand( p, pObj, i )
+        if ( Gia_ObjIsTail(p, i) )
+            Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
+        else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
+            Vec_IntPush( vRefinedC, i );
+    Ssc_GiaSimProcessRefined( p, vRefinedC );
+    Vec_IntFree( vRefinedC );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+