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

Merge pull request #316 from YosysHQ/povik/yosyshq-commands 

Pull command changes from YosysHQ fork
This commit is contained in:
alanminko 2024-08-08 14:59:31 -07:00 committed by GitHub
parent e6b36cb5da 5444cf281c
commit 0129b4c60a
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
19 changed files with 1045 additions and 132 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/saig/saig.h
View File

@ -114,7 +114,7 @@ extern Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * v
extern int Saig_ManDetectConstrTest( Aig_Man_t * p );
extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigConstr2.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
// -- jlong -- begin
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );

5
src/aig/saig/saigConstr2.c
View File

@ -939,7 +939,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nCo
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
@ -1000,7 +1000,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
if ( fSeqCleanup )
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}

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

@ -29343,17 +29343,20 @@ usage:
int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtkRes;
int c;
int nFrames;
int nConfs;
int nProps;
int fRemove;
int fPurge;
int fStruct;
int fInvert;
int fOldAlgo;
int fVerbose;
int nConstrs;
extern void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
@ -29361,13 +29364,14 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
nConfs = 1000;
nProps = 1000;
fRemove = 0;
fPurge = 0;
fStruct = 0;
fInvert = 0;
fOldAlgo = 0;
fVerbose = 0;
nConstrs = -1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrpsiavh" ) ) != EOF )
{
switch ( c )
{
@ -29418,6 +29422,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRemove ^= 1;
break;
case 'p':
fPurge ^= 1;
break;
case 's':
fStruct ^= 1;
break;
@ -29453,7 +29460,22 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Constraints are not defined.\n" );
return 0;
}
Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );
if ( fPurge )
{
Abc_Print( 1, "Constraints are removed.\n" );
pNtkRes = Abc_NtkMakeOnePo( pNtk, 0, Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) );
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
pNtk = Abc_FrameReadNtk(pAbc);
}
else
Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );
pNtk->nConstrs = 0;
return 0;
}
@ -29498,7 +29520,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" );
Abc_Print( -2, "usage: constr [-FCPN num] [-rpisavh]\n" );
Abc_Print( -2, "\t a toolkit for constraint manipulation\n" );
Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" );
Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" );
@ -29507,7 +29529,8 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
Abc_Print( -2, "\t-N num : manually set the last <num> POs to be constraints [default = %d]\n", nConstrs );
Abc_Print( -2, "\t-r : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" );
Abc_Print( -2, "\t-r : manually remove the constraints, converting them to POs [default = %s]\n", fRemove? "yes": "no" );
Abc_Print( -2, "\t-p : remove constraints instead of converting them to POs [default = %s]\n", fPurge? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" );
Abc_Print( -2, "\t-a : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" );
@ -29687,14 +29710,16 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int fCompl;
int fVerbose;
int fSeqCleanup;
int c;
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fCompl = 0;
fVerbose = 0;
fSeqCleanup = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cvsh" ) ) != EOF )
{
switch ( c )
{
@ -29704,6 +29729,9 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 's':
fSeqCleanup ^= 1;
break;
case 'h':
goto usage;
default:
@ -29733,7 +29761,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsComb(pNtk) )
Abc_Print( 0, "The network is combinational.\n" );
// modify the current network
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose );
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose, fSeqCleanup );
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
@ -29748,6 +29776,7 @@ usage:
Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" );
Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-s : toggle performing sequential cleanup [default = %s]\n", fSeqCleanup? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -30218,7 +30247,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF )
{
switch ( c )
{
@ -30339,9 +30368,21 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pInvFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" );
goto usage;
}
pPars->pCexFilePrefix = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'a':
pPars->fSolveAll ^= 1;
break;
case 'l':
pPars->fAnytime ^= 1;
break;
case 'x':
pPars->fStoreCex ^= 1;
break;
@ -30446,7 +30487,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-X <prefix>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@ -30461,7 +30502,9 @@ usage:
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" );
Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as <pref>*.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled");
Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-l : toggle anytime schedule when solving all outputs [default = %s]\n", pPars->fAnytime? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );

4
src/base/abci/abcDar.c
View File

@ -4682,7 +4682,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nPr
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@ -4690,7 +4690,7 @@ Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose, fSeqCleanup );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);

447
src/base/io/io.c
View File

@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
@ -116,6 +117,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
@ -686,6 +688,331 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode )
{
FILE * pFile;
Abc_Cex_t * pCex;
Abc_Cex_t * pCexCare;
Vec_Int_t * vNums;
int c, nRegs = -1, nFrames = -1;
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
return -1;
}
vNums = Vec_IntAlloc( 100 );
int usedX = 0;
*fOldFormat = 0;
int MaxLine = 1000000;
char *Buffer;
int BufferLen = 0;
int state = 0;
int iPo = 0;
nFrames = -1;
int status = 0;
int i;
int nRegsNtk = 0;
Abc_Obj_t * pObj;
Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
Buffer = ABC_ALLOC( char, MaxLine );
while ( fgets( Buffer, MaxLine, pFile ) != NULL )
{
if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' )
continue;
BufferLen = strlen(Buffer) - 1;
Buffer[BufferLen] = '\0';
if (state==0 && BufferLen>1) {
// old format detected
*fOldFormat = 1;
state = 2;
iPo = 0;
status = 1;
}
if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') {
// old format detected, first line was actually register
*fOldFormat = 1;
state = 3;
Vec_IntPush( vNums, status );
status = 1;
}
if (Buffer[0] == '.' )
break;
switch(state) {
case 0 :
{
char c = Buffer[0];
if ( c == '0' || c == '1' || c == '2' ) {
status = c - '0' ;
state = 1;
} else if ( c == 'x' ) {
// old format with one x state latch
usedX = 1;
// set to 2 so we can Abc_LatchSetInitNone
// acts like 0 when setting bits
Vec_IntPush( vNums, 2 );
nRegs = Vec_IntSize(vNums);
state = 3;
} else {
printf( "ERROR: Bad aiger status line.\n" );
return -1;
}
}
break;
case 1 :
iPo = atoi(Buffer+1);
state = 2;
break;
case 2 :
for (i=0; i<BufferLen;i++) {
char c = Buffer[i];
if ( c == '0' || c == '1' )
Vec_IntPush( vNums, c - '0' );
else if ( c == 'x') {
usedX = 1;
// set to 2 so we can Abc_LatchSetInitNone
// acts like 0 when setting bits
Vec_IntPush( vNums, 2 );
}
}
nRegs = Vec_IntSize(vNums);
if ( nRegs < nRegsNtk )
{
printf( "WARNING: Register number is smaller than in Ntk. Appending.\n" );
for (i=0; i<nRegsNtk-nRegs;i++) {
Vec_IntPush( vNums, 0 );
}
nRegs = Vec_IntSize(vNums);
}
else if ( nRegs > nRegsNtk )
{
printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" );
Vec_IntShrink( vNums, nRegsNtk );
nRegs = nRegsNtk;
}
state = 3;
break;
default:
for (i=0; i<BufferLen;i++) {
char c = Buffer[i];
if ( c == '0' || c == '1' )
Vec_IntPush( vNums, c - '0' );
else if ( c == 'x') {
usedX = 1;
Vec_IntPush( vNums, 2 );
}
}
nFrames++;
break;
}
}
fclose( pFile );
if (usedX && !xMode)
printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
int iFrameCex = nFrames;
if ( nRegs < 0 )
{
if (status == 0 || *fOldFormat == 0)
printf( "Counter-example is not available.\n" );
else
printf( "ERROR: Cannot read register number.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( nRegs != nRegsNtk )
{
printf( "ERROR: Register number not coresponding to Ntk.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( Vec_IntSize(vNums)-nRegs == 0 )
{
printf( "ERROR: Cannot read counter example.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
{
printf( "ERROR: Incorrect number of bits.\n" );
Vec_IntFree( vNums );
return -1;
}
int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1);
if ( nPi != Abc_NtkPiNum(pNtk) )
{
printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( iPo >= Abc_NtkPoNum(pNtk) )
{
printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" );
iPo = 0;
}
Abc_NtkForEachLatch( pNtk, pObj, i ) {
if ( Vec_IntEntry(vNums, i) == 1 )
Abc_LatchSetInit1(pObj);
else if ( Vec_IntEntry(vNums, i) == 2 && xMode )
Abc_LatchSetInitNone(pObj);
else
Abc_LatchSetInit0(pObj);
}
pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 );
pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1);
// the zero-based number of PO, for which verification failed
// fails in Bmc_CexVerify if not less than actual number of PO
pCex->iPo = iPo;
pCexCare->iPo = iPo;
// the zero-based number of the time-frame, for which verificaiton failed
pCex->iFrame = iFrameCex;
pCexCare->iFrame = iFrameCex;
assert( Vec_IntSize(vNums) == pCex->nBits );
for ( c = 0; c < pCex->nBits; c++ ) {
if ( Vec_IntEntry(vNums, c) == 1)
{
Abc_InfoSetBit( pCex->pData, c );
Abc_InfoSetBit( pCexCare->pData, c );
}
else if ( Vec_IntEntry(vNums, c) == 2 && xMode )
{
// nothing to set
}
else
Abc_InfoSetBit( pCexCare->pData, c );
}
Vec_IntFree( vNums );
Abc_CexFreeP( ppCex );
if ( ppCex )
*ppCex = pCex;
else
Abc_CexFree( pCex );
Abc_CexFreeP( ppCexCare );
if ( ppCexCare )
*ppCexCare = pCexCare;
else
Abc_CexFree( pCexCare );
if ( pnFrames )
*pnFrames = nFrames;
return status;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
Abc_Cex_t * pCex = NULL;
Abc_Cex_t * pCexCare = NULL;
char * pFileName;
FILE * pFile;
int fCheck = 1;
int fXMode = 0;
int c;
int fOldFormat = 0;
int verified;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'x':
fXMode ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the input file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
return 1;
}
fclose( pFile );
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
Abc_FrameClearVerifStatus( pAbc );
pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode);
if ( fOldFormat && !fCheck )
printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" );
if ( fCheck && pAbc->Status==1) {
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false );
if (!verified)
{
printf( "Checking CEX for any PO.\n" );
int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false );
Aig_ManStop( pAig );
if (verified < 0)
{
Abc_CexFreeP(&pCex);
Abc_CexFreeP(&pCexCare);
return 1;
}
pAbc->pCex->iPo = verified;
}
Abc_CexFreeP(&pCexCare);
Abc_FrameReplaceCex( pAbc, &pCex );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\n" );
fprintf( pAbc->Err, "\t reads the witness cex\n" );
fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-x : read x bits for verification [default = %s]\n", fXMode? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -2549,10 +2876,15 @@ void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex
}
extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose );
extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose );
void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin,
int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose )
int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo,
int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended )
{
Abc_Cex_t * pCare = NULL;
Abc_Obj_t * pObj;
int i, f;
if ( fPrintFull )
@ -2568,15 +2900,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
Abc_CexFreeP( &pCexFull );
}
else if ( fNames )
else
{
Abc_Cex_t * pCare = NULL;
if ( fNames )
{
fprintf( pFile, "# FALSIFYING OUTPUTS:");
fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
}
if ( fMinimize )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
fprintf( pFile, "# FALSIFYING OUTPUTS:");
fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
if ( fUseOldMin )
{
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
@ -2584,21 +2918,47 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
}
else if ( fUseSatBased )
pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
{
if ( Abc_NtkPoNum( pNtk ) == 1 )
pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
else
printf( "SAT-based CEX minimization requires having a single PO.\n" );
}
else if ( fCexInfo )
{
Gia_Man_t * p = Gia_ManFromAigSimple( pAig );
Abc_Cex_t * pCexImpl = NULL;
Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
Abc_Cex_t * pCexEss;
if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) )
printf( "Counter-example care-set verification has failed.\n" );
pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
// pCare is pCexMin from Bmc_CexTest
pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) )
printf( "Counter-example min-set verification has failed.\n" );
Abc_CexFreeP( &pCexStates );
Abc_CexFreeP( &pCexImpl );
Abc_CexFreeP( &pCexCare );
Abc_CexFreeP( &pCexEss );
}
else
pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
Aig_ManStop( pAig );
if(pCare == NULL)
if(pCare == NULL)
printf( "Counter-example minimization has failed.\n" );
}
else
if (fNames)
{
fprintf( pFile, "# FALSIFYING OUTPUTS:");
fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
fprintf( pFile, "\n");
fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
}
fprintf( pFile, "\n");
fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
if ( fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
{
int * pValues;
int nXValues = 0, iFlop = 0, iPivotPi = -1;
@ -2638,29 +2998,36 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
}
else
{
if (fExtended && fAiger && !fNames) {
fprintf( pFile, "1\n");
fprintf( pFile, "b%d\n", pCex->iPo);
}
// output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
if ( fNames )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
else
fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
if ( !fNames && fAiger)
fprintf( pFile, "\n");
// output PI values (while skipping the minimized ones)
for ( f = 0; f <= pCex->iFrame; f++ )
for ( f = 0; f <= pCex->iFrame; f++ ) {
Abc_NtkForEachPi( pNtk, pObj, i )
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
if ( fNames )
fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
else
fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
else if ( !fNames )
fprintf( pFile, "x");
if ( !fNames && fAiger)
fprintf( pFile, "\n");
}
if (fExtended && fAiger && !fNames)
fprintf( pFile, ".\n");
}
Abc_CexFreeP( &pCare );
}
else
{
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
{
if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0)
fprintf( pFile, "\n");
fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
}
}
}
/**Function*************************************************************
@ -2689,9 +3056,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
int fPrintFull = 0;
int fUseFfNames = 0;
int fVerbose = 0;
int fCexInfo = 0;
int fExtended = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF )
{
switch ( c )
{
@ -2728,6 +3097,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
case 'v':
fVerbose ^= 1;
break;
case 'x':
fCexInfo ^= 1;
break;
case 't':
fExtended ^= 1;
break;
case 'h':
goto usage;
default:
@ -2776,8 +3151,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
if ( pAbc->pCex )
{
Abc_NtkDumpOneCex( pFile, pNtk, pCex,
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose );
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
}
else if ( pAbc->vCexVec )
{
@ -2785,10 +3160,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
{
if ( pCex == NULL )
continue;
fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i );
fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i );
Abc_NtkDumpOneCex( pFile, pNtk, pCex,
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose );
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
}
}
fprintf( pFile, "# DONE\n" );
@ -2832,8 +3207,10 @@ usage:
fprintf( pAbc->Err, "\t-u : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-t : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );
fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" );

2
src/base/wlc/wlcMem.c
View File

@ -1024,7 +1024,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
pAig->nConstrs = 1;
pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 );
pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0, 1 );
Aig_ManStop( pTempAig );
pAbs = Gia_ManFromAigSimple( pAig );
Aig_ManStop( pAig );

4
src/map/if/ifMap.c
View File

@ -460,7 +460,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut->Delay = If_CutDelay( p, pObj, pCut );
if ( pCut->Delay == -1 )
continue;
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon && pCutSet->nCuts > 0 )
continue;
// compute area of the cut (this area may depend on the application specific cost)
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
@ -558,7 +558,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
continue;
// check if the cut satisfies the required times
// assert( pCut->Delay == If_CutDelay( p, pTemp, pCut ) );
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon && pCutSet->nCuts > 0 )
continue;
// set the phase attribute
pCut->fCompl = pObj->fPhase ^ pTemp->fPhase;

48
src/map/scl/sclLiberty.c
View File

@ -57,12 +57,12 @@ typedef struct Scl_Item_t_ Scl_Item_t;
struct Scl_Item_t_
{
int Type; // Scl_LibertyType_t
int iLine; // file line where the item's spec begins
long iLine; // file line where the item's spec begins
Scl_Pair_t Key; // key part
Scl_Pair_t Head; // head part
Scl_Pair_t Body; // body part
int Next; // next item in the list
int Child; // first child item
long Next; // next item in the list
long Child; // first child item
};
typedef struct Scl_Tree_t_ Scl_Tree_t;
@ -71,9 +71,9 @@ struct Scl_Tree_t_
char * pFileName; // input Liberty file name
char * pContents; // file contents
long nContents; // file size
int nLines; // line counter
int nItems; // number of items
int nItermAlloc; // number of items allocated
long nLines; // line counter
long nItems; // number of items
long nItermAlloc; // number of items allocated
Scl_Item_t * pItems; // the items
char * pError; // the error string
abctime clkStart; // beginning time
@ -89,11 +89,11 @@ static inline int Scl_LibertyGlobMatch(const char * pattern, const char
#endif
}
static inline Scl_Item_t * Scl_LibertyRoot( Scl_Tree_t * p ) { return p->pItems; }
static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, int v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; }
static inline int Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((int)strlen(pStr) != Pair.End-Pair.Beg); }
static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, long v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; }
static inline long Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((long)strlen(pStr) != Pair.End-Pair.Beg); }
static inline void Scl_PrintWord( FILE * pFile, Scl_Tree_t * p, Scl_Pair_t Pair ) { char * pBeg = p->pContents+Pair.Beg, * pEnd = p->pContents+Pair.End; while ( pBeg < pEnd ) fputc( *pBeg++, pFile ); }
static inline void Scl_PrintSpace( FILE * pFile, int nOffset ) { int i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); }
static inline int Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; }
static inline void Scl_PrintSpace( FILE * pFile, long nOffset ) { long i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); }
static inline long Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; }
#define Scl_ItemForEachChild( p, pItem, pChild ) \
for ( pChild = Scl_LibertyItem(p, pItem->Child); pChild; pChild = Scl_LibertyItem(p, pChild->Next) )
@ -181,9 +181,9 @@ int Scl_LibertyParseDump( Scl_Tree_t * p, char * pFileName )
SeeAlso []
***********************************************************************/
int Scl_LibertyCountItems( char * pBeg, char * pEnd )
long Scl_LibertyCountItems( char * pBeg, char * pEnd )
{
int Counter = 0;
long Counter = 0;
for ( ; pBeg < pEnd; pBeg++ )
Counter += (*pBeg == '(' || *pBeg == ':');
return Counter;
@ -228,11 +228,11 @@ void Scl_LibertyWipeOutComments( char * pBeg, char * pEnd )
}
}
}
static inline int Scl_LibertyCharIsSpace( char c )
static inline long Scl_LibertyCharIsSpace( char c )
{
return c == ' ' || c == '\t' || c == '\r' || c == '\n' || c == '\\';
}
static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine )
static inline long Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine )
{
char * pPos = *ppPos;
for ( ; pPos < pEnd; pPos++ )
@ -250,7 +250,7 @@ static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * p
return pPos == pEnd;
}
// skips entry delimited by " :;(){}" and returns 1 if reached the end
static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd )
static inline long Scl_LibertySkipEntry( char ** ppPos, char * pEnd )
{
char * pPos = *ppPos;
if ( *pPos == '\"' )
@ -277,7 +277,7 @@ static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd )
// finds the matching closing symbol
static inline char * Scl_LibertyFindMatch( char * pPos, char * pEnd )
{
int Counter = 0;
long Counter = 0;
assert( *pPos == '(' || *pPos == '{' );
if ( *pPos == '(' )
{
@ -387,10 +387,10 @@ char * Scl_LibertyReadString( Scl_Tree_t * p, Scl_Pair_t Pair )
Buffer[Pair.End-Pair.Beg] = 0;
return Buffer;
}
int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName )
long Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName )
{
Scl_Item_t * pItem;
int Counter = 0;
long Counter = 0;
Scl_ItemForEachChildName( p, pRoot, pItem, pName )
Counter++;
return Counter;
@ -407,7 +407,7 @@ int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName )
SeeAlso []
***********************************************************************/
int Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd )
long Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd )
{
Scl_Item_t * pItem;
Scl_Pair_t Key, Head, Body;
@ -513,7 +513,7 @@ exit:
if ( p->pError == NULL )
{
p->pError = ABC_ALLOC( char, 1000 );
sprintf( p->pError, "File \"%s\". Line %6d. Failed to parse entry \"%s\".\n",
sprintf( p->pError, "File \"%s\". Line %6ld. Failed to parse entry \"%s\".\n",
p->pFileName, p->nLines, Scl_LibertyReadString(p, Key) );
}
return -1;
@ -556,7 +556,7 @@ char * Scl_LibertyFileContents( char * pFileName, long nContents )
{
FILE * pFile = fopen( pFileName, "rb" );
char * pContents = ABC_ALLOC( char, nContents+1 );
int RetValue = 0;
long RetValue = 0;
RetValue = fread( pContents, nContents, 1, pFile );
fclose( pFile );
pContents[nContents] = 0;
@ -565,7 +565,7 @@ char * Scl_LibertyFileContents( char * pFileName, long nContents )
void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr )
{
FILE * pFile = fopen( pFileName, "wb" );
int RetValue = 0;
long RetValue = 0;
if ( pFile == NULL )
{
printf( "Scl_LibertyStringDump(): The output file is unavailable.\n" );
@ -721,10 +721,10 @@ int Scl_LibertyReadCellIsThreeState( Scl_Tree_t * p, Scl_Item_t * pCell )
return 1;
return 0;
}
int Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell )
long Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell )
{
Scl_Item_t * pPin;
int Counter = 0;
long Counter = 0;
Scl_ItemForEachChildName( p, pCell, pPin, "pin" )
if ( Scl_LibertyReadPinFormula(p, pPin) )
Counter++;

3
src/proof/pdr/pdr.h
View File

@ -72,6 +72,7 @@ struct Pdr_Par_t_
int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output
int fStoreCex; // enable storing counter-examples in MO mode
int fAnytime; // enable anytime scheduling
int fUseBridge; // use bridge interface
int fUsePropOut; // use property output
int nFailOuts; // the number of failed outputs
@ -84,6 +85,7 @@ struct Pdr_Par_t_
abctime timeLastSolved; // the time when the last output was solved
Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
char * pInvFileName; // invariable file name
char * pCexFilePrefix; // CEX output prefix
};
////////////////////////////////////////////////////////////////////////
@ -95,6 +97,7 @@ struct Pdr_Par_t_
////////////////////////////////////////////////////////////////////////
/*=== pdrCore.c ==========================================================*/
extern void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex );
extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );

374
src/proof/pdr/pdrCore.c
View File

@ -80,6 +80,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->nDropOuts = 0; // the number of timed out outputs
pPars->timeLastSolved = 0; // last one solved
pPars->pInvFileName = NULL; // invariant file name
pPars->pCexFilePrefix = NULL; // CEX output prefix
}
/**Function*************************************************************
@ -135,6 +136,150 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
return pCubeMin;
}
void Pdr_ManCompactNullClauses( Pdr_Man_t * p, int k )
{
Pdr_Set_t * pCubeK;
Vec_Ptr_t * vArrayK;
int j;
vArrayK = Vec_VecEntry( p->vClauses, k );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
if ( pCubeK != NULL )
continue;
Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
Vec_PtrPop(vArrayK);
j--;
}
}
int Pdr_ManPushInfAndRecycledClauses( Pdr_Man_t * p )
{
Pdr_Set_t * pTemp, * pCubeK;
Vec_Ptr_t * vArrayK, * vArrayK1;
Aig_Obj_t * pObj;
int j, k, m, RetValue2, fReduce = p->fNewInfClauses;
p->fNewInfClauses = 0;
k = Vec_PtrSize(p->vSolvers) - 2;
assert (k >= 0);
if ( fReduce && p->pPars->fVeryVerbose )
Abc_Print( 1, "Reducing inf and recycled clauses for frame %d.\n", k );
vArrayK = Vec_VecEntry( p->vClauses, k );
vArrayK1 = Vec_VecEntry( p->vClauses, k + 1 );
Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetBoundSizeLextCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
if ( pCubeK == NULL || pCubeK->iBound != PDR_INF_BOUND )
continue;
if (fReduce)
{
// remove cubes in the same frame that are contained by pCubeK
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
{
if ( pTemp == NULL )
continue;
// This is not needed here due to the sort order we're using
// if ( pTemp->iBound > pCubeK->iBound )
// continue;
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue;
pTemp->iBound = 0;
Pdr_SetDeref( pTemp );
Vec_PtrWriteEntry( vArrayK, m, NULL );
}
}
// Is it already implied by other clauses?
RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0;
if ( RetValue2 == -1 )
{
Pdr_ManCompactNullClauses( p, k );
return -1;
}
if ( RetValue2 == 1 )
{
pCubeK->iBound = 0;
p->nInfClauses--;
Pdr_SetDeref( pCubeK );
Vec_PtrWriteEntry( vArrayK, j, NULL );
continue;
}
Pdr_ManSolverAddClause( p, k+1, pCubeK );
Vec_PtrWriteEntry( vArrayK, j, NULL );
Vec_PtrPush( vArrayK1, pCubeK );
}
if ( (p->pPars->fAnytime || p->pPars->fSolveAll) && fReduce )
{
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) >= 0 )
continue;
RetValue2 = Pdr_ManCheckCube( p, k+1, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
if ( RetValue2 == -1 )
{
Pdr_ManCompactNullClauses( p, k );
return -1;
}
if ( RetValue2 == 1 )
{
// if the output is already in timeout we need to adjust the stats!
if ( Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == -1 )
p->pPars->nDropOuts--;
Abc_Print( 1, "Proved output %d in frame %d.\n", p->iOutCur, k );
p->pPars->nProveOuts++;
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 1 );
}
}
}
// Extra debug checks
// Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, j )
// {
// assert( pCubeK1->iBound == PDR_INF_BOUND );
// assert( Pdr_ManCheckCubeCs( p, k+1, pCubeK1 ) != 0 );
// assert( Pdr_ManCheckCube( p, k, pCubeK1, NULL, 0, 0, 1 ) != 0 );
// }
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
if ( pCubeK == NULL || pCubeK->iBound <= k )
continue;
// Is it already implied by other clauses?
RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0;
if ( RetValue2 == -1 )
{
Pdr_ManCompactNullClauses( p, k );
return -1;
}
if ( RetValue2 == 1 )
{
Pdr_SetDeref( pCubeK );
Vec_PtrWriteEntry( vArrayK, j, NULL );
continue;
}
Pdr_ManSolverAddClause( p, k+1, pCubeK );
Vec_PtrWriteEntry( vArrayK, j, NULL );
Vec_PtrPush( vArrayK1, pCubeK );
}
// Compact NULL entries
Pdr_ManCompactNullClauses( p, k );
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if the state could be blocked.]
@ -152,7 +297,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
Vec_Ptr_t * vArrayK, * vArrayK1;
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
int Counter = 0;
abctime clk = Abc_Clock();
assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
@ -161,11 +305,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
Counter++;
// remove cubes in the same frame that are contained by pCubeK
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
{
if ( pTemp->iBound > pCubeK->iBound )
continue;
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue;
Pdr_SetDeref( pTemp );
@ -197,6 +341,9 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// check if the clause subsumes others
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
{
// Subsuming a clause of the invariant with a non-invariant clause could break the invariant
if ( pCubeK1->iBound > pCubeK->iBound )
continue;
if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
continue;
Pdr_SetDeref( pCubeK1 );
@ -205,6 +352,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
i--;
}
// add the last clause
pCubeK->iBound = k+1;
Vec_PtrPush( vArrayK1, pCubeK );
Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
Vec_PtrPop(vArrayK);
@ -222,6 +370,8 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// remove cubes in the same frame that are contained by pCubeK
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
{
if ( pTemp->iBound > pCubeK->iBound )
continue;
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue;
/*
@ -907,6 +1057,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
while ( !Pdr_QueueIsEmpty(p) )
{
Counter++;
if (Counter % 100 == 0) {
Pdr_ManPrintProgress( p, 1, Abc_Clock() - p->tStart );
}
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
return 0; // SAT
@ -986,6 +1139,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
p->nAbsFlops++;
Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
}
pCubeMin->iBound = k;
Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
p->nCubes++;
// add clause
@ -1026,6 +1180,38 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
return 1;
}
void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex )
{
int i, f, iBit;
size_t iCexPathSize;
char * pCexPath;
FILE * pCexFile;
iCexPathSize = snprintf( NULL, 0, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ) + 1;
pCexPath = (char *)malloc( iCexPathSize );
snprintf( pCexPath, iCexPathSize, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo );
Abc_Print( 1, "Writing CEX for output %d to %s\n", pCex->iPo, pCexPath );
pCexFile = fopen( pCexPath, "w" );
free( pCexPath );
fprintf( pCexFile, "1\n");
fprintf( pCexFile, "b%d\n", pCex->iPo);
iBit = 0;
for ( i = 0; i < pCex->nRegs; i++, iBit++ )
putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile );
putc( '\n', pCexFile );
for ( f = 0; f <= pCex->iFrame; f++ )
{
for ( i = 0; i < pCex->nPis; i++, iBit++ )
putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile );
putc( '\n', pCexFile );
}
fprintf( pCexFile, ".\n");
fclose( pCexFile );
}
/**Function*************************************************************
Synopsis []
@ -1043,24 +1229,36 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_Set_t * pCube = NULL;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew;
int iFrame, RetValue = -1;
int iFrame, i, RetValue = -1, SomeActive = 1, ClausesAdded = 1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0;
p->tStart = clkStart;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
assert( Vec_PtrSize(p->vSolvers) == 0 );
// in the multi-output mode, mark trivial POs (those fed by const0) as solved
if ( p->pPars->fSolveAll )
Saig_ManForEachPo( p->pAig, pObj, iFrame )
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
if ( p->pPars->fSolveAll || p->pPars->fAnytime )
Saig_ManForEachPo( p->pAig, pObj, i )
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) && Vec_IntEntry( p->pPars->vOutMap, i ) == -2)
{
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat
Abc_Print( 1, "Proved output %d in frame 0 (trivial).\n", i );
p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
Gia_ManToBridgeResult( stdout, 1, NULL, i );
}
// create the first timeframe
p->pPars->timeLastSolved = Abc_Clock();
Pdr_ManCreateSolver( p, (iFrame = 0) );
if ( p->vInfCubes != NULL )
{
Vec_PtrForEachEntry( Pdr_Set_t *, p->vInfCubes, pCube, i )
{
Pdr_ManSolverAddClause( p, 0, pCube );
Vec_VecPush( p->vClauses, 0, pCube );
}
pCube = NULL;
}
while ( 1 )
{
int fRefined = 0;
@ -1080,11 +1278,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->nFrames = iFrame;
assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
p->iUseFrame = Abc_MaxInt(iFrame, 1);
SomeActive = 0;
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
// skip disproved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
continue;
// skip otuput that was already solved
if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == 1 )
continue;
// skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
continue;
@ -1100,7 +1302,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pAig->pSeqModel = pCexNew;
return 0; // SAT
}
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( !p->pPars->fNotVerbose )
@ -1109,6 +1311,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
@ -1124,6 +1328,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->timeLastSolved = Abc_Clock();
continue;
}
SomeActive += 1;
// try to solve this output
if ( p->pTime4Outs )
{
@ -1168,6 +1373,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( RetValue == 0 )
{
ClausesAdded = 1;
RetValue = Pdr_ManBlockCube( p, pCube );
if ( RetValue == -1 )
{
@ -1217,11 +1423,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
@ -1239,6 +1447,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // all SAT
Pdr_QueueClean( p );
pCube = NULL;
SomeActive--;
break; // keep solving
}
if ( p->pPars->fVerbose )
@ -1252,13 +1461,19 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
abctime timeSince = Abc_Clock() - clkOne;
assert( p->pTime4Outs[p->iOutCur] > 0 );
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) ) // undecided
{
SomeActive--;
p->pPars->nDropOuts++;
if ( p->pPars->vOutMap )
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
{
if ( p->pPars->fAnytime )
Abc_Print( 1, "Timing out on output %*d in frame %d (retrying in next anytime pass).\n", nOutDigits, p->iOutCur, iFrame );
else
Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
}
}
p->timeToStopOne = 0;
}
@ -1279,6 +1494,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );
if ( p->pPars->fAnytime && ClausesAdded )
Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) );
Pdr_ManSetPropertyOutput( p, iFrame );
Pdr_ManCreateSolver( p, ++iFrame );
if ( fPrintClauses )
@ -1287,14 +1506,23 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintClauses( p, 0 );
}
// push clauses into this timeframe
RetValue = Pdr_ManPushClauses( p );
if ( RetValue == -1 )
RetValue = 0;
if ( p->pPars->fAnytime )
{
RetValue = Pdr_ManPushInfAndRecycledClauses( p );
ClausesAdded = 0;
}
RetValue = RetValue == -1 ? -1 : Pdr_ManPushClauses( p );
if ( RetValue == -1 || !SomeActive )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
{
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
if ( !SomeActive )
Abc_Print( 1, "All outputs solved or timed out in frame %d.\n", iFrame );
else if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
@ -1306,22 +1534,34 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
if ( !p->pPars->fAnytime )
{
if ( !p->pPars->fSilent )
Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
}
p->pPars->iFrame = iFrame;
// count the number of UNSAT outputs
p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
// convert previously 'unknown' into 'unsat'
if ( p->pPars->vOutMap )
for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
{
for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ )
if ( Vec_IntEntry(p->pPars->vOutMap, i) == -2 ) // unknown
{
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat
Abc_Print( 1, "Proved output %d in frame %d (converged).\n", i );
p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
Gia_ManToBridgeResult( stdout, 1, NULL, i );
}
if ( p->pPars->nDropOuts > 0 )
return -1;
}
else
{
// count the number of UNSAT outputs
p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
}
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT
if ( p->pPars->nFailOuts > 0 )
@ -1379,6 +1619,61 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pdr_ManResetReuseInvariant( Pdr_Man_t * p )
{
int i, k, nTimeOutU;
Pdr_Set_t * pCla;
sat_solver * pSat;
Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) );
Vec_PtrClear( p->vInfCubes );
Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
Vec_PtrPush( p->vInfCubes, pCla );
Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
sat_solver_delete( pSat );
Vec_PtrFree( p->vSolvers );
Vec_VecFree( p->vClauses );
Pdr_QueueStop( p );
Vec_IntFree( p->vActVars );
p->vSolvers = Vec_PtrAlloc( 0 );
p->vClauses = Vec_VecAlloc( 0 );
p->pQueue = NULL;
p->vActVars = Vec_IntAlloc( 256 );
Vec_IntFill (p->vPrio, Vec_IntSize(p->vPrio), 0);
p->nAbsFlops = 0;
for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ )
{
p->pTime4Outs[i] = p->pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
if ( Vec_IntEntry(p->pPars->vOutMap, i) == -1 ) // timeout
Vec_IntWriteEntry( p->pPars->vOutMap, i, -2 ); // unknown
}
p->pPars->nDropOuts = 0;
p->pPars->nTimeOutOne *= 2;
nTimeOutU = p->pPars->nTimeOutOne * (Saig_ManPoNum(p->pAig) - p->pPars->nProveOuts - p->pPars->nFailOuts);
p->pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX
Abc_Print( 1, "Starting new anytime pass, reusing clauses.\n" );
}
/**Function*************************************************************
Synopsis []
@ -1393,12 +1688,21 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{
Pdr_Man_t * p;
int k, RetValue;
int k, RetValue, nTimeOutU;
abctime clk = Abc_Clock();
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
if ( pPars->fAnytime )
{
if ( pPars->nTimeOutOne == 0 )
pPars->nTimeOutOne = 200;
}
if ( pPars->nTimeOutOne && !(pPars->fSolveAll || pPars->fAnytime) )
pPars->nTimeOutOne = 0;
if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
{
nTimeOutU = pPars->nTimeOutOne * (Saig_ManPoNum(pAig) - pPars->nProveOuts - pPars->nFailOuts);
pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX
}
if ( pPars->fVerbose )
{
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
@ -1414,7 +1718,17 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
}
ABC_FREE( pAig->pSeqModel );
p = Pdr_ManStart( pAig, pPars, NULL );
RetValue = Pdr_ManSolveInt( p );
while (1) {
RetValue = Pdr_ManSolveInt( p );
if ( RetValue == -1 && Saig_ManPoNum(p->pAig) == pPars->nProveOuts + pPars->nFailOuts )
RetValue = pPars->nFailOuts == 0;
if ( RetValue == -1 && pPars->fAnytime )
Pdr_ManResetReuseInvariant( p );
else
break;
}
if ( RetValue == 0 )
assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
if ( p->vCexes )

8
src/proof/pdr/pdrIncr.c
View File

@ -379,6 +379,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
int iFrame, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0;
p->tStart = clkStart;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
// assert( Vec_PtrSize(p->vSolvers) == 0 );
// in the multi-output mode, mark trivial POs (those fed by const0) as solved
@ -484,7 +485,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
p->pAig->pSeqModel = pCexNew;
return 0; // SAT
}
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( !p->pPars->fNotVerbose )
@ -493,6 +494,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
@ -676,7 +679,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
//if ( p->pPars->fUseAbs && p->vAbsFlops )
// printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
p->nQueLim = iFrame + p->pPars->nRestLimit;
p->nQueLimStep = 1;
assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, iFrame );
Pdr_ManCreateSolver( p, ++iFrame );

8
src/proof/pdr/pdrInt.h
View File

@ -58,6 +58,8 @@
#define sat_solver_compress(s)
#endif
#define PDR_INF_BOUND ((int)((~((unsigned int)0)) >> 1))
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
@ -76,6 +78,7 @@ struct Pdr_Set_t_
{
word Sign; // signature
int nRefs; // ref counter
int iBound; // known to hold up to this frame, INT_MAX = inf
int nTotal; // total literals
int nLits; // num flop literals
int Lits[0];
@ -156,8 +159,11 @@ struct Pdr_Man_t_
int nQueCur;
int nQueMax;
int nQueLim;
int nQueLimStep;
int nXsimRuns;
int nXsimLits;
int nInfClauses;
int fNewInfClauses;
// runtime
abctime timeToStop;
abctime timeToStopOne;
@ -172,6 +178,7 @@ struct Pdr_Man_t_
abctime tCnf;
abctime tAbs;
abctime tTotal;
abctime tStart;
};
////////////////////////////////////////////////////////////////////////
@ -253,6 +260,7 @@ extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec
extern void ZPdr_SetPrint( Pdr_Set_t * p );
extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
extern int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
extern void Pdr_OblDeref( Pdr_Obl_t * p );

77
src/proof/pdr/pdrInv.c
View File

@ -48,14 +48,15 @@ ABC_NAMESPACE_IMPL_START
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
{
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
int i, ThisSize, Length, LengthStart, kLast, Value, Width;
if ( Vec_PtrSize(p->vSolvers) < 2 )
{
Abc_Print(1, "Frame " );
Abc_Print(1, "Clauses " );
Abc_Print(1, "Max Queue " );
Abc_Print(1, "Flops " );
Abc_Print(1, "Cex " );
if ( p->pPars->fUseAbs )
Abc_Print(1, "Cex " );
Abc_Print(1, "Time" );
Abc_Print(1, "\n" );
return;
@ -64,8 +65,12 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
return;
// count the total length of the printout
Length = 0;
kLast = Vec_VecSize( p->vClauses ) - 1;
Vec_VecForEachLevel( p->vClauses, vVec, i )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1 - (i == kLast ? p->nInfClauses : 0) );
if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 )
Length += 2 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+1);
// determine the starting point
LengthStart = Abc_MaxInt( 0, Length - 60 );
Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 );
@ -78,26 +83,37 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
Length = 0;
Vec_VecForEachLevel( p->vClauses, vVec, i )
{
Value = Vec_PtrSize(vVec) - (i == kLast ? p->nInfClauses : 0);
Width = 1 + Abc_Base10Log(Value+1);
if ( Length < LengthStart )
{
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
Length += Width;
continue;
}
Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
Abc_Print( 1, " %d", Value );
Length += Width;
ThisSize += Width;
}
if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 )
{
Abc_Print( 1, " ~%d", Vec_PtrSize(p->vInfCubes) );
Length += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2);
ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2);
}
for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%5d", p->nQueMax );
Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
if ( p->pPars->fUseAbs )
Abc_Print( 1, "%4d", p->nCexes );
Abc_Print( 1, "%4d", p->nCexes );
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
if ( p->pPars->nTimeOutOne )
Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts );
if ( p->pPars->fAnytime )
Abc_Print( 1, " PRV =%3d", p->pPars->nProveOuts );
Abc_Print( 1, "%s", fClose ? "\n":"\r" );
if ( fClose )
p->nQueMax = 0, p->nCexes = 0;
@ -123,7 +139,7 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 )
if ( pCube->iBound != PDR_INF_BOUND )
continue;
for ( n = 0; n < pCube->nLits; n++ )
{
@ -376,7 +392,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
Count = 0;
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 )
if ( pCube->iBound != PDR_INF_BOUND )
continue;
Count++;
}
@ -406,7 +422,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
// output cubes
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 )
if ( pCube->iBound != PDR_INF_BOUND )
continue;
Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
fprintf( pFile, " 1\n" );
@ -452,7 +468,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
// output cubes
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 )
if ( pCube->iBound != PDR_INF_BOUND )
continue;
Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
}
@ -566,7 +582,7 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
// add the clauses
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 ) // skip non-inductive
if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) // skip known non-inf
continue;
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
@ -576,31 +592,45 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
// check each clause
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 ) // skip non-inductive
if ( pCube->iBound >= 0 ) // skip clauses with known inf-ness
continue;
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
if ( RetValue != l_False ) // mark as non-inductive
if ( RetValue != l_False ) // mark as non-inf
{
pCube->nRefs = -1;
pCube->iBound = ~pCube->iBound;
fChanges = 1;
}
else
Counter++;
}
Vec_Ptr_t *vLevel;
sat_solver_delete( (sat_solver *)Vec_PtrPop( p->vSolvers ) );
vLevel = (Vec_Ptr_t *)Vec_PtrPop( (Vec_Ptr_t *)p->vClauses );
assert (Vec_PtrSize( vLevel ) == 0);
Vec_PtrFree( vLevel );
Vec_IntPop( p->vActVars );
//Abc_Print(1, "Clauses = %d.\n", Counter );
//sat_solver_delete( pSat );
return fChanges;
}
Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
{
Vec_Int_t * vResult;
Vec_Ptr_t * vCubes;
Pdr_Set_t * pCube;
int i, v, kStart;
int i, v, kStart, kMax;
// collect cubes used in the inductive invariant
kMax = Vec_PtrSize( p->vSolvers );
kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart );
// mark all non-inf clauses as candidates
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
if (pCube->iBound != PDR_INF_BOUND)
pCube->iBound = ~pCube->iBound;
// refine as long as there are changes
if ( fReduce )
while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
@ -609,14 +639,23 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
Vec_IntPush( vResult, 0 );
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
if ( pCube->nRefs == -1 ) // skip non-inductive
if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) {
Vec_PtrWriteEntry( vCubes, i, Vec_PtrEntryLast( vCubes ) );
Vec_PtrPop( vCubes );
i--;
continue;
}
if (pCube->iBound != PDR_INF_BOUND)
{
p->nInfClauses++;
p->fNewInfClauses = 1;
pCube->iBound = PDR_INF_BOUND;
}
Vec_IntAddToEntry( vResult, 0, 1 );
Vec_IntPush( vResult, pCube->nLits );
for ( v = 0; v < pCube->nLits; v++ )
Vec_IntPush( vResult, pCube->Lits[v] );
}
//Vec_PtrFree( vCubes );
Vec_PtrFreeP( &p->vInfCubes );
p->vInfCubes = vCubes;
Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );

3
src/proof/pdr/pdrMan.c
View File

@ -296,8 +296,9 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
}
if ( pPars->fSolveAll )
{
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
if ( pPars->fSolveAll || p->pPars->fAnytime )
{
p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
}

3
src/proof/pdr/pdrSat.c
View File

@ -99,7 +99,8 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
// add the clauses
Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
Pdr_ManSolverAddClause( p, k, pCube );
if ( pCube != NULL )
Pdr_ManSolverAddClause( p, k, pCube );
return pSat;
}

39
src/proof/pdr/pdrUtil.c
View File

@ -71,6 +71,7 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
p->nLits = Vec_IntSize(vLits);
p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
p->nRefs = 1;
p->iBound = 0;
p->Sign = 0;
for ( i = 0; i < p->nLits; i++ )
{
@ -104,6 +105,7 @@ Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
p->nLits = pSet->nLits - 1;
p->nTotal = pSet->nTotal - 1;
p->nRefs = 1;
p->iBound = 0;
p->Sign = 0;
for ( i = 0; i < pSet->nTotal; i++ )
{
@ -138,6 +140,7 @@ Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
p->nLits = nLits;
p->nTotal = nLits + pSet->nTotal - pSet->nLits;
p->nRefs = 1;
p->iBound = 0;
p->Sign = 0;
for ( i = 0; i < nLits; i++ )
{
@ -171,6 +174,7 @@ Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
p->nLits = pSet->nLits;
p->nTotal = pSet->nTotal;
p->nRefs = 1;
p->iBound = 0;
p->Sign = pSet->Sign;
for ( i = 0; i < pSet->nTotal; i++ )
p->Lits[i] = pSet->Lits[i];
@ -501,6 +505,41 @@ int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
{
Pdr_Set_t * p1 = *pp1;
Pdr_Set_t * p2 = *pp2;
if (p1->iBound > p2->iBound)
return -1;
if (p1->iBound < p2->iBound)
return 1;
if (p1->nLits < p2->nLits)
return -1;
if (p1->nLits > p2->nLits)
return 1;
int i;
for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
{
if ( p1->Lits[i] > p2->Lits[i] )
return -1;
if ( p1->Lits[i] < p2->Lits[i] )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis []

4
src/sat/bmc/bmc.h
View File

@ -227,7 +227,8 @@ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars
extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
@ -238,6 +239,7 @@ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC
/*=== bmcCexTool.c ==========================================================*/
extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
extern int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
/*=== bmcICheck.c ==========================================================*/
extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );

38
src/sat/bmc/bmcCexCare.c
View File

@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
SeeAlso []
***********************************************************************/
void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
{
int result;
Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
if ( fVerbose )
{
@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
printf( "Minimized: " );
Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
}
if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
result = Bmc_CexVerify( pGia, pCex, pCexMin );
if ( !result )
printf( "Counter-example verification has failed.\n" );
else
printf( "Counter-example verification succeeded.\n" );
Gia_ManStop( pGia );
return result;
}
/*
{
@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
}
*/
/**Function*************************************************************
Synopsis [Verifies the care set of the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
{
int iPo;
Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
if ( fVerbose )
{
printf( "Original : " );
Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
printf( "Minimized: " );
Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
}
iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
if ( iPo < 0 )
printf( "Counter-example verification has failed.\n" );
else
printf( "Counter-example verification succeeded.\n" );
Gia_ManStop( pGia );
return iPo;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

47
src/sat/bmc/bmcCexTools.c
View File

@ -374,6 +374,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
return Gia_ObjTerSimGet1(pObj);
}
/**Function*************************************************************
Synopsis [Verifies the care set of the counter-example for an arbitrary PO.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
{
Gia_Obj_t * pObj;
int i, k;
// assert( pCex->nRegs > 0 );
// assert( pCexCare->nRegs == 0 );
Gia_ObjTerSimSet0( Gia_ManConst0(p) );
Gia_ManForEachRi( p, pObj, k )
Gia_ObjTerSimSet0( pObj );
for ( i = 0; i <= pCex->iFrame; i++ )
{
Gia_ManForEachPi( p, pObj, k )
{
if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
Gia_ObjTerSimSetX( pObj );
else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachRo( p, pObj, k )
Gia_ObjTerSimRo( p, pObj );
Gia_ManForEachAnd( p, pObj, k )
Gia_ObjTerSimAnd( pObj );
Gia_ManForEachCo( p, pObj, k )
Gia_ObjTerSimCo( pObj );
}
for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
{
pObj = Gia_ManPo( p, i );
if (Gia_ObjTerSimGet1(pObj))
return i;
}
return -1;
}
/**Function*************************************************************
Synopsis [Computes internal states of the CEX.]