diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 05:05:22 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 05:05:22 -0700 |
commit | c30a0af71c219dcdd42322c411b805bb674d14b7 (patch) | |
tree | 8f6a5e2b004bfbc95cdbae7b6a2191bad286bdca /src/aig/gia | |
parent | 97751e43b71792ded1947d98945e1e832325be6d (diff) | |
download | abc-c30a0af71c219dcdd42322c411b805bb674d14b7.tar.gz abc-c30a0af71c219dcdd42322c411b805bb674d14b7.tar.bz2 abc-c30a0af71c219dcdd42322c411b805bb674d14b7.zip |
Improvements to QBF solver; new quantification command &qvar.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaQbf.c | 92 |
1 files changed, 80 insertions, 12 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index f00c1d6f..4ca0bac3 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -330,31 +330,58 @@ void Gia_QbfFree( Qbf_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_QbfQuantify( Gia_Man_t * p, int nPars ) +Gia_Man_t * Gia_QbfQuantifyOne( Gia_Man_t * p, int iVar, int fAndAll, int fOrAll ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i, m, nMints = (1 << (Gia_ManPiNum(p) - nPars)); - assert( Gia_ManPoNum(p) == 1 ); + Vec_Int_t * vCofs; + int i, c; pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); + Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; - for ( i = 0; i < nPars; i++ ) - Gia_ManAppendCi(pNew); - for ( m = 0; m < nMints; m++ ) + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // compute cofactors + vCofs = Vec_IntAlloc( 2 * Gia_ManPoNum(p) ); + for ( c = 0; c < 2; c++ ) { - Gia_ManForEachPi( p, pObj, i ) - pObj->Value = (i < nPars) ? Gia_Obj2Lit(pNew, Gia_ManPi(pNew, i)) : ((m >> (i - nPars)) & 1); + Gia_ManPi(p, iVar)->Value = c; Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachCo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + Vec_IntPush( vCofs, Gia_ObjFanin0Copy(pObj) ); + } + if ( fAndAll ) + { + for ( i = 0; i < Gia_ManPoNum(p); i++ ) + Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Vec_IntEntry(vCofs, i), Vec_IntEntry(vCofs, Gia_ManPoNum(p)+i)) ); + } + else if ( fOrAll ) + { + for ( i = 0; i < Gia_ManPoNum(p); i++ ) + Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Vec_IntEntry(vCofs, i), Vec_IntEntry(vCofs, Gia_ManPoNum(p)+i)) ); + } + else + { + Vec_IntForEachEntry( vCofs, c, i ) + Gia_ManAppendCo( pNew, c ); } + Vec_IntFree( vCofs ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); - assert( Gia_ManPiNum(pNew) == nPars ); - assert( Gia_ManPoNum(pNew) == nMints ); + return pNew; +} +Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll ) +{ + Gia_Man_t * pNew, * pTemp; int v; + pNew = Gia_ManDup( p ); + for ( v = Gia_ManPiNum(p) - 1; v >= nPars; v-- ) + { + pNew = Gia_QbfQuantifyOne( pTemp = pNew, v, fAndAll, fOrAll ); + Gia_ManStop( pTemp ); + } return pNew; } @@ -396,6 +423,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ assert( Gia_ManPiNum(pNew) == nPars ); return pNew; } +/* int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); @@ -415,6 +443,46 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) return 0; return 1; } +*/ +void Cnf_SpecialDataLift( Cnf_Dat_t * p, int nVarsPlus, int firstPiVar, int lastPiVar) +{ + int v, var; + for ( v = 0; v < p->nLiterals; v++ ) + { + var = p->pClauses[0][v] / 2; + if (var < firstPiVar || var >= lastPiVar) + p->pClauses[0][v] += 2*nVarsPlus; + else + p->pClauses[0][v] -= 2*firstPiVar; + } +} + +int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) +{ + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + int i, useold = 0; + int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1 + pCnf->pMan = NULL; + + if (useold) + Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); + else + Cnf_SpecialDataLift( pCnf, sat_solver_nvars(p->pSatSyn), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) ); + + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( p->pSatSyn, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + { + Cnf_DataFree( pCnf ); + return 0; + } + Cnf_DataFree( pCnf ); + // add connection clauses + if (useold) + for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ ) + if ( !sat_solver_add_buffer( p->pSatSyn, i, iFirstVar+i, 0 ) ) + return 0; + return 1; +} /**Function************************************************************* |