diff options
Diffstat (limited to 'src/aig/cnf')
| -rw-r--r-- | src/aig/cnf/cnf.h | 2 | ||||
| -rw-r--r-- | src/aig/cnf/cnfMan.c | 64 | ||||
| -rw-r--r-- | src/aig/cnf/cnfWrite.c | 2 |
3 files changed, 64 insertions, 4 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 5c7a594e..77c87f3f 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -134,7 +134,7 @@ extern void Cnf_ManStop( Cnf_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); -void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ); +void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); 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 ) { diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index a46069e6..8c23d859 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -207,6 +207,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // allocate CNF pCnf = ALLOC( Cnf_Dat_t, 1 ); memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->pMan = p->pManAig; pCnf->nLiterals = nLiterals; pCnf->nClauses = nClauses; pCnf->pClauses = ALLOC( int *, nClauses + 1 ); @@ -346,6 +347,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) // allocate CNF pCnf = ALLOC( Cnf_Dat_t, 1 ); memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->pMan = p; pCnf->nLiterals = nLiterals; pCnf->nClauses = nClauses; pCnf->pClauses = ALLOC( int *, nClauses + 1 ); |