Skip to content

Add per-object origin tracking (vOrigins) to Gia_Man_t #487

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
robtaylor wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Add per-object origin tracking (vOrigins) to Gia_Man_t #487

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
376f487
Add per-object origin tracking (vOrigins) to Gia_Man_t
robtaylor Feb 28, 2026
58dfff9
Propagate vOrigins through all ABC9 engines
robtaylor Mar 5, 2026
f2633f2
Multi-origin vOrigins with inline buffer optimization
robtaylor Mar 14, 2026
f2af506
Add &origins and &origins_id commands for origin tracking
robtaylor Mar 17, 2026
4f03583
Add per-node origin cap (nOriginsMax) to bound accumulation
robtaylor Apr 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
112 changes: 112 additions & 0 deletions src/aig/gia/gia.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <limits.h>

#include "misc/vec/vec.h"
#include "misc/vec/vecWec.h"
Expand All @@ -45,6 +46,35 @@ ABC_NAMESPACE_HEADER_START
#define GIA_NONE 0x1FFFFFFF
#define GIA_VOID 0x0FFFFFFF

// Multi-origin tracking: small-buffer optimization with overflow
#ifndef GIA_ORIGINS_INLINE
#define GIA_ORIGINS_INLINE 4 // number of inline origin slots (configurable at compile time)
#endif

typedef union {
struct {
int origins[GIA_ORIGINS_INLINE]; // -1 = unused slot
} inl;
struct {
int sentinel; // INT_MIN marks overflow mode
int count; // number of origins in overflow array
int * overflow; // heap-allocated origin array
} ovf;
} Gia_OriginsEntry_t;

#define GIA_ORIGINS_STRIDE ((int)(sizeof(Gia_OriginsEntry_t) / sizeof(int)))
#define GIA_ORIGINS_SENTINEL INT_MIN

// Compile-time checks: inline slots must cover the overflow header
// (sentinel + count + pointer; minimum 4 ints on 64-bit), and must
// not exceed the hardcoded initial overflow capacity of 8.
#if GIA_ORIGINS_INLINE < 4
# error "GIA_ORIGINS_INLINE must be >= 4 (overflow header needs sentinel+count+ptr, min 4 ints on 64-bit)"
#endif
#if GIA_ORIGINS_INLINE > 7
# error "GIA_ORIGINS_INLINE must be <= 7 (initial overflow capacity is 8)"
#endif

////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -190,6 +220,8 @@ struct Gia_Man_t_
Vec_Int_t * vIdsOrig; // original object IDs
Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
Vec_Int_t * vEquLitIds; // original object IDs proved equivalent
Vec_Int_t * vOrigins; // per-object origin mapping (from "y" extension)
int nOriginsMax; // max origins per object (0 = unlimited)
Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
Expand Down Expand Up @@ -462,6 +494,78 @@ static inline int Gia_ManIsConst0Lit( int iLit ) { return (iLit ==
static inline int Gia_ManIsConst1Lit( int iLit ) { return (iLit == 1); }
static inline int Gia_ManIsConstLit( int iLit ) { return (iLit <= 1); }

// Multi-origin accessors
static inline Gia_OriginsEntry_t * Gia_ObjOriginsEntry( Gia_Man_t * p, int iObj )
{
return (Gia_OriginsEntry_t *)(Vec_IntArray(p->vOrigins) + iObj * GIA_ORIGINS_STRIDE);
}
static inline int Gia_ObjOriginsIsOverflow( Gia_OriginsEntry_t * e )
{
return e->inl.origins[0] == GIA_ORIGINS_SENTINEL;
}
static inline int Gia_ObjOriginsNum( Gia_Man_t * p, int iObj )
{
Gia_OriginsEntry_t * e;
int k;
if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
return 0;
e = Gia_ObjOriginsEntry( p, iObj );
if ( Gia_ObjOriginsIsOverflow(e) )
return e->ovf.count;
for ( k = 0; k < GIA_ORIGINS_INLINE; k++ )
if ( e->inl.origins[k] == -1 ) break;
return k;
}
static inline int Gia_ObjOriginsGet( Gia_Man_t * p, int iObj, int idx )
{
Gia_OriginsEntry_t * e;
if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
return -1;
e = Gia_ObjOriginsEntry( p, iObj );
if ( Gia_ObjOriginsIsOverflow(e) )
return (idx < e->ovf.count) ? e->ovf.overflow[idx] : -1;
return (idx < GIA_ORIGINS_INLINE) ? e->inl.origins[idx] : -1;
}
// Backward compatible: get first/primary origin
static inline int Gia_ObjOrigin( Gia_Man_t * p, int iObj )
{
Gia_OriginsEntry_t * e;
if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
return -1;
e = Gia_ObjOriginsEntry( p, iObj );
if ( Gia_ObjOriginsIsOverflow(e) )
return e->ovf.count > 0 ? e->ovf.overflow[0] : -1;
return e->inl.origins[0];
}
// Set single origin (clears any existing, for initialization)
static inline void Gia_ObjSetOrigin( Gia_Man_t * p, int iObj, int iOrig )
{
Gia_OriginsEntry_t * e;
int k;
if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
return;
e = Gia_ObjOriginsEntry( p, iObj );
if ( Gia_ObjOriginsIsOverflow(e) && e->ovf.overflow )
ABC_FREE( e->ovf.overflow );
e->inl.origins[0] = iOrig;
for ( k = 1; k < GIA_ORIGINS_INLINE; k++ )
e->inl.origins[k] = -1;
}
// Grow vOrigins to accommodate object iObj
static inline void Gia_ManOriginsGrow( Gia_Man_t * p, int iObj )
{
Vec_IntFillExtra( p->vOrigins, (iObj + 1) * GIA_ORIGINS_STRIDE, -1 );
}
// Allocate vOrigins for nObjs objects (all entries initialized to -1)
static inline Vec_Int_t * Gia_ManOriginsAlloc( int nObjs )
{
return Vec_IntStartFull( nObjs * GIA_ORIGINS_STRIDE );
}
// Iteration macro (caller must declare int _nOrig before use, or use nOrig variant)
#define Gia_ObjForEachOrigin( p, iObj, orig, idx ) \
for ( idx = 0, _nOrig = Gia_ObjOriginsNum(p, iObj); \
(idx < _nOrig) && ((orig = Gia_ObjOriginsGet(p, iObj, idx)), 1); idx++ )

static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
Expand Down Expand Up @@ -1348,6 +1452,14 @@ extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p, int fRevFan
extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
extern Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft );
extern void Gia_ObjAddOrigin( Gia_Man_t * p, int iObj, int iOrig );
extern void Gia_ObjUnionOrigins( Gia_Man_t * p, int iDst, Gia_Man_t * pSrc, int iSrc );
extern void Gia_ManOriginsFreeOverflows( Gia_Man_t * p );
extern void Gia_ManOriginsReset( Gia_Man_t * p );
extern void Gia_ManOriginsDup( Gia_Man_t * pNew, Gia_Man_t * pOld );
extern void Gia_ManOriginsDupVec( Gia_Man_t * pNew, Gia_Man_t * pOld, Vec_Int_t * vCopies );
extern void Gia_ManOriginsAfterRoundTrip( Gia_Man_t * pNew, Gia_Man_t * pOld );
extern void Gia_ManOriginsDupIf( Gia_Man_t * pNew, Gia_Man_t * p, void * pIfMan );
extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
Expand Down
3 changes: 3 additions & 0 deletions src/aig/gia/giaAig.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -600,6 +600,7 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
Aig_ManStop( pTemp );
pGia = Gia_ManFromAig( pNew );
Aig_ManStop( pNew );
Gia_ManOriginsAfterRoundTrip( pGia, p );
Gia_ManTransferTiming( pGia, p );
return pGia;
}
Expand Down Expand Up @@ -658,6 +659,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
Gia_ManStop( pGia );
pGia = Gia_ManDup( p );
}
else
Gia_ManOriginsAfterRoundTrip( pGia, p );
Gia_ManTransferTiming( pGia, p );
return pGia;
}
Expand Down
65 changes: 62 additions & 3 deletions src/aig/gia/giaAiger.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,44 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" );
}
else {
if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
if ( fVerbose ) printf( "Skipped extension \"y\" for vEquLitIds (AIG is rehashed).\n" );
}
// populate vOrigins using vNodes to map AIG→GIA object indices
// sentinel -2 at pData[0] distinguishes new format from old
if ( vNodes && nInts >= 1 && ((int *)pCur)[0] == -2 ) {
// new multi-origin format: sentinel, then [count, lit0, lit1, ...] per AIG object
int k, nAigObjs = Vec_IntSize(vNodes);
int * pData = (int *)pCur;
int pos = 1; // skip sentinel
pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) );
for ( k = 0; k < nAigObjs && pos < nInts; k++ )
{
int giaLit = Vec_IntEntry( vNodes, k );
int giaObj = Abc_Lit2Var( giaLit );
int nOrig = pData[pos++];
int j;
for ( j = 0; j < nOrig && pos < nInts; j++, pos++ )
{
int rawLit = pData[pos];
if ( rawLit >= 0 && giaObj < Gia_ManObjNum(pNew) )
Gia_ObjAddOrigin( pNew, giaObj, Abc_Lit2Var(rawLit) );
}
}
if ( fVerbose ) printf( "Finished reading extension \"y\" (multi-origin).\n" );
}
else if ( vNodes && nInts == Vec_IntSize(vNodes) ) {
// old single-origin format: one literal per AIG object
int k;
int * pData = (int *)pCur;
pNew->vOrigins = Gia_ManOriginsAlloc( Gia_ManObjNum(pNew) );
for ( k = 0; k < nInts; k++ )
{
int giaLit = Vec_IntEntry( vNodes, k );
int giaObj = Abc_Lit2Var( giaLit );
int rawLit = pData[k];
if ( rawLit >= 0 && giaObj < Gia_ManObjNum(pNew) )
Gia_ObjSetOrigin( pNew, giaObj, Abc_Lit2Var(rawLit) );
}
}
pCur += 4*nInts;
}
Expand Down Expand Up @@ -1836,8 +1873,30 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
}
// write object classes
if ( p->vEquLitIds )
// write object origins (vOrigins takes priority over vEquLitIds)
// New variable-length format: sentinel -2, then for each object [count, lit0, lit1, ...]
if ( p->vOrigins )
{
int k, nObjs = Gia_ManObjNum(p);
Vec_Int_t * vData = Vec_IntAlloc( 1 + nObjs * 2 );
assert( Vec_IntSize(p->vOrigins) >= nObjs * GIA_ORIGINS_STRIDE );
Vec_IntPush( vData, -2 ); // sentinel distinguishes new format from old
for ( k = 0; k < nObjs; k++ )
{
int nOrig = Gia_ObjOriginsNum( p, k );
int idx, orig, _nOrig;
Vec_IntPush( vData, nOrig );
Gia_ObjForEachOrigin( p, k, orig, idx )
Vec_IntPush( vData, orig >= 0 ? 2 * orig : -1 );
}
fprintf( pFile, "y" );
Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(vData) );
fwrite( Vec_IntArray(vData), 1, (size_t)4*Vec_IntSize(vData), pFile );
if ( fVerbose ) printf( "Finished writing extension \"y\" (multi-origin, %d ints for %d objs).\n",
Vec_IntSize(vData), nObjs );
Vec_IntFree( vData );
}
else if ( p->vEquLitIds )
{
fprintf( pFile, "y" );
Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
Expand Down
2 changes: 2 additions & 0 deletions src/aig/gia/giaBalAig.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -420,6 +420,7 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p, int fStrict )
}
assert( !fStrict || Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) );
Gia_ManHashStop( pNew );
Gia_ManOriginsDup( pNew, p );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// perform cleanup
pNew = Gia_ManCleanup( pTemp = pNew );
Expand Down Expand Up @@ -819,6 +820,7 @@ Gia_Man_t * Dam_ManMultiAig( Dam_Man_t * pMan )
}
// assert( Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) );
Gia_ManHashStop( pNew );
Gia_ManOriginsDup( pNew, p );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// perform cleanup
pNew = Gia_ManCleanup( pTemp = pNew );
Expand Down
Loading