Skip to content

A
abc
Commit 51583557 by Alan Mishchenko
Options

Added support for constraints in AIGER (bug fix).

parent fdf79ed4
Showing with 71 additions and 33 deletions
src/aig/gia/gia.h
......@@ -650,6 +650,7 @@ extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
......
src/aig/gia/giaAiger.c
......@@ -569,7 +569,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
{
Gia_Man_t * pNew, * pTemp;
Vec_Int_t * vLits = NULL;
Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
int iObj, iNode0, iNode1;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
......@@ -625,6 +625,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
}
// create the AND gates
Gia_ManHashAlloc( pNew );
for ( i = 0; i < nAnds; i++ )
{
uLit = ((i + 1 + nInputs + nLatches) << 1);
......@@ -635,8 +636,9 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
// Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
}
Gia_ManHashStop( pNew );
// remember the place where symbols begin
pSymbols = pCur;
......@@ -680,6 +682,17 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Vec_IntFree( vLits );
}
// create the POs
for ( i = 0; i < nOutputs; i++ )
Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
for ( i = 0; i < nLatches; i++ )
Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
Vec_IntFree( vDrivers );
// create the latches
Gia_ManSetRegNum( pNew, nLatches );
// check if there are other types of information to read
pCur = pSymbols;
if ( (char *)pCur + 1 < pContents + nFileSize && *pCur == 'c' )
......@@ -838,54 +851,33 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
if ( !fBreakUsed )
{
nInvars = nConstr = 0;
vPoTypes = Vec_IntStart( Gia_ManPoNum(pNew) );
Vec_IntForEachEntry( vPoNames, Entry, i )
{
if ( Entry == ~0 )
continue;
if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
{
Vec_IntWriteEntry( vPoTypes, i, 1 );
nConstr++;
}
if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 )
{
Vec_IntWriteEntry( vPoTypes, i, 2 );
nInvars++;
}
// move constraints forward in the PO list
if ( nConstr || nInvars )
{
int k = nLatches;
Vec_Int_t * vDriversCopy = Vec_IntDup( vDrivers );
Vec_IntForEachEntry( vPoNames, Entry, i )
if ( Entry == ~0 || (strncmp( pContents+Entry, "constraint:", 11 ) != 0 && strncmp( pContents+Entry, "invariant:", 10 ) != 0) )
Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) );
Vec_IntForEachEntry( vPoNames, Entry, i )
if ( Entry != ~0 && strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) ^ 1 ); // flip polarity!!!
// update the PO count
nOutputs -= nInvars;
assert( k == nLatches + nOutputs );
Vec_IntFree( vDriversCopy );
// mark constraints
pNew->nConstrs = nConstr;
}
if ( nConstr )
fprintf( stdout, "Recognized and added %d constraints.\n", nConstr );
if ( nInvars )
fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars );
if ( nConstr == 0 && nInvars == 0 )
Vec_IntFreeP( &vPoTypes );
}
Vec_IntFree( vPoNames );
}
}
// create the POs
for ( i = 0; i < nOutputs; i++ )
Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
for ( i = 0; i < nLatches; i++ )
Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
Vec_IntFree( vDrivers );
// create the latches
Gia_ManSetRegNum( pNew, nLatches );
// skipping the comments
Vec_IntFree( vNodes );
/*
......@@ -897,6 +889,13 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
return NULL;
}
*/
// clean the PO drivers
if ( vPoTypes )
{
pNew = Gia_ManDupWithConstraints( pTemp = pNew, vPoTypes );
Gia_ManStop( pTemp );
Vec_IntFreeP( &vPoTypes );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
......
src/aig/gia/giaDup.c
......@@ -948,13 +948,13 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// dup second AIG
Gia_ManConst0(p2)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManPi(p2, i)->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachAnd( p2, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p2, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
......@@ -1466,6 +1466,44 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, nConstr = 0;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
if ( Vec_IntEntry(vPoTypes, i) == 0 ) // regular PO
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
if ( Vec_IntEntry(vPoTypes, i) == 1 ) // constraint (should be complemented!)
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ^ 1 ), nConstr++;
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// Gia_ManDupRemapEquiv( pNew, p );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew->nConstrs = nConstr;
assert( Gia_ManIsNormalized(pNew) );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment