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

Upgrading "twoexact" to read relations in an updated format.

This commit is contained in:
Alan Mishchenko 2024-05-15 09:33:57 -07:00
parent 6ad6539c0f
commit c906dfb748
2 changed files with 50 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/misc/vec/vecWrd.h
View File

@ -1368,6 +1368,27 @@ static inline void Vec_WrdDumpBool( char * pFileName, Vec_Wrd_t * p, int nWords,
printf( "Written %d bits of simulation data for %d objects into file \"%s\".\n", nBits, Vec_WrdSize(p)/nWords, pFileName );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_WrdPrintBin( Vec_Wrd_t * p, int nWords )
{
int i, k, nNodes = Vec_WrdSize(p) / nWords;
assert( Vec_WrdSize(p) % nWords == 0 );
printf( "The array contains %d bit-strings of %d bits:\n", nNodes, 64*nWords );
for ( i = 0; i < nNodes; i++, printf("\n") )
for ( k = 0; k < 64*nWords; k++ )
printf( "%d", Abc_InfoHasBit((unsigned*)Vec_WrdEntryP(p, i*nWords), k) );
}
/**Function*************************************************************
Synopsis []
@ -1396,6 +1417,7 @@ static inline void Vec_WrdPrintHex( Vec_Wrd_t * p, int nWords )
{
int i, nNodes = Vec_WrdSize(p) / nWords;
assert( Vec_WrdSize(p) % nWords == 0 );
printf( "The array contains %d bit-strings of %d bits:\n", nNodes, 64*nWords );
for ( i = 0; i < nNodes; i++ )
Vec_WrdDumpHexOne( stdout, Vec_WrdEntryP(p, i*nWords), nWords );
}

29
src/sat/bmc/bmcMaj.c
View File

@ -23,6 +23,7 @@
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "aig/miniaig/miniaig.h"
#include "base/io/ioResub.h"
ABC_NAMESPACE_IMPL_START
@ -3714,9 +3715,35 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
{
Mini_Aig_t * pMini = NULL;
Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
int nDivs, nOuts, nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
int i, k, nDivs, nOuts, nVars = 0;
if ( !strcmp(pFileName + strlen(pFileName) - 3, "rel") )
nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
else if ( !strcmp(pFileName + strlen(pFileName) - 3, "pla") ) {
Abc_RData_t * p = Abc_ReadPla( pFileName );
Abc_RData_t * p2 = p ? Abc_RData2Rel( p ) : NULL;
if ( !p || !p2 ) return;
//Abc_WritePla(p, "_/_rel/test.pla", 0);
//Abc_WritePla(p2, "_/_rel/test2.pla", 1);
nDivs = 0;
nOuts = p->nOuts;
nVars = p->nIns;
vSimsDiv = Vec_WrdStart( p->nPats );
for ( k = 0; k < p->nIns; k++ )
for ( i = 0; i < p->nPats; i++ )
if ( Abc_RDataGetIn(p2, k, i) )
Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
vSimsOut = Vec_WrdStart( 1 << p->nOuts );
for ( k = 0; k < (1 << p->nOuts); k++ )
for ( i = 0; i < p->nPats; i++ )
if ( Abc_RDataGetOut(p2, k, i) )
Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
}
else
printf( "Unknown file extension in file \"%s\".\n", pFileName );
if ( nVars == 0 )
return;
//Vec_WrdPrintBin( vSimsDiv, 1 );
//Vec_WrdPrintBin( vSimsOut, 1 );
Exa6_SortSims( vSimsDiv, vSimsOut );
pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose );
Vec_WrdFreeP( &vSimsDiv );