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

Enabling Glucose in SAT sweeping: &fraig -g.

This commit is contained in:
Alan Mishchenko 2017-09-18 09:36:08 -07:00
parent 12d21480de
commit 36858c5365
4 changed files with 1074 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -33236,13 +33236,14 @@ usage:
int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Gia_Man_t * pTemp;
int c, fUseAlgo = 0;
int c, fUseAlgo = 0, fUseAlgoG = 0;
Cec_ManFraSetDefaultParams( pPars );
pPars->fSatSweeping = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcknwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngwvh" ) ) != EOF )
{
switch ( c )
{
@ -33330,6 +33331,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'n':
fUseAlgo ^= 1;
break;
case 'g':
fUseAlgoG ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@ -33347,13 +33351,15 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fUseAlgo )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcknwvh]\n" );
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdckngwvh]\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 );
@ -33367,6 +33373,7 @@ usage:
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-g : toggle using another new implementation [default = %s]\n", fUseAlgoG? "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" );
Abc_Print( -2, "\t-h : print the command usage\n");

1048
src/proof/cec/cecSatG.c Normal file
View File

File diff suppressed because it is too large Load Diff

10
src/sat/glucose/AbcGlucose.cpp
View File

@ -71,6 +71,11 @@ void glucose_solver_stop(Gluco::SimpSolver* S)
delete S;
}
void glucose_solver_reset(Gluco::SimpSolver* S)
{
S->reset();
}
int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits)
{
vec<Lit> lits;
@ -142,6 +147,11 @@ void bmcg_sat_solver_stop(bmcg_sat_solver* s)
{
glucose_solver_stop((Gluco::SimpSolver*)s);
}
void bmcg_sat_solver_reset(bmcg_sat_solver* s)
{
glucose_solver_reset((Gluco::SimpSolver*)s);
}
int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
{

6
src/sat/glucose/AbcGlucose.h
View File

@ -33,6 +33,11 @@
ABC_NAMESPACE_HEADER_START
#define GLUCOSE_UNSAT -1
#define GLUCOSE_SAT 1
#define GLUCOSE_UNDEC 0
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@ -67,6 +72,7 @@ typedef void bmcg_sat_solver;
extern bmcg_sat_solver * bmcg_sat_solver_start();
extern void bmcg_sat_solver_stop( bmcg_sat_solver* s );
extern void bmcg_sat_solver_reset( bmcg_sat_solver* s );
extern int bmcg_sat_solver_addclause( bmcg_sat_solver* s, int * plits, int nlits );
extern void bmcg_sat_solver_setcallback( bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) );
extern int bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits, int nlits );