diff options
Diffstat (limited to 'src/aig/cnf/cnfMan.c')
-rw-r--r-- | src/aig/cnf/cnfMan.c | 693 |
1 files changed, 0 insertions, 693 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c deleted file mode 100644 index 6b107651..00000000 --- a/src/aig/cnf/cnfMan.c +++ /dev/null @@ -1,693 +0,0 @@ -/**CFile**************************************************************** - - FileName [cnfMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [AIG-to-CNF conversion.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: cnfMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cnf.h" -#include "satSolver.h" -#include "satSolver2.h" -#include "zlib.h" - -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); } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Starts the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Man_t * Cnf_ManStart() -{ - Cnf_Man_t * p; - int i; - // allocate the manager - p = ABC_ALLOC( Cnf_Man_t, 1 ); - memset( p, 0, sizeof(Cnf_Man_t) ); - // derive internal data structures - 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 * Aig_TruthWordNum(p->nMergeLimit) ); - for ( i = 1; i < 4; i++ ) - p->pTruths[i] = p->pTruths[i-1] + Aig_TruthWordNum(p->nMergeLimit); - p->vMemory = Vec_IntAlloc( 1 << 18 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 ); -} - -/**Function************************************************************* - - 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 * vCiIds; - Aig_Obj_t * pObj; - int i; - vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPi( p, pObj, i ) - Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); - return vCiIds; -} - -/**Function************************************************************* - - 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 * pCnf; - int i; - pCnf = ABC_ALLOC( Cnf_Dat_t, 1 ); - memset( pCnf, 0, sizeof(Cnf_Dat_t) ); - 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[nClauses] = pCnf->pClauses[0] + nLiterals; - pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) ); -// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) ); - for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) - pCnf->pVarNums[i] = -1; - return pCnf; -} - -/**Function************************************************************* - - Synopsis [Allocates the new CNF.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ) -{ - 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 ); - 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; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataFree( Cnf_Dat_t * p ) -{ - if ( p == NULL ) - return; - 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************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) -{ - Aig_Obj_t * pObj; - int v; - 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; -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ) -{ - p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] ); -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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++ ) - { - 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, "\n" ); - } - fprintf( pFile, "\n" ); -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable ) -{ - gzFile pFile; - int * pLit, * pStop, i; - pFile = gzopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - 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 ); - 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" ); - } - gzprintf( pFile, "\n" ); - gzclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) -{ - FILE * pFile; - int * pLit, * pStop, i; - if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) - { - Cnf_DataWriteIntoFileGz( p, pFileName, fReadable ); - return; - } - pFile = fopen( pFileName, "w" ); - if ( pFile == NULL ) - { - 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 ); - 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" ); - } - fprintf( pFile, "\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Cnf_DataWriteIntoSolverInt( void * pSolver, Cnf_Dat_t * p, int nFrames, int fInit ) -{ - 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++ ) - { - if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) - { - sat_solver_delete( pSat ); - return NULL; - } - } - if ( nFrames > 1 ) - { - Aig_Obj_t * pObjLo, * pObjLi; - int nLitsAll, * pLits, Lits[2]; - nLitsAll = 2 * p->nVars; - pLits = p->pClauses[0]; - for ( f = 1; f < nFrames; f++ ) - { - // add equality of register inputs/outputs for different timeframes - 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 ) ) - { - sat_solver_delete( pSat ); - return NULL; - } - Lits[0]++; - Lits[1]--; - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return NULL; - } - } - // add clauses for the next timeframe - for ( i = 0; i < p->nLiterals; i++ ) - pLits[i] += nLitsAll; - for ( i = 0; i < p->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) - { - sat_solver_delete( pSat ); - return NULL; - } - } - } - // return literals to their original state - nLitsAll = (f-1) * nLitsAll; - for ( i = 0; i < p->nLiterals; i++ ) - pLits[i] -= nLitsAll; - } - if ( fInit ) - { - Aig_Obj_t * pObjLo; - int Lits[1]; - Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) - { - Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) ) - { - sat_solver_delete( pSat ); - return NULL; - } - } - } - status = sat_solver_simplify(pSat); - if ( status == 0 ) - { - sat_solver_delete( pSat ); - return NULL; - } - return pSat; -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) -{ - return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit ); -} - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) -{ - sat_solver2 * pSat; - int i, f, status; - assert( nFrames > 0 ); - pSat = sat_solver2_new(); - 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] ) ) - { - sat_solver2_delete( pSat ); - return NULL; - } - } - if ( nFrames > 1 ) - { - Aig_Obj_t * pObjLo, * pObjLi; - int nLitsAll, * pLits, Lits[2]; - nLitsAll = 2 * p->nVars; - pLits = p->pClauses[0]; - for ( f = 1; f < nFrames; f++ ) - { - // add equality of register inputs/outputs for different timeframes - 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 ) ) - { - sat_solver2_delete( pSat ); - return NULL; - } - Lits[0]++; - Lits[1]--; - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver2_delete( pSat ); - return NULL; - } - } - // add clauses for the next timeframe - for ( i = 0; i < p->nLiterals; i++ ) - pLits[i] += nLitsAll; - for ( i = 0; i < p->nClauses; i++ ) - { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) - { - sat_solver2_delete( pSat ); - return NULL; - } - } - } - // return literals to their original state - nLitsAll = (f-1) * nLitsAll; - for ( i = 0; i < p->nLiterals; i++ ) - pLits[i] -= nLitsAll; - } - if ( fInit ) - { - Aig_Obj_t * pObjLo; - int Lits[1]; - Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) - { - Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) ) - { - sat_solver2_delete( pSat ); - return NULL; - } - } - } - status = sat_solver2_simplify(pSat); - if ( status == 0 ) - { - sat_solver2_delete( pSat ); - return NULL; - } - return pSat; -} - -/**Function************************************************************* - - Synopsis [Adds the OR-clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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_ManPoNum(pCnf->pMan) ); - 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) ) ) - { - ABC_FREE( pLits ); - return 0; - } - ABC_FREE( pLits ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds the OR-clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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_ManPoNum(pCnf->pMan) ); - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) ) - { - ABC_FREE( pLits ); - return 0; - } - ABC_FREE( pLits ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds the OR-clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) -{ - sat_solver * pSat = (sat_solver *)p; - Aig_Obj_t * pObj; - int i, Lit; - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Transforms polarity of the internal veriables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ) -{ - 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 ) - { - if ( !fTransformPos && Aig_ObjIsPo(pObj) ) - continue; - if ( pCnf->pVarNums[pObj->Id] >= 0 ) - pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; - } - // transform literals - 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] ); - } - ABC_FREE( pVarToPol ); -} - -/**Function************************************************************* - - Synopsis [Adds constraints for the two-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC ) -{ - lit Lits[3]; - 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 ) ) - 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 ) ) - 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 ) ) - 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 ) ) - return 0; - - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |