luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Counterexamples now work in Bridge

This commit is contained in:
Niklas Een 2012-03-03 10:10:07 -08:00
parent 929e5e16e6
commit 5b800e05de
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/misc/util/utilBridge.c
View File

@ -209,8 +209,9 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding) Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth
Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete
Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // n frames Gia_WriteAigerEncodeStr( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
iBit = pCex->nRegs; iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ ) for ( f = 0; f <= pCex->iFrame; f++ )
{ {
@ -220,6 +221,7 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
} }
assert( iBit == pCex->nBits ); assert( iBit == pCex->nBits );
Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example) Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
Gia_WriteAigerEncodeStr( vStr, pCex->nRegs ); // num of flops
for ( i = 0; i < pCex->nRegs; i++ ) for ( i = 0; i < pCex->nRegs; i++ )
Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!! Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
// RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); // RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );