diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/giaDup.c | 33 | ||||
-rw-r--r-- | src/aig/gia/giaMf.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaQbf.c | 6 |
3 files changed, 38 insertions, 5 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 029d1599..81362276 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -426,6 +426,39 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + { + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ) { Gia_Man_t * pNew; diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 03848f1e..b90e7bc9 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -346,9 +346,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachAndReverseId( p->pGia, Id ) if ( Mf_ObjMapRefNum(p, Id) ) Vec_IntWriteEntry( vCnfIds, Id, Id ), iVar++; + Vec_IntWriteEntry( vCnfIds, 0, 0 ); Gia_ManForEachCiId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, Id ); - Vec_IntWriteEntry( vCnfIds, 0, 0 ); assert( iVar == nVars ); } else @@ -358,9 +358,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachAndReverseId( p->pGia, Id ) if ( Mf_ObjMapRefNum(p, Id) ) Vec_IntWriteEntry( vCnfIds, Id, iVar++ ); + Vec_IntWriteEntry( vCnfIds, 0, iVar++ ); Gia_ManForEachCiId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, iVar++ ); - Vec_IntWriteEntry( vCnfIds, 0, iVar++ ); assert( iVar == nVars ); } // generate CNF diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index a14ec443..b7d678b3 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -75,7 +75,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose abctime clkStart = Abc_Clock(); pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; Cnf_DataFree( pCnf ); // iterate through the SAT assignment vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) ); @@ -180,7 +180,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) p->nPars = nPars; p->nVars = Gia_ManPiNum(pGia) - nPars; p->fVerbose = fVerbose; - p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + 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) ); @@ -280,7 +280,7 @@ 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, 1, 0 ); - int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1; + 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++ ) |