diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
commit | 65687f72ae77440628c21d63966656c1049c4981 (patch) | |
tree | 27a4c7800e372349f1521daac76c0b30e2578ca1 /src/aig/cnf/cnfMan.c | |
parent | 369f008e69a4f201cbc7c890a08221086bee4698 (diff) | |
download | abc-65687f72ae77440628c21d63966656c1049c4981.tar.gz abc-65687f72ae77440628c21d63966656c1049c4981.tar.bz2 abc-65687f72ae77440628c21d63966656c1049c4981.zip |
Version abc71208
Diffstat (limited to 'src/aig/cnf/cnfMan.c')
-rw-r--r-- | src/aig/cnf/cnfMan.c | 64 |
1 files changed, 61 insertions, 3 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 1edc012a..4ac06b48 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -172,12 +172,13 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) SeeAlso [] ***********************************************************************/ -void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) +void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) { sat_solver * pSat; - int i, status; + int i, f, status; + assert( nFrames > 0 ); pSat = sat_solver_new(); - sat_solver_setnvars( pSat, p->nVars ); + sat_solver_setnvars( pSat, p->nVars * nFrames ); for ( i = 0; i < p->nClauses; i++ ) { if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) @@ -186,6 +187,63 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) return NULL; } } + if ( nFrames > 1 ) + { + Aig_Obj_t * pObjLo, * pObjLi; + int nLitsAll, * pLits, Lits[2]; + nLitsAll = 2 * p->nVars; + pLits = p->pClauses[0]; + for ( f = 1; f < nFrames; f++ ) + { + // add equality of register inputs/outputs for different timeframes + Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i ) + { + Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 ); + Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + Lits[0]++; + Lits[1]--; + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + // add clauses for the next timeframe + for ( i = 0; i < p->nLiterals; i++ ) + pLits[i] += nLitsAll; + for ( i = 0; i < p->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + } + // return literals to their original state + nLitsAll = (f-1) * nLitsAll; + for ( i = 0; i < p->nLiterals; i++ ) + pLits[i] -= nLitsAll; + } + if ( fInit ) + { + Aig_Obj_t * pObjLo; + int Lits[1]; + Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) + { + Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + } status = sat_solver_simplify(pSat); if ( status == 0 ) { |