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

Adding switch to replace proved outputs by const0.

This commit is contained in:
Alan Mishchenko 2020-12-16 00:06:31 -08:00
parent 901560bb23
commit 06094ade87
10 changed files with 86 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1250,7 +1250,7 @@ extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia );
extern void Cbs_ManStop( Cbs_Man_t * p );
extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose );
extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p );
/*=== giaCTas.c ============================================================*/

4
src/aig/gia/giaCSat.c
View File

@ -1034,7 +1034,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
{
extern void Gia_ManCollectTest( Gia_Man_t * pAig );
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
@ -1105,6 +1105,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
}
if ( status == 1 )
{
if ( f0Proved )
Gia_ManPatchCoDriver( pAig, i, 0 );
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += Abc_Clock() - clk;

60
src/aig/gia/giaEquiv.c
View File

@ -2818,6 +2818,66 @@ Gia_Man_t * Cec4_ManSatSolverChoices( Gia_Man_t * p, Gia_Man_t * pNew )
return pCho;
}
/**Function*************************************************************
Synopsis [Converting AIG after SAT sweeping into AIG with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCombSpecReduce( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pRepr; int i, iLit;
Vec_Int_t * vXors = Vec_IntAlloc( 100 );
Gia_Man_t * pTemp, * pNew = Gia_ManStart( Gia_ManObjNum(p) );
assert( p->pReprs && p->pNexts );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManLevelNum(p);
Gia_ManSetPhase(p);
Gia_ManFillValue(p);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManHashAlloc( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
pRepr = Gia_ObjReprObj( p, i );
if ( pRepr && Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
{
//if ( Gia_ObjLevel(p, pRepr) > Gia_ObjLevel(p, pObj) + 50 )
//printf( "%d %d ", Gia_ObjLevel(p, pRepr), Gia_ObjLevel(p, pObj) );
iLit = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
Vec_IntPush( vXors, Gia_ManHashXor( pNew, pObj->Value, iLit ) );
pObj->Value = iLit;
}
}
Gia_ManHashStop( pNew );
if ( Vec_IntSize(vXors) == 0 )
Vec_IntPush( vXors, 0 );
Vec_IntForEachEntry( vXors, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vXors );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
void Gia_ManCombSpecReduceTest( Gia_Man_t * p, char * pFileName )
{
Gia_Man_t * pSrm = Gia_ManCombSpecReduce( p );
if ( pFileName == NULL )
pFileName = "test.aig";
Gia_AigerWrite( pSrm, pFileName, 0, 0, 0 );
Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManStop( pSrm );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -36120,10 +36120,10 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ParSat_t ParsSat, * pPars = &ParsSat;
Gia_Man_t * pTemp;
int c;
int fNewSolver = 0, fCSat = 0;
int fNewSolver = 0, fCSat = 0, f0Proved = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxzvh" ) ) != EOF )
{
switch ( c )
{
@ -36178,6 +36178,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'x':
fNewSolver ^= 1;
break;
case 'z':
f0Proved ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -36199,7 +36202,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( pPars->fLearnCls )
vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else if ( pPars->fNonChrono )
vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, f0Proved, pPars->fVerbose );
else
vCounters = Cbs_ManSolveMiter( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
Vec_IntFree( vCounters );
@ -36207,7 +36210,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
pTemp = Cec_ManSatSolving( pAbc->pGia, pPars, f0Proved );
Abc_FrameUpdateGia( pAbc, pTemp );
}
if ( pAbc->pGia->vSeqModelVec )
@ -36219,7 +36222,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" );
Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxzvh]\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 );
@ -36230,6 +36233,7 @@ usage:
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 using new solver [default = %s]\n", fNewSolver? "yes": "no" );
Abc_Print( -2, "\t-z : toggle replacing proved cones by const0 [default = %s]\n", f0Proved? "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;

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

@ -219,7 +219,7 @@ extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent );
extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved );
extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
/*=== cecSeq.c ==========================================================*/
extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex );

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

@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
// found counter-examples to speculation
clk2 = Abc_Clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );

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

@ -232,14 +232,14 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved )
{
Gia_Man_t * pNew;
Cec_ManPat_t * pPat;
pPat = Cec_ManPatStart();
Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved );
// pNew = Gia_ManDupDfsSkip( pAig );
pNew = Gia_ManDup( pAig );
pNew = Gia_ManCleanup( pAig );
Cec_ManPatStop( pPat );
pNew->vSeqModelVec = pAig->vSeqModelVec;
pAig->vSeqModelVec = NULL;
@ -445,7 +445,7 @@ clk = Abc_Clock();
if ( pPars->fRunCSat )
Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
else
Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv );
Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv, 0 );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{

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

@ -996,7 +996,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// found counter-examples to speculation
clk2 = Abc_Clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );

2
src/proof/cec/cecInt.h
View File

@ -204,7 +204,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern 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 );
extern 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, int f0Proved );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );

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

@ -696,7 +696,7 @@ Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
}
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 )
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, int f0Proved )
{
Bar_Progress_t * pProgress = NULL;
Cec_ManSat_t * p;
@ -747,6 +747,9 @@ clk2 = Abc_Clock();
if ( pPars->fSaveCexes && status != -1 )
Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
if ( f0Proved && status == 1 )
Gia_ManPatchCoDriver( pAig, i, 0 );
/*
if ( status == -1 )
{
@ -807,7 +810,7 @@ void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t *
{
Vec_Str_t * vStatus;
Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0, 0 );
Gia_Obj_t * pObj;
int i, status, iStart = 0;
assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );