diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-10 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-10 08:01:00 -0700 |
| commit | 9d09f583b6ea1181ebd5af1654acd3432c427445 (patch) | |
| tree | 2ea6fb1cc6f70871f861dd0ccbe7f8522c34c765 /src/aig/cnf | |
| parent | 9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff (diff) | |
| download | abc-9d09f583b6ea1181ebd5af1654acd3432c427445.tar.gz abc-9d09f583b6ea1181ebd5af1654acd3432c427445.tar.bz2 abc-9d09f583b6ea1181ebd5af1654acd3432c427445.zip | |
Version abc80610
Diffstat (limited to 'src/aig/cnf')
| -rw-r--r-- | src/aig/cnf/cnf.h | 2 | ||||
| -rw-r--r-- | src/aig/cnf/cnfMan.c | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index e664b1bc..bf109b17 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -139,7 +139,7 @@ extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); -extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); +extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); /*=== 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 b6ed3da0..fc71f936 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -362,7 +362,7 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) +int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) { sat_solver * pSat = p; Aig_Obj_t * pObj; @@ -371,8 +371,12 @@ void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) Aig_ManForEachPo( pCnf->pMan, pObj, i ) pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) ) - assert( 0 ); + { + free( pLits ); + return 0; + } free( pLits ); + return 1; } //////////////////////////////////////////////////////////////////////// |