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/aig/gia/giaSatoko.c | 3 +- src/aig/gia/giaSupp.c | 7 ++-- src/proof/cec/cecSat.c | 18 +++++----- src/proof/pdr/pdrInt.h | 7 ++-- 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 ++-- src/sat/satoko/satoko.h | 21 ++++++++++- src/sat/satoko/solver.c | 34 +++++++++--------- src/sat/satoko/solver.h | 47 +++--------------------- src/sat/satoko/solver_api.c | 88 ++++++++++++++++++++++++++++++++++++--------- 14 files changed, 166 insertions(+), 137 deletions(-) diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index 5e04502d..aaf9daaa 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.c @@ -21,7 +21,6 @@ #include "gia.h" #include "sat/cnf/cnf.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START @@ -133,7 +132,7 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) if ( pSat ) { status = satoko_solve( pSat ); - Cost = (unsigned)pSat->stats.n_conflicts; + Cost = satoko_stats(pSat)->n_conflicts; satoko_destroy( pSat ); } else diff --git a/src/aig/gia/giaSupp.c b/src/aig/gia/giaSupp.c index 589084f9..272c94c6 100644 --- a/src/aig/gia/giaSupp.c +++ b/src/aig/gia/giaSupp.c @@ -20,7 +20,6 @@ #include "gia.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -389,7 +388,7 @@ Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ) p->vFanins = Vec_PtrAlloc( 100 ); p->vSatVars = Vec_IntAlloc( 100 ); p->iPattern = 1; - p->pSat->opts.learnt_ratio = 0; // prevent garbage collection + satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection return p; } void Gia_Man2SuppStop( Gia_Man2Min_t * p ) @@ -725,7 +724,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p ) // assert( iTemp == -1 ); Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 ); Vec_IntClear( p->vSatVars ); - assert( solver_varnum(p->pSat) == 0 ); + assert( satoko_varnum(p->pSat) == 0 ); iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 ); iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 ); satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) ); @@ -739,7 +738,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p ) assert( Gia_Min2ManSimulate(p) == 1 ); for ( n = 0; n < 2; n++ ) Vec_IntForEachEntry( p->vCis[n], iTemp, i ) - Gia_Min2SimSetInputBit( p, iTemp, var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == LIT_TRUE, p->iPattern ); + Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern ); //assert( Gia_Min2ManSimulate(p) == 0 ); p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1; p->nSatSat++; diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index c32ed7f9..aa9d8f10 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -21,7 +21,6 @@ #include "aig/gia/gia.h" #include "misc/util/utilTruth.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #include "cec.h" ABC_NAMESPACE_IMPL_START @@ -660,6 +659,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) { Cec2_Man_t * p; Gia_Obj_t * pObj; int i; + satoko_opts_t Pars; //assert( Gia_ManRegNum(pAig) == 0 ); p = ABC_CALLOC( Cec2_Man_t, 1 ); memset( p, 0, sizeof(Cec2_Man_t) ); @@ -675,6 +675,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) Gia_ManHashAlloc( p->pNew ); Vec_IntFill( &p->pNew->vCopies, Gia_ManObjNum(p->pNew), -1 ); // SAT solving + memset( &Pars, 0, sizeof(satoko_opts_t) ); p->pSat = satoko_create(); p->vFrontier = Vec_PtrAlloc( 1000 ); p->vFanins = Vec_PtrAlloc( 100 ); @@ -682,7 +683,8 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) p->vSatVars = Vec_IntAlloc( 100 ); p->vObjSatPairs = Vec_IntAlloc( 100 ); p->vCexTriples = Vec_IntAlloc( 100 ); - p->pSat->opts.conf_limit = pPars->nConfLimit; + Pars.conf_limit = pPars->nConfLimit; + satoko_configure(p->pSat, &Pars); // remember pointer to the solver in the AIG manager pAig->pData = p->pSat; return p; @@ -742,7 +744,7 @@ int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat ) return pObj->fMark1; Gia_ObjSetTravIdCurrentId(p, iObj); if ( Gia_ObjIsCi(pObj) ) - return pObj->fMark1 = var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == LIT_TRUE; + return pObj->fMark1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == SATOKO_LIT_TRUE; assert( Gia_ObjIsAnd(pObj) ); Value0 = Cec2_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj); Value1 = Cec2_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj); @@ -750,8 +752,8 @@ int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat ) } void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat ) { -// int val0 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == LIT_TRUE; -// int val1 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == LIT_TRUE; +// int val0 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == SATOKO_LIT_TRUE; +// int val1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == SATOKO_LIT_TRUE; int Value0, Value1; Gia_ManIncrementTravId( p ); Value0 = Cec2_ManVerify_rec( p, iObj0, pSat ); @@ -805,7 +807,7 @@ int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase ) if (iObj1 < iObj0) iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0; assert( iObj0 < iObj1 ); - assert( p->pPars->fUseCones || solver_varnum(p->pSat) == 0 ); + assert( p->pPars->fUseCones || satoko_varnum(p->pSat) == 0 ); if ( !iObj0 && Cec2_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 ) Cec2_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), satoko_add_variable(p->pSat, 0) ); iVar0 = Cec2_ObjGetCnfVar( p, iObj0 ); @@ -859,7 +861,7 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj ) p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1; assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords ); Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i ) - Cec2_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE ); + Cec2_ObjSimSetInputBit( p->pAig, IdAig, satoko_var_polarity(p->pSat, IdSat) == SATOKO_LIT_TRUE ); p->timeSatSat += Abc_Clock() - clk; RetValue = 0; } @@ -884,7 +886,7 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj ) clk = Abc_Clock(); satoko_rollback( p->pSat ); p->timeExtra += Abc_Clock() - clk; - p->pSat->stats.n_conflicts = 0; + satoko_stats(p->pSat)->n_conflicts = 0; return RetValue; } void Cec2_ManPrintStats( Gia_Man_t * p, Cec2_Par_t * pPars, Cec2_Man_t * pMan ) diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 639276db..ea6b24af 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -38,7 +38,6 @@ #include "sat/bsat/satSolver.h" #else #include "sat/satoko/satoko.h" - #include "sat/satoko/solver.h" #define l_Undef 0 #define l_True 1 #define l_False -1 @@ -47,13 +46,13 @@ #define sat_solver_delete satoko_destroy #define zsat_solver_new_seed(s) satoko_create() #define zsat_solver_restart_seed(s,a) satoko_reset(s) - #define sat_solver_nvars solver_varnum + #define sat_solver_nvars satoko_varnum #define sat_solver_setnvars satoko_setnvars #define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b) #define sat_solver_final satoko_final_conflict #define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c) - #define sat_solver_var_value solver_read_cex_varvalue - #define sat_solver_set_runtime_limit solver_set_runtime_limit + #define sat_solver_var_value satoko_read_cex_varvalue + #define sat_solver_set_runtime_limit satoko_set_runtime_limit #define sat_solver_compress(s) #endif 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) ) diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 537cc394..5c0de7ad 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -25,6 +25,12 @@ enum { SATOKO_UNSAT = -1 }; +enum { + SATOKO_LIT_FALSE = 1, + SATOKO_LIT_TRUE = 0, + SATOKO_VAR_UNASSING = 3 +}; + struct solver_t_; typedef struct solver_t_ satoko_t; @@ -120,7 +126,20 @@ extern int satoko_final_conflict(satoko_t *, int **); * file will not be a DIMACS. (value 1 will use 0 as ID). */ extern void satoko_write_dimacs(satoko_t *, char *, int, int); -extern satoko_stats_t satoko_stats(satoko_t *); +extern satoko_stats_t * satoko_stats(satoko_t *); +extern satoko_opts_t * satoko_options(satoko_t *); + +extern int satoko_varnum(satoko_t *); +extern int satoko_clausenum(satoko_t *); +extern int satoko_learntnum(satoko_t *); +extern int satoko_conflictnum(satoko_t *); +extern void satoko_set_stop(satoko_t *, int *); +extern void satoko_set_stop_func(satoko_t *s, int (*fnct)(int)); +extern void satoko_set_runid(satoko_t *, int); +extern int satoko_read_cex_varvalue(satoko_t *, int); +extern abctime satoko_set_runtime_limit(satoko_t *, abctime); +extern char satoko_var_polarity(satoko_t *, unsigned); + ABC_NAMESPACE_HEADER_END #endif /* satoko__satoko_h */ diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index b35574ab..9f5d3424 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -43,8 +43,8 @@ static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level unsigned *lits = &(c->data[0].lit); assert(var_reason(s, var) != UNDEF); - if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { - assert(lit_value(s, lits[1]) == LIT_TRUE); + if (c->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { + assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); stk_swap(unsigned, lits[0], lits[1]); } @@ -117,7 +117,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits) watch_list_foreach_bin(s->watches, w, neg_lit) { unsigned imp_lit = w->blocker; if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp && - lit_value(s, imp_lit) == LIT_TRUE) { + lit_value(s, imp_lit) == SATOKO_LIT_TRUE) { counter++; vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1)); } @@ -186,7 +186,7 @@ static inline unsigned solver_decide(solver_t *s) { unsigned next_var = UNDEF; - while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) { + while (next_var == UNDEF || var_value(s, next_var) != SATOKO_VAR_UNASSING) { if (heap_size(s->var_order) == 0) { next_var = UNDEF; return UNDEF; @@ -195,14 +195,14 @@ static inline unsigned solver_decide(solver_t *s) if (solver_has_marks(s) && !var_mark(s, next_var)) next_var = UNDEF; } - return var2lit(next_var, var_polarity(s, next_var)); + return var2lit(next_var, satoko_var_polarity(s, next_var)); } static inline void solver_new_decision(solver_t *s, unsigned lit) { if (solver_has_marks(s) && !var_mark(s, lit2var(lit))) return; - assert(var_value(s, lit2var(lit)) == VAR_UNASSING); + assert(var_value(s, lit2var(lit)) == SATOKO_VAR_UNASSING); vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); solver_enqueue(s, lit, UNDEF); } @@ -270,8 +270,8 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt clause = clause_fetch(s, cref); lits = &(clause->data[0].lit); - if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { - assert(lit_value(s, lits[1]) == LIT_TRUE); + if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { + assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); stk_swap(unsigned, lits[0], lits[1] ); } @@ -522,7 +522,7 @@ void solver_cancel_until(solver_t *s, unsigned level) unsigned var = lit2var(vec_uint_at(s->trail, i)); vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var)); - vec_char_assign(s->assigns, var, VAR_UNASSING); + vec_char_assign(s->assigns, var, SATOKO_VAR_UNASSING); vec_uint_assign(s->reasons, var, UNDEF); if (!heap_in_heap(s->var_order, var)) heap_insert(s->var_order, var); @@ -550,9 +550,9 @@ unsigned solver_propagate(solver_t *s) watch_list_foreach_bin(s->watches, i, p) { if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) continue; - if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING) + if (var_value(s, lit2var(i->blocker)) == SATOKO_VAR_UNASSING) solver_enqueue(s, i->blocker, i->cref); - else if (lit_value(s, i->blocker) == LIT_FALSE) + else if (lit_value(s, i->blocker) == SATOKO_LIT_FALSE) return i->cref; } @@ -567,7 +567,7 @@ unsigned solver_propagate(solver_t *s) *j++ = *i++; continue; } - if (lit_value(s, i->blocker) == LIT_TRUE) { + if (lit_value(s, i->blocker) == SATOKO_LIT_TRUE) { *j++ = *i++; continue; } @@ -585,13 +585,13 @@ unsigned solver_propagate(solver_t *s) w.blocker = lits[0]; /* If 0th watch is true, then clause is already satisfied. */ - if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE) + if (lits[0] != i->blocker && lit_value(s, lits[0]) == SATOKO_LIT_TRUE) *j++ = w; else { /* Look for new watch */ unsigned k; for (k = 2; k < clause->size; k++) { - if (lit_value(s, lits[k]) != LIT_FALSE) { + if (lit_value(s, lits[k]) != SATOKO_LIT_FALSE) { lits[1] = lits[k]; lits[k] = neg_lit; watch_list_push(vec_wl_at(s->watches, lit_compl(lits[1])), w, 0); @@ -602,7 +602,7 @@ unsigned solver_propagate(solver_t *s) *j++ = w; /* Clause becomes unit under this assignment */ - if (lit_value(s, lits[0]) == LIT_FALSE) { + if (lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { conf_cref = i->cref; s->i_qhead = vec_uint_size(s->trail); i++; @@ -665,9 +665,9 @@ char solver_search(solver_t *s) next_lit = UNDEF; while (solver_dlevel(s) < vec_uint_size(s->assumptions)) { unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s)); - if (lit_value(s, lit) == LIT_TRUE) { + if (lit_value(s, lit) == SATOKO_LIT_TRUE) { vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); - } else if (lit_value(s, lit) == LIT_FALSE) { + } else if (lit_value(s, lit) == SATOKO_LIT_FALSE) { solver_analyze_final(s, lit_compl(lit)); return SATOKO_UNSAT; } else { diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index ee7b84e2..1a20632f 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -30,11 +30,7 @@ #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -enum { - LIT_FALSE = 1, - LIT_TRUE = 0, - VAR_UNASSING = 3 -}; + #define UNDEF 0xFFFFFFFF @@ -145,11 +141,6 @@ static inline char var_value(solver_t *s, unsigned var) return vec_char_at(s->assigns, var); } -static inline char var_polarity(solver_t *s, unsigned var) -{ - return vec_char_at(s->polarity, var); -} - static inline unsigned var_dlevel(solver_t *s, unsigned var) { return vec_uint_at(s->levels, var); @@ -226,45 +217,15 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason) return SATOKO_OK; } -static inline int solver_varnum(solver_t *s) -{ - return vec_char_size(s->assigns); -} -static inline int solver_clausenum(solver_t *s) -{ - return vec_uint_size(s->originals); -} -static inline int solver_learntnum(solver_t *s) -{ - return vec_uint_size(s->learnts); -} -static inline int solver_conflictnum(solver_t *s) -{ - return satoko_stats(s).n_conflicts; -} - -static inline int solver_has_marks(solver_t *s) +static inline int solver_has_marks(satoko_t *s) { return (int)(s->marks != NULL); } -static inline int solver_stop(solver_t *s) + +static inline int solver_stop(satoko_t *s) { return s->pstop && *s->pstop; } -static inline void solver_set_stop(solver_t *s, int * pstop) -{ - s->pstop = pstop; -} -static inline int solver_read_cex_varvalue(solver_t *s, int ivar) -{ - return var_polarity(s, ivar) == LIT_TRUE; -} -static abctime solver_set_runtime_limit(solver_t* s, abctime Limit) -{ - abctime nRuntimeLimit = s->nRuntimeLimit; - s->nRuntimeLimit = Limit; - return nRuntimeLimit; -} //===------------------------------------------------------------------------=== // Inline clause functions diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 0d073ec7..837d64e7 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -27,7 +27,7 @@ static inline void solver_rebuild_order(solver_t *s) vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns)); for (var = 0; var < vec_char_size(s->assigns); var++) - if (var_value(s, var) == VAR_UNASSING) + if (var_value(s, var) == SATOKO_VAR_UNASSING) vec_uint_push_back(vars, var); heap_build(s->var_order, vars); vec_uint_free(vars); @@ -38,7 +38,7 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause) unsigned i; unsigned *lits = &(clause->data[0].lit); for (i = 0; i < clause->size; i++) - if (lit_value(s, lits[i]) == LIT_TRUE) + if (lit_value(s, lits[i]) == SATOKO_LIT_TRUE) return SATOKO_OK; return SATOKO_ERR; } @@ -226,7 +226,7 @@ int satoko_simplify(solver_t * s) void satoko_setnvars(solver_t *s, int nvars) { int i; - for (i = solver_varnum(s); i < nvars; i++) + for (i = satoko_varnum(s); i < nvars; i++) satoko_add_variable(s, 0); } @@ -237,7 +237,7 @@ int satoko_add_variable(solver_t *s, char sign) vec_wl_push(s->watches); vec_act_push_back(s->activity, 0); vec_uint_push_back(s->levels, 0); - vec_char_push_back(s->assigns, VAR_UNASSING); + vec_char_push_back(s->assigns, SATOKO_VAR_UNASSING); vec_char_push_back(s->polarity, sign); vec_uint_push_back(s->reasons, UNDEF); vec_uint_push_back(s->stamps, 0); @@ -258,15 +258,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size) qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare); max_var = lit2var(lits[size - 1]); while (max_var >= vec_act_size(s->activity)) - satoko_add_variable(s, LIT_FALSE); + satoko_add_variable(s, SATOKO_LIT_FALSE); vec_uint_clear(s->temp_lits); j = 0; prev_lit = UNDEF; for (i = 0; i < (unsigned)size; i++) { - if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE) + if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE) return SATOKO_OK; - else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) { + else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == SATOKO_VAR_UNASSING) { prev_lit = lits[i]; vec_uint_push_back(s->temp_lits, lits[i]); } @@ -287,7 +287,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size) void satoko_assump_push(solver_t *s, int lit) { - assert(lit2var(lit) < solver_varnum(s)); + assert(lit2var(lit) < satoko_varnum(s)); // printf("[Satoko] Push assumption: %d\n", lit); vec_uint_push_back(s->assumptions, lit); } @@ -337,8 +337,8 @@ int satoko_solve_assumptions(solver_t *s, int * plits, int nlits) { int i, status; // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions)); - // printf("[Satoko] + Variables: %d\n", solver_varnum(s)); - // printf("[Satoko] + Clauses: %d\n", solver_clausenum(s)); + // printf("[Satoko] + Variables: %d\n", satoko_varnum(s)); + // printf("[Satoko] + Clauses: %d\n", satoko_clausenum(s)); // printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail)); // printf("[Satoko] + Queue head: %d\n", s->i_qhead); // solver_debug_check_trail(s); @@ -365,9 +365,14 @@ int satoko_final_conflict(solver_t *s, int **out) return vec_uint_size(s->final_conflict); } -satoko_stats_t satoko_stats(satoko_t *s) +satoko_stats_t * satoko_stats(satoko_t *s) { - return s->stats; + return &s->stats; +} + +satoko_opts_t * satoko_options(satoko_t *s) +{ + return &s->opts; } void satoko_bookmark(satoko_t *s) @@ -493,7 +498,7 @@ void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars) { int i; if (!solver_has_marks(s)) - s->marks = vec_char_init(solver_varnum(s), 0); + s->marks = vec_char_init(satoko_varnum(s), 0); for (i = 0; i < n_vars; i++) { var_set_mark(s, pvars[i]); vec_sdbl_assign(s->activity, pvars[i], 0); @@ -532,11 +537,11 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) } fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig); for (i = 0; i < vec_char_size(s->assigns); i++) { - if ( var_value(s, i) != VAR_UNASSING ) { + if ( var_value(s, i) != SATOKO_VAR_UNASSING ) { if (zero_var) - fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i) : i); + fprintf(file, "%d\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i) : i); else - fprintf(file, "%d 0\n", var_value(s, i) == LIT_FALSE ? -(int)(i + 1) : i + 1); + fprintf(file, "%d 0\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i + 1) : i + 1); } } array = vec_uint_data(s->originals); @@ -552,5 +557,56 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) } +int satoko_varnum(satoko_t *s) +{ + return vec_char_size(s->assigns); +} + +int satoko_clausenum(satoko_t *s) +{ + return vec_uint_size(s->originals); +} + +int satoko_learntnum(satoko_t *s) +{ + return vec_uint_size(s->learnts); +} + +int satoko_conflictnum(satoko_t *s) +{ + return satoko_stats(s)->n_conflicts; +} + +void satoko_set_stop(satoko_t *s, int * pstop) +{ + s->pstop = pstop; +} + +void satoko_set_stop_func(satoko_t *s, int (*fnct)(int)) +{ + s->pFuncStop = fnct; +} + +void satoko_set_runid(satoko_t *s, int id) +{ + s->RunId = id; +} + +int satoko_read_cex_varvalue(satoko_t *s, int ivar) +{ + return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE; +} + +abctime satoko_set_runtime_limit(satoko_t* s, abctime Limit) +{ + abctime nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} + +char satoko_var_polarity(satoko_t *s, unsigned var) +{ + return vec_char_at(s->polarity, var); +} ABC_NAMESPACE_IMPL_END -- cgit v1.2.3