diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 15:33:31 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 15:33:31 -0700 |
| commit | 2427563269566c458f475dfe6fa4388dac80aa02 (patch) | |
| tree | 5a663c7bac47e63b72fcb431ea26d9ab1879e5e7 /src/sat/cnf | |
| parent | 05c8b785318534b960d5b263dac5b6013a1884dd (diff) | |
| download | abc-2427563269566c458f475dfe6fa4388dac80aa02.tar.gz abc-2427563269566c458f475dfe6fa4388dac80aa02.tar.bz2 abc-2427563269566c458f475dfe6fa4388dac80aa02.zip | |
Changes to clause mapping.
Diffstat (limited to 'src/sat/cnf')
| -rw-r--r-- | src/sat/cnf/cnfMan.c | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 10043882..a8c63bf5 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -453,7 +453,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) sat_solver2_setnvars( pSat, p->nVars * nFrames ); for ( i = 0; i < p->nClauses; i++ ) { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -472,14 +472,14 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) { Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 ); Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) { sat_solver2_delete( pSat ); return NULL; } Lits[0]++; Lits[1]--; - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -490,7 +490,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) pLits[i] += nLitsAll; for ( i = 0; i < p->nClauses; i++ ) { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -509,7 +509,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) { Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 1, 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -572,7 +572,7 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) ); Aig_ManForEachCo( pCnf->pMan, pObj, i ) pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) ) + if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan), 0 ) ) { ABC_FREE( pLits ); return 0; |