summaryrefslogtreecommitdiffstats
path: root/src/temp/esop
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/esop')
-rw-r--r--src/temp/esop/esop.h723
-rw-r--r--src/temp/esop/esopMan.c117
-rw-r--r--src/temp/esop/esopMin.c299
-rw-r--r--src/temp/esop/esopUtil.c277
-rw-r--r--src/temp/esop/module.make3
5 files changed, 1419 insertions, 0 deletions
diff --git a/src/temp/esop/esop.h b/src/temp/esop/esop.h
new file mode 100644
index 00000000..5f95f371
--- /dev/null
+++ b/src/temp/esop/esop.h
@@ -0,0 +1,723 @@
+/**CFile****************************************************************
+
+ FileName [esop.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Cover manipulation package.]
+
+ Synopsis [Internal declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: esop.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __ESOP_H__
+#define __ESOP_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <stdio.h>
+#include "vec.h"
+#include "mem.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Esop_Man_t_ Esop_Man_t;
+typedef struct Esop_Cube_t_ Esop_Cube_t;
+typedef struct Mem_Fixed_t_ Mem_Fixed_t;
+
+struct Esop_Man_t_
+{
+ int nVars; // the number of vars
+ int nWords; // the number of words
+ Mem_Fixed_t * pMemMan1; // memory manager for cubes
+ Mem_Fixed_t * pMemMan2; // memory manager for cubes
+ Mem_Fixed_t * pMemMan4; // memory manager for cubes
+ Mem_Fixed_t * pMemMan8; // memory manager for cubes
+ // temporary cubes
+ Esop_Cube_t * pOne0; // tautology cube
+ Esop_Cube_t * pOne1; // tautology cube
+ Esop_Cube_t * pTriv0; // trivial cube
+ Esop_Cube_t * pTriv1; // trivial cube
+ Esop_Cube_t * pTemp; // cube for computing the distance
+ Esop_Cube_t * pBubble; // cube used as a separator
+ // temporary storage for the new cover
+ int nCubes; // the number of cubes
+ Esop_Cube_t ** ppStore; // storage for cubes by number of literals
+};
+
+struct Esop_Cube_t_
+{
+ Esop_Cube_t * pNext; // the pointer to the next cube in the cover
+ unsigned nVars : 10; // the number of variables
+ unsigned nWords : 12; // the number of machine words
+ unsigned nLits : 10; // the number of literals in the cube
+ unsigned uData[1]; // the bit-data for the cube
+};
+
+#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
+#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#define REALLOC(type, obj, num) \
+ ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+ ((type *) malloc(sizeof(type) * (num))))
+
+// iterators through the entries in the linked lists of cubes
+#define Esop_CoverForEachCube( pCover, pCube ) \
+ for ( pCube = pCover; \
+ pCube; \
+ pCube = pCube->pNext )
+#define Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \
+ for ( pCube = pCover, \
+ pCube2 = pCube? pCube->pNext: NULL; \
+ pCube; \
+ pCube = pCube2, \
+ pCube2 = pCube? pCube->pNext: NULL )
+#define Esop_CoverForEachCubePrev( pCover, pCube, ppPrev ) \
+ for ( pCube = pCover, \
+ ppPrev = &(pCover); \
+ pCube; \
+ ppPrev = &pCube->pNext, \
+ pCube = pCube->pNext )
+
+
+// macros to get hold of bits and values in the cubes
+static inline int Esop_CubeHasBit( Esop_Cube_t * p, int i ) { return (p->uData[i >> 5] & (1<<(i & 31))) > 0; }
+static inline void Esop_CubeSetBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] |= (1<<(i & 31)); }
+static inline void Esop_CubeXorBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] ^= (1<<(i & 31)); }
+static inline int Esop_CubeGetVar( Esop_Cube_t * p, int Var ) { return 3 & (p->uData[(Var<<1)>>5] >> ((Var<<1) & 31)); }
+static inline void Esop_CubeXorVar( Esop_Cube_t * p, int Var, int Value ) { p->uData[(Var<<1)>>5] ^= (Value<<((Var<<1) & 31)); }
+static inline int Esop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
+
+/*=== esopMem.c ===========================================================*/
+extern Mem_Fixed_t * Mem_FixedStart( int nEntrySize );
+extern void Mem_FixedStop( Mem_Fixed_t * p, int fVerbose );
+extern char * Mem_FixedEntryFetch( Mem_Fixed_t * p );
+extern void Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry );
+extern void Mem_FixedRestart( Mem_Fixed_t * p );
+extern int Mem_FixedReadMemUsage( Mem_Fixed_t * p );
+/*=== esopMin.c ===========================================================*/
+extern void Esop_EsopMinimize( Esop_Man_t * p );
+extern void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube );
+/*=== esopMan.c ===========================================================*/
+extern Esop_Man_t * Esop_ManAlloc( int nVars );
+extern void Esop_ManClean( Esop_Man_t * p, int nSupp );
+extern void Esop_ManFree( Esop_Man_t * p );
+/*=== esopUtil.c ===========================================================*/
+extern void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube );
+extern void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover );
+extern void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p );
+extern void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop );
+extern void Esop_CoverCheck( Esop_Man_t * p );
+extern int Esop_CubeCheck( Esop_Cube_t * pCube );
+extern Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize );
+extern void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover );
+extern int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates the cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CubeAlloc( Esop_Man_t * p )
+{
+ Esop_Cube_t * pCube;
+ if ( p->nWords <= 1 )
+ pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan1 );
+ else if ( p->nWords <= 2 )
+ pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan2 );
+ else if ( p->nWords <= 4 )
+ pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan4 );
+ else if ( p->nWords <= 8 )
+ pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan8 );
+ pCube->pNext = NULL;
+ pCube->nVars = p->nVars;
+ pCube->nWords = p->nWords;
+ pCube->nLits = 0;
+ memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
+ return pCube;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the cube representing elementary var.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CubeAllocVar( Esop_Man_t * p, int iVar, int fCompl )
+{
+ Esop_Cube_t * pCube;
+ pCube = Esop_CubeAlloc( p );
+ Esop_CubeXorBit( pCube, iVar*2+fCompl );
+ pCube->nLits = 1;
+ return pCube;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CubeDup( Esop_Man_t * p, Esop_Cube_t * pCopy )
+{
+ Esop_Cube_t * pCube;
+ pCube = Esop_CubeAlloc( p );
+ memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+ pCube->nLits = pCopy->nLits;
+ return pCube;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CubeRecycle( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+ if ( pCube->nWords <= 1 )
+ Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube );
+ else if ( pCube->nWords <= 2 )
+ Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube );
+ else if ( pCube->nWords <= 4 )
+ Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube );
+ else if ( pCube->nWords <= 8 )
+ Mem_FixedEntryRecycle( p->pMemMan8, (char *)pCube );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the cube cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CoverRecycle( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube, * pCube2;
+ if ( pCover == NULL )
+ return;
+ if ( pCover->nWords <= 1 )
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube );
+ else if ( pCover->nWords <= 2 )
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube );
+ else if ( pCover->nWords <= 4 )
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube );
+ else if ( pCover->nWords <= 8 )
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ Mem_FixedEntryRecycle( p->pMemMan8, (char *)pCube );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the cube cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CoverDup( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube, * pCubeNew;
+ Esop_Cube_t * pCoverNew = NULL, ** ppTail = &pCoverNew;
+ Esop_CoverForEachCube( pCover, pCube )
+ {
+ pCubeNew = Esop_CubeDup( p, pCube );
+ *ppTail = pCubeNew;
+ ppTail = &pCubeNew->pNext;
+ }
+ *ppTail = NULL;
+ return pCoverNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of cubes in the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubeCountLits( Esop_Cube_t * pCube )
+{
+ unsigned uData;
+ int Count = 0, i, w;
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ {
+ uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+ for ( i = 0; i < 32; i += 2 )
+ if ( uData & (1 << i) )
+ Count++;
+ }
+ return Count;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of cubes in the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CubeGetLits( Esop_Cube_t * pCube, Vec_Int_t * vLits )
+{
+ unsigned uData;
+ int i, w;
+ Vec_IntClear( vLits );
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ {
+ uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+ for ( i = 0; i < 32; i += 2 )
+ if ( uData & (1 << i) )
+ Vec_IntPush( vLits, w*16 + i/2 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of cubes in the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CoverCountCubes( Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube;
+ int Count = 0;
+ Esop_CoverForEachCube( pCover, pCube )
+ Count++;
+ return Count;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Checks if two cubes are disjoint.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubesDisjoint( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 )
+{
+ unsigned uData;
+ int i;
+ assert( pCube0->nVars == pCube1->nVars );
+ for ( i = 0; i < (int)pCube0->nWords; i++ )
+ {
+ uData = pCube0->uData[i] & pCube1->uData[i];
+ uData = (uData | (uData >> 1)) & 0x55555555;
+ if ( uData != 0x55555555 )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the disjoint variables of the two cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CoverGetDisjVars( Esop_Cube_t * pThis, Esop_Cube_t * pCube, Vec_Int_t * vVars )
+{
+ unsigned uData;
+ int i, w;
+ Vec_IntClear( vVars );
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ {
+ uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
+ uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
+ if ( uData == 0 )
+ continue;
+ for ( i = 0; i < 32; i += 2 )
+ if ( uData & (1 << i) )
+ Vec_IntPush( vVars, w*16 + i/2 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if two cubes are disjoint.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubesDistOne( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, Esop_Cube_t * pTemp )
+{
+ unsigned uData;
+ int i, fFound = 0;
+ for ( i = 0; i < (int)pCube0->nWords; i++ )
+ {
+ uData = pCube0->uData[i] ^ pCube1->uData[i];
+ if ( uData == 0 )
+ {
+ if ( pTemp ) pTemp->uData[i] = 0;
+ continue;
+ }
+ if ( fFound )
+ return 0;
+ uData = (uData | (uData >> 1)) & 0x55555555;
+ if ( (uData & (uData-1)) > 0 ) // more than one 1
+ return 0;
+ if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
+ fFound = 1;
+ }
+ if ( fFound == 0 )
+ {
+ printf( "\n" );
+ Esop_CubeWrite( stdout, pCube0 );
+ Esop_CubeWrite( stdout, pCube1 );
+ printf( "Error: Esop_CubesDistOne() looks at two equal cubes!\n" );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if two cubes are disjoint.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubesDistTwo( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, int * pVar0, int * pVar1 )
+{
+ unsigned uData;//, uData2;
+ int i, k, Var0 = -1, Var1 = -1;
+ for ( i = 0; i < (int)pCube0->nWords; i++ )
+ {
+ uData = pCube0->uData[i] ^ pCube1->uData[i];
+ if ( uData == 0 )
+ continue;
+ if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
+ return 0;
+ uData = (uData | (uData >> 1)) & 0x55555555;
+ if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
+ return 0;
+ for ( k = 0; k < 32; k += 2 )
+ if ( uData & (1 << k) )
+ {
+ if ( Var0 == -1 )
+ Var0 = 16 * i + k/2;
+ else if ( Var1 == -1 )
+ Var1 = 16 * i + k/2;
+ else
+ return 0;
+ }
+ /*
+ if ( Var0 >= 0 )
+ {
+ uData &= 0xFFFF;
+ uData2 = (uData >> 16);
+ if ( uData && uData2 )
+ return 0;
+ if ( uData )
+ {
+ }
+ uData }= uData2;
+ uData &= 0x
+ }
+ */
+ }
+ if ( Var0 >= 0 && Var1 >= 0 )
+ {
+ *pVar0 = Var0;
+ *pVar1 = Var1;
+ return 1;
+ }
+ if ( Var0 == -1 || Var1 == -1 )
+ {
+ printf( "\n" );
+ Esop_CubeWrite( stdout, pCube0 );
+ Esop_CubeWrite( stdout, pCube1 );
+ printf( "Error: Esop_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Makes the produce of two cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CubesProduct( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 )
+{
+ Esop_Cube_t * pCube;
+ int i;
+ assert( pCube0->nVars == pCube1->nVars );
+ pCube = Esop_CubeAlloc( p );
+ for ( i = 0; i < p->nWords; i++ )
+ pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
+ pCube->nLits = Esop_CubeCountLits( pCube );
+ return pCube;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Makes the produce of two cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Esop_Cube_t * Esop_CubesXor( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 )
+{
+ Esop_Cube_t * pCube;
+ int i;
+ assert( pCube0->nVars == pCube1->nVars );
+ pCube = Esop_CubeAlloc( p );
+ for ( i = 0; i < p->nWords; i++ )
+ pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
+ pCube->nLits = Esop_CubeCountLits( pCube );
+ return pCube;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Makes the produce of two cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubesAreEqual( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 )
+{
+ int i;
+ for ( i = 0; i < (int)pCube0->nWords; i++ )
+ if ( pCube0->uData[i] != pCube1->uData[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CubeIsContained( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 )
+{
+ int i;
+ for ( i = 0; i < (int)pCube0->nWords; i++ )
+ if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the cube into the result of merging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CubesTransform( Esop_Cube_t * pCube, Esop_Cube_t * pDist, Esop_Cube_t * pMask )
+{
+ int w;
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ {
+ pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w];
+ pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the cube into the result of distance-1 merging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CubesTransformOr( Esop_Cube_t * pCube, Esop_Cube_t * pDist )
+{
+ int w;
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ pCube->uData[w] |= pDist->uData[w];
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Sorts the cover in the increasing number of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Esop_CoverExpandRemoveEqual( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube, * pCube2, * pThis;
+ if ( pCover == NULL )
+ {
+ Esop_ManClean( p, p->nVars );
+ return;
+ }
+ Esop_ManClean( p, pCover->nVars );
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ {
+ // go through the linked list
+ Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+ if ( Esop_CubesAreEqual( pCube, pThis ) )
+ {
+ Esop_CubeRecycle( p, pCube );
+ break;
+ }
+ if ( pThis != NULL )
+ continue;
+ pCube->pNext = p->ppStore[pCube->nLits];
+ p->ppStore[pCube->nLits] = pCube;
+ p->nCubes++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Esop_CoverContainsCube( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+ Esop_Cube_t * pThis;
+ int i;
+/*
+ // this cube cannot be equal to any cube
+ Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+ {
+ if ( Esop_CubesAreEqual( pCube, pThis ) )
+ {
+ Esop_CubeWrite( stdout, pCube );
+ assert( 0 );
+ }
+ }
+*/
+ // try to find a containing cube
+ for ( i = 0; i <= (int)pCube->nLits; i++ )
+ Esop_CoverForEachCube( p->ppStore[i], pThis )
+ {
+ // skip the bubble
+ if ( pThis != p->pBubble && Esop_CubeIsContained( pThis, pCube ) )
+ return 1;
+ }
+ return 0;
+}
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/esop/esopMan.c b/src/temp/esop/esopMan.c
new file mode 100644
index 00000000..5c411349
--- /dev/null
+++ b/src/temp/esop/esopMan.c
@@ -0,0 +1,117 @@
+/**CFile****************************************************************
+
+ FileName [esopMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Cover manipulation package.]
+
+ Synopsis [SOP manipulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: esopMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the minimization manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Esop_Man_t * Esop_ManAlloc( int nVars )
+{
+ Esop_Man_t * pMan;
+ // start the manager
+ pMan = ALLOC( Esop_Man_t, 1 );
+ memset( pMan, 0, sizeof(Esop_Man_t) );
+ pMan->nVars = nVars;
+ pMan->nWords = Esop_BitWordNum( nVars * 2 );
+ pMan->pMemMan1 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) );
+ pMan->pMemMan2 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) );
+ pMan->pMemMan4 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) );
+ pMan->pMemMan8 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (8 - 1) );
+ // allocate storage for the temporary cover
+ pMan->ppStore = ALLOC( Esop_Cube_t *, pMan->nVars + 1 );
+ // create tautology cubes
+ Esop_ManClean( pMan, nVars );
+ pMan->pOne0 = Esop_CubeAlloc( pMan );
+ pMan->pOne1 = Esop_CubeAlloc( pMan );
+ pMan->pTemp = Esop_CubeAlloc( pMan );
+ pMan->pBubble = Esop_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0;
+ // create trivial cubes
+ Esop_ManClean( pMan, 1 );
+ pMan->pTriv0 = Esop_CubeAllocVar( pMan, 0, 0 );
+ pMan->pTriv1 = Esop_CubeAllocVar( pMan, 0, 0 );
+ Esop_ManClean( pMan, nVars );
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cleans the minimization manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_ManClean( Esop_Man_t * p, int nSupp )
+{
+ // set the size of the cube manager
+ p->nVars = nSupp;
+ p->nWords = Esop_BitWordNum(2*nSupp);
+ // clean the storage
+ memset( p->ppStore, 0, sizeof(Esop_Cube_t *) * (nSupp + 1) );
+ p->nCubes = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the minimization manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_ManFree( Esop_Man_t * p )
+{
+ Mem_FixedStop ( p->pMemMan1, 0 );
+ Mem_FixedStop ( p->pMemMan2, 0 );
+ Mem_FixedStop ( p->pMemMan4, 0 );
+ Mem_FixedStop ( p->pMemMan8, 0 );
+ free( p->ppStore );
+ free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/esop/esopMin.c b/src/temp/esop/esopMin.c
new file mode 100644
index 00000000..7a460f8e
--- /dev/null
+++ b/src/temp/esop/esopMin.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+
+ FileName [esopMin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Cover manipulation package.]
+
+ Synopsis [ESOP manipulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: esopMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Esop_EsopRewrite( Esop_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [ESOP minimization procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_EsopMinimize( Esop_Man_t * p )
+{
+ int nCubesInit, nCubesOld, nIter;
+ if ( p->nCubes < 3 )
+ return;
+ nIter = 0;
+ nCubesInit = p->nCubes;
+ do {
+ nCubesOld = p->nCubes;
+ Esop_EsopRewrite( p );
+ nIter++;
+ }
+ while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of rewriting using distance 2 cubes.]
+
+ Description [The weakness of this procedure is that it tries each cube
+ with only one distance-2 cube. If this pair does not lead to improvement
+ the cube is inserted into the cover anyhow, and we try another pair.
+ A possible improvement would be to try this cube with all distance-2
+ cubes, until an improvement is found, or until all such cubes are tried.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_EsopRewrite( Esop_Man_t * p )
+{
+ Esop_Cube_t * pCube, ** ppPrev;
+ Esop_Cube_t * pThis, ** ppPrevT;
+ int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
+ int nPairs = 0;
+
+ // insert the bubble before the first cube
+ p->pBubble->pNext = p->ppStore[0];
+ p->ppStore[0] = p->pBubble;
+ p->pBubble->nLits = 0;
+
+ // go through the cubes
+ while ( 1 )
+ {
+ // get the index of the bubble
+ Index = p->pBubble->nLits;
+
+ // find the bubble
+ Esop_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+ if ( pCube == p->pBubble )
+ break;
+ assert( pCube == p->pBubble );
+
+ // remove the bubble, get the next cube after the bubble
+ *ppPrev = p->pBubble->pNext;
+ pCube = p->pBubble->pNext;
+ if ( pCube == NULL )
+ for ( Index++; Index <= p->nVars; Index++ )
+ if ( p->ppStore[Index] )
+ {
+ ppPrev = &(p->ppStore[Index]);
+ pCube = p->ppStore[Index];
+ break;
+ }
+ // stop if there is no more cubes
+ if ( pCube == NULL )
+ break;
+
+ // find the first dist2 cube
+ Esop_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+ if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+ break;
+ if ( pThis == NULL && Index < p->nVars )
+ Esop_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+ if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+ break;
+ if ( pThis == NULL && Index < p->nVars - 1 )
+ Esop_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+ if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+ break;
+ // continue if there is no dist2 cube
+ if ( pThis == NULL )
+ {
+ // insert the bubble after the cube
+ p->pBubble->pNext = pCube->pNext;
+ pCube->pNext = p->pBubble;
+ p->pBubble->nLits = pCube->nLits;
+ continue;
+ }
+ nPairs++;
+
+ // remove the cubes, insert the bubble instead of pCube
+ *ppPrevT = pThis->pNext;
+ *ppPrev = p->pBubble;
+ p->pBubble->pNext = pCube->pNext;
+ p->pBubble->nLits = pCube->nLits;
+ p->nCubes -= 2;
+
+ // Exorlink-2:
+ // A{v00} B{v01} + A{v10} B{v11} =
+ // A{v00+v10} B{v01} + A{v10} B{v01+v11} =
+ // A{v00} B{v01+v11} + A{v00+v10} B{v11}
+
+ // save the dist2 parameters
+ v00 = Esop_CubeGetVar( pCube, Var0 );
+ v01 = Esop_CubeGetVar( pCube, Var1 );
+ v10 = Esop_CubeGetVar( pThis, Var0 );
+ v11 = Esop_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Esop_CubeWrite( stdout, pCube );
+//Esop_CubeWrite( stdout, pThis );
+
+ // derive the first pair of resulting cubes
+ Esop_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits -= (v00 != 3);
+ pCube->nLits += ((v00 ^ v10) != 3);
+ Esop_CubeXorVar( pThis, Var1, v01 );
+ pThis->nLits -= (v11 != 3);
+ pThis->nLits += ((v01 ^ v11) != 3);
+
+ // add the cubes
+ nCubesOld = p->nCubes;
+ Esop_EsopAddCube( p, pCube );
+ Esop_EsopAddCube( p, pThis );
+ // check if the cubes were absorbed
+ if ( p->nCubes < nCubesOld + 2 )
+ continue;
+
+ // pull out both cubes
+ assert( pThis == p->ppStore[pThis->nLits] );
+ p->ppStore[pThis->nLits] = pThis->pNext;
+ assert( pCube == p->ppStore[pCube->nLits] );
+ p->ppStore[pCube->nLits] = pCube->pNext;
+ p->nCubes -= 2;
+
+ // derive the second pair of resulting cubes
+ Esop_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits -= ((v00 ^ v10) != 3);
+ pCube->nLits += (v00 != 3);
+ Esop_CubeXorVar( pCube, Var1, v11 );
+ pCube->nLits -= (v01 != 3);
+ pCube->nLits += ((v01 ^ v11) != 3);
+
+ Esop_CubeXorVar( pThis, Var0, v00 );
+ pThis->nLits -= (v10 != 3);
+ pThis->nLits += ((v00 ^ v10) != 3);
+ Esop_CubeXorVar( pThis, Var1, v01 );
+ pThis->nLits -= ((v01 ^ v11) != 3);
+ pThis->nLits += (v11 != 3);
+
+ // add them anyhow
+ Esop_EsopAddCube( p, pCube );
+ Esop_EsopAddCube( p, pThis );
+ }
+// printf( "Pairs = %d ", nPairs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the cube to storage.]
+
+ Description [Returns 0 if the cube is added or removed. Returns 1
+ if the cube is glued with some other cube and has to be added again.
+ Do not forget to clean the storage!]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Esop_EsopAddCubeInt( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+ Esop_Cube_t * pThis, ** ppPrev;
+ // try to find the identical cube
+ Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+ {
+ if ( Esop_CubesAreEqual( pCube, pThis ) )
+ {
+ *ppPrev = pThis->pNext;
+ Esop_CubeRecycle( p, pCube );
+ Esop_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 0;
+ }
+ }
+ // find a distance-1 cube if it exists
+ if ( pCube->nLits < pCube->nVars )
+ Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+ {
+ if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Esop_CubesTransform( pCube, pThis, p->pTemp );
+ pCube->nLits++;
+ Esop_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+ {
+ if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Esop_CubesTransform( pCube, pThis, p->pTemp );
+ pCube->nLits--;
+ Esop_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ if ( pCube->nLits > 0 )
+ Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+ {
+ if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Esop_CubesTransform( pCube, pThis, p->pTemp );
+ Esop_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ // add the cube
+ pCube->pNext = p->ppStore[pCube->nLits];
+ p->ppStore[pCube->nLits] = pCube;
+ p->nCubes++;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the cube to storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+ assert( pCube != p->pBubble );
+ assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
+ while ( Esop_EsopAddCubeInt( p, pCube ) );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/esop/esopUtil.c b/src/temp/esop/esopUtil.c
new file mode 100644
index 00000000..7230cc87
--- /dev/null
+++ b/src/temp/esop/esopUtil.c
@@ -0,0 +1,277 @@
+/**CFile****************************************************************
+
+ FileName [esopUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Cover manipulation package.]
+
+ Synopsis [Utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: esopUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube )
+{
+ int i;
+ assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
+ for ( i = 0; i < (int)pCube->nVars; i++ )
+ if ( Esop_CubeHasBit(pCube, i*2) )
+ {
+ if ( Esop_CubeHasBit(pCube, i*2+1) )
+ fprintf( pFile, "-" );
+ else
+ fprintf( pFile, "0" );
+ }
+ else
+ {
+ if ( Esop_CubeHasBit(pCube, i*2+1) )
+ fprintf( pFile, "1" );
+ else
+ fprintf( pFile, "?" );
+ }
+ fprintf( pFile, " 1\n" );
+// fprintf( pFile, " %d\n", pCube->nLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube;
+ Esop_CoverForEachCube( pCover, pCube )
+ Esop_CubeWrite( pFile, pCube );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p )
+{
+ Esop_Cube_t * pCube;
+ int i;
+ for ( i = 0; i <= p->nVars; i++ )
+ {
+ Esop_CoverForEachCube( p->ppStore[i], pCube )
+ {
+ printf( "%2d : ", i );
+ if ( pCube == p->pBubble )
+ {
+ printf( "Bubble\n" );
+ continue;
+ }
+ Esop_CubeWrite( pFile, pCube );
+ }
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop )
+{
+ char Buffer[1000];
+ Esop_Cube_t * pCube;
+ FILE * pFile;
+ int i;
+ sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
+ for ( i = strlen(Buffer) - 1; i >= 0; i-- )
+ if ( Buffer[i] == '<' || Buffer[i] == '>' )
+ Buffer[i] = '_';
+ pFile = fopen( Buffer, "w" );
+ fprintf( pFile, "# %s cover for output %s generated by ABC\n", fEsop? "ESOP":"SOP", pName );
+ fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
+ fprintf( pFile, ".o %d\n", 1 );
+ fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) );
+ if ( fEsop ) fprintf( pFile, ".type esop\n" );
+ Esop_CoverForEachCube( pCover, pCube )
+ Esop_CubeWrite( pFile, pCube );
+ fprintf( pFile, ".e\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CoverCheck( Esop_Man_t * p )
+{
+ Esop_Cube_t * pCube;
+ int i;
+ for ( i = 0; i <= p->nVars; i++ )
+ Esop_CoverForEachCube( p->ppStore[i], pCube )
+ assert( i == (int)pCube->nLits );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Esop_CubeCheck( Esop_Cube_t * pCube )
+{
+ int i;
+ for ( i = 0; i < (int)pCube->nVars; i++ )
+ if ( Esop_CubeGetVar( pCube, i ) == 0 )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the cover from the sorted structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize )
+{
+ Esop_Cube_t * pCov = NULL, ** ppTail = &pCov;
+ Esop_Cube_t * pCube, * pCube2;
+ int i;
+ for ( i = 0; i <= nSuppSize; i++ )
+ {
+ Esop_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
+ {
+ assert( i == (int)pCube->nLits );
+ *ppTail = pCube;
+ ppTail = &pCube->pNext;
+ assert( pCube->uData[0] ); // not a bubble
+ }
+ }
+ *ppTail = NULL;
+ return pCov;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sorts the cover in the increasing number of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube, * pCube2;
+ Esop_ManClean( p, p->nVars );
+ Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+ {
+ pCube->pNext = p->ppStore[pCube->nLits];
+ p->ppStore[pCube->nLits] = pCube;
+ p->nCubes++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sorts the cover in the increasing number of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+ Esop_Cube_t * pCube;
+ int i, Counter;
+ if ( pCover == NULL )
+ return 0;
+ // clean the cube
+ for ( i = 0; i < (int)pCover->nWords; i++ )
+ p->pTemp->uData[i] = ~((unsigned)0);
+ // add the bit data
+ Esop_CoverForEachCube( pCover, pCube )
+ for ( i = 0; i < (int)pCover->nWords; i++ )
+ p->pTemp->uData[i] &= pCube->uData[i];
+ // count the vars
+ Counter = 0;
+ for ( i = 0; i < (int)pCover->nVars; i++ )
+ Counter += ( Esop_CubeGetVar(p->pTemp, i) != 3 );
+ return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/esop/module.make b/src/temp/esop/module.make
new file mode 100644
index 00000000..1003ccc1
--- /dev/null
+++ b/src/temp/esop/module.make
@@ -0,0 +1,3 @@
+SRC += src/temp/esop/esopMan.c \
+ src/temp/esop/esopMin.c \
+ src/temp/esop/esopUtil.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-10 16:10:15 +0000