diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-26 20:32:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-26 20:32:46 -0700 |
| commit | 036be3a54124fa5bd609e7926c94190581168bc5 (patch) | |
| tree | 32d44cdbd1bc28fa40551c69807f83d972306ed8 /src/sat/cnf | |
| parent | d0ea4853ec8da057f76f7846d895c0207670cb11 (diff) | |
| download | abc-036be3a54124fa5bd609e7926c94190581168bc5.tar.gz abc-036be3a54124fa5bd609e7926c94190581168bc5.tar.bz2 abc-036be3a54124fa5bd609e7926c94190581168bc5.zip | |
Experiments with don't-cares.
Diffstat (limited to 'src/sat/cnf')
| -rw-r--r-- | src/sat/cnf/cnf.h | 3 | ||||
| -rw-r--r-- | src/sat/cnf/cnfMan.c | 32 |
2 files changed, 18 insertions, 17 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index ca08a146..6c6cbeb3 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -156,7 +156,8 @@ extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); -extern void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ); +extern Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar ); +extern void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index a2d74b1c..bf2a5b8a 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -193,7 +193,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) /**Function************************************************************* - Synopsis [Writes CNF into a file.] + Synopsis [] Description [] @@ -215,26 +215,26 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) for ( v = 0; v < p->nLiterals; v++ ) p->pClauses[0][v] += 2*nVarsPlus; } - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ) +Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar ) { - p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] ); + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int v; + assert( p->pMan == NULL ); + for ( v = 0; v < p->nLiterals; v++ ) + if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar ) + Vec_IntPush( vLits, v ); + return vLits; +} +void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits ) +{ + int i, iLit; + assert( p->pMan == NULL ); + Vec_IntForEachEntry( vLits, iLit, i ) + p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2*nVarsPlus; } /**Function************************************************************* - Synopsis [Writes CNF into a file.] + Synopsis [] Description [] |