From d74b33eba6fe84794ee11abb011728d0f754cc40 Mon Sep 17 00:00:00 2001 From: Advay Singh Date: Thu, 23 Apr 2026 13:09:26 -0500 Subject: [PATCH] Added fix for write_cnf adding extra clauses on direct PI-PO --- src/sat/cnf/cnfMan.c | 734 +++++++++++++++++++------------------ test/write_cnf_dangling.sh | 60 +++ 2 files changed, 445 insertions(+), 349 deletions(-) create mode 100755 test/write_cnf_dangling.sh diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 16a4cf219..cfcc437f1 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -9,7 +9,7 @@ Synopsis [] Author [Alan Mishchenko] - + Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] @@ -25,13 +25,47 @@ ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; } -static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) : (Lit >> 1); } +static inline int Cnf_Lit2Var(int Lit) { return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1; } +static inline int Cnf_Lit2Var2(int Lit) { return (Lit & 1) ? -(Lit >> 1) : (Lit >> 1); } + +// Emits unit clauses for DIMACS variables that are declared in the header +// but never referenced in any clause. After strash, a primary input that +// is wired directly to a primary output has no fanout into any AND node, +// so the Tseitin encoder leaves the corresponding DIMACS variable without +// any connecting clause. Such a dangling variable silently doubles the +// model count of the output formula, breaking #SAT and uniform sampling. +// Forcing each unreferenced declared variable to a fixed polarity restores +// the original number of satisfying assignments without affecting the set +// of assignments over live variables. Pass pFile == NULL to only count. +static int Cnf_DataWriteDanglingUnitClauses(FILE *pFile, Cnf_Dat_t *p) +{ + char *pUsed; + int *pLit, *pStop; + int i, v, iVar, nExtra = 0; + if (p->nVars <= 0) + return 0; + pUsed = ABC_CALLOC(char, p->nVars + 1); + for (i = 0; i < p->nClauses; i++) + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + { + iVar = (*pLit >> 1) + 1; + if (iVar >= 1 && iVar <= p->nVars) + pUsed[iVar] = 1; + } + for (v = 1; v <= p->nVars; v++) + if (!pUsed[v]) + { + if (pFile) + fprintf(pFile, "-%d 0\n", v); + nExtra++; + } + ABC_FREE(pUsed); + return nExtra; +} //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -42,29 +76,29 @@ static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) Synopsis [Starts the fraiging manager.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Cnf_Man_t * Cnf_ManStart() +Cnf_Man_t *Cnf_ManStart() { - Cnf_Man_t * p; + Cnf_Man_t *p; int i; // allocate the manager - p = ABC_ALLOC( Cnf_Man_t, 1 ); - memset( p, 0, sizeof(Cnf_Man_t) ); + p = ABC_ALLOC(Cnf_Man_t, 1); + memset(p, 0, sizeof(Cnf_Man_t)); // derive internal data structures - Cnf_ReadMsops( &p->pSopSizes, &p->pSops ); + Cnf_ReadMsops(&p->pSopSizes, &p->pSops); // allocate memory manager for cuts p->pMemCuts = Aig_MmFlexStart(); p->nMergeLimit = 10; // allocate temporary truth tables - p->pTruths[0] = ABC_ALLOC( unsigned, 4 * Abc_TruthWordNum(p->nMergeLimit) ); - for ( i = 1; i < 4; i++ ) - p->pTruths[i] = p->pTruths[i-1] + Abc_TruthWordNum(p->nMergeLimit); - p->vMemory = Vec_IntAlloc( 1 << 18 ); + p->pTruths[0] = ABC_ALLOC(unsigned, 4 * Abc_TruthWordNum(p->nMergeLimit)); + for (i = 1; i < 4; i++) + p->pTruths[i] = p->pTruths[i - 1] + Abc_TruthWordNum(p->nMergeLimit); + p->vMemory = Vec_IntAlloc(1 << 18); return p; } @@ -73,21 +107,21 @@ Cnf_Man_t * Cnf_ManStart() Synopsis [Stops the fraiging manager.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_ManStop( Cnf_Man_t * p ) +void Cnf_ManStop(Cnf_Man_t *p) { - Vec_IntFree( p->vMemory ); - ABC_FREE( p->pTruths[0] ); - Aig_MmFlexStop( p->pMemCuts, 0 ); - ABC_FREE( p->pSopSizes ); - ABC_FREE( p->pSops[1] ); - ABC_FREE( p->pSops ); - ABC_FREE( p ); + Vec_IntFree(p->vMemory); + ABC_FREE(p->pTruths[0]); + Aig_MmFlexStop(p->pMemCuts, 0); + ABC_FREE(p->pSopSizes); + ABC_FREE(p->pSops[1]); + ABC_FREE(p->pSops); + ABC_FREE(p); } /**Function************************************************************* @@ -95,18 +129,19 @@ void Cnf_ManStop( Cnf_Man_t * p ) Synopsis [Returns the array of CI IDs.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +Vec_Int_t *Cnf_DataCollectPiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p) { - Aig_Obj_t * pObj; int i; - Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) ); - Aig_ManForEachCi( p, pObj, i ) - Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + Aig_Obj_t *pObj; + int i; + Vec_Int_t *vCiIds = Vec_IntAlloc(Aig_ManCiNum(p)); + Aig_ManForEachCi(p, pObj, i) + Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]); return vCiIds; } @@ -115,25 +150,25 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Synopsis [Allocates the new CNF.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals ) +Cnf_Dat_t *Cnf_DataAlloc(Aig_Man_t *pAig, int nVars, int nClauses, int nLiterals) { - Cnf_Dat_t * pCnf; - pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); + Cnf_Dat_t *pCnf; + pCnf = ABC_CALLOC(Cnf_Dat_t, 1); pCnf->pMan = pAig; pCnf->nVars = nVars; pCnf->nClauses = nClauses; pCnf->nLiterals = nLiterals; - pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); - pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); + pCnf->pClauses = ABC_ALLOC(int *, nClauses + 1); + pCnf->pClauses[0] = ABC_ALLOC(int, nLiterals); pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - if ( pCnf->pVarNums ) - pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) ); + if (pCnf->pVarNums) + pCnf->pVarNums = ABC_FALLOC(int, Aig_ManObjNumMax(pAig)); return pCnf; } @@ -142,54 +177,55 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter Synopsis [Allocates the new CNF.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ) +Cnf_Dat_t *Cnf_DataDup(Cnf_Dat_t *p) { - Cnf_Dat_t * pCnf; + Cnf_Dat_t *pCnf; int i; - pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals ); - memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals ); - if ( p->pVarNums ) - memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) ); - for ( i = 1; i < p->nClauses; i++ ) + pCnf = Cnf_DataAlloc(p->pMan, p->nVars, p->nClauses, p->nLiterals); + memcpy(pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals); + if (p->pVarNums) + memcpy(pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan)); + for (i = 1; i < p->nClauses; i++) pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]); return pCnf; } -Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit ) +Cnf_Dat_t *Cnf_DataDupCof(Cnf_Dat_t *p, int Lit) { - Cnf_Dat_t * pCnf; + Cnf_Dat_t *pCnf; int i; - pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 ); - memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals ); - if ( pCnf->pVarNums ) - memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) ); - for ( i = 1; i < p->nClauses; i++ ) + pCnf = Cnf_DataAlloc(p->pMan, p->nVars, p->nClauses + 1, p->nLiterals + 1); + memcpy(pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals); + if (pCnf->pVarNums) + memcpy(pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan)); + for (i = 1; i < p->nClauses; i++) pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]); pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals; pCnf->pClauses[p->nClauses][0] = Lit; - assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 ); + assert(pCnf->pClauses[p->nClauses + 1] == pCnf->pClauses[0] + p->nLiterals + 1); return pCnf; } -Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits ) +Cnf_Dat_t *Cnf_DataDupCofArray(Cnf_Dat_t *p, Vec_Int_t *vLits) { - Cnf_Dat_t * pCnf; + Cnf_Dat_t *pCnf; int i, iLit; - pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) ); - memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals ); - if ( pCnf->pVarNums ) - memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) ); - for ( i = 1; i < p->nClauses; i++ ) + pCnf = Cnf_DataAlloc(p->pMan, p->nVars, p->nClauses + Vec_IntSize(vLits), p->nLiterals + Vec_IntSize(vLits)); + memcpy(pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals); + if (pCnf->pVarNums) + memcpy(pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan)); + for (i = 1; i < p->nClauses; i++) pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]); - Vec_IntForEachEntry( vLits, iLit, i ) { - pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i; - pCnf->pClauses[p->nClauses+i][0] = iLit; + Vec_IntForEachEntry(vLits, iLit, i) + { + pCnf->pClauses[p->nClauses + i] = pCnf->pClauses[0] + p->nLiterals + i; + pCnf->pClauses[p->nClauses + i][0] = iLit; } - assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) ); + assert(pCnf->pClauses[p->nClauses + Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals + Vec_IntSize(vLits)); return pCnf; } @@ -198,24 +234,24 @@ Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataFree( Cnf_Dat_t * p ) +void Cnf_DataFree(Cnf_Dat_t *p) { - if ( p == NULL ) + if (p == NULL) return; - Vec_IntFreeP( &p->vMapping ); - ABC_FREE( p->pClaPols ); - ABC_FREE( p->pObj2Clause ); - ABC_FREE( p->pObj2Count ); - ABC_FREE( p->pClauses[0] ); - ABC_FREE( p->pClauses ); - ABC_FREE( p->pVarNums ); - ABC_FREE( p ); + Vec_IntFreeP(&p->vMapping); + ABC_FREE(p->pClaPols); + ABC_FREE(p->pObj2Clause); + ABC_FREE(p->pObj2Count); + ABC_FREE(p->pClauses[0]); + ABC_FREE(p->pClauses); + ABC_FREE(p->pVarNums); + ABC_FREE(p); } /**Function************************************************************* @@ -223,40 +259,39 @@ void Cnf_DataFree( Cnf_Dat_t * p ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) +void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus) { - Aig_Obj_t * pObj; + Aig_Obj_t *pObj; int v; - if ( p->pMan ) + if (p->pMan) { - Aig_ManForEachObj( p->pMan, pObj, v ) - if ( p->pVarNums[pObj->Id] >= 0 ) - p->pVarNums[pObj->Id] += nVarsPlus; + Aig_ManForEachObj(p->pMan, pObj, v) if (p->pVarNums[pObj->Id] >= 0) + p->pVarNums[pObj->Id] += nVarsPlus; } - for ( v = 0; v < p->nLiterals; v++ ) - p->pClauses[0][v] += 2*nVarsPlus; + for (v = 0; v < p->nLiterals; v++) + p->pClauses[0][v] += 2 * nVarsPlus; } -void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips ) +void Cnf_DataCollectFlipLits(Cnf_Dat_t *p, int iFlipVar, Vec_Int_t *vFlips) { int v; - assert( p->pMan == NULL ); - Vec_IntClear( vFlips ); - for ( v = 0; v < p->nLiterals; v++ ) - if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar ) - Vec_IntPush( vFlips, v ); + assert(p->pMan == NULL); + Vec_IntClear(vFlips); + for (v = 0; v < p->nLiterals; v++) + if (Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar) + Vec_IntPush(vFlips, v); } -void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits ) +void Cnf_DataLiftAndFlipLits(Cnf_Dat_t *p, int nVarsPlus, Vec_Int_t *vLits) { int i, iLit; - assert( p->pMan == NULL ); - Vec_IntForEachEntry( vLits, iLit, i ) - p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2*nVarsPlus; + assert(p->pMan == NULL); + Vec_IntForEachEntry(vLits, iLit, i) + p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2 * nVarsPlus; } /**Function************************************************************* @@ -264,24 +299,24 @@ void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) +void Cnf_DataPrint(Cnf_Dat_t *p, int fReadable) { - FILE * pFile = stdout; - int * pLit, * pStop, i; - fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); - for ( i = 0; i < p->nClauses; i++ ) + FILE *pFile = stdout; + int *pLit, *pStop, i; + fprintf(pFile, "p cnf %d %d\n", p->nVars, p->nClauses); + for (i = 0; i < p->nClauses; i++) { - for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 ); - fprintf( pFile, "\n" ); + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + fprintf(pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-" : "", fReadable ? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit) + 1); + fprintf(pFile, "\n"); } - fprintf( pFile, "\n" ); + fprintf(pFile, "\n"); } /**Function************************************************************* @@ -289,88 +324,88 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) Synopsis [Writes CNF into a file.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ) +void Cnf_DataWriteIntoFileGz(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists) { gzFile pFile; - int * pLit, * pStop, i, VarId; - pFile = gzopen( pFileName, "wb" ); - if ( pFile == NULL ) + int *pLit, *pStop, i, VarId; + pFile = gzopen(pFileName, "wb"); + if (pFile == NULL) { - printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + printf("Cnf_WriteIntoFile(): Output file cannot be opened.\n"); return; } - gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); - if ( vForAlls ) + gzprintf(pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n"); + gzprintf(pFile, "p cnf %d %d\n", p->nVars, p->nClauses); + if (vForAlls) { - gzprintf( pFile, "a " ); - Vec_IntForEachEntry( vForAlls, VarId, i ) - gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - gzprintf( pFile, "0\n" ); + gzprintf(pFile, "a "); + Vec_IntForEachEntry(vForAlls, VarId, i) + gzprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + gzprintf(pFile, "0\n"); } - if ( vExists ) + if (vExists) { - gzprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists, VarId, i ) - gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - gzprintf( pFile, "0\n" ); + gzprintf(pFile, "e "); + Vec_IntForEachEntry(vExists, VarId, i) + gzprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + gzprintf(pFile, "0\n"); } - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - gzprintf( pFile, "0\n" ); + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + gzprintf(pFile, "%d ", fReadable ? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit)); + gzprintf(pFile, "0\n"); } - gzprintf( pFile, "\n" ); - gzclose( pFile ); + gzprintf(pFile, "\n"); + gzclose(pFile); } -void Cnf_DataWriteIntoFileInvGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 ) +void Cnf_DataWriteIntoFileInvGz(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vExists1, Vec_Int_t *vForAlls, Vec_Int_t *vExists2) { gzFile pFile; - int * pLit, * pStop, i, VarId; - pFile = gzopen( pFileName, "wb" ); - if ( pFile == NULL ) + int *pLit, *pStop, i, VarId; + pFile = gzopen(pFileName, "wb"); + if (pFile == NULL) { - printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + printf("Cnf_WriteIntoFile(): Output file cannot be opened.\n"); return; } - gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); - if ( vExists1 ) + gzprintf(pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n"); + gzprintf(pFile, "p cnf %d %d\n", p->nVars, p->nClauses); + if (vExists1) { - gzprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists1, VarId, i ) - gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - gzprintf( pFile, "0\n" ); + gzprintf(pFile, "e "); + Vec_IntForEachEntry(vExists1, VarId, i) + gzprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + gzprintf(pFile, "0\n"); } - if ( vForAlls ) + if (vForAlls) { - gzprintf( pFile, "a " ); - Vec_IntForEachEntry( vForAlls, VarId, i ) - gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - gzprintf( pFile, "0\n" ); + gzprintf(pFile, "a "); + Vec_IntForEachEntry(vForAlls, VarId, i) + gzprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + gzprintf(pFile, "0\n"); } - if ( vExists2 ) + if (vExists2) { - gzprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists2, VarId, i ) - gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - gzprintf( pFile, "0\n" ); + gzprintf(pFile, "e "); + Vec_IntForEachEntry(vExists2, VarId, i) + gzprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + gzprintf(pFile, "0\n"); } - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - gzprintf( pFile, "0\n" ); + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + gzprintf(pFile, "%d ", fReadable ? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit)); + gzprintf(pFile, "0\n"); } - gzprintf( pFile, "\n" ); - gzclose( pFile ); + gzprintf(pFile, "\n"); + gzclose(pFile); } /**Function************************************************************* @@ -378,98 +413,101 @@ void Cnf_DataWriteIntoFileInvGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Synopsis [Writes CNF into a file.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ) +void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists) { - FILE * pFile; - int * pLit, * pStop, i, VarId; - if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) + FILE *pFile; + int *pLit, *pStop, i, VarId, nExtra; + if (!strncmp(pFileName + strlen(pFileName) - 3, ".gz", 3)) { - Cnf_DataWriteIntoFileGz( p, pFileName, fReadable, vForAlls, vExists ); + Cnf_DataWriteIntoFileGz(p, pFileName, fReadable, vForAlls, vExists); return; } - pFile = fopen( pFileName, "w" ); - if ( pFile == NULL ) + pFile = fopen(pFileName, "w"); + if (pFile == NULL) { - printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + printf("Cnf_WriteIntoFile(): Output file cannot be opened.\n"); return; } - fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); - if ( vForAlls ) + nExtra = Cnf_DataWriteDanglingUnitClauses(NULL, p); + fprintf(pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n"); + fprintf(pFile, "p cnf %d %d\n", p->nVars, p->nClauses + nExtra); + if (vForAlls) { - fprintf( pFile, "a " ); - Vec_IntForEachEntry( vForAlls, VarId, i ) - fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - fprintf( pFile, "0\n" ); + fprintf(pFile, "a "); + Vec_IntForEachEntry(vForAlls, VarId, i) + fprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + fprintf(pFile, "0\n"); } - if ( vExists ) + if (vExists) { - fprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists, VarId, i ) - fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - fprintf( pFile, "0\n" ); + fprintf(pFile, "e "); + Vec_IntForEachEntry(vExists, VarId, i) + fprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + fprintf(pFile, "0\n"); } - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - fprintf( pFile, "0\n" ); + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + fprintf(pFile, "%d ", fReadable ? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit)); + fprintf(pFile, "0\n"); } - fprintf( pFile, "\n" ); - fclose( pFile ); + if (nExtra) + Cnf_DataWriteDanglingUnitClauses(pFile, p); + fprintf(pFile, "\n"); + fclose(pFile); } -void Cnf_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 ) +void Cnf_DataWriteIntoFileInv(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vExists1, Vec_Int_t *vForAlls, Vec_Int_t *vExists2) { - FILE * pFile; - int * pLit, * pStop, i, VarId; - if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) + FILE *pFile; + int *pLit, *pStop, i, VarId; + if (!strncmp(pFileName + strlen(pFileName) - 3, ".gz", 3)) { - Cnf_DataWriteIntoFileInvGz( p, pFileName, fReadable, vExists1, vForAlls, vExists2 ); + Cnf_DataWriteIntoFileInvGz(p, pFileName, fReadable, vExists1, vForAlls, vExists2); return; } - pFile = fopen( pFileName, "w" ); - if ( pFile == NULL ) + pFile = fopen(pFileName, "w"); + if (pFile == NULL) { - printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + printf("Cnf_WriteIntoFile(): Output file cannot be opened.\n"); return; } - fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); - if ( vExists1 ) + fprintf(pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n"); + fprintf(pFile, "p cnf %d %d\n", p->nVars, p->nClauses); + if (vExists1) { - fprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists1, VarId, i ) - fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - fprintf( pFile, "0\n" ); + fprintf(pFile, "e "); + Vec_IntForEachEntry(vExists1, VarId, i) + fprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + fprintf(pFile, "0\n"); } - if ( vForAlls ) + if (vForAlls) { - fprintf( pFile, "a " ); - Vec_IntForEachEntry( vForAlls, VarId, i ) - fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - fprintf( pFile, "0\n" ); + fprintf(pFile, "a "); + Vec_IntForEachEntry(vForAlls, VarId, i) + fprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + fprintf(pFile, "0\n"); } - if ( vExists2 ) + if (vExists2) { - fprintf( pFile, "e " ); - Vec_IntForEachEntry( vExists2, VarId, i ) - fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); - fprintf( pFile, "0\n" ); + fprintf(pFile, "e "); + Vec_IntForEachEntry(vExists2, VarId, i) + fprintf(pFile, "%d ", fReadable ? VarId : VarId + 1); + fprintf(pFile, "0\n"); } - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - fprintf( pFile, "0\n" ); + for (pLit = p->pClauses[i], pStop = p->pClauses[i + 1]; pLit < pStop; pLit++) + fprintf(pFile, "%d ", fReadable ? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit)); + fprintf(pFile, "0\n"); } - fprintf( pFile, "\n" ); - fclose( pFile ); + fprintf(pFile, "\n"); + fclose(pFile); } /**Function************************************************************* @@ -477,89 +515,89 @@ void Cnf_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, V Synopsis [Writes CNF into a file.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void * Cnf_DataWriteIntoSolverInt( void * pSolver, Cnf_Dat_t * p, int nFrames, int fInit ) +void *Cnf_DataWriteIntoSolverInt(void *pSolver, Cnf_Dat_t *p, int nFrames, int fInit) { - sat_solver * pSat = (sat_solver *)pSolver; + sat_solver *pSat = (sat_solver *)pSolver; int i, f, status; - assert( nFrames > 0 ); - assert( pSat ); -// pSat = sat_solver_new(); - sat_solver_setnvars( pSat, p->nVars * nFrames ); - for ( i = 0; i < p->nClauses; i++ ) + assert(nFrames > 0); + assert(pSat); + // pSat = sat_solver_new(); + sat_solver_setnvars(pSat, p->nVars * nFrames); + for (i = 0; i < p->nClauses; i++) { - if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if (!sat_solver_addclause(pSat, p->pClauses[i], p->pClauses[i + 1])) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } } - if ( nFrames > 1 ) + if (nFrames > 1) { - Aig_Obj_t * pObjLo, * pObjLi; - int nLitsAll, * pLits, Lits[2]; + Aig_Obj_t *pObjLo, *pObjLi; + int nLitsAll, *pLits, Lits[2]; nLitsAll = 2 * p->nVars; pLits = p->pClauses[0]; - for ( f = 1; f < nFrames; f++ ) + for (f = 1; f < nFrames; f++) { // add equality of register inputs/outputs for different timeframes - Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i ) + Aig_ManForEachLiLoSeq(p->pMan, pObjLi, pObjLo, i) { - Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 ); - Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + Lits[0] = (f - 1) * nLitsAll + toLitCond(p->pVarNums[pObjLi->Id], 0); + Lits[1] = f * nLitsAll + toLitCond(p->pVarNums[pObjLo->Id], 1); + if (!sat_solver_addclause(pSat, Lits, Lits + 2)) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } Lits[0]++; Lits[1]--; - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + if (!sat_solver_addclause(pSat, Lits, Lits + 2)) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } } // add clauses for the next timeframe - for ( i = 0; i < p->nLiterals; i++ ) + for (i = 0; i < p->nLiterals; i++) pLits[i] += nLitsAll; - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if (!sat_solver_addclause(pSat, p->pClauses[i], p->pClauses[i + 1])) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } } } // return literals to their original state - nLitsAll = (f-1) * nLitsAll; - for ( i = 0; i < p->nLiterals; i++ ) + nLitsAll = (f - 1) * nLitsAll; + for (i = 0; i < p->nLiterals; i++) pLits[i] -= nLitsAll; } - if ( fInit ) + if (fInit) { - Aig_Obj_t * pObjLo; + Aig_Obj_t *pObjLo; int Lits[1]; - Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) + Aig_ManForEachLoSeq(p->pMan, pObjLo, i) { - Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) ) + Lits[0] = toLitCond(p->pVarNums[pObjLo->Id], 1); + if (!sat_solver_addclause(pSat, Lits, Lits + 1)) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } } } status = sat_solver_simplify(pSat); - if ( status == 0 ) + if (status == 0) { - sat_solver_delete( pSat ); + sat_solver_delete(pSat); return NULL; } return pSat; @@ -570,15 +608,15 @@ void * Cnf_DataWriteIntoSolverInt( void * pSolver, Cnf_Dat_t * p, int nFrames, i Synopsis [Writes CNF into a file.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) +void *Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit) { - return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit ); + return Cnf_DataWriteIntoSolverInt(sat_solver_new(), p, nFrames, fInit); } /**Function************************************************************* @@ -586,88 +624,88 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) Synopsis [Writes CNF into a file.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) +void *Cnf_DataWriteIntoSolver2(Cnf_Dat_t *p, int nFrames, int fInit) { - sat_solver2 * pSat; + sat_solver2 *pSat; int i, f, status; - assert( nFrames > 0 ); + assert(nFrames > 0); pSat = sat_solver2_new(); - sat_solver2_setnvars( pSat, p->nVars * nFrames ); - for ( i = 0; i < p->nClauses; i++ ) + 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], 0 ) ) + if (!sat_solver2_addclause(pSat, p->pClauses[i], p->pClauses[i + 1], 0)) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } } - if ( nFrames > 1 ) + if (nFrames > 1) { - Aig_Obj_t * pObjLo, * pObjLi; - int nLitsAll, * pLits, Lits[2]; + Aig_Obj_t *pObjLo, *pObjLi; + int nLitsAll, *pLits, Lits[2]; nLitsAll = 2 * p->nVars; pLits = p->pClauses[0]; - for ( f = 1; f < nFrames; f++ ) + for (f = 1; f < nFrames; f++) { // add equality of register inputs/outputs for different timeframes - Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i ) + Aig_ManForEachLiLoSeq(p->pMan, pObjLi, pObjLo, i) { - 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, 0 ) ) + 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, 0)) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } Lits[0]++; Lits[1]--; - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) + if (!sat_solver2_addclause(pSat, Lits, Lits + 2, 0)) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } } // add clauses for the next timeframe - for ( i = 0; i < p->nLiterals; i++ ) + for (i = 0; i < p->nLiterals; i++) pLits[i] += nLitsAll; - for ( i = 0; i < p->nClauses; i++ ) + for (i = 0; i < p->nClauses; i++) { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) ) + if (!sat_solver2_addclause(pSat, p->pClauses[i], p->pClauses[i + 1], 0)) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } } } // return literals to their original state - nLitsAll = (f-1) * nLitsAll; - for ( i = 0; i < p->nLiterals; i++ ) + nLitsAll = (f - 1) * nLitsAll; + for (i = 0; i < p->nLiterals; i++) pLits[i] -= nLitsAll; } - if ( fInit ) + if (fInit) { - Aig_Obj_t * pObjLo; + Aig_Obj_t *pObjLo; int Lits[1]; - Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) + Aig_ManForEachLoSeq(p->pMan, pObjLo, i) { - Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 1, 0 ) ) + Lits[0] = toLitCond(p->pVarNums[pObjLo->Id], 1); + if (!sat_solver2_addclause(pSat, Lits, Lits + 1, 0)) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } } } status = sat_solver2_simplify(pSat); - if ( status == 0 ) + if (status == 0) { - sat_solver2_delete( pSat ); + sat_solver2_delete(pSat); return NULL; } return pSat; @@ -678,26 +716,26 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) Synopsis [Adds the OR-clause.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) +int Cnf_DataWriteOrClause(void *p, Cnf_Dat_t *pCnf) { - sat_solver * pSat = (sat_solver *)p; - Aig_Obj_t * pObj; - int i, * pLits; - pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) ); - Aig_ManForEachCo( pCnf->pMan, pObj, i ) - pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) ) + sat_solver *pSat = (sat_solver *)p; + Aig_Obj_t *pObj; + int i, *pLits; + pLits = ABC_ALLOC(int, Aig_ManCoNum(pCnf->pMan)); + Aig_ManForEachCo(pCnf->pMan, pObj, i) + pLits[i] = toLitCond(pCnf->pVarNums[pObj->Id], 0); + if (!sat_solver_addclause(pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan))) { - ABC_FREE( pLits ); + ABC_FREE(pLits); return 0; } - ABC_FREE( pLits ); + ABC_FREE(pLits); return 1; } @@ -706,26 +744,26 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) Synopsis [Adds the OR-clause.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) +int Cnf_DataWriteOrClause2(void *p, Cnf_Dat_t *pCnf) { - sat_solver2 * pSat = (sat_solver2 *)p; - Aig_Obj_t * pObj; - int i, * pLits; - 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), 0 ) ) + sat_solver2 *pSat = (sat_solver2 *)p; + Aig_Obj_t *pObj; + int i, *pLits; + 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), 0)) { - ABC_FREE( pLits ); + ABC_FREE(pLits); return 0; } - ABC_FREE( pLits ); + ABC_FREE(pLits); return 1; } @@ -734,21 +772,21 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) Synopsis [Adds the OR-clause.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) +int Cnf_DataWriteAndClauses(void *p, Cnf_Dat_t *pCnf) { - sat_solver * pSat = (sat_solver *)p; - Aig_Obj_t * pObj; + sat_solver *pSat = (sat_solver *)p; + Aig_Obj_t *pObj; int i, Lit; - Aig_ManForEachCo( pCnf->pMan, pObj, i ) + Aig_ManForEachCo(pCnf->pMan, pObj, i) { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + Lit = toLitCond(pCnf->pVarNums[pObj->Id], 0); + if (!sat_solver_addclause(pSat, &Lit, &Lit + 1)) return 0; } return 1; @@ -759,35 +797,35 @@ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) Synopsis [Transforms polarity of the internal veriables.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ) +void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos) { - Aig_Obj_t * pObj; - int * pVarToPol; + Aig_Obj_t *pObj; + int *pVarToPol; int i, iVar; // create map from the variable number to its polarity - pVarToPol = ABC_CALLOC( int, pCnf->nVars ); - Aig_ManForEachObj( pCnf->pMan, pObj, i ) + pVarToPol = ABC_CALLOC(int, pCnf->nVars); + Aig_ManForEachObj(pCnf->pMan, pObj, i) { - if ( !fTransformPos && Aig_ObjIsCo(pObj) ) + if (!fTransformPos && Aig_ObjIsCo(pObj)) continue; - if ( pCnf->pVarNums[pObj->Id] >= 0 ) - pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; + if (pCnf->pVarNums[pObj->Id] >= 0) + pVarToPol[pCnf->pVarNums[pObj->Id]] = pObj->fPhase; } // transform literals - for ( i = 0; i < pCnf->nLiterals; i++ ) + for (i = 0; i < pCnf->nLiterals; i++) { iVar = lit_var(pCnf->pClauses[0][i]); - assert( iVar < pCnf->nVars ); - if ( pVarToPol[iVar] ) - pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] ); + assert(iVar < pCnf->nVars); + if (pVarToPol[iVar]) + pCnf->pClauses[0][i] = lit_neg(pCnf->pClauses[0][i]); } - ABC_FREE( pVarToPol ); + ABC_FREE(pVarToPol); } /**Function************************************************************* @@ -795,39 +833,39 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ) Synopsis [Adds constraints for the two-input AND-gate.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC ) +int Cnf_DataAddXorClause(void *pSat, int iVarA, int iVarB, int iVarC) { lit Lits[3]; - assert( iVarA > 0 && iVarB > 0 && iVarC > 0 ); + assert(iVarA > 0 && iVarB > 0 && iVarC > 0); - Lits[0] = toLitCond( iVarA, 1 ); - Lits[1] = toLitCond( iVarB, 1 ); - Lits[2] = toLitCond( iVarC, 1 ); - if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) + Lits[0] = toLitCond(iVarA, 1); + Lits[1] = toLitCond(iVarB, 1); + Lits[2] = toLitCond(iVarC, 1); + if (!sat_solver_addclause((sat_solver *)pSat, Lits, Lits + 3)) return 0; - Lits[0] = toLitCond( iVarA, 1 ); - Lits[1] = toLitCond( iVarB, 0 ); - Lits[2] = toLitCond( iVarC, 0 ); - if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) + Lits[0] = toLitCond(iVarA, 1); + Lits[1] = toLitCond(iVarB, 0); + Lits[2] = toLitCond(iVarC, 0); + if (!sat_solver_addclause((sat_solver *)pSat, Lits, Lits + 3)) return 0; - Lits[0] = toLitCond( iVarA, 0 ); - Lits[1] = toLitCond( iVarB, 1 ); - Lits[2] = toLitCond( iVarC, 0 ); - if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) + Lits[0] = toLitCond(iVarA, 0); + Lits[1] = toLitCond(iVarB, 1); + Lits[2] = toLitCond(iVarC, 0); + if (!sat_solver_addclause((sat_solver *)pSat, Lits, Lits + 3)) return 0; - Lits[0] = toLitCond( iVarA, 0 ); - Lits[1] = toLitCond( iVarB, 0 ); - Lits[2] = toLitCond( iVarC, 1 ); - if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) + Lits[0] = toLitCond(iVarA, 0); + Lits[1] = toLitCond(iVarB, 0); + Lits[2] = toLitCond(iVarC, 1); + if (!sat_solver_addclause((sat_solver *)pSat, Lits, Lits + 3)) return 0; return 1; @@ -837,6 +875,4 @@ int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_IMPL_END - diff --git a/test/write_cnf_dangling.sh b/test/write_cnf_dangling.sh new file mode 100755 index 000000000..bbb80b7dc --- /dev/null +++ b/test/write_cnf_dangling.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# Regression test for berkeley-abc/abc#479 +# +# After "strash", a primary input wired directly to a primary output becomes +# a dangling PI: it shows up in the DIMACS header's variable count but the +# Tseitin encoder emits no clause mentioning it. Such a free variable +# silently doubles the model count of the written formula, breaking #SAT +# and uniform sampling. +# +# The fix in Cnf_DataWriteIntoFile() detects DIMACS variables that are +# declared in the header but unreferenced in any clause, and emits a unit +# clause pinning each of them to false. The two cases below exercise that +# behaviour against the abc binary. + +set -eu + +ABC=${ABC:-./abc} +TMP=$(mktemp -d) +trap 'rm -rf "$TMP"' EXIT + +fail() { echo "FAIL: $1" >&2; exit 1; } + +run_case() { + local name=$1 input=$2 + local in="$TMP/$name.in.cnf" out="$TMP/$name.out.cnf" + printf '%s' "$input" > "$in" + "$ABC" -q "read_cnf $in; strash; write_cnf $out" > /dev/null + + # Extract declared variable count from the header. + local header + header=$(grep -m1 '^p cnf ' "$out") + local nVars + nVars=$(echo "$header" | awk '{print $3}') + + # Every variable 1..nVars must appear (positive or negated) in some clause. + local v + for v in $(seq 1 "$nVars"); do + if ! grep -Eq "(^|[ \t-])$v( |$)" "$out"; then + cat "$out" >&2 + fail "$name: variable $v declared in header but never used in any clause" + fi + done + echo "PASS: $name ($header)" +} + +# Case 1: original reproducer from issue #479 -- a single PI wired directly +# to a single PO. Before the fix, the output was "p cnf 3 2" with clauses +# "-3 0" and "2 0", leaving variable 1 unconstrained. +run_case "pi_to_po_direct" "p cnf 1 1 +1 0 +" + +# Case 2: two independent PIs, each a direct wire to its own PO. Both PIs +# end up dangling after strash. +run_case "two_pis_two_pos" "p cnf 2 2 +1 0 +2 0 +" + +echo "All regression tests passed."