Experiments with pattern generation.

abclib.dsp

@@ -5095,6 +5095,10 @@ SOURCE=.\src\aig\gia\giaPat.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaPat2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaPf.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -622,6 +622,8 @@ static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * p
 static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )        { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1;                }
 static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )          { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds);          }
 static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )         { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1);      }
+static inline int          Gia_ObjUpdateTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )      { if ( Gia_ObjIsTravIdCurrent(p, pObj) )  return 1; Gia_ObjSetTravIdCurrent(p, pObj);  return 0; }
+static inline int          Gia_ObjUpdateTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )     { if ( Gia_ObjIsTravIdPrevious(p, pObj) ) return 1; Gia_ObjSetTravIdPrevious(p, pObj); return 0; }
 static inline void         Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id )                 { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds;                     }
 static inline void         Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id )                { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1;                 }
 static inline int          Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id )                  { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds);           }

src/aig/gia/giaSimBase.c

@@ -2522,6 +2522,106 @@ int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Serialization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSim2ArrayOne( Vec_Wrd_t * vSimsPi, Vec_Int_t * vRes )
+{
+    word * pInfo = Vec_WrdArray(vSimsPi); int w, i;
+    word * pCare = pInfo + Vec_WrdSize(vSimsPi);
+    Vec_IntClear( vRes );
+    for ( w = 0; w < Vec_WrdSize(vSimsPi); w++ )
+        if ( pCare[w] )
+            for ( i = 0; i < 64; i++ )
+                if ( Abc_TtGetBit(pCare, w*64+i) )
+                    Vec_IntPush( vRes, Abc_Var2Lit(w*64+i, Abc_TtGetBit(pInfo, w*64+i)) );
+    Vec_IntPush( vRes, Vec_WrdSize(vSimsPi) );
+}
+Vec_Wec_t * Gia_ManSim2Array( Vec_Ptr_t * vSims )
+{
+    Vec_Wec_t * vRes = Vec_WecStart( Vec_PtrSize(vSims) );
+    Vec_Int_t * vLevel; int i;
+    Vec_WecForEachLevel( vRes, vLevel, i )
+        Gia_ManSim2ArrayOne( (Vec_Wrd_t *)Vec_PtrEntry(vSims, i), vLevel );
+    return vRes;
+}
+
+Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes )
+{
+    int i, iLit, nWords = Vec_IntEntryLast(vRes);
+    Vec_Wrd_t * vSimsPi = Vec_WrdStart( 2*nWords );
+    word * pInfo = Vec_WrdArray(vSimsPi);
+    word * pCare = pInfo + nWords;
+    Vec_IntPop( vRes );
+    Vec_IntForEachEntry( vRes, iLit, i )
+    {
+        Abc_TtXorBit( pCare, Abc_Lit2Var(iLit) );
+        if ( Abc_LitIsCompl(iLit) )
+            Abc_TtXorBit( pInfo, Abc_Lit2Var(iLit) );
+    }
+    Vec_IntPush( vRes, nWords );
+    Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
+    return vSimsPi;
+}
+Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes )
+{
+    Vec_Ptr_t * vSims = Vec_PtrAlloc( Vec_WecSize(vRes) );
+    Vec_Int_t * vLevel; int i;
+    Vec_WecForEachLevel( vRes, vLevel, i )
+        Vec_PtrPush( vSims, Gia_ManArray2SimOne(vLevel) );
+    return vSims;
+}
+
+void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi )
+{
+    Vec_Ptr_t * vTemp = Vec_PtrAlloc( 2 );
+    Vec_PtrPushTwo( vTemp, vSimsPi, vSimsPi );
+    {
+        Vec_Wec_t * vRes = Gia_ManSim2Array( vTemp );
+        Vec_WecDumpBin( "temp.sims", vRes, 1 );
+        {
+            Vec_Wec_t * vRes = Vec_WecReadBin( "temp.sims", 1 );
+            Vec_Ptr_t * vTemp2 = Gia_ManArray2Sim( vRes );
+            Vec_Wrd_t * vSimsPi2 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 0 );
+            Vec_Wrd_t * vSimsPi3 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 1 );
+
+            Abc_TtAnd( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi)+Vec_WrdSize(vSimsPi), Vec_WrdSize(vSimsPi), 0 );
+
+            vSimsPi->nSize *= 2;
+            vSimsPi2->nSize *= 2;
+            vSimsPi3->nSize *= 2;
+            Vec_WrdDumpHex( "test1.hex", vSimsPi,  1, 1 );
+            Vec_WrdDumpHex( "test2.hex", vSimsPi2, 1, 1 );
+            Vec_WrdDumpHex( "test3.hex", vSimsPi3, 1, 1 );
+            vSimsPi->nSize /= 2;
+            vSimsPi2->nSize /= 2;
+            vSimsPi3->nSize /= 2;
+
+            if ( Vec_WrdEqual( vSimsPi, vSimsPi2 ) )
+                printf( "Success.\n" );
+            else
+                printf( "Failure.\n" );
+            if ( Vec_WrdEqual( vSimsPi, vSimsPi3 ) )
+                printf( "Success.\n" );
+            else
+                printf( "Failure.\n" );
+            Vec_WrdFree( vSimsPi2 );
+            Vec_WrdFree( vSimsPi3 );
+            Vec_PtrFree( vTemp2 );
+            Vec_WecFree( vRes );
+        }
+        Vec_WecFree( vRes );
+    }
+    Vec_PtrFree( vTemp );
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/module.make

@@ -60,6 +60,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaOf.c \
     src/aig/gia/giaPack.c \
     src/aig/gia/giaPat.c \
+    src/aig/gia/giaPat2.c \
     src/aig/gia/giaPf.c \
     src/aig/gia/giaQbf.c \
     src/aig/gia/giaReshape1.c \

src/misc/vec/vecWec.h

@@ -791,6 +791,83 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [File interface.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecDumpBin( char * pFileName, Vec_Wec_t * p, int fVerbose )
+{
+    Vec_Int_t * vLevel;
+    int i, nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    nSize = Vec_WecSize(p);
+    RetValue = fwrite( &nSize, 1, sizeof(int), pFile );
+    Vec_WecForEachLevel( p, vLevel, i )
+    {
+        nSize = Vec_IntSize(vLevel);
+        RetValue += fwrite( &nSize, 1, sizeof(int), pFile );
+        RetValue += fwrite( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile );
+    }
+    fclose( pFile );
+    if ( RetValue != (int)sizeof(int)*(Vec_WecSizeSize(p)+Vec_WecSize(p)+1) )
+        printf( "Error writing data into file.\n" );
+    if ( fVerbose )
+        printf( "Written %d integer arrays into file \"%s\".\n", Vec_WecSize(p), pFileName );
+}
+static inline Vec_Wec_t * Vec_WecReadBin( char * pFileName, int fVerbose )
+{
+    Vec_Wec_t * p = NULL; Vec_Int_t * vLevel; int i, nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );
+    nSize = ftell( pFile );
+    if ( nSize == 0 )
+    {
+        printf( "The input file is empty.\n" );
+        fclose( pFile );
+        return NULL;
+    }
+    if ( nSize % sizeof(int) > 0 )
+    {
+        printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", (int)(nSize % sizeof(int)) );
+        fclose( pFile );
+        return NULL;
+    }
+    rewind( pFile );
+    RetValue = fread( &nSize, 1, sizeof(int), pFile );
+    assert( RetValue == 4 );
+    p = Vec_WecStart( nSize );
+    Vec_WecForEachLevel( p, vLevel, i )
+    {
+        RetValue = fread( &nSize, 1, sizeof(int), pFile );
+        assert( RetValue == 4 );
+        Vec_IntFill( vLevel, nSize, 0 );
+        RetValue = fread( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile );
+        assert( RetValue == 4*nSize );
+    }
+    fclose( pFile );
+    if ( fVerbose )
+        printf( "Read %d integer arrays from file \"%s\".\n", Vec_WecSize(p), pFileName );
+    return p;
+}
+
+
 ABC_NAMESPACE_HEADER_END
 
 #endif

src/sat/bsat/satSolver.h

@@ -292,6 +292,24 @@ static inline int sat_solver_final(sat_solver* s, int ** ppArray)
     return s->conf_final.size;
 }
 
+static inline void sat_solver_randomize( sat_solver * pSat, int iVar, int nVars )
+{
+    int i, nPols = 0, * pVars = ABC_ALLOC( int, nVars );
+    for ( i = 0; i < nVars; i++ )
+        if ( Abc_Random(0) & 1 )
+            pVars[nPols++] = iVar + i;
+    sat_solver_set_polarity( pSat, pVars, nPols );
+    for ( i = 0; i < nVars; i++ )
+        pVars[i] = iVar + i;
+    for ( i = 0; i < nVars; i++ )
+    {
+        int j = Abc_Random(0) % nVars;
+        ABC_SWAP( int, pVars[i], pVars[j] );
+    }
+    sat_solver_set_var_activity( pSat, pVars, nVars );
+    ABC_FREE( pVars );
+}
+
 static inline abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
 {
     abctime nRuntimeLimit = s->nRuntimeLimit;