diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-03 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-03 08:01:00 -0700 |
commit | a8db621dc96768cf2cf543be905d534579847020 (patch) | |
tree | c5c11558d1adf35b474cebd78d89b2e5ae1bc1bc /src/aig/cnf/cnfMan.c | |
parent | d6804597a397379f826810a736ccbe99bf56c497 (diff) | |
download | abc-a8db621dc96768cf2cf543be905d534579847020.tar.gz abc-a8db621dc96768cf2cf543be905d534579847020.tar.bz2 abc-a8db621dc96768cf2cf543be905d534579847020.zip |
Version abc70703
Diffstat (limited to 'src/aig/cnf/cnfMan.c')
-rw-r--r-- | src/aig/cnf/cnfMan.c | 173 |
1 files changed, 173 insertions, 0 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c new file mode 100644 index 00000000..d1d1fc21 --- /dev/null +++ b/src/aig/cnf/cnfMan.c @@ -0,0 +1,173 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+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 = 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 = Dar_MmFlexStart(); + p->nMergeLimit = 10; + // allocate temporary truth tables + p->pTruths[0] = ALLOC( unsigned, 4 * Dar_TruthWordNum(p->nMergeLimit) ); + for ( i = 1; i < 4; i++ ) + p->pTruths[i] = p->pTruths[i-1] + Dar_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 ); + free( p->pTruths[0] ); + Dar_MmFlexStop( p->pMemCuts, 0 ); + free( p->pSopSizes ); + free( p->pSops[1] ); + free( p->pSops ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataFree( Cnf_Dat_t * p ) +{ + if ( p == NULL ) + return; + free( p->pClauses[0] ); + free( p->pClauses ); + free( p->pVarNums ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) +{ + FILE * pFile; + int * pLit, * pStop, i; + 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 %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 ", Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "0\n" ); + } + fprintf( pFile, "\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) +{ + sat_solver * pSat; + int i; + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, p->nVars ); + 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 pSat; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |