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/cnf.h | |
| 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/cnf.h')
| -rw-r--r-- | src/sat/cnf/cnf.h | 3 |
1 files changed, 2 insertions, 1 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 ); |