diff options
| author | Niklas Een <niklas@een.se> | 2012-03-03 10:10:07 -0800 |
|---|---|---|
| committer | Niklas Een <niklas@een.se> | 2012-03-03 10:10:07 -0800 |
| commit | 5b800e05def2962c5bd515d535b5a3d7aa4ecfcd (patch) | |
| tree | 10905968ca9647deeac3a3598969d60b80c4c06f /src/misc/util | |
| parent | 929e5e16e64adc0169ec8c412a97ea9b0f5e6547 (diff) | |
| download | abc-5b800e05def2962c5bd515d535b5a3d7aa4ecfcd.tar.gz abc-5b800e05def2962c5bd515d535b5a3d7aa4ecfcd.tar.bz2 abc-5b800e05def2962c5bd515d535b5a3d7aa4ecfcd.zip | |
Counterexamples now work in Bridge
Diffstat (limited to 'src/misc/util')
| -rw-r--r-- | src/misc/util/utilBridge.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c index 3fd24936..cad98935 100644 --- a/src/misc/util/utilBridge.c +++ b/src/misc/util/utilBridge.c @@ -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)1 ); // size of vector (Armin's encoding) Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth + 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; for ( f = 0; f <= pCex->iFrame; f++ ) { @@ -220,6 +221,7 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex ) } assert( iBit == pCex->nBits ); 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++ ) Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!! // RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); |