From 3d01abf481c0115beb5f2aea48ea9007a3e29c39 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Jul 2013 21:01:06 -0700 Subject: Experiment with 'pdr'. --- src/proof/pdr/pdrCnf.c | 146 ++++++++++++++++++++++++++++++++++++++++--------- src/proof/pdr/pdrInt.h | 2 +- src/proof/pdr/pdrSat.c | 12 ++-- src/sat/cnf/cnf.h | 2 + src/sat/cnf/cnfMan.c | 1 + src/sat/cnf/cnfUtil.c | 60 ++++++++++++++++++++ 6 files changed, 189 insertions(+), 34 deletions(-) (limited to 'src') diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index 9d2af1d6..0553af3d 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/src/proof/pdr/pdrCnf.c @@ -67,6 +67,8 @@ static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ +//#define USE_PG +#ifdef USE_PG static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) { Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj); @@ -80,7 +82,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb int iVarNew = Vec_IntSize( vVar2Ids ); assert( iVarNew > 0 ); Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) ); - Vec_IntWriteEntry( vId2Vars, k, iVarNew ); + Vec_IntWriteEntry( vId2Vars, k, iVarNew << 2 ); sat_solver_setnvars( pSat, iVarNew + 1 ); if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output { @@ -93,42 +95,128 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb } return Vec_IntEntry( vId2Vars, k ); } - -/**Function************************************************************* - - Synopsis [Recursively adds CNF for the given object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level ) +int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol ) { Vec_Int_t * vLits; sat_solver * pSat; Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k); int nVarCount = Vec_IntSize(vVar2Ids); int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj ); - int * pLit, i, iVar, nClauses, iFirstClause, RetValue; - if ( nVarCount == Vec_IntSize(vVar2Ids) ) - return iVarThis; - assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) ); + int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue; + int PolPres = (iVarThis & 3); + iVarThis >>= 2; if ( Aig_ObjIsCi(pObj) ) return iVarThis; - nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; - iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; - assert( nClauses > 0 ); +// Pol = 3; +// if ( nVarCount != Vec_IntSize(vVar2Ids) || (Pol & ~PolPres) ) + if ( (Pol & ~PolPres) ) + { + *Vec_IntEntryP( p->pvId2Vars + Aig_ObjId(pObj), k ) |= Pol; + iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; + iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; + assert( iClaBeg < iClaEnd ); +/* + if ( (Pol & ~PolPres) != 3 ) + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + { + printf( "Clause %5d : ", i ); + for ( iVar = 0; iVar < 4; iVar++ ) + printf( "%d ", ((unsigned)p->pCnf2->pClaPols[i] >> (2*iVar)) & 3 ); + printf( " " ); + for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) + printf( "%6d ", *pLit ); + printf( "\n" ); + } +*/ + pSat = Pdr_ManSolver(p, k); + vLits = Vec_WecEntry( p->vVLits, Level ); + if ( (Pol & ~PolPres) == 3 ) + { + assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) ); + for ( i = iClaBeg; i < iClaEnd; i++ ) + { + Vec_IntClear( vLits ); + Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) ); + for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) + { + iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, 3 ); + Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); + } + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + assert( RetValue ); + (void) RetValue; + } + } + else // if ( (Pol & ~PolPres) == 2 || (Pol & ~PolPres) == 1 ) // write pos/neg polarity + { + assert( (Pol & ~PolPres) ); + for ( i = iClaBeg; i < iClaEnd; i++ ) + if ( 2 - !Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) == (Pol & ~PolPres) ) // taking opposite literal + { + Vec_IntClear( vLits ); + Vec_IntPush( vLits, toLitCond( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) ); + for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) + { + iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 ); + Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); + } + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + assert( RetValue ); + (void) RetValue; + } + } + } + return iVarThis; +} + +#else +static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int * pfNewVar ) +{ + Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj); + assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 ); + if ( Vec_IntSize(vId2Vars) == 0 ) + Vec_IntGrow(vId2Vars, 2 * k + 1); + if ( Vec_IntGetEntry(vId2Vars, k) == 0 ) + { + sat_solver * pSat = Pdr_ManSolver(p, k); + Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k); + int iVarNew = Vec_IntSize( vVar2Ids ); + assert( iVarNew > 0 ); + Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) ); + Vec_IntWriteEntry( vId2Vars, k, iVarNew ); + sat_solver_setnvars( pSat, iVarNew + 1 ); + if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output + { + int Lit = toLitCond( iVarNew, 1 ); + int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue == 1 ); + (void) RetValue; + sat_solver_compress( pSat ); + } + *pfNewVar = 1; + } + return Vec_IntEntry( vId2Vars, k ); +} +int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol ) +{ + Vec_Int_t * vLits; + sat_solver * pSat; + int fNewVar = 0, iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj, &fNewVar ); + int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue; + if ( Aig_ObjIsCi(pObj) || !fNewVar ) + return iVarThis; + iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; + iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; + assert( iClaBeg < iClaEnd ); pSat = Pdr_ManSolver(p, k); vLits = Vec_WecEntry( p->vVLits, Level ); - for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + for ( i = iClaBeg; i < iClaEnd; i++ ) { Vec_IntClear( vLits ); - for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) + Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) ); + for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) { - iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1 ); + iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, Pol ); Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); } RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); @@ -137,6 +225,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level ) } return iVarThis; } +#endif /**Function************************************************************* @@ -149,12 +238,12 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level ) SeeAlso [] ***********************************************************************/ -int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) +int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj ) { if ( p->pPars->fMonoCnf ) return Pdr_ObjSatVar1( p, k, pObj ); else - return Pdr_ObjSatVar2( p, k, pObj, 0 ); + return Pdr_ObjSatVar2( p, k, pObj, 0, Pol ); } @@ -277,7 +366,7 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, assert( p->vVar2Reg == NULL ); p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars ); Saig_ManForEachLi( p->pAig, pObj, i ) - Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i ); + Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, 3, pObj), i ); } pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit ); sat_solver_set_runtime_limit( pSat, p->timeToStop ); @@ -303,6 +392,9 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, if ( p->pCnf2 == NULL ) { p->pCnf2 = Cnf_DeriveOtherWithMan( p->pCnfMan, p->pAig, 0 ); +#ifdef USE_PG + p->pCnf2->pClaPols = Cnf_DataDeriveLitPolarities( p->pCnf2 ); +#endif p->pvId2Vars = ABC_CALLOC( Vec_Int_t, Aig_ManObjNumMax(p->pAig) ); Vec_PtrGrow( &p->vVar2Ids, 256 ); } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 9267ef1e..0eb6bd81 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -156,7 +156,7 @@ static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p ) /*=== pdrCex.c ==========================================================*/ extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); /*=== pdrCnf.c ==========================================================*/ -extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ); +extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj ); extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit ); diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 663a0e2f..31c05ce6 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -57,9 +57,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) Vec_VecExpand( p->vClauses, k ); Vec_IntPush( p->vActVars, 0 ); // add property cone -// Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); Saig_ManForEachPo( p->pAig, pObj, i ) - Pdr_ObjSatVar( p, k, pObj ); + Pdr_ObjSatVar( p, k, 1, pObj ); return pSat; } @@ -146,6 +145,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom int i, iVar, iVarMax = 0; abctime clk = Abc_Clock(); Vec_IntClear( p->vLits ); + assert( !(fNext && fCompl) ); for ( i = 0; i < pCube->nLits; i++ ) { if ( pCube->Lits[i] == -1 ) @@ -154,7 +154,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) ); else pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) ); - iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 ); iVarMax = Abc_MaxInt( iVarMax, iVar ); Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) ); } @@ -185,7 +185,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; - Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal + Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); assert( RetValue == 1 ); } @@ -235,7 +235,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t pSat = Pdr_ManSolver(p, k); Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i ) { - iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 ); Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); } } @@ -293,7 +293,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr if ( pCube == NULL ) // solve the property { clk = Abc_Clock(); - Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails) + Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails) Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); sat_solver_set_runtime_limit( pSat, Limit ); diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index e5079a46..ba41ef4e 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -63,6 +63,7 @@ struct Cnf_Dat_t_ int * pVarNums; // the number of CNF variable for each node ID (-1 if unused) int * pObj2Clause; // the mapping of objects into clauses int * pObj2Count; // the mapping of objects into clause number + unsigned char * pClaPols; // polarity of input literals in each clause Vec_Int_t * vMapping; // mapping of internal nodes }; @@ -176,6 +177,7 @@ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ); extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ); extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); +extern unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ); /*=== cnfWrite.c ========================================================*/ extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 2aa5df6f..8a155f78 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -182,6 +182,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) if ( p == NULL ) return; Vec_IntFreeP( &p->vMapping ); + ABC_FREE( p->pClaPols ); ABC_FREE( p->pObj2Clause ); ABC_FREE( p->pObj2Count ); ABC_FREE( p->pClauses[0] ); diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index e3828863..98b494b3 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -229,6 +229,66 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) return vCoIds; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ) +{ + int i, c, iClaBeg, iClaEnd, * pLit; + unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); + unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); + unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses ); + for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ ) + { + if ( p->pObj2Count[i] == 0 ) + continue; + iClaBeg = p->pObj2Clause[i]; + iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i]; + // go through the negative polarity clauses + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + if ( Abc_LitIsCompl(p->pClauses[c][0]) ) + pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + else + pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + // record these clauses + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + if ( Abc_LitIsCompl(p->pClauses[c][0]) ) + pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + else + pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + // clean negative polarity + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0; + } + ABC_FREE( pPols0 ); + ABC_FREE( pPols1 ); +/* +// for ( c = 0; c < p->nClauses; c++ ) + for ( c = 0; c < 100; c++ ) + { + printf( "Clause %6d : ", c ); + for ( i = 0; i < 4; i++ ) + printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 ); + printf( " " ); + for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ ) + printf( "%6d ", *pLit ); + printf( "\n" ); + } +*/ + return pPres; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3