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

Experiments with SAT sweeping.

This commit is contained in:
Alan Mishchenko 2017-04-11 22:12:18 -07:00
parent 79584f5e20
commit b1eaf714f2
4 changed files with 15 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -12385,7 +12385,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Cba_PrsReadBlifTest();
}
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
Acb_DataReadTest();
// Acb_DataReadTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@ -32928,7 +32928,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManFraSetDefaultParams( pPars );
pPars->fSatSweeping = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcnwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcknwvh" ) ) != EOF )
{
switch ( c )
{
@ -33010,6 +33010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fRunCSat ^= 1;
break;
case 'k':
pPars->fUseCones ^= 1;
break;
case 'n':
fUseAlgo ^= 1;
break;
@ -33036,7 +33039,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcnwvh]\n" );
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcknwvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
@ -33048,6 +33051,7 @@ usage:
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using logic cones in the SAT solver [default = %s]\n", pPars->fUseCones? "yes": "no" );
Abc_Print( -2, "\t-n : toggle using new implementation [default = %s]\n", fUseAlgo? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );

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

@ -108,6 +108,7 @@ struct Cec_ParFra_t_
int fColorDiff; // miter with separate outputs
int fSatSweeping; // enable SAT sweeping
int fRunCSat; // enable another solver
int fUseCones; // use cones
int fUseOrigIds; // enable recording of original IDs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats

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

@ -138,6 +138,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
p->fDualOut = 0; // miter with separate outputs
p->fColorDiff = 0; // miter with separate outputs
p->fSatSweeping = 0; // enable SAT sweeping
p->fUseCones = 0; // use cones
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
p->iOutFail = -1; // the failed output

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

@ -101,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p )
p->nItersMax = 10; // max number of iterations
p->nConfLimit = 1000; // conflict limit at a node
p->fIsMiter = 0; // this is a miter
p->fUseCones = 0; // use logic cones
p->fUseCones = 1; // use logic cones
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
}
@ -968,7 +968,11 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
continue;
}
if ( Cec2_ManSweepNode(pMan, i) )
{
if ( Gia_ObjProved(p, i) )
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
continue;
}
pObj->Value = ~0;
Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) );
fDisproved = 1;
@ -1011,6 +1015,7 @@ Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 )
// pPars->nSimRounds = pPars0->nRounds; // simulation rounds
// pPars->nItersMax = pPars0->nItersMax; // max number of iterations
pPars->nConfLimit = pPars0->nBTLimit; // conflict limit at a node
pPars->fUseCones = pPars0->fUseCones;
pPars->fVerbose = pPars0->fVerbose;
// Gia_ManComputeGiaEquivs( p, 100000, 0 );
// Gia_ManEquivPrintClasses( p, 1, 0 );