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

Improvements in the proof-logging SAT solver.

This commit is contained in:
Alan Mishchenko 2012-07-11 12:45:46 -07:00
parent 5f3ba152e5
commit b9ee5d8564
18 changed files with 648 additions and 581 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -210,7 +210,10 @@ struct Gia_ParVta_t_
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nLearntMax; // max number of learned clauses
int nLearnedMax; // max number of learned clauses
int nLearnedStart; // max number of learned clauses
int nLearnedDelta; // delta increase of learned clauses
int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
int fUseTermVars; // use terminal variables

51
src/aig/gia/giaAbsGla.c
View File

@ -129,36 +129,6 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prints integer number using 6 characters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_PrintInt( int i )
{
Abc_Print( 1, " " );
if ( i > -1000 && i < 1000 )
Abc_Print( 1, " %4d", i );
else if ( i > -10000 && i < 10000 )
Abc_Print( 1, "%4.2fk", (float)i/1000 );
else if ( i > -100000 && i < 100000 )
Abc_Print( 1, "%4.1fk", (float)i/1000 );
else if ( i > -1000000 && i < 1000000 )
Abc_Print( 1, "%4.0fk", (float)i/1000 );
else if ( i > -10000000 && i < 10000000 )
Abc_Print( 1, "%4.2fm", (float)i/1000000 );
else if ( i > -100000000 && i < 100000000 )
Abc_Print( 1, "%4.1fm", (float)i/1000000 );
else if ( i > -1000000000 && i < 1000000000 )
Abc_Print( 1, "%4.0fm", (float)i/1000000 );
}
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
@ -1129,7 +1099,11 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 );
p->pSat = sat_solver2_new();
// p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
p->pSat->nLearntStart = p->pPars->nLearnedStart;
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
p->nSatVars = 1;
return p;
}
@ -1243,8 +1217,8 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla )
@ -1660,7 +1634,7 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
{
if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
return;
Abc_Print( 1, "%3d :", nFrames-1 );
Abc_Print( 1, "%4d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
@ -1794,7 +1768,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
Vec_Int_t * vCore, * vPPis;
Abc_Cex_t * pCex = NULL;
int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1;
clock_t clk = clock(), clk2;
clock_t clk2, clk = clock();
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@ -1834,7 +1808,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
}
}
// start the manager
clk = clock();
p = Gla_ManStart( pAig, pPars );
p->timeInit = clock() - clk;
// set runtime limit
@ -1844,8 +1817,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
Abc_Print( 1, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n",
pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n",
pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}
for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )

53
src/aig/gia/giaAbsVta.c
View File

@ -135,36 +135,6 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prints integer number using 6 characters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_PrintInt( int i )
{
Abc_Print( 1, " " );
if ( i > -1000 && i < 1000 )
Abc_Print( 1, " %4d", i );
else if ( i > -10000 && i < 10000 )
Abc_Print( 1, "%4.2fk", (float)i/1000 );
else if ( i > -100000 && i < 100000 )
Abc_Print( 1, "%4.1fk", (float)i/1000 );
else if ( i > -1000000 && i < 1000000 )
Abc_Print( 1, "%4.0fk", (float)i/1000 );
else if ( i > -10000000 && i < 10000000 )
Abc_Print( 1, "%4.2fm", (float)i/1000000 );
else if ( i > -100000000 && i < 100000000 )
Abc_Print( 1, "%4.1fm", (float)i/1000000 );
else if ( i > -1000000000 && i < 1000000000 )
Abc_Print( 1, "%4.0fm", (float)i/1000000 );
}
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
@ -183,7 +153,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearntMax = 1000; // max number of learned clauses
p->nLearnedMax = 1000; // max number of learned clauses
p->nLearnedStart = 1000; // max number of learned clauses
p->nLearnedDelta = 200; // max number of learned clauses
p->nLearnedPerce = 40; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
@ -1065,7 +1038,11 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
// p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
p->pSat->nLearntStart = p->pPars->nLearnedStart;
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
// start the abstraction
assert( pGia->vObjClasses != NULL );
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
@ -1087,8 +1064,8 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Vga_ManStop( Vta_Man_t * p )
{
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
@ -1261,7 +1238,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
return fChanges;
// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
Abc_Print( 1, "%3d :", nFrames-1 );
Abc_Print( 1, "%4d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", p->nSeenGla );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
@ -1605,8 +1582,10 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%\n",
pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n",
pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
// Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
}

2
src/aig/ivy/ivyFraig.c
View File

@ -2923,7 +2923,7 @@ printf( "***************\n" );
***********************************************************************/
int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
{
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Vec_Int_t * vLeaves;
Aig_Man_t * pMan;
Aig_Obj_t * pObj;

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

@ -17692,7 +17692,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fPartition;
int fMiter;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@ -18943,13 +18943,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewSolver;
int fVerbose;
int nConfLimit;
int nStartLearned;
int nDeltaLearned;
int nRatioLearned;
int nLearnedStart;
int nLearnedDelta;
int nLearnedPerce;
int nInsLimit;
clock_t clk;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
// set defaults
fAlignPol = 0;
fAndOuts = 0;
@ -18957,11 +18957,11 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
nConfLimit = 0;
nInsLimit = 0;
nStartLearned = 0;
nDeltaLearned = 0;
nRatioLearned = 0;
nLearnedStart = 0;
nLearnedDelta = 0;
nLearnedPerce = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CISDRpanvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpanvh" ) ) != EOF )
{
switch ( c )
{
@ -18987,15 +18987,15 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInsLimit < 0 )
goto usage;
break;
case 'S':
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nStartLearned = atoi(argv[globalUtilOptind]);
nLearnedStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nStartLearned < 0 )
if ( nLearnedStart < 0 )
goto usage;
break;
case 'D':
@ -19004,20 +19004,20 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
nDeltaLearned = atoi(argv[globalUtilOptind]);
nLearnedDelta = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nDeltaLearned < 0 )
if ( nLearnedDelta < 0 )
goto usage;
break;
case 'R':
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
goto usage;
}
nRatioLearned = atoi(argv[globalUtilOptind]);
nLearnedPerce = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRatioLearned < 0 )
if ( nLearnedPerce < 0 )
goto usage;
break;
case 'p':
@ -19063,7 +19063,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
clk = clock();
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
{
@ -19085,14 +19085,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: dsat [-CISDR num] [-panvh]\n" );
Abc_Print( -2, "usage: dsat [-CILDE num] [-panvh]\n" );
Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
Abc_Print( -2, "\t derives CNF from the current network and leave it unchanged\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
Abc_Print( -2, "\t-S num : starting value for learned clause removal [default = %d]\n", nStartLearned );
Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nDeltaLearned );
Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", nRatioLearned );
Abc_Print( -2, "\t-L num : starting value for learned clause removal [default = %d]\n", nLearnedStart );
Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nLearnedDelta );
Abc_Print( -2, "\t-E num : ratio percentage for learned clause removal [default = %d]\n", nLearnedPerce );
Abc_Print( -2, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
Abc_Print( -2, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
Abc_Print( -2, "\t-n : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
@ -27548,7 +27548,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, fStartVta = 0;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfkadvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadvh" ) ) != EOF )
{
switch ( c )
{
@ -27602,9 +27602,31 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearntMax = atoi(argv[globalUtilOptind]);
pPars->nLearnedStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearntMax < 0 )
if ( pPars->nLearnedStart < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedDelta = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedDelta < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedPerce = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedPerce < 0 )
goto usage;
break;
case 'T':
@ -27696,12 +27718,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fkadvh]\n" );
Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadvh]\n" );
Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
Abc_Print( -2, "\t-E num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
@ -27731,7 +27755,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtradvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtradvh" ) ) != EOF )
{
switch ( c )
{
@ -27785,9 +27809,31 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearntMax = atoi(argv[globalUtilOptind]);
pPars->nLearnedStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearntMax < 0 )
if ( pPars->nLearnedStart < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedDelta = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedDelta < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLearnedPerce = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearnedPerce < 0 )
goto usage;
break;
case 'T':
@ -27873,13 +27919,15 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-tradvh]\n" );
Abc_Print( -2, "usage: &vta [-FSPCLDETR num] [-A file] [-tradvh]\n" );
Abc_Print( -2, "\t variable-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
Abc_Print( -2, "\t-E num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"vabs.aig\"]\n" );

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

@ -1403,7 +1403,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
SeeAlso []
***********************************************************************/
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue;//, clk = clock();
@ -1411,7 +1411,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
assert( Abc_NtkLatchNum(pNtk) == 0 );
// assert( Abc_NtkPoNum(pNtk) == 1 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;

2
src/base/abci/abcQbf.c
View File

@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///

19
src/misc/util/abc_global.h
View File

@ -285,6 +285,25 @@ static inline void Abc_Print( int level, const char * format, ... )
va_end( args );
}
static inline void Abc_PrintInt( int i )
{
Abc_Print( 1, " " );
if ( i > -1000 && i < 1000 )
Abc_Print( 1, " %4d", i );
else if ( i > -10000 && i < 10000 )
Abc_Print( 1, "%4.2fk", (double)i/1000 );
else if ( i > -100000 && i < 100000 )
Abc_Print( 1, "%4.1fk", (double)i/1000 );
else if ( i > -1000000 && i < 1000000 )
Abc_Print( 1, "%4.0fk", (double)i/1000 );
else if ( i > -10000000 && i < 10000000 )
Abc_Print( 1, "%4.2fm", (double)i/1000000 );
else if ( i > -100000000 && i < 100000000 )
Abc_Print( 1, "%4.1fm", (double)i/1000000 );
else if ( i > -1000000000 && i < 1000000000 )
Abc_Print( 1, "%4.0fm", (double)i/1000000 );
}
static inline void Abc_PrintTime( int level, const char * pStr, clock_t time )
{
ABC_PRT( pStr, time );

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

@ -285,7 +285,7 @@ static inline int Fra_ImpCreate( int Left, int Right )
////////////////////////////////////////////////////////////////////////
/*=== fraCec.c ========================================================*/
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/

14
src/proof/fra/fraCec.c
View File

@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
{
if ( fNewSolver )
{
@ -181,12 +181,12 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
return 1;
}
if ( nStartLearned )
pSat->nLearntStart = nStartLearned;
if ( nDeltaLearned )
pSat->nLearntDelta = nDeltaLearned;
if ( nRatioLearned )
pSat->nLearntRatio = nRatioLearned;
if ( nLearnedStart )
pSat->nLearntStart = nLearnedStart;
if ( nLearnedDelta )
pSat->nLearntDelta = nLearnedDelta;
if ( nLearnedPerce )
pSat->nLearntRatio = nLearnedPerce;
if ( fVerbose )
pSat->fVerbose = fVerbose;

115
src/sat/bsat/satClause.h
View File

@ -33,6 +33,11 @@ ABC_NAMESPACE_HEADER_START
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
//#define LEARNT_MAX_START_DEFAULT 0
#define LEARNT_MAX_START_DEFAULT 10000
#define LEARNT_MAX_INCRE_DEFAULT 1000
#define LEARNT_MAX_RATIO_DEFAULT 50
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -40,9 +45,6 @@ ABC_NAMESPACE_HEADER_START
//=================================================================================================
// Clause datatype + minor functions:
typedef int lit;
typedef int cla;
typedef struct clause_t clause;
struct clause_t
{
@ -90,14 +92,16 @@ static inline int Sat_MemIntSize( int size, int lrn ) { return (s
static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); }
//static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i])); return (clause *)(p->pPages[i] + k ); }
static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { return (clause *)(p->pPages[i] + k); }
static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert( k ); return (clause *)(p->pPages[i] + k); }
//static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); }
static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); }
static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return h ? Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ) : NULL; }
static inline int Sat_MemEntryNum( Sat_Mem_t * p, int lrn ) { return p->nEntries[lrn]; }
static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) | k; }
static inline cla Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] ); }
static inline int Sat_MemClauseUsed( Sat_Mem_t * p, cla h ) { return h < p->BookMarkH[(h & p->uLearnedMask) > 0]; }
static inline double Sat_MemMemoryHand( Sat_Mem_t * p, cla h ) { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4); }
static inline double Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn ) { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) ); }
static inline double Sat_MemMemoryAllUsed( Sat_Mem_t * p ) { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 ); }
@ -108,9 +112,10 @@ static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1.
// i is page number
// k is page offset
#define Sat_MemForEachClause( p, c, i, k ) \
for ( i = 0; i <= p->iPage[0]; i += 2 ) \
for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
// this macro has to be fixed (Sat_MemClauseSize does not work for problem clauses in proof mode)
//#define Sat_MemForEachClause( p, c, i, k ) \
// for ( i = 0; i <= p->iPage[0]; i += 2 ) \
// for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
#define Sat_MemForEachLearned( p, c, i, k ) \
for ( i = 1; i <= p->iPage[1]; i += 2 ) \
@ -130,7 +135,8 @@ static inline lit clause_read_lit( cla h ) { return (li
static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; }
static inline int clause_learnt( clause * c ) { return c->lrn; }
static inline int clause_id( clause * c ) { assert(c->lrn); return c->lits[c->size]; }
static inline int clause_id( clause * c ) { return c->lits[c->size]; }
static inline int clause_set_id( clause * c, int id ) { c->lits[c->size] = id; }
static inline int clause_size( clause * c ) { return c->size; }
static inline lit * clause_begin( clause * c ) { return c->lits; }
static inline lit * clause_end( clause * c ) { return c->lits + c->size; }
@ -147,6 +153,26 @@ static inline void clause_print( clause * c )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocating vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Sat_MemCountL( Sat_Mem_t * p )
{
clause * c;
int i, k, Count = 0;
Sat_MemForEachLearned( p, c, i, k )
Count++;
return Count;
}
/**Function*************************************************************
Synopsis [Allocating vector.]
@ -216,10 +242,10 @@ static inline void Sat_MemRestart( Sat_Mem_t * p )
***********************************************************************/
static inline void Sat_MemBookMark( Sat_Mem_t * p )
{
p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
p->BookMarkE[0] = p->nEntries[0];
p->BookMarkE[1] = p->nEntries[1];
p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
}
static inline void Sat_MemRollBack( Sat_Mem_t * p )
{
@ -227,8 +253,8 @@ static inline void Sat_MemRollBack( Sat_Mem_t * p )
p->nEntries[1] = p->BookMarkE[1];
p->iPage[0] = Sat_MemHandPage( p, p->BookMarkH[0] );
p->iPage[1] = Sat_MemHandPage( p, p->BookMarkH[1] );
Sat_MemWriteLimit( p->pPages[0], Sat_MemHandShift( p, p->BookMarkH[0] ) );
Sat_MemWriteLimit( p->pPages[1], Sat_MemHandShift( p, p->BookMarkH[1] ) );
Sat_MemWriteLimit( p->pPages[p->iPage[0]], Sat_MemHandShift( p, p->BookMarkH[0] ) );
Sat_MemWriteLimit( p->pPages[p->iPage[1]], Sat_MemHandShift( p, p->BookMarkH[1] ) );
}
/**Function*************************************************************
@ -266,15 +292,15 @@ static inline void Sat_MemFree( Sat_Mem_t * p )
SeeAlso []
***********************************************************************/
static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn )
static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn, int fPlus1 )
{
clause * c;
int * pPage = p->pPages[p->iPage[lrn]];
int nInts = Sat_MemIntSize( nSize, lrn );
int nInts = Sat_MemIntSize( nSize, lrn | fPlus1 );
assert( nInts + 3 < (1 << p->nPageSize) );
// need two extra at the begining of the page and one extra in the end
if ( Sat_MemLimit(pPage) + nInts >= (1 << p->nPageSize) )
{
if ( Sat_MemLimit(pPage) + nInts + 2 >= (1 << p->nPageSize) )
{
p->iPage[lrn] += 2;
if ( p->iPage[lrn] >= p->nPagesAlloc )
{
@ -293,8 +319,8 @@ static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn
c->lrn = lrn;
if ( pArray )
memcpy( c->lits, pArray, sizeof(int) * nSize );
if ( lrn )
c->lits[c->size] = p->nEntries[1];
if ( lrn | fPlus1 )
c->lits[c->size] = p->nEntries[lrn];
p->nEntries[lrn]++;
Sat_MemIncLimit( pPage, nInts );
return Sat_MemHandCurrent(p, lrn) - nInts;
@ -333,15 +359,46 @@ static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn )
***********************************************************************/
static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
{
clause * c;
int i, k, iNew = 1, kNew = 2, nInts, Counter = 0;
clause * c, * cPivot = NULL;
int i, k, iNew = 1, kNew = 2, nInts, fStartLooking, Counter = 0;
int hLimit = Sat_MemHandCurrent(p, 1);
if ( hLimit == Sat_MemHand(p, 1, 2) )
return 0;
if ( fDoMove && p->BookMarkH[1] )
{
// move the pivot
assert( p->BookMarkH[1] >= Sat_MemHand(p, 1, 2) && p->BookMarkH[1] <= hLimit );
// get the pivot and remember it may be pointed offlimit
cPivot = Sat_MemClauseHand( p, p->BookMarkH[1] );
if ( p->BookMarkH[1] < hLimit && !cPivot->mark )
{
p->BookMarkH[1] = cPivot->lits[cPivot->size];
cPivot = NULL;
}
// else find the next used clause after cPivot
}
// iterate through the learned clauses
fStartLooking = 0;
Sat_MemForEachLearned( p, c, i, k )
{
assert( c->lrn );
// skip marked entry
if ( c->mark )
{
// if pivot is a marked clause, start looking for the next non-marked one
if ( cPivot && cPivot == c )
{
fStartLooking = 1;
cPivot = NULL;
}
continue;
}
// if we started looking before, we found it!
if ( fStartLooking )
{
fStartLooking = 0;
p->BookMarkH[1] = c->lits[c->size];
}
// compute entry size
nInts = Sat_MemClauseSize(c);
assert( !(nInts & 1) );
@ -380,12 +437,24 @@ static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
}
if ( fDoMove )
{
// update the counter
p->nEntries[1] = Counter;
// update the page count
p->iPage[1] = iNew;
// set the limit of the last page
Sat_MemWriteLimit( p->pPages[iNew], kNew );
// update the counter
p->nEntries[1] = Counter;
// check if the pivot need to be updated
if ( p->BookMarkH[1] )
{
if ( cPivot )
{
p->BookMarkH[1] = Sat_MemHandCurrent(p, 1);
p->BookMarkE[1] = p->nEntries[1];
}
else
p->BookMarkE[1] = clause_id(Sat_MemClauseHand( p, p->BookMarkH[1] ));
}
}
return Counter;
}

125
src/sat/bsat/satProof.c
View File

@ -18,7 +18,11 @@
***********************************************************************/
#include "satSolver2.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "misc/vec/vecSet.h"
#include "aig/aig/aig.h"
@ -26,7 +30,6 @@
ABC_NAMESPACE_IMPL_START
/*
Proof is represented as a vector of records.
A resolution record is represented by a handle (an offset in this vector).
@ -35,8 +38,6 @@ ABC_NAMESPACE_IMPL_START
They are marked by bitshifting by 2 bits up and setting the LSB to 1
*/
/*
typedef struct satset_t satset;
struct satset_t
{
@ -45,21 +46,20 @@ struct satset_t
unsigned partA : 1;
unsigned nEnts : 29;
int Id;
lit pEnts[0];
int pEnts[0];
};
#define satset_foreach_entry( p, c, h, s ) \
for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline satset* Proof_ClauseRead ( Vec_Int_t* p, cla h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); }
static inline satset* Proof_NodeRead ( Vec_Set_t* p, cla h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); }
//static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); }
//static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return (satset *)Vec_IntEntryP( p, h );}
static inline satset* Proof_NodeRead ( Vec_Set_t* p, int h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); }
static inline int Proof_NodeWordNum ( int nEnts ) { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1); }
void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ) { Proof_NodeRead(p, h)->nEnts = nEnts; }
// iterating through nodes in the proof
#define Proof_ForeachClauseVec( pVec, p, pNode, i ) \
for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )
@ -71,10 +71,10 @@ static inline int Proof_NodeWordNum ( int nEnts ) { assert( nE
// iterating through fanins of a proof node
#define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )
#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ )
//#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \
// for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
//#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \
// for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ )
////////////////////////////////////////////////////////////////////////
@ -252,6 +252,7 @@ int Proof_MarkUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
SeeAlso []
***********************************************************************/
/*
void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
{
satset * pFanin;
@ -288,6 +289,7 @@ void Sat_ProofReduceCheck( sat_solver2 * s )
c->Id = 0;
Vec_PtrFree( vVisited );
}
*/
/**Function*************************************************************
@ -300,6 +302,7 @@ void Sat_ProofReduceCheck( sat_solver2 * s )
SeeAlso []
***********************************************************************/
/*
void Sat_ProofReduce2( sat_solver2 * s )
{
Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
@ -361,20 +364,24 @@ void Sat_ProofReduce2( sat_solver2 * s )
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
Sat_ProofReduceCheck( s );
// Sat_ProofReduceCheck( s );
}
*/
void Sat_ProofReduce( sat_solver2 * s )
int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
{
Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
// Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
// Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
// Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
int fVerbose = 0;
Vec_Ptr_t * vUsed;
satset * pNode, * pFanin, * pPivot;
int i, j, k, hTemp, nSize;
clock_t clk = clock();
static clock_t TimeTotal = 0;
int RetValue;
// collect visited nodes
nSize = Proof_MarkUsedRec( vProof, vRoots );
@ -390,20 +397,20 @@ void Sat_ProofReduce( sat_solver2 * s )
pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
Vec_PtrPush( vUsed, pNode );
// update fanins
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
else // problem clause
assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
// else // problem clause
// assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
}
// update roots
Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
Vec_IntWriteEntry( vRoots, i, pNode->Id );
// determine new pivot
assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(vProof) );
pPivot = Proof_NodeRead( vProof, s->hProofPivot );
s->hProofPivot = Vec_SetHandCurrentS(vProof);
s->iProofPivot = Vec_PtrSize(vUsed);
assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) );
pPivot = Proof_NodeRead( vProof, hProofPivot );
RetValue = Vec_SetHandCurrentS(vProof);
// s->iProofPivot = Vec_PtrSize(vUsed);
// compact the nodes
Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
{
@ -411,8 +418,8 @@ void Sat_ProofReduce( sat_solver2 * s )
memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
if ( pPivot && pPivot <= pNode )
{
s->hProofPivot = hTemp;
s->iProofPivot = i;
RetValue = hTemp;
// s->iProofPivot = i;
pPivot = NULL;
}
}
@ -432,8 +439,10 @@ void Sat_ProofReduce( sat_solver2 * s )
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
Vec_SetShrinkLimits( vProof );
// Sat_ProofReduceCheck( s );
return RetValue;
}
#if 0
/**Function*************************************************************
@ -565,7 +574,7 @@ void Sat_ProofCheck( sat_solver2 * s )
Vec_SetFree( vResolves );
Vec_IntFree( vUsed );
}
#endif
/**Function*************************************************************
@ -578,33 +587,38 @@ void Sat_ProofCheck( sat_solver2 * s )
SeeAlso []
***********************************************************************/
Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Int_t * vUsed, int fUseIds )
Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed )
{
Vec_Int_t * vCore;
satset * pNode, * pFanin;
int i, k;//, clk = clock();
unsigned * pBitMap;
int i, k, MaxCla = 0;
// find the largest number
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( pFanin == NULL )
MaxCla = Abc_MaxInt( MaxCla, pNode->pEnts[k] >> 2 );
// allocate bitmap
pBitMap = ABC_CALLOC( unsigned, Abc_BitWordNum(MaxCla) + 1 );
// collect leaves
vCore = Vec_IntAlloc( 1000 );
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
pNode->Id = 0;
Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k )
if ( pFanin && !pFanin->mark )
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( pFanin == NULL )
{
pFanin->mark = 1;
Vec_IntPush( vCore, pNode->pEnts[k] >> 2 );
int Entry = (pNode->pEnts[k] >> 2);
if ( Abc_InfoHasBit(pBitMap, Entry) )
continue;
Abc_InfoSetBit(pBitMap, Entry);
Vec_IntPush( vCore, Entry );
}
}
// clean core clauses and reexpress core in terms of clause IDs
Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
{
assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
pNode->mark = 0;
if ( fUseIds )
Vec_IntWriteEntry( vCore, i, pNode->Id );
}
ABC_FREE( pBitMap );
// Vec_IntUniqify( vCore );
return vCore;
}
#if 0
/**Function*************************************************************
Synopsis [Verifies that variables are labeled correctly.]
@ -687,7 +701,8 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
// collect visited nodes
vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
// collect core clauses (cleans vUsed and vCore)
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
vCore = Sat_ProofCollectCore( vProof, vUsed );
// vCore arrived in terms of clause handles
// map variables into their global numbers
vVarMap = Vec_IntStartFull( s->size );
@ -789,7 +804,8 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
// collect visited nodes
vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
// collect core clauses (cleans vUsed and vCore)
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
vCore = Sat_ProofCollectCore( vProof, vUsed, 0 );
// vCore arrived in terms of clause handles
// map variables into their global numbers
vVarMap = Vec_IntStartFull( s->size );
@ -864,6 +880,8 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
return pRes;
}
#endif
/**Function*************************************************************
Synopsis [Computes UNSAT core.]
@ -875,19 +893,16 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
SeeAlso []
***********************************************************************/
void * Sat_ProofCore( sat_solver2 * s )
void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
Vec_Int_t Roots = { 1, 1, &hRoot }, * vRoots = &Roots;
Vec_Int_t * vCore, * vUsed;
int hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
// collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
// collect core clauses
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 );
vCore = Sat_ProofCollectCore( vProof, vUsed );
Vec_IntFree( vUsed );
return vCore;
}

14
src/sat/bsat/satSolver.c
View File

@ -29,11 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
//#define LEARNT_MAX_START_DEFAULT 0
#define LEARNT_MAX_START_DEFAULT 20000
#define LEARNT_MAX_INCRE_DEFAULT 1000
#define LEARNT_MAX_RATIO_DEFAULT 50
#define SAT_USE_ANALYZE_FINAL
//=================================================================================================
@ -426,7 +421,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
// create new clause
// h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
h = Sat_MemAppend( &s->Mem, begin, size, learnt );
h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 );
assert( !(h & 1) );
if ( s->hLearnts == -1 && learnt )
s->hLearnts = h;
@ -919,13 +914,12 @@ sat_solver* sat_solver_new(void)
// Vec_SetAlloc_(&s->Mem, 15);
Sat_MemAlloc_(&s->Mem, 14);
s->hLearnts = -1;
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
s->binary = clause_read( s, s->hBinary );
s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
s->nLearntMax = s->nLearntStart;
// initialize vectors
@ -1089,7 +1083,7 @@ void sat_solver_rollback( sat_solver* s )
int i;
Sat_MemRestart( &s->Mem );
s->hLearnts = -1;
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
s->binary = clause_read( s, s->hBinary );
veci_resize(&s->act_clas, 0);
@ -1098,7 +1092,7 @@ void sat_solver_rollback( sat_solver* s )
for ( i = 0; i < s->size*2; i++ )
s->wlists[i].size = 0;
s->nLearntMax = s->nLearntStart;
s->nDBreduces = 0;
// initialize other vars
s->size = 0;

9
src/sat/bsat/satSolver.h
View File

@ -28,8 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <string.h>
#include <assert.h>
#include "satClause.h"
#include "satVec.h"
#include "satClause.h"
#include "misc/vec/vecSet.h"
ABC_NAMESPACE_HEADER_START
@ -98,6 +98,8 @@ struct sat_solver_t
int hLearnts; // the first learnt clause
int hBinary; // the special binary clause
clause * binary;
veci* wlists; // watcher lists
veci act_clas; // contain clause activities
// activities
#ifdef USE_FLOAT_ACTIVITY
@ -112,7 +114,6 @@ struct sat_solver_t
unsigned* activity; // A heuristic measurement of the activity of a variable.
#endif
veci* wlists; //
// varinfo * vi; // variable information
int* levels; //
char* assigns; // Current values of variables.
@ -141,13 +142,11 @@ struct sat_solver_t
int fVerbose;
stats_t stats;
int nLearntMax; // max number of learned clauses
int nLearntStart; // starting learned clause limit
int nLearntDelta; // delta of learned clause limit
int nLearntRatio; // ratio percentage of learned clauses
int nLearntMax; // max number of learned clauses
int nDBreduces; // number of DB reductions
// veci learned; // contain learnt clause handles
veci act_clas; // contain clause activities
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications

617
src/sat/bsat/satSolver2.c
View File

File diff suppressed because it is too large Load Diff

76
src/sat/bsat/satSolver2.h
View File

@ -21,15 +21,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef ABC__sat__bsat__satSolver2_h
#define ABC__sat__bsat__satSolver2_h
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satClause.h"
#include "satVec.h"
#include "satClause.h"
#include "misc/vec/vecSet.h"
ABC_NAMESPACE_HEADER_START
@ -63,17 +63,12 @@ extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
// global variables
extern int var_is_partA (sat_solver2* s, int v);
extern void var_set_partA(sat_solver2* s, int v, int partA);
// clause grouping (these two only work after creating a clause before the solver is called)
extern int clause2_is_partA (sat_solver2* s, int handle);
extern void clause2_set_partA(sat_solver2* s, int handle, int partA);
// other clause functions
extern int clause2_id(sat_solver2* s, int h);
// proof-based APIs
extern void * Sat_ProofCore( sat_solver2 * s );
extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
extern void Sat_ProofReduce( sat_solver2 * s );
extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
extern void Sat_ProofCheck( sat_solver2 * s );
//=================================================================================================
@ -106,28 +101,27 @@ struct sat_solver2_t
unsigned* activity; // A heuristic measurement of the activity of a variable.
#endif
int nUnits; // the total number of unit clauses
int nof_learnts; // the number of clauses to trigger reduceDB
int nLearntMax; // enables using reduce DB method
int nLearntStart; // starting learned clause limit
int nLearntDelta; // delta of learned clause limit
int nLearntRatio; // ratio percentage of learned clauses
int nDBreduces; // number of DB reductions
int fNotUseRandom; // do not allow random decisions with a fixed probability
int fSkipSimplify; // set to one to skip simplification of the clause database
int fProofLogging; // enable proof-logging
int fVerbose;
// clauses
veci clauses; // clause memory
veci learnts; // learnt memory
Sat_Mem_t Mem;
veci* wlists; // watcher lists (for each literal)
veci claActs; // clause activities
veci act_clas; // clause activities
veci claProofs; // clause proofs
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int nof_learnts; // the number of clauses to trigger reduceDB
// rollback
int iVarPivot; // the pivot for variables
int iTrailPivot; // the pivot for trail
int iProofPivot; // the pivot for proof records
int hClausePivot; // the pivot for problem clause
int hLearntPivot; // the pivot for learned clause
int hProofPivot; // the pivot for proof records
// internal state
@ -155,7 +149,8 @@ struct sat_solver2_t
// proof logging
Vec_Set_t Proofs; // sequence of proof records
veci temp_proof; // temporary place to store proofs
int nUnits; // the total number of unit clauses
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
// statistics
stats_t stats;
@ -164,40 +159,13 @@ struct sat_solver2_t
clock_t nRuntimeLimit; // external limit on runtime
};
typedef struct satset_t satset;
struct satset_t
{
unsigned learnt : 1;
unsigned mark : 1;
unsigned partA : 1;
unsigned nEnts : 29;
int Id;
lit pEnts[0];
};
static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); }
static inline int clause2_proofid(sat_solver2* s, clause* c, int partA) { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : ((clause_id(c)+1)<<2) | (partA<<1) | 1; }
static inline satset* satset_read (veci* p, cla h ) { return h ? (satset*)(veci_begin(p) + h) : NULL; }
static inline cla satset_handle (veci* p, satset* c) { return (cla)((int *)c - veci_begin(p)); }
static inline int satset_check (veci* p, satset* c) { return (int*)c > veci_begin(p) && (int*)c < veci_begin(p) + veci_size(p); }
static inline int satset_size (int nLits) { return sizeof(satset)/4 + nLits; }
static inline void satset_print (satset * c) {
int i;
printf( "{ " );
for ( i = 0; i < (int)c->nEnts; i++ )
printf( "%d ", (c->pEnts[i] & 1)? -(c->pEnts[i] >> 1) : c->pEnts[i] >> 1 );
printf( "}\n" );
}
#define satset_foreach_entry( p, c, h, s ) \
for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
#define satset_foreach_entry_vec( pVec, p, c, i ) \
for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ )
#define satset_foreach_var( p, var, i, start ) \
for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
#define satset_foreach_lit( p, lit, i, start ) \
for ( i = start; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ )
#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 )
#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 )
// these two only work after creating a clause before the solver is called
static inline int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; }
static inline void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; }
static inline int clause2_id(sat_solver2* s, int h) { return clause_id(clause2_read(s, h)); }
//=================================================================================================
// Public APIs:
@ -265,10 +233,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
assert( s->qhead == s->qtail );
s->iVarPivot = s->size;
s->iTrailPivot = s->qhead;
s->iProofPivot = Vec_SetEntryNum(&s->Proofs);
s->hClausePivot = veci_size(&s->clauses);
s->hLearntPivot = veci_size(&s->learnts);
s->hProofPivot = Vec_SetHandCurrent(&s->Proofs);
Sat_MemBookMark( &s->Mem );
}
static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )

2
src/sat/bsat/satUtil.c
View File

@ -211,6 +211,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
printf( "propagations : %10d\n", (int)s->stats.propagations );
// printf( "inspects : %10d\n", (int)s->stats.inspects );
// printf( "inspects2 : %10d\n", (int)s->stats.inspects2 );
/*
printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n",
1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20),
100.0 * (s->cap - s->size) / s->cap,
@ -218,6 +219,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
100.0 * (s->clauses.cap - s->clauses.size +
s->learnts.cap - s->learnts.size) /
(s->clauses.cap + s->learnts.cap) );
*/
}
/**Function*************************************************************

3
src/sat/bsat/satVec.h
View File

@ -127,6 +127,9 @@ static inline void vecp_remove(vecp* v, void* e)
#endif
#endif
typedef int lit;
typedef int cla;
typedef char lbool;
static const int var_Undef = -1;