summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigUtil.c23
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAiger.c158
-rw-r--r--src/aig/gia/giaUtil.c24
-rw-r--r--src/aig/ioa/ioaReadAig.c71
-rw-r--r--src/aig/ioa/ioaWriteAig.c10
7 files changed, 260 insertions, 29 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 346302c5..731f7c84 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -689,6 +689,7 @@ extern void Aig_ManSetPhase( Aig_Man_t * pAig );
extern Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig );
extern void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
extern void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
+extern void Aig_ManInvertConstraints( Aig_Man_t * pAig );
/*=== aigWin.c =========================================================*/
extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 5e58fcbe..8cbaa63b 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -1565,6 +1565,29 @@ void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
}
}
+/**Function*************************************************************
+
+ Synopsis [Complements the constraint outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManInvertConstraints( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ if ( Aig_ManConstrNum(pAig) == 0 )
+ return;
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
+ Aig_ObjChild0Flip( pObj );
+ }
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d3165526..5ec8de3f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -819,6 +819,8 @@ extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
+extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
+
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 9be5681a..a7d8e481 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -350,6 +350,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
int iObj, iNode0, iNode1;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
+ int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
char * pContents, * pName;
unsigned uLit0, uLit1, uLit;
@@ -370,25 +371,76 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
return NULL;
}
- // read the file type
- pCur = (unsigned char *)pContents; while ( *pCur++ != ' ' );
+ // read the parameters (M I L O A + B C J F)
+ pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
- nTotal = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
- nInputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
- nLatches = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
- nOutputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
- nAnds = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
+ nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ if ( *pCur == ' ' )
+ {
+ assert( nOutputs == 0 );
+ // read the number of properties
+ pCur++;
+ nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nBad;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nConstr;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nJust;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nFair;
+ }
+ if ( *pCur != '\n' )
+ {
+ fprintf( stdout, "The parameter line is in a wrong format.\n" );
+ ABC_FREE( pContents );
+ return NULL;
+ }
+ pCur++;
+
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
+ fprintf( stdout, "The number of objects does not match.\n" );
ABC_FREE( pContents );
- fprintf( stdout, "The paramters are wrong.\n" );
return NULL;
}
+ if ( nJust || nFair )
+ {
+ fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
+ ABC_FREE( pContents );
+ return NULL;
+ }
+
+ if ( nConstr )
+ {
+ if ( nConstr == 1 )
+ fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+ else
+ fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+ }
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
@@ -396,6 +448,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Gia_UtilStrsav( pFileName );
ABC_FREE( pName );
+ pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_IntAlloc( 1 + nTotal );
@@ -548,6 +601,10 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
}
Vec_IntFree( vNodes );
+ // update polarity of the additional outputs
+ if ( nBad || nConstr || nJust || nFair )
+ Gia_ManInvertConstraints( pNew );
+
// skipping the comments
/*
// check the result
@@ -580,31 +637,81 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
int iObj, iNode0, iNode1;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+ int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
unsigned uLit0, uLit1, uLit;
- // read the file type
- pCur = (unsigned char *)pContents; while ( *pCur++ != ' ' );
+ // read the parameters (M I L O A + B C J F)
+ pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
- nTotal = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
- nInputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
- nLatches = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
- nOutputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
+ nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
- nAnds = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
+ nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ if ( *pCur == ' ' )
+ {
+ assert( nOutputs == 0 );
+ // read the number of properties
+ pCur++;
+ nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nBad;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nConstr;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nJust;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nFair;
+ }
+ if ( *pCur != '\n' )
+ {
+ fprintf( stdout, "The parameter line is in a wrong format.\n" );
+ return NULL;
+ }
+ pCur++;
+
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
- ABC_FREE( pContents );
- fprintf( stdout, "The paramters are wrong.\n" );
+ fprintf( stdout, "The number of objects does not match.\n" );
+ return NULL;
+ }
+ if ( nJust || nFair )
+ {
+ fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
return NULL;
}
+ if ( nConstr )
+ {
+ if ( nConstr == 1 )
+ fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+ else
+ fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+ }
+
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
+ pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_IntAlloc( 1 + nTotal );
@@ -903,6 +1010,11 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
return NULL;
}
*/
+
+ // update polarity of the additional outputs
+ if ( nBad || nConstr || nJust || nFair )
+ Gia_ManInvertConstraints( pNew );
+
// clean the PO drivers
if ( vPoTypes )
{
@@ -1243,14 +1355,19 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
p = pInit;
// write the header "M I L O A" where M = I + L + A
- fprintf( pFile, "aig%s %u %u %u %u %u\n",
+ fprintf( pFile, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Gia_ManCiNum(p) + Gia_ManAndNum(p),
Gia_ManPiNum(p),
Gia_ManRegNum(p),
- Gia_ManPoNum(p),
+ Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
Gia_ManAndNum(p) );
+ // write the extended header "B C J F"
+ if ( Gia_ManConstrNum(p) )
+ fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
+ fprintf( pFile, "\n" );
+ Gia_ManInvertConstraints( p );
if ( !fCompact )
{
// write latch drivers
@@ -1268,6 +1385,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
+ Gia_ManInvertConstraints( p );
// write the nodes into the buffer
Pos = 0;
@@ -1372,6 +1490,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
fwrite( Buffer, 1, 4, pFile );
fwrite( p->pSwitching, 1, nSize, pFile );
}
+/*
// write constraints
if ( p->nConstrs )
{
@@ -1380,6 +1499,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
fprintf( pFile, "c" );
fwrite( Buffer, 1, 4, pFile );
}
+*/
// write name
if ( p->pName )
fprintf( pFile, "n%s%c", p->pName, '\0' );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index b9a50220..f19f0602 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1224,6 +1224,30 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Complements the constraint outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManInvertConstraints( Gia_Man_t * pAig )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ if ( Gia_ManConstrNum(pAig) == 0 )
+ return;
+ Gia_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
+ Gia_ObjFlipFaninC0( pObj );
+ }
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index 096e82e4..17c93e58 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -109,6 +109,7 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Aig_Obj_t * pObj, * pNode0, * pNode1;
Aig_Man_t * pNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+ int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
char * pDrivers, * pSymbols, * pCur;//, * pType;
unsigned uLit0, uLit1, uLit;
@@ -119,27 +120,77 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
return NULL;
}
- // read the file type
- pCur = pContents; while ( *pCur++ != ' ' );
+ // read the parameters (M I L O A + B C J F)
+ pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
- nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
+ nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
- nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
+ nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
- nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
+ nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
- nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
+ nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
- nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
+ nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ if ( *pCur == ' ' )
+ {
+ assert( nOutputs == 0 );
+ // read the number of properties
+ pCur++;
+ nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nBad;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nConstr;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nJust;
+ }
+ if ( *pCur == ' ' )
+ {
+ // read the number of properties
+ pCur++;
+ nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+ nOutputs += nFair;
+ }
+ if ( *pCur != '\n' )
+ {
+ fprintf( stdout, "The parameter line is in a wrong format.\n" );
+ return NULL;
+ }
+ pCur++;
+
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
- fprintf( stdout, "The paramters are wrong.\n" );
+ fprintf( stdout, "The number of objects does not match.\n" );
+ return NULL;
+ }
+ if ( nJust || nFair )
+ {
+ fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
return NULL;
}
+ if ( nConstr )
+ {
+ if ( nConstr == 1 )
+ fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+ else
+ fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+ }
+
// allocate the empty AIG
pNew = Aig_ManStart( nAnds );
+ pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@@ -352,6 +403,10 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Aig_ManCleanup( pNew );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
+ // update polarity of the additional outputs
+ if ( nBad || nConstr || nJust || nFair )
+ Aig_ManInvertConstraints( pNew );
+
// check the result
if ( fCheck && !Aig_ManCheck( pNew ) )
{
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 7aa975f2..2f682775 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -466,18 +466,23 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
Ioa_ObjSetAigerNum( pObj, nNodes++ );
// write the header "M I L O A" where M = I + L + A
- fprintf( pFile, "aig%s %u %u %u %u %u\n",
+ fprintf( pFile, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan),
Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManRegNum(pMan),
- Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
+ Aig_ManConstrNum(pMan) ? 0 : Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManNodeNum(pMan) );
+ // write the extended header "B C J F"
+ if ( Aig_ManConstrNum(pMan) )
+ fprintf( pFile, " %u %u", Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
+ fprintf( pFile, "\n" );
// if the driver node is a constant, we need to complement the literal below
// because, in the AIGER format, literal 0/1 is represented as number 0/1
// while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
+ Aig_ManInvertConstraints( pMan );
if ( !fCompact )
{
// write latch drivers
@@ -502,6 +507,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
+ Aig_ManInvertConstraints( pMan );
// write the nodes into the buffer
Pos = 0;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:34:17 +0000