summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAbsGla.c19
-rw-r--r--src/aig/gia/giaAbsVta.c17
-rw-r--r--src/base/abci/abc.c22
-rw-r--r--src/sat/bsat/satProof.c5
-rw-r--r--src/sat/bsat/satSolver.h1
-rw-r--r--src/sat/bsat/satSolver2.c10
7 files changed, 46 insertions, 31 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 97a7b7b7..c537a31b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -223,7 +223,8 @@ struct Gia_ParVta_t_
int fDumpVabs; // dumps the abstracted model
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
- int iFrame; // the number of frames covered
+ int iFrame; // the number of frames covered
+ int nFramesNoChange; // the number of last frames without changes
};
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 6505c2f2..117ad3e0 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -509,7 +509,7 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
{
int i;//, Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
- assert( (int)pRef->Sign == Sign );
+// assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit )
return;
if ( p->pPars->fPropFanout )
@@ -1214,8 +1214,9 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
- 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 );
+ Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
+ sat_solver2_nlearnts(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 )
@@ -1805,7 +1806,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
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" );
+ 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 )
{
@@ -1891,9 +1892,13 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
nCoreSize = Vec_IntSize( vCore );
Gia_GlaAddToCounters( p, vCore );
if ( i == 0 )
+ {
+ p->pPars->nFramesNoChange++;
Vec_IntFree( vCore );
+ }
else
{
+ p->pPars->nFramesNoChange = 0;
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
@@ -1967,9 +1972,9 @@ finish:
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
- Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
+ Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
@@ -1978,7 +1983,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
else
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index f7c1e5a5..85d51a42 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1062,8 +1062,9 @@ 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: 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 );
+ Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
+ sat_solver2_nlearnts(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 );
@@ -1534,7 +1535,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
printf( "Sequential miter is trivially UNSAT.\n" );
return 1;
- }
+ }
ABC_FREE( pAig->pCexSeq );
pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
printf( "Sequential miter is trivially SAT.\n" );
@@ -1564,7 +1565,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
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" );
+ Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
}
assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
@@ -1665,9 +1666,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
// reset the counter of frames without change
nCountNoChange = 1;
+ p->pPars->nFramesNoChange = 0;
}
else if ( ++nCountNoChange == 2 ) // time to send
{
+ p->pPars->nFramesNoChange++;
if ( Abc_FrameIsBridgeMode() )
{
// cancel old one if it was sent
@@ -1709,9 +1712,9 @@ finish:
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
- Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
+ Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
@@ -1720,7 +1723,7 @@ finish:
else
{
p->pPars->iFrame++;
- Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
+ Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
}
}
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 68d0e073..6caf37cb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27891,7 +27891,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "There is no AIG.\n" );
- return 1;
+ return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
@@ -27971,12 +27971,12 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no AIG.\n" );
- return 1;
+ return 0;
}
if ( pAbc->pGia->vObjClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" );
- return 1;
+ return 0;
}
Vec_IntFreeP( &pAbc->pGia->vGateClasses );
pAbc->pGia->vGateClasses = Gia_VtaConvertToGla( pAbc->pGia, pAbc->pGia->vObjClasses );
@@ -28034,17 +28034,17 @@ int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" );
- return 1;
+ return 0;
}
if ( pAbc->pGia->vGateClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" );
- return 1;
+ return 0;
}
if ( pAbc->nFrames < 1 )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames );
- return 1;
+ return 0;
}
Vec_IntFreeP( &pAbc->pGia->vObjClasses );
pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames );
@@ -28091,12 +28091,12 @@ int Abc_CommandAbc9Fla2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no AIG.\n" );
- return 1;
+ return 0;
}
if ( pAbc->pGia->vFlopClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no gate-level abstraction is defined.\n" );
- return 1;
+ return 0;
}
Vec_IntFreeP( &pAbc->pGia->vGateClasses );
pAbc->pGia->vGateClasses = Gia_FlaConvertToGla( pAbc->pGia, pAbc->pGia->vFlopClasses );
@@ -28142,12 +28142,12 @@ int Abc_CommandAbc9Gla2Fla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no AIG.\n" );
- return 1;
+ return 0;
}
if ( pAbc->pGia->vGateClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no gate-level abstraction is defined.\n" );
- return 1;
+ return 0;
}
Vec_IntFreeP( &pAbc->pGia->vFlopClasses );
pAbc->pGia->vFlopClasses = Gia_GlaConvertToFla( pAbc->pGia, pAbc->pGia->vGateClasses );
@@ -28194,7 +28194,7 @@ int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" );
- return 1;
+ return 0;
}
pTemp = Gia_ManReparam( pAbc->pGia, fVerbose );
Abc_CommandUpdate9( pAbc, pTemp );
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 680b1996..eeadf09e 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
if ( pNode->Id == 0 )
continue;
pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
+ assert( pNode->Id > 0 );
Vec_PtrPush( vUsed, pNode );
// update fanins
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
+ {
+ assert( pFanin->Id > 0 );
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) );
}
@@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
if ( pPivot && pPivot <= pNode )
{
RetValue = hTemp;
-// s->iProofPivot = i;
pPivot = NULL;
}
}
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 520e8284..eace9eea 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -30,7 +30,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satVec.h"
#include "satClause.h"
-#include "misc/vec/vecSet.h"
ABC_NAMESPACE_HEADER_START
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cb6199ec..2cd825b7 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -164,7 +164,7 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
if ( s->fProofLogging )
{
int ProofId = clause2_proofid(s, c, 0);
- assert( ProofId > 0 );
+ assert( (ProofId >> 2) > 0 );
veci_resize( &s->temp_proof, 0 );
veci_push( &s->temp_proof, 0 );
veci_push( &s->temp_proof, 0 );
@@ -178,7 +178,7 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
- assert( ProofId > 0 );
+ assert( (ProofId >> 2) > 0 );
veci_push( &s->temp_proof, ProofId );
}
}
@@ -1417,7 +1417,10 @@ void sat_solver2_reducedb(sat_solver2* s)
break;
}
if ( j < nLearnedOld / 6 )
+ {
+ ABC_FREE( pSortValues );
return;
+ }
// mark learned clauses to remove
Counter = j = 0;
@@ -1439,6 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
s->stats.learnts--;
}
}
+ ABC_FREE( pSortValues );
// if ( j == nLearnedOld )
// return;
@@ -1717,6 +1721,7 @@ void sat_solver2_verify( sat_solver2* s )
// Abc_Print(1, "Verification passed.\n" );
}
*/
+
// checks how many watched clauses are satisfied by 0-level assignments
// (this procedure may be called before setting up a new bookmark for rollback)
int sat_solver2_check_watched( sat_solver2* s )
@@ -1754,7 +1759,6 @@ int sat_solver2_check_watched( sat_solver2* s )
return 0;
}
-
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)
{
int restart_iter = 0;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 19:20:50 +0000