From ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Tue, 29 Aug 2017 09:40:51 +0200 Subject: Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages --- src/sat/bmc/bmcBmc.c | 7 +++---- src/sat/bmc/bmcBmc2.c | 11 +++++------ src/sat/bmc/bmcBmc3.c | 29 ++++++++++++++--------------- src/sat/bmc/bmcBmcS.c | 15 +++++++-------- src/sat/bmc/bmcMesh.c | 9 ++++----- src/sat/bmc/bmcMesh2.c | 7 +++---- 6 files changed, 36 insertions(+), 42 deletions(-) (limited to 'src/sat/bmc') diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c index 8f7452e5..6ab8a92e 100644 --- a/src/sat/bmc/bmcBmc.c +++ b/src/sat/bmc/bmcBmc.c @@ -22,7 +22,6 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #include "bmc.h" ABC_NAMESPACE_IMPL_START @@ -190,7 +189,7 @@ int * Sat2_SolverGetModel( satoko_t * p, int * pVars, int nVars ) int i; pModel = ABC_CALLOC( int, nVars+1 ); for ( i = 0; i < nVars; i++ ) - pModel[i] = solver_read_cex_varvalue(p, pVars[i]); + pModel[i] = satoko_read_cex_varvalue(p, pVars[i]); return pModel; } @@ -320,8 +319,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); printf( "Conf =%8.0f. Imp =%11.0f. ", - (double)(pSat ? pSat->stats.conflicts : solver_conflictnum(pSat2)), - (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2).n_propagations) ); + (double)(pSat ? pSat->stats.conflicts : satoko_conflictnum(pSat2)), + (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2)->n_propagations) ); ABC_PRT( "T", Abc_Clock() - clkPart ); clkPart = Abc_Clock(); fflush( stdout ); diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c index 5c2df0d7..f9d65bbb 100644 --- a/src/sat/bmc/bmcBmc2.c +++ b/src/sat/bmc/bmcBmc2.c @@ -21,7 +21,6 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #include "proof/ssw/ssw.h" #include "bmc.h" @@ -690,7 +689,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) iVarNum = Saig_BmcSatNum( p, pObjFrm ); if ( iVarNum == 0 ) continue; - if ( p->pSat2 ? solver_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) ) + if ( p->pSat2 ? satoko_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) ) Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i ); } } @@ -729,7 +728,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) { if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart ) continue; - if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll ) + if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll ) return l_Undef; VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); @@ -838,7 +837,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( nTimeOut ) { if ( p->pSat2 ) - solver_set_runtime_limit( p->pSat2, nTimeToStop ); + satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -867,7 +866,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ", Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, - p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2) ); + p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) ); printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) ); printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); printf( "\n" ); @@ -922,7 +921,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { if ( p->iFrameLast >= p->nFramesMax ) printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll ) + else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll ) printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); else if ( nTimeOut && Abc_Clock() > nTimeToStop ) printf( "Reached timeout (%d seconds).\n", nTimeOut ); diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 26c93b72..f990a982 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -22,7 +22,6 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #include "misc/vec/vecHsh.h" #include "misc/vec/vecWec.h" #include "bmc.h" @@ -798,9 +797,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) p->pSat ? p->pSat->nLearntDelta : 0, p->pSat ? p->pSat->nLearntRatio : 0, p->pSat ? p->pSat->nDBreduces : 0, - p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2), + p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2), nUsedVars, - 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2)) ); + 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2)) ); Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n", p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps ); } @@ -1382,7 +1381,7 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) int iLit = Saig_ManBmcLiteral( p, pObjPi, j ); if ( p->pSat2 ) { - if ( iLit != ~0 && solver_read_cex_varvalue(p->pSat2, lit_var(iLit)) ) + if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) ) Abc_InfoSetBit( pCex->pData, iBit + k ); } else @@ -1465,8 +1464,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) } else { - p->pSat2->RunId = p->pPars->RunId; - p->pSat2->pFuncStop = p->pPars->pFuncStop; + satoko_set_runid(p->pSat2, p->pPars->RunId); + satoko_set_stop_func(p->pSat2, p->pPars->pFuncStop); } if ( pPars->fSolveAll && p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); @@ -1483,7 +1482,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) if ( nTimeToStop ) { if ( p->pSat2 ) - solver_set_runtime_limit( p->pSat2, nTimeToStop ); + satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1614,7 +1613,7 @@ clkOther += Abc_Clock() - clk2; assert( p->pTime4Outs[i] > 0 ); clkOne = Abc_Clock(); if ( p->pSat2 ) - solver_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() ); + satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() ); else sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() ); } @@ -1673,8 +1672,8 @@ nTimeSat += clkSatRun; { Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : solver_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); // ABC_PRT( "Time", Abc_Clock() - clk ); @@ -1721,7 +1720,7 @@ nTimeSat += clkSatRun; if ( nTimeToStop ) { if ( p->pSat2 ) - solver_set_runtime_limit( p->pSat2, nTimeToStop ); + satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1738,7 +1737,7 @@ nTimeSat += clkSatRun; Lit = Saig_ManBmcCreateCnf( p, pObj, f ); if ( p->pSat2 ) { - if ( solver_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) + if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) continue; } else @@ -1781,7 +1780,7 @@ nTimeUndec += clkSatRun; } if ( pPars->fVerbose ) { - if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > 1 ) + if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 1 ) { fFirst = 0; // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f ); @@ -1789,8 +1788,8 @@ nTimeUndec += clkSatRun; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : solver_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); if ( pPars->fSolveAll ) diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 1bfcd9d0..ea8ec2f6 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -21,7 +21,6 @@ #include "bmc.h" #include "sat/cnf/cnf.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" //#define ABC_USE_EXT_SOLVERS 1 @@ -41,8 +40,8 @@ #define bmc_sat_solver_addclause satoko_add_clause #define bmc_sat_solver_addvar(s) satoko_add_variable(s, 0) #define bmc_sat_solver_solve satoko_solve_assumptions - #define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue - #define bmc_sat_solver_setstop solver_set_stop + #define bmc_sat_solver_read_cex_varvalue satoko_read_cex_varvalue + #define bmc_sat_solver_setstop satoko_set_stop #endif @@ -546,7 +545,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd ) if ( pNew == NULL ) return NULL; clk = Abc_Clock(); - pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 ); + pCnf = (Cnf_Dat_t *) Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 ); pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) ); pMap[0] = 0; Gia_ManForEachObj1( pNew, pObj, i ) @@ -584,10 +583,10 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim return; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); #ifndef ABC_USE_EXT_SOLVERS - Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) ); - Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) ); - Abc_Print( 1, "Conf =%9.0f. ", (double)solver_conflictnum(p->pSats[0]) ); + Abc_Print( 1, "Var =%8.0f. ", (double)satoko_varnum(p->pSats[0]) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)satoko_clausenum(p->pSats[0]) ); + Abc_Print( 1, "Learn =%9.0f. ",(double)satoko_learntnum(p->pSats[0]) ); + Abc_Print( 1, "Conf =%9.0f. ", (double)satoko_conflictnum(p->pSats[0]) ); #else Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses ); diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c index 6da70a1c..ee27496f 100644 --- a/src/sat/bmc/bmcMesh.c +++ b/src/sat/bmc/bmcMesh.c @@ -20,7 +20,6 @@ #include "bmc.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START @@ -53,9 +52,9 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][ ***********************************************************************/ static inline int Bmc_MeshVarValue( satoko_t * p, int v ) { -// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v); -// return value == LIT_TRUE; - return var_polarity(p, v) == LIT_TRUE; +// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v); +// return value == SATOKO_LIT_TRUE; + return satoko_var_polarity(p, v) == SATOKO_LIT_TRUE; } /**Function************************************************************* @@ -360,7 +359,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose ) } printf( "Satisfying solution found. " ); /* - iVar = solver_varnum(pSat); + iVar = satoko_varnum(pSat); for ( i = 0; i < iVar; i++ ) if ( Bmc_MeshVarValue(pSat, i) ) printf( "%d ", i ); diff --git a/src/sat/bmc/bmcMesh2.c b/src/sat/bmc/bmcMesh2.c index e6662d7c..1553e5bb 100644 --- a/src/sat/bmc/bmcMesh2.c +++ b/src/sat/bmc/bmcMesh2.c @@ -20,7 +20,6 @@ #include "bmc.h" //#include "sat/satoko/satoko.h" -//#include "sat/satoko/solver.h" #include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -56,8 +55,8 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][ ***********************************************************************/ static inline int Bmc_MeshVarValue2( sat_solver * p, int v ) { -// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v); -// return value == LIT_TRUE; +// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v); +// return value == SATOKO_LIT_TRUE; return sat_solver_var_value( p, v ); } @@ -370,7 +369,7 @@ void Bmc_MeshTest2( Gia_Man_t * p, int X, int Y, int T, int fVerbose ) } printf( "Satisfying solution found. " ); /* -// iVar = solver_varnum(pSat); +// iVar = satoko_varnum(pSat); iVar = sat_solver_nvars(pSat); for ( i = 0; i < iVar; i++ ) if ( Bmc_MeshVarValue2(pSat, i) ) -- cgit v1.2.3