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

Adding &sat -x to save CEXes for multi-output combinational miters.

This commit is contained in:
Alan Mishchenko 2018-05-06 22:13:18 -07:00
parent aa313189c4
commit ccf529695d
4 changed files with 56 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -655,6 +655,25 @@ Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes )
Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
return vStatuses;
}
Vec_Int_t * Abc_FrameDeriveStatusArray2( Vec_Ptr_t * vCexes )
{
Vec_Int_t * vStatuses;
Abc_Cex_t * pCex;
int i;
if ( vCexes == NULL )
return NULL;
vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
if ( pCex == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
{
Vec_IntWriteEntry( vStatuses, i, 1 ); // set this output as UNSAT
Vec_PtrWriteEntry( vCexes, i, NULL );
}
else if ( pCex != NULL )
Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
return vStatuses;
}
/**Function*************************************************************
@ -2765,8 +2784,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_CexPrintStats( pTemp );
}
}
if ( Counter )
printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
// if ( Counter )
// printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
}
}
if ( pAbc->vStatuses )
@ -33675,7 +33694,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewSolver = 0, fCSat = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF )
{
switch ( c )
{
@ -33727,6 +33746,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fCSat ^= 1;
break;
case 'x':
pPars->fSaveCexes ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -33759,10 +33781,16 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
}
if ( pAbc->pGia->vSeqModelVec )
{
Vec_Int_t * vStatuses = Abc_FrameDeriveStatusArray2( pAbc->pGia->vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
}
return 0;
usage:
Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" );
Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" );
Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@ -33772,6 +33800,7 @@ usage:
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
Abc_Print( -2, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
Abc_Print( -2, "\t-x : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

1
src/proof/cec/cec.h
View File

@ -51,6 +51,7 @@ struct Cec_ParSat_t_
int fCheckMiter; // the circuit is the miter
// int fFirstStop; // stop on the first sat output
int fLearnCls; // perform clause learning
int fSaveCexes; // saves counter-examples
int fVerbose; // verbose stats
};

2
src/proof/cec/cecCore.c
View File

@ -241,6 +241,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
// pNew = Gia_ManDupDfsSkip( pAig );
pNew = Gia_ManDup( pAig );
Cec_ManPatStop( pPat );
pNew->vSeqModelVec = pAig->vSeqModelVec;
pAig->vSeqModelVec = NULL;
return pNew;
}

20
src/proof/cec/cecSolve.c
View File

@ -673,6 +673,21 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
{
Abc_Cex_t * pCex;
int i;
pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
pCex->iPo = iOut;
pCex->iFrame = 0;
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
int iVar = Cec_ObjSatNum(p, Gia_ManCi(p->pAig, i));
if ( iVar > 0 && sat_solver_var_value(p->pSat, iVar) )
pCex->pData[i>>5] |= (1<<(i & 31));
}
return pCex;
}
void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
{
Bar_Progress_t * pProgress = NULL;
@ -680,6 +695,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
Gia_Obj_t * pObj;
int i, status;
abctime clk = Abc_Clock(), clk2;
Vec_PtrFreeP( &pAig->vSeqModelVec );
if ( pPars->fSaveCexes )
pAig->vSeqModelVec = Vec_PtrStart( Gia_ManCoNum(pAig) );
// reset the manager
if ( pPat )
{
@ -715,6 +733,8 @@ clk2 = Abc_Clock();
assert( OrigId1 >= 0 && OrigId2 >= 0 );
Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
}
if ( pPars->fSaveCexes && status != -1 )
Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
/*
if ( status == -1 )