From 2427563269566c458f475dfe6fa4388dac80aa02 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Jul 2012 15:33:31 -0700 Subject: Changes to clause mapping. --- src/sat/cnf/cnfMan.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/sat/cnf') 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; -- cgit v1.2.3