diff options
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 [] |