diff options
| -rw-r--r-- | src/aig/gia/giaQbf.c | 35 |
1 files changed, 25 insertions, 10 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 33216ce3..dd040548 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -43,7 +43,9 @@ struct Qbf_Man_t_ sat_solver * pSatSyn; // synthesis instance Vec_Int_t * vValues; // variable values Vec_Int_t * vParMap; // parameter mapping + Vec_Int_t * vLits; // literals for the SAT solver abctime clkStart; // global timeout + abctime clkSat; // SAT solver time }; extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); @@ -67,7 +69,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) { // original problem: \exists p \forall x \exists y. M(p,x,y) // negated problem: \forall p \exists x \exists y. !M(p,x,y) - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); Vec_Int_t * vVarMap, * vForAlls, * vExists; Gia_Obj_t * pObj; char * pFileName; @@ -108,18 +110,23 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) ***********************************************************************/ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 ); - Qbf_Man_t * p = ABC_CALLOC( Qbf_Man_t, 1 ); + Qbf_Man_t * p; + Cnf_Dat_t * pCnf; + Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); + pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); + p = ABC_CALLOC( Qbf_Man_t, 1 ); p->clkStart = Abc_Clock(); p->pGia = pGia; p->nPars = nPars; p->nVars = Gia_ManPiNum(pGia) - nPars; p->fVerbose = fVerbose; - p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 2; + p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->pSatSyn = sat_solver_new(); p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) ); p->vParMap = Vec_IntStartFull( nPars ); + p->vLits = Vec_IntAlloc( nPars ); sat_solver_setnvars( p->pSatSyn, nPars ); Cnf_DataFree( pCnf ); return p; @@ -128,6 +135,7 @@ void Gia_QbfFree( Qbf_Man_t * p ) { sat_solver_delete( p->pSatVer ); sat_solver_delete( p->pSatSyn ); + Vec_IntFree( p->vLits ); Vec_IntFree( p->vValues ); Vec_IntFree( p->vParMap ); ABC_FREE( p ); @@ -166,8 +174,8 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ } int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 0, 0 ); - int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 2; + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1; pCnf->pMan = NULL; Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); for ( i = 0; i < pCnf->nClauses; i++ ) @@ -198,7 +206,7 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues ) { int i; - Vec_IntClear( vValues ); + Vec_IntClear( p->vValues ); for ( i = 0; i < p->nPars; i++ ) Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) ); } @@ -228,9 +236,10 @@ int Gia_QbfVerify( Qbf_Man_t * p, Vec_Int_t * vValues ) { int i, Entry, RetValue; assert( Vec_IntSize(vValues) == p->nPars ); + Vec_IntClear( p->vLits ); Vec_IntForEachEntry( vValues, Entry, i ) - Vec_IntWriteEntry( vValues, i, Abc_Var2Lit(p->iParVarBeg+i, !Entry) ); - RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(vValues), Vec_IntLimit(vValues), 0, 0, 0, 0 ); + Vec_IntPush( p->vLits, Abc_Var2Lit(p->iParVarBeg+i, !Entry) ); + RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 ); if ( RetValue == l_True ) { Vec_IntClear( vValues ); @@ -256,6 +265,7 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose ); Gia_Man_t * pCof; int i, status, RetValue = 0; + abctime clk; assert( Gia_ManRegNum(pGia) == 0 ); Vec_IntFill( p->vValues, nPars, 0 ); for ( i = 0; Gia_QbfVerify(p, p->vValues) && (!nIterLimit || i < nIterLimit); i++ ) @@ -267,7 +277,9 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i Gia_ManStop( pCof ); if ( status == 0 ) { RetValue = 1; break; } // synthesize next assignment + clk = Abc_Clock(); status = sat_solver_solve( p->pSatSyn, NULL, NULL, nConfLimit, 0, 0, 0 ); + p->clkSat += Abc_Clock() - clk; if ( fVerbose ) Gia_QbfPrint( p, p->vValues, i ); if ( status == l_Undef ) { RetValue = -1; break; } @@ -284,7 +296,10 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i printf( "The problem is UNSAT. " ); else printf( "The problem is SAT. " ); - Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + printf( "\n" ); + Abc_PrintTime( 1, "SAT ", p->clkSat ); + Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat ); + Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart ); if ( RetValue == 0 ) { assert( Vec_IntSize(p->vValues) == nPars ); |