summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h5
-rw-r--r--src/aig/gia/giaAbsGla.c51
-rw-r--r--src/aig/gia/giaAbsVta.c53
-rw-r--r--src/aig/ivy/ivyFraig.c2
-rw-r--r--src/base/abci/abc.c116
-rw-r--r--src/base/abci/abcDar.c4
-rw-r--r--src/base/abci/abcQbf.c2
-rw-r--r--src/misc/util/abc_global.h19
-rw-r--r--src/proof/fra/fra.h2
-rw-r--r--src/proof/fra/fraCec.c14
-rw-r--r--src/sat/bsat/satClause.h115
-rw-r--r--src/sat/bsat/satProof.c125
-rw-r--r--src/sat/bsat/satSolver.c14
-rw-r--r--src/sat/bsat/satSolver.h9
-rw-r--r--src/sat/bsat/satSolver2.c609
-rw-r--r--src/sat/bsat/satSolver2.h76
-rw-r--r--src/sat/bsat/satUtil.c2
-rw-r--r--src/sat/bsat/satVec.h3
18 files changed, 644 insertions, 577 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3eda381d..97a7b7b7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 49bcc6a0..c5444119 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -131,36 +131,6 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
/**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.]
Description []
@@ -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 )
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index e2dfc90d..4e6f3eee 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -137,36 +137,6 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
/**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.]
Description []
@@ -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" );
}
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 234f403a..776a41b3 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -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;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index daf265e8..68d0e073 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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->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->nLearntMax < 0 )
+ 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->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->nLearntMax < 0 )
+ 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" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 82656d98..8333f39d 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -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;
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index a77ddf94..237a56f5 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -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 ///
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index ea214d86..204ed90d 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -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 );
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 8be02e45..1690b463 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -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 ========================================================*/
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index 0e483b1f..3e7addb2 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -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;
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 8b1a1294..7769dc36 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -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; }
@@ -158,6 +164,26 @@ static inline void clause_print( clause * c )
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.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize )
{
assert( nPageSize > 8 && nPageSize < 32 );
@@ -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;
}
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index eaadf71d..a669d2be 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -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;
}
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 2e3af2dd..5472e25d 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -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;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8998b78c..520e8284 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -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
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 58ea531c..0bca05ed 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -30,9 +30,11 @@ ABC_NAMESPACE_IMPL_START
#define SAT_USE_PROOF_LOGGING
+static int Time = 0;
+
//=================================================================================================
// Debug:
-
+
//#define VERBOSEDEBUG
// For derivation output (verbosity level 2)
@@ -136,28 +138,19 @@ static inline void solver2_clear_marks(sat_solver2* s) {
//=================================================================================================
// Clause datatype + minor functions:
-static inline satset* clause2_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); }
-static inline cla clause2_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
-static inline int clause2_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
-static inline int clause2_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
-static inline int clause2_is_used(sat_solver2* s, cla h) { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot); }
-
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
-//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL; }
+//static inline clause* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL; }
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; }
static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
-static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause2_read(s, s->units[v]); }
+static inline clause* var_unit_clause(sat_solver2* s, int v) { return clause2_read(s, s->units[v]); }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){
assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++;
}
-//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
-// these two only work after creating a clause before the solver is called
-int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; }
-void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; }
-int clause2_id(sat_solver2* s, int h) { return clause2_read(s, h)->Id; }
+#define clause_foreach_var( p, var, i, start ) \
+ for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ )
//=================================================================================================
// Simple helpers:
@@ -168,7 +161,7 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l
//=================================================================================================
// Proof logging:
-static inline void proof_chain_start( sat_solver2* s, satset* c )
+static inline void proof_chain_start( sat_solver2* s, clause* c )
{
if ( s->fProofLogging )
{
@@ -181,11 +174,11 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
}
}
-static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
+static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{
if ( s->fProofLogging )
{
- satset* c = cls ? cls : var_unit_clause( s, Var );
+ clause* c = cls ? cls : var_unit_clause( s, Var );
int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
assert( ProofId > 0 );
veci_push( &s->temp_proof, ProofId );
@@ -196,9 +189,9 @@ static inline int proof_chain_stop( sat_solver2* s )
{
if ( s->fProofLogging )
{
+ extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
- satset * c = (satset *)Vec_SetEntry( &s->Proofs, h );
- c->nEnts = veci_size(&s->temp_proof) - 2;
+ Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 );
return h;
}
return 0;
@@ -292,12 +285,12 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause2_rescale(sat_solver2* s) {
- static int Total = 0;
- float * claActs = (float *)veci_begin(&s->claActs);
+ static clock_t Total = 0;
+ float * act_clas = (float *)veci_begin(&s->act_clas);
int i;
clock_t clk = clock();
- for (i = 0; i < veci_size(&s->claActs); i++)
- claActs[i] *= (float)1e-20;
+ for (i = 0; i < veci_size(&s->act_clas); i++)
+ act_clas[i] *= (float)1e-20;
s->cla_inc *= (float)1e-20;
Total += clock() - clk;
@@ -311,11 +304,11 @@ static inline void act_var_bump(sat_solver2* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,v);
}
-static inline void act_clause2_bump(sat_solver2* s, satset*c) {
- float * claActs = (float *)veci_begin(&s->claActs);
- assert( c->Id < veci_size(&s->claActs) );
- claActs[c->Id] += s->cla_inc;
- if (claActs[c->Id] > (float)1e20)
+static inline void act_clause2_bump(sat_solver2* s, clause*c) {
+ float * act_clas = (float *)veci_begin(&s->act_clas);
+ assert( c->Id < veci_size(&s->act_clas) );
+ act_clas[c->Id] += s->cla_inc;
+ if (act_clas[c->Id] > (float)1e20)
act_clause2_rescale(s);
}
static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
@@ -332,14 +325,14 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause2_rescale(sat_solver2* s) {
-// static int Total = 0;
- int i;//, clk = clock();
- unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
- for (i = 1; i < veci_size(&s->claActs); i++)
- claActs[i] >>= 14;
+// static clock_t Total = 0;
+// clock_t clk = clock();
+ int i;
+ unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
+ for (i = 0; i < veci_size(&s->act_clas); i++)
+ act_clas[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-
// Total += clock() - clk;
// Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
@@ -351,11 +344,12 @@ static inline void act_var_bump(sat_solver2* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,v);
}
-static inline void act_clause2_bump(sat_solver2* s, satset*c) {
- unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
- assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
- claActs[c->Id] += s->cla_inc;
- if (claActs[c->Id] & 0x80000000)
+static inline void act_clause2_bump(sat_solver2* s, clause*c) {
+ unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
+ int Id = clause_id(c);
+ assert( Id >= 0 && Id < veci_size(&s->act_clas) );
+ act_clas[Id] += s->cla_inc;
+ if (act_clas[Id] & 0x80000000)
act_clause2_rescale(s);
}
static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
@@ -366,89 +360,61 @@ static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc
//=================================================================================================
// Clause functions:
+static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
+{
+ int i, lev, minl = 0, lbd = 0;
+ for (i = 0; i < (int)c->size; i++) {
+ lev = var_level(s, lit_var(c->lits[i]));
+ if ( !(minl & (1 << (lev & 31))) ) {
+ minl |= 1 << (lev & 31);
+ lbd++;
+ }
+ }
+ return lbd;
+}
+
static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
{
- satset* c;
- int i, Cid, nLits = end - begin;
- assert(nLits < 1 || begin[0] >= 0);
- assert(nLits < 2 || begin[1] >= 0);
- assert(nLits < 1 || lit_var(begin[0]) < s->size);
- assert(nLits < 2 || lit_var(begin[1]) < s->size);
- // add memory if needed
-
- // assign clause ID
- if ( learnt )
+ clause* c;
+ int h, size = end - begin;
+ assert(size < 1 || begin[0] >= 0);
+ assert(size < 2 || begin[1] >= 0);
+ assert(size < 1 || lit_var(begin[0]) < s->size);
+ assert(size < 2 || lit_var(begin[1]) < s->size);
+ // create new clause
+ h = Sat_MemAppend( &s->Mem, begin, size, learnt, 1 );
+ assert( !(h & 1) );
+ c = clause2_read( s, h );
+ if (learnt)
{
- if ( veci_size(&s->learnts) + satset_size(nLits) > s->learnts.cap )
- {
- int nMemAlloc = s->learnts.cap ? 2 * s->learnts.cap : (1 << 20);
- s->learnts.ptr = ABC_REALLOC( int, veci_begin(&s->learnts), nMemAlloc );
- // Abc_Print(1, "Reallocing from %d to %d...\n", s->learnts.cap, nMemAlloc );
- s->learnts.cap = nMemAlloc;
- if ( veci_size(&s->learnts) == 0 )
- veci_push( &s->learnts, -1 );
- }
- // create clause
- c = (satset*)(veci_begin(&s->learnts) + veci_size(&s->learnts));
- ((int*)c)[0] = 0;
- c->learnt = learnt;
- c->nEnts = nLits;
- for (i = 0; i < nLits; i++)
- c->pEnts[i] = begin[i];
- // count the clause
- s->stats.learnts++;
- s->stats.learnts_literals += nLits;
- c->Id = s->stats.learnts;
- assert( c->Id == veci_size(&s->claActs) );
- veci_push(&s->claActs, 0);
+ if ( s->fProofLogging )
+ assert( proof_id );
+ c->lbd = sat_clause_compute_lbd( s, c );
+ assert( clause_id(c) == veci_size(&s->act_clas) );
if ( proof_id )
veci_push(&s->claProofs, proof_id);
- if ( nLits > 2 )
+// veci_push(&s->act_clas, (1<<10));
+ veci_push(&s->act_clas, 0);
+ if ( size > 2 )
act_clause2_bump( s,c );
- // extend storage
- Cid = (veci_size(&s->learnts) << 1) | 1;
- s->learnts.size += satset_size(nLits);
- assert( veci_size(&s->learnts) <= s->learnts.cap );
- assert(((ABC_PTRUINT_T)c & 3) == 0);
-// Abc_Print(1, "Clause for proof %d: ", proof_id );
-// satset_print( c );
+ s->stats.learnts++;
+ s->stats.learnts_literals += size;
// remember the last one
- s->hLearntLast = Cid;
+ s->hLearntLast = h;
}
else
{
- if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap )
- {
- int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
- s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
- // Abc_Print(1, "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
- s->clauses.cap = nMemAlloc;
- if ( veci_size(&s->clauses) == 0 )
- veci_push( &s->clauses, -1 );
- }
- // create clause
- c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
- ((int*)c)[0] = 0;
- c->learnt = learnt;
- c->nEnts = nLits;
- for (i = 0; i < nLits; i++)
- c->pEnts[i] = begin[i];
- // count the clause
+ assert( clause_id(c) == (int)s->stats.clauses );
s->stats.clauses++;
- s->stats.clauses_literals += nLits;
- c->Id = s->stats.clauses;
- // extend storage
- Cid = (veci_size(&s->clauses) << 1);
- s->clauses.size += satset_size(nLits);
- assert( veci_size(&s->clauses) <= s->clauses.cap );
- assert(((ABC_PTRUINT_T)c & 3) == 0);
+ s->stats.clauses_literals += size;
}
// watch the clause
- if ( nLits > 1 ){
- veci_push(solver2_wlist(s,lit_neg(begin[0])),Cid);
- veci_push(solver2_wlist(s,lit_neg(begin[1])),Cid);
+ if ( size > 1 )
+ {
+ veci_push(solver2_wlist(s,lit_neg(begin[0])),h);
+ veci_push(solver2_wlist(s,lit_neg(begin[1])),h);
}
- return Cid;
+ return h;
}
//=================================================================================================
@@ -472,17 +438,6 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
s->reasons[v] = from; // = from << 1;
s->trail[s->qtail++] = l;
order_assigned(s, v);
-/*
- if ( solver2_dlevel(s) == 0 )
- {
- satset * c = from ? clause2_read( s, from ) : NULL;
- Abc_Print(1, "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) );
- if ( c )
- satset_print( c );
- else
- Abc_Print(1, "<none>\n" );
- }
-*/
return true;
}
}
@@ -589,7 +544,7 @@ static double solver2_progress(sat_solver2* s)
| stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/
/*
-void Solver::analyzeFinal(satset* confl, bool skip_first)
+void Solver::analyzeFinal(clause* confl, bool skip_first)
{
// -- NOTE! This code is relatively untested. Please report bugs!
conflict.clear();
@@ -628,7 +583,7 @@ void Solver::analyzeFinal(satset* confl, bool skip_first)
}
*/
-static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
+static int solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
{
int i, j, x;//, start;
veci_resize(&s->conf_final,0);
@@ -636,7 +591,7 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
return s->hProofLast;
proof_chain_start( s, conf );
assert( veci_size(&s->tagged) == 0 );
- satset_foreach_var( conf, x, i, skip_first ){
+ clause_foreach_var( conf, x, i, skip_first ){
if ( var_level(s,x) )
var_set_tag(s, x, 1);
else
@@ -647,10 +602,10 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
x = lit_var(s->trail[i]);
if (var_tag(s,x)){
- satset* c = clause2_read(s, var_reason(s,x));
+ clause* c = clause2_read(s, var_reason(s,x));
if (c){
proof_chain_resolve( s, c, x );
- satset_foreach_var( c, x, j, 1 ){
+ clause_foreach_var( c, x, j, 1 ){
if ( var_level(s,x) )
var_set_tag(s, x, 1);
else
@@ -672,7 +627,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
// tag[1]: Processed by this procedure
// tag[2]: 0=non-removable, 1=removable
- satset* c;
+ clause* c;
int i, x;
// skip visited
@@ -686,7 +641,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
return 0;
}
- satset_foreach_var( c, x, i, 1 ){
+ clause_foreach_var( c, x, i, 1 ){
if (var_tag(s,x) & 1)
solver2_lit_removable_rec(s, x);
else{
@@ -706,7 +661,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
static int solver2_lit_removable(sat_solver2* s, int x)
{
- satset* c;
+ clause* c;
int i, top;
if ( !var_reason(s,x) )
return 0;
@@ -731,7 +686,7 @@ static int solver2_lit_removable(sat_solver2* s, int x)
}
x >>= 1;
c = clause2_read(s, var_reason(s,x));
- satset_foreach_var( c, x, i, 1 ){
+ clause_foreach_var( c, x, i, 1 ){
if (var_tag(s,x) || !var_level(s,x))
continue;
if (!var_reason(s,x) || !var_lev_mark(s,x)){
@@ -747,7 +702,7 @@ static int solver2_lit_removable(sat_solver2* s, int x)
static void solver2_logging_order(sat_solver2* s, int x)
{
- satset* c;
+ clause* c;
int i;
if ( (var_tag(s,x) & 4) )
return;
@@ -766,7 +721,7 @@ static void solver2_logging_order(sat_solver2* s, int x)
c = clause2_read(s, var_reason(s,x));
// if ( !c )
// Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" );
- satset_foreach_var( c, x, i, 1 ){
+ clause_foreach_var( c, x, i, 1 ){
if ( !var_level(s,x) || (var_tag(s,x) & 1) )
continue;
veci_push(&s->stack, x << 1);
@@ -777,19 +732,19 @@ static void solver2_logging_order(sat_solver2* s, int x)
static void solver2_logging_order_rec(sat_solver2* s, int x)
{
- satset* c;
+ clause* c;
int i, y;
if ( (var_tag(s,x) & 8) )
return;
c = clause2_read(s, var_reason(s,x));
- satset_foreach_var( c, y, i, 1 )
+ clause_foreach_var( c, y, i, 1 )
if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
solver2_logging_order_rec(s, y);
var_add_tag(s, x, 8);
veci_push(&s->min_step_order, x);
}
-static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
+static int solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
{
int cnt = 0;
lit p = 0;
@@ -805,9 +760,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
veci_push(learnt,lit_Undef);
while ( 1 ){
assert(c != 0);
- if (c->learnt)
+ if (c->lrn)
act_clause2_bump(s,c);
- satset_foreach_var( c, x, j, (int)(p > 0) ){
+ clause_foreach_var( c, x, j, (int)(p > 0) ){
assert(x >= 0 && x < s->size);
if ( var_tag(s, x) )
continue;
@@ -821,7 +776,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
if (var_level(s,x) == solver2_dlevel(s))
cnt++;
else
- veci_push(learnt,c->pEnts[j]);
+ veci_push(learnt,c->lits[j]);
}
while (!var_tag(s, lit_var(s->trail[ind--])));
@@ -864,7 +819,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
c = clause2_read(s, var_reason(s,vars[i]));
proof_chain_resolve( s, c, vars[i] );
- satset_foreach_var(c, x, k, 1)
+ clause_foreach_var(c, x, k, 1)
if ( var_level(s,x) == 0 )
proof_chain_resolve( s, NULL, x );
}
@@ -913,9 +868,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
return proof_id;
}
-satset* solver2_propagate(sat_solver2* s)
+clause* solver2_propagate(sat_solver2* s)
{
- satset* c, * confl = NULL;
+ clause* c, * confl = NULL;
veci* ws;
lit* lits, false_lit, p, * stop, * k;
cla* begin,* end, *i, *j;
@@ -931,7 +886,7 @@ satset* solver2_propagate(sat_solver2* s)
s->stats.propagations++;
for (i = j = begin; i < end; ){
c = clause2_read(s,*i);
- lits = c->pEnts;
+ lits = c->lits;
// Make sure the false literal is data[1]:
false_lit = lit_neg(p);
@@ -946,7 +901,7 @@ satset* solver2_propagate(sat_solver2* s)
*j++ = *i;
else{
// Look for new watch:
- stop = lits + c->nEnts;
+ stop = lits + c->size;
for (k = lits + 2; k < stop; k++){
if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
lits[1] = *k;
@@ -962,7 +917,7 @@ satset* solver2_propagate(sat_solver2* s)
int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
// Log production of top-level unit clause:
proof_chain_start( s, c );
- satset_foreach_var( c, x, k, 1 ){
+ clause_foreach_var( c, x, k, 1 ){
assert( var_level(s, x) == 0 );
proof_chain_resolve( s, NULL, x );
}
@@ -986,6 +941,8 @@ satset* solver2_propagate(sat_solver2* s)
*j++ = *i;
// Clause is unit under assignment:
+ if ( c->lrn )
+ c->lbd = sat_clause_compute_lbd(s, c);
if (!solver2_enqueue(s,Lit, *i)){
confl = clause2_read(s,*i++);
// Copy the remaining watches:
@@ -1024,7 +981,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
veci_new(&learnt_clause);
for (;;){
- satset* confl = solver2_propagate(s);
+ clause* confl = solver2_propagate(s);
if (confl != 0){
// CONFLICT
int blevel;
@@ -1138,9 +1095,13 @@ sat_solver2* sat_solver2_new(void)
#endif
s->fSkipSimplify = 1;
s->fNotUseRandom = 0;
- s->nLearntMax = 0;
s->fVerbose = 0;
+ 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
veci_new(&s->order);
veci_new(&s->trail_lim);
@@ -1152,32 +1113,20 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->mark_levels);
veci_new(&s->min_lit_order);
veci_new(&s->min_step_order);
- veci_new(&s->learnt_live);
- veci_new(&s->claActs); veci_push(&s->claActs, -1);
- veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
+// veci_new(&s->learnt_live);
+
+ Sat_MemAlloc_( &s->Mem, 14 );
+ veci_new(&s->act_clas);
+ veci_new(&s->claProofs);
if ( s->fProofLogging )
Vec_SetAlloc_( &s->Proofs, 20 );
- // prealloc clause
- assert( !s->clauses.ptr );
- s->clauses.cap = (1 << 20);
- s->clauses.ptr = ABC_ALLOC( int, s->clauses.cap );
- veci_push(&s->clauses, -1);
- // prealloc learnt
- assert( !s->learnts.ptr );
- s->learnts.cap = (1 << 20);
- s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap );
- veci_push(&s->learnts, -1);
-
// initialize clause pointers
s->hLearntLast = -1; // the last learnt clause
s->hProofLast = -1; // the last proof ID
// initialize rollback
s->iVarPivot = 0; // the pivot for variables
s->iTrailPivot = 0; // the pivot for trail
- s->iProofPivot = 0; // the pivot for proof records
- s->hClausePivot = 1; // the pivot for problem clause
- s->hLearntPivot = 1; // the pivot for learned clause
s->hProofPivot = 1; // the pivot for proof records
return s;
}
@@ -1243,11 +1192,11 @@ void sat_solver2_delete(sat_solver2* s)
if ( fVerify )
{
veci * pCore = (veci *)Sat_ProofCore( s );
- Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
+// Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
veci_delete( pCore );
ABC_FREE( pCore );
- if ( s->fProofLogging )
- Sat_ProofCheck( s );
+// if ( s->fProofLogging )
+// Sat_ProofCheck( s );
}
// report statistics
@@ -1264,11 +1213,12 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->mark_levels);
veci_delete(&s->min_lit_order);
veci_delete(&s->min_step_order);
- veci_delete(&s->learnt_live);
- veci_delete(&s->claActs);
+// veci_delete(&s->learnt_live);
+ veci_delete(&s->act_clas);
veci_delete(&s->claProofs);
- veci_delete(&s->clauses);
- veci_delete(&s->learnts);
+// veci_delete(&s->clauses);
+// veci_delete(&s->lrns);
+ Sat_MemFree_( &s->Mem );
// veci_delete(&s->proofs);
Vec_SetFree_( &s->Proofs );
@@ -1290,6 +1240,8 @@ void sat_solver2_delete(sat_solver2* s)
ABC_FREE(s->model );
}
ABC_FREE(s);
+
+// Abc_PrintTime( 1, "Time", Time );
}
@@ -1358,9 +1310,9 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
{
// Log production of top-level unit clause:
int x, k, proof_id, CidNew;
- satset* c = clause2_read(s, Cid);
+ clause* c = clause2_read(s, Cid);
proof_chain_start( s, c );
- satset_foreach_var( c, x, k, 1 )
+ clause_foreach_var( c, x, k, 1 )
proof_chain_resolve( s, NULL, x );
proof_id = proof_chain_stop( s );
// generate a new clause
@@ -1400,127 +1352,178 @@ void luby2_test()
void sat_solver2_reducedb(sat_solver2* s)
{
static clock_t TimeTotal = 0;
- satset * c, * pivot;
- cla h,* pArray,* pArray2;
- int * pPerm, * pClaAct, nClaAct, ActCutOff;
- int i, j, k, hTemp, hHandle, LastSize = 0;
+ Sat_Mem_t * pMem = &s->Mem;
+ clause * c;
+ int nLearnedOld = veci_size(&s->act_clas);
+ int * act_clas = veci_begin(&s->act_clas);
+ int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
+ int i, j, k, Id, nSelected, LastSize = 0;
int Counter, CounterStart;
clock_t clk = clock();
+ static int Count = 0;
+ Count++;
+ assert( s->nLearntMax );
+ s->nDBreduces++;
+// printf( "Calling reduceDB with %d clause limit and parameters (%d %d %d).\n", s->nLearntMax, s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
- // check if it is time to reduce
- if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
- return;
+/*
+ // find the new limit
s->nLearntMax = s->nLearntMax * 11 / 10;
-
// preserve 1/10 of last clauses
CounterStart = s->stats.learnts - (s->nLearntMax / 10);
-
// preserve 1/10 of most active clauses
- pClaAct = veci_begin(&s->claActs) + 1;
- nClaAct = veci_size(&s->claActs) - 1;
- pPerm = Abc_MergeSortCost( pClaAct, nClaAct );
- assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] );
- ActCutOff = pClaAct[pPerm[nClaAct*9/10]];
+ pSortValues = veci_begin(&s->act_clas);
+ pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
+ assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
+ nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]];
+ ABC_FREE( pPerm );
+// nCutoffValue = ABC_INFINITY;
+*/
+
+
+ // find the new limit
+ s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
+ // preserve 1/20 of last clauses
+ CounterStart = nLearnedOld - (s->nLearntMax / 20);
+ // preserve 3/4 of most active clauses
+ nSelected = nLearnedOld*s->nLearntRatio/100;
+ // create sorting values
+ pSortValues = ABC_ALLOC( int, nLearnedOld );
+ Sat_MemForEachLearned( pMem, c, i, k )
+ {
+ Id = clause_id(c);
+ pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
+// pSortValues[Id] = act_clas[Id];
+ assert( pSortValues[Id] >= 0 );
+ }
+ // find non-decreasing permutation
+ pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
+ assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
+ nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
ABC_FREE( pPerm );
-// ActCutOff = ABC_INFINITY;
+// nCutoffValue = ABC_INFINITY;
- // mark learned clauses to remove
- Counter = 0;
- veci_resize( &s->learnt_live, 0 );
- sat_solver_foreach_learnt( s, c, h )
+ // count how many clauses satisfy the condition
+ Counter = j = 0;
+ Sat_MemForEachLearned( pMem, c, i, k )
{
- if ( Counter++ > CounterStart || c->nEnts < 3 || pClaAct[c->Id-1] >= ActCutOff || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 )
- veci_push( &s->learnt_live, h );
+ assert( c->mark == 0 );
+ if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
+ {
+ }
else
- c->mark = 1;
+ j++;
+ if ( j >= nLearnedOld / 6 )
+ break;
}
- // report the results
- if ( s->fVerbose )
- Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
- veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts );
-
- // remap clause proofs and clauses
- hHandle = 1;
- pArray = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
- pArray2 = veci_begin(&s->claActs);
- satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
+ if ( j < nLearnedOld / 6 )
+ return;
+
+ // mark learned clauses to remove
+ Counter = j = 0;
+ pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
+ Sat_MemForEachLearned( pMem, c, i, k )
{
- if ( pArray )
- pArray[i+1] = pArray[c->Id];
- pArray2[i+1] = pArray2[c->Id];
- c->Id = hHandle; hHandle += satset_size(c->nEnts);
+ assert( c->mark == 0 );
+ if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
+ {
+ pSortValues[j] = pSortValues[clause_id(c)];
+ if ( pClaProofs )
+ pClaProofs[j] = pClaProofs[clause_id(c)];
+ j++;
+ }
+ else // delete
+ {
+ c->mark = 1;
+ s->stats.learnts_literals -= clause_size(c);
+ s->stats.learnts--;
+ }
}
+// if ( j == nLearnedOld )
+// return;
+
+ assert( s->stats.learnts == (unsigned)j );
+ assert( Counter == nLearnedOld );
+ veci_resize(&s->act_clas,j);
if ( s->fProofLogging )
- veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1);
- veci_resize(&s->claActs,veci_size(&s->learnt_live)+1);
+ veci_resize(&s->claProofs,j);
+
+ // update ID of each clause to be its new handle
+ Counter = Sat_MemCompactLearned( pMem, 0 );
+ assert( Counter == (int)s->stats.learnts );
- // update reason clauses
+ // update reasons
for ( i = 0; i < s->size; i++ )
- if ( s->reasons[i] && (s->reasons[i] & 1) )
- {
- c = clause2_read( s, s->reasons[i] );
- assert( c->mark == 0 );
- s->reasons[i] = (c->Id << 1) | 1;
- }
+ {
+ if ( !s->reasons[i] ) // no reason
+ continue;
+ if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
+ continue;
+ if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
+ continue;
+ c = clause2_read( s, s->reasons[i] );
+ assert( c->mark == 0 );
+ s->reasons[i] = clause_id(c); // updating handle here!!!
+ }
- // compact watches
+ // update watches
for ( i = 0; i < s->size*2; i++ )
{
- pArray = veci_begin(&s->wlists[i]);
+ int * pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
- if ( !(pArray[k] & 1) ) // problem clause
+ {
+ if ( clause_is_lit(pArray[k]) ) // 2-lit clause
pArray[j++] = pArray[k];
- else if ( !(c = clause2_read(s, pArray[k]))->mark ) // useful learned clause
- pArray[j++] = (c->Id << 1) | 1;
+ else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
+ pArray[j++] = pArray[k];
+ else
+ {
+ c = clause2_read(s, pArray[k]);
+ if ( !c->mark ) // useful learned clause
+ pArray[j++] = clause_id(c); // updating handle here!!!
+ }
+ }
veci_resize(&s->wlists[i],j);
}
+
// compact units
if ( s->fProofLogging )
- for ( i = 0; i < s->size; i++ )
- if ( s->units[i] && (s->units[i] & 1) )
- {
- c = clause2_read( s, s->units[i] );
- assert( c->mark == 0 );
- s->units[i] = (c->Id << 1) | 1;
- }
- // compact clauses
- pivot = satset_read( &s->learnts, s->hLearntPivot );
- s->hLearntPivot = hTemp = hHandle;
- satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
- {
- hTemp = c->Id; c->Id = i + 1;
- LastSize = satset_size(c->nEnts);
- memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*LastSize );
- if ( pivot && pivot <= c )
- {
- s->hLearntPivot = hTemp;
- pivot = NULL;
- }
- }
- assert( hHandle == hTemp + LastSize );
- veci_resize(&s->learnts,hHandle);
- s->stats.learnts = veci_size(&s->learnt_live);
- assert( s->hLearntPivot <= veci_size(&s->learnts) );
- assert( s->hClausePivot <= veci_size(&s->clauses) );
+ for ( i = 0; i < s->size; i++ )
+ if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
+ {
+ c = clause2_read( s, s->units[i] );
+ assert( c->mark == 0 );
+ s->units[i] = clause_id(c);
+ }
+
+ // perform final move of the clauses
+ Counter = Sat_MemCompactLearned( pMem, 1 );
+ assert( Counter == (int)s->stats.learnts );
// compact proof (compacts 'proofs' and update 'claProofs')
if ( s->fProofLogging )
- Sat_ProofReduce( s );
+ s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+
+ // report the results
TimeTotal += clock() - clk;
if ( s->fVerbose )
- Abc_PrintTime( 1, "Time", TimeTotal );
+ {
+ Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
+ s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
+ Abc_PrintTime( 1, "Time", TimeTotal );
+ }
}
// reverses to the previously bookmarked point
void sat_solver2_rollback( sat_solver2* s )
{
+ Sat_Mem_t * pMem = &s->Mem;
int i, k, j;
+ static int Count = 0;
+ Count++;
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
- assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) );
- assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
- assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
// reset implication queue
solver2_canceluntil_rollback( s, s->iTrailPivot );
@@ -1538,42 +1541,32 @@ void sat_solver2_rollback( sat_solver2* s )
}
}
// compact watches
- if ( s->hClausePivot > 1 || s->hLearntPivot > 1 )
- {
- for ( i = 0; i < s->size*2; i++ )
- {
- cla* pArray = veci_begin(&s->wlists[i]);
- for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
- if ( clause2_is_used(s, pArray[k]) )
- pArray[j++] = pArray[k];
- veci_resize(&s->wlists[i],j);
- }
- }
- // reset problem clauses
- if ( s->hClausePivot < veci_size(&s->clauses) )
+ for ( i = 0; i < s->iVarPivot*2; i++ )
{
- satset* first = satset_read(&s->clauses, s->hClausePivot);
- s->stats.clauses = first->Id-1;
- veci_resize(&s->clauses, s->hClausePivot);
- }
- // resetn learned clauses
- if ( s->hLearntPivot < veci_size(&s->learnts) )
- {
- satset* first = satset_read(&s->learnts, s->hLearntPivot);
- veci_resize(&s->claActs, first->Id);
- if ( s->fProofLogging ) {
- veci_resize(&s->claProofs, first->Id);
-// Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot); // <- some bug here
-// Vec_SetShrink(&s->Proofs, s->hProofPivot);
- Sat_ProofReduce( s );
- }
- s->stats.learnts = first->Id-1;
- veci_resize(&s->learnts, s->hLearntPivot);
+ cla* pArray = veci_begin(&s->wlists[i]);
+ for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
+ if ( Sat_MemClauseUsed(pMem, pArray[k]) )
+ pArray[j++] = pArray[k];
+ veci_resize(&s->wlists[i],j);
}
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
+ // reset clause counts
+ s->stats.clauses = pMem->BookMarkE[0];
+ s->stats.learnts = pMem->BookMarkE[1];
+ // rollback clauses
+ Sat_MemRollBack( pMem );
+
+ // resize learned arrays
+ veci_resize(&s->act_clas, s->stats.learnts);
+ if ( s->fProofLogging )
+ {
+ veci_resize(&s->claProofs, s->stats.learnts);
+ Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here
+// Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+ }
// initialize other vars
s->size = s->iVarPivot;
@@ -1614,9 +1607,6 @@ void sat_solver2_rollback( sat_solver2* s )
// initialize rollback
s->iVarPivot = 0; // the pivot for variables
s->iTrailPivot = 0; // the pivot for trail
- s->iProofPivot = 0; // the pivot for proof records
- s->hClausePivot = 1; // the pivot for problem clause
- s->hLearntPivot = 1; // the pivot for learned clause
s->hProofPivot = 1; // the pivot for proof records
}
}
@@ -1630,9 +1620,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
for (i = 0; i < s->cap*2; i++)
Mem += s->wlists[i].cap * sizeof(int);
Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists );
- Mem += s->clauses.cap * sizeof(int);
- Mem += s->learnts.cap * sizeof(int);
- Mem += s->claActs.cap * sizeof(int);
+ Mem += s->act_clas.cap * sizeof(int);
Mem += s->claProofs.cap * sizeof(int);
// Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity );
// Mem += s->cap * sizeof(char); // ABC_FREE(s->tags );
@@ -1651,7 +1639,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons );
Mem += s->cap * sizeof(int); // ABC_FREE(s->units );
Mem += s->cap * sizeof(int); // ABC_FREE(s->model );
-
Mem += s->tagged.cap * sizeof(int);
Mem += s->stack.cap * sizeof(int);
Mem += s->order.cap * sizeof(int);
@@ -1661,9 +1648,9 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
Mem += s->mark_levels.cap * sizeof(int);
Mem += s->min_lit_order.cap * sizeof(int);
Mem += s->min_step_order.cap * sizeof(int);
- Mem += s->learnt_live.cap * sizeof(int);
Mem += s->temp_proof.cap * sizeof(int);
-// Mem += Vec_ReportMemory( &s->Mem );
+ Mem += Sat_MemMemoryAll( &s->Mem );
+// Mem += Vec_ReportMemory( &s->Proofs );
return Mem;
}
double sat_solver2_memory_proof( sat_solver2* s )
@@ -1673,6 +1660,7 @@ double sat_solver2_memory_proof( sat_solver2* s )
// find the clause in the watcher lists
+/*
int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
{
int i, k, Found = 0;
@@ -1697,25 +1685,26 @@ int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
}
return Found;
}
-
+*/
+/*
// verify that all problem clauses are satisfied
void sat_solver2_verify( sat_solver2* s )
{
- satset * c;
+ clause * c;
int i, k, v, Counter = 0;
- satset_foreach_entry( &s->clauses, c, i, 1 )
+ clause_foreach_entry( &s->clauses, c, i, 1 )
{
- for ( k = 0; k < (int)c->nEnts; k++ )
+ for ( k = 0; k < (int)c->size; k++ )
{
- v = lit_var(c->pEnts[k]);
- if ( sat_solver2_var_value(s, v) ^ lit_sign(c->pEnts[k]) )
+ v = lit_var(c->lits[k]);
+ if ( sat_solver2_var_value(s, v) ^ lit_sign(c->lits[k]) )
break;
}
- if ( k == (int)c->nEnts )
+ if ( k == (int)c->size )
{
Abc_Print(1, "Clause %d is not satisfied. ", c->Id );
- satset_print( c );
- sat_solver2_find_clause( s, satset_handle(&s->clauses, c), 1 );
+ clause_print( c );
+ sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 );
Counter++;
}
}
@@ -1724,7 +1713,7 @@ void sat_solver2_verify( sat_solver2* s )
// else
// Abc_Print(1, "Verification passed.\n" );
}
-
+*/
int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
{
@@ -1761,7 +1750,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (!solver2_assume(p)){
GClause r = reason[var(p)];
if (r != Gclause2_NULL){
- satset* confl;
+ clause* confl;
if (r.isLit()){
confl = propagate_tmpbin;
(*confl)[1] = ~p;
@@ -1775,7 +1764,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
conflict.push(~p);
cancelUntil(0);
return false; }
- satset* confl = propagate();
+ clause* confl = propagate();
if (confl != NULL){
analyzeFinal(confl), assert(conflict.size() > 0);
cancelUntil(0);
@@ -1793,10 +1782,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
veci_push(&s->trail_lim,s->qtail);
if (!solver2_enqueue(s,p,0))
{
- satset* r = clause2_read(s, lit_reason(s,p));
+ clause* r = clause2_read(s, lit_reason(s,p));
if (r != NULL)
{
- satset* confl = r;
+ clause* confl = r;
proof_id = solver2_analyze_final(s, confl, 1);
veci_push(&s->conf_final, lit_neg(p));
}
@@ -1816,7 +1805,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
}
else
{
- satset* confl = solver2_propagate(s);
+ clause* confl = solver2_propagate(s);
if (confl != NULL){
proof_id = solver2_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0);
@@ -1851,8 +1840,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
}
if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
break;
- // reduce the set of learnt clauses:
- sat_solver2_reducedb(s);
+ // reduce the set of learnt clauses
+ if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax )
+ sat_solver2_reducedb(s);
// perform next run
nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
status = solver2_search(s, nof_conflicts);
@@ -1872,5 +1862,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
return status;
}
+void * Sat_ProofCore( sat_solver2 * s )
+{
+ extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
+ return Proof_DeriveCore( &s->Proofs, s->hProofLast );
+}
ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index cba57638..36d2a1ad 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -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 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++ )
+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; }
-#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 )
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 1694ae01..05b9403d 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -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*************************************************************
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 8a711007..8cc8ba4e 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 01:19:56 +0000