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

New way to generate counter-examples.

This commit is contained in:
Alan Mishchenko 2024-05-08 23:13:31 -07:00
parent 3c56ccb8fb
commit c194c112ae
2 changed files with 184 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
src/aig/gia/giaPat2.c
View File

@ -184,13 +184,15 @@ static inline int Min_ManAppendCo( Min_Man_t * p, int iLit0 )
***********************************************************************/
void Min_ManFromGia_rec( Min_Man_t * pNew, Gia_Man_t * p, int iObj )
{
Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int iLit0, iLit1;
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj) );
Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj) );
pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
iLit0 = Gia_ObjFanin0Copy(pObj);
iLit1 = Gia_ObjFanin1Copy(pObj);
pObj->Value = Min_ManAppendObj( pNew, Abc_MinInt(iLit0, iLit1), Abc_MaxInt(iLit0, iLit1) );
}
Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts )
{
@ -205,7 +207,7 @@ Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts )
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFaninLit0p(p, pObj) );
pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
else
{
@ -403,8 +405,10 @@ static inline char Min_LitIsImplied2( Min_Man_t * p, int iLit )
char Val1 = Min_LitValL(p, iLit1);
assert( Min_LitIsNode(p, iLit) ); // internal node
assert( Min_LitValL(p, iLit) == 2 ); // unassigned
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
Val0 = Min_LitIsImplied1(p, iLit0);
Val1 = Min_LitValL(p, iLit1);
}
if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
Val1 = Min_LitIsImplied1(p, iLit1);
if ( Min_LitIsXor(iLit, iLit0, iLit1) )
@ -427,8 +431,10 @@ static inline char Min_LitIsImplied3( Min_Man_t * p, int iLit )
char Val1 = Min_LitValL(p, iLit1);
assert( Min_LitIsNode(p, iLit) ); // internal node
assert( Min_LitValL(p, iLit) == 2 ); // unassigned
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
Val0 = Min_LitIsImplied2(p, iLit0);
Val1 = Min_LitValL(p, iLit1);
}
if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
Val1 = Min_LitIsImplied2(p, iLit1);
if ( Min_LitIsXor(iLit, iLit0, iLit1) )
@ -451,8 +457,10 @@ static inline char Min_LitIsImplied4( Min_Man_t * p, int iLit )
char Val1 = Min_LitValL(p, iLit1);
assert( Min_LitIsNode(p, iLit) ); // internal node
assert( Min_LitValL(p, iLit) == 2 ); // unassigned
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
Val0 = Min_LitIsImplied3(p, iLit0);
Val1 = Min_LitValL(p, iLit1);
}
if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
Val1 = Min_LitIsImplied3(p, iLit1);
if ( Min_LitIsXor(iLit, iLit0, iLit1) )
@ -475,8 +483,10 @@ static inline char Min_LitIsImplied5( Min_Man_t * p, int iLit )
char Val1 = Min_LitValL(p, iLit1);
assert( Min_LitIsNode(p, iLit) ); // internal node
assert( Min_LitValL(p, iLit) == 2 ); // unassigned
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
Val0 = Min_LitIsImplied4(p, iLit0);
Val1 = Min_LitValL(p, iLit1);
}
if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
Val1 = Min_LitIsImplied4(p, iLit1);
if ( Min_LitIsXor(iLit, iLit0, iLit1) )
@ -1351,6 +1361,71 @@ void Min_ManTest2( Gia_Man_t * p )
Vec_WrdFreeP( &vSimsPi );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort )
{
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) {
printf( "Cannot open output file name \"%s\".\n", pFileName );
return;
}
Gia_Obj_t * pObj;
char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
Gia_ManForEachCo( p, pObj, i ) {
if ( Gia_ObjFaninLit0p(p, Gia_ManCo(p, i)) == 0 ) {
fprintf( pFile, "%d :\n", i );
nOuts[0]++;
}
else if ( fShort ) {
for ( c = 0; c < nCexes; c++ ) {
Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
fprintf( pFile, "%d :", i );
Vec_IntForEachEntry( vPat, iLit, k )
fprintf( pFile, " %d", iLit );
fprintf( pFile, "\n" );
}
nOuts[1]++;
}
else {
for ( c = 0; c < nCexes; c++ ) {
Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
memset(pLine, '-', Gia_ManCiNum(p) );
Vec_IntForEachEntry( vPat, iLit, k )
pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
fprintf( pFile, "%d : %s\n", i, pLine );
}
nOuts[1]++;
}
}
printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into file \"%s\".\n",
nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );
fclose( pFile );
free( pLine );
}
void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose )
{
unsigned Start = Abc_Random(1);
Vec_Int_t * vStats[3] = {0}; int i;
Vec_Wec_t * vCexes = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes );
Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
for ( i = 0; i < 3; i++ )
Vec_IntFreeP( &vStats[i] );
Vec_WecFree( vCexes );
Start = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

104
src/base/abci/abc.c
View File

@ -604,6 +604,7 @@ static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9PutOnTop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1390,7 +1391,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&putontop", Abc_CommandAbc9PutOnTop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gencex", Abc_CommandAbc9GenCex, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
// extern Mf_ManTruthCount();
@ -52659,7 +52661,6 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
@ -52764,6 +52765,105 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose );
char * pFileName = (char *)"cexes.txt";
int nMinCexes = 1;
int nMaxTries = 10;
int fUseSim = 1;
int fUseSat = 1;
int fShort = 0;
int fVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nMinCexes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nMinCexes < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
nMaxTries = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nMaxTries < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" );
goto usage;
}
pFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 's':
fUseSim ^= 1;
break;
case 't':
fUseSat ^= 1;
break;
case 'c':
fShort ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
return 0;
}
Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fVerbose, 0 );
return 0;
usage:
Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcvh]\n" );
Abc_Print( -2, "\t generates satisfying assignments for each output of the miter\n" );
Abc_Print( -2, "\t-C num : the number of timeframes [default = %d]\n", nMinCexes );
Abc_Print( -2, "\t-M num : the max simulation runs before using SAT [default = %d]\n", nMaxTries );
Abc_Print( -2, "\t-F file : the output file name [default = %s]\n", pFileName );
Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %d]\n", fUseSim ? "yes": "no" );
Abc_Print( -2, "\t-t : toggles using SAT solving [default = %d]\n", fUseSat ? "yes": "no" );
Abc_Print( -2, "\t-c : toggles outputing care literals only [default = %d]\n", fShort ? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []