summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cnf')
-rw-r--r--src/aig/cnf/cnf.h2
-rw-r--r--src/aig/cnf/cnfMan.c64
-rw-r--r--src/aig/cnf/cnfWrite.c2
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 );