Skip to content

A
abc
Commit d3ad7fba by Alan Mishchenko
Options

Several small changes and fixes.

parent 86a0ae0b
Showing with 46 additions and 31 deletions
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)); }
......
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
......
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 );
}
}
}
......
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 );
......
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;
}
}
......
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
......
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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment