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/aig/saig/saigGlaPba2.c | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 5e745f4c..cff7b7fc 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -72,7 +72,7 @@ struct Aig_Gla3Man_t_ static inline int Aig_Gla3AddConst( sat_solver2 * pSat, int iVar, int fCompl ) { lit Lit = toLitCond( iVar, fCompl ); - if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1 ) ) + if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1, 0 ) ) return 0; return 1; } @@ -94,12 +94,12 @@ static inline int Aig_Gla3AddBuffer( sat_solver2 * pSat, int iVar0, int iVar1, i Lits[0] = toLitCond( iVar0, 0 ); Lits[1] = toLitCond( iVar1, !fCompl ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar0, 1 ); Lits[1] = toLitCond( iVar1, fCompl ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; return 1; @@ -122,18 +122,18 @@ static inline int Aig_Gla3AddNode( sat_solver2 * pSat, int iVar, int iVar0, int Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar0, fCompl0 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar1, fCompl1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar, 0 ); Lits[1] = toLitCond( iVar0, !fCompl0 ); Lits[2] = toLitCond( iVar1, !fCompl1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 3 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ) ) return 0; return 1; @@ -302,7 +302,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p ) vPoLits = Vec_IntAlloc( p->nFramesMax ); for ( f = p->nStart; f < p->nFramesMax; f++ ) Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManCo(p->pAig, 0), f) ); - sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); + sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits), 0 ); Vec_IntFree( vPoLits ); Vec_IntPush( p->vCla2Obj, 0 ); Vec_IntPush( p->vCla2Fra, 0 ); -- cgit v1.2.3