summaryrefslogtreecommitdiffstats
path: root/src/abc8/cnf/cnfMan.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/abc8/cnf/cnfMan.c')
-rw-r--r--src/abc8/cnf/cnfMan.c282
1 files changed, 0 insertions, 282 deletions
diff --git a/src/abc8/cnf/cnfMan.c b/src/abc8/cnf/cnfMan.c
deleted file mode 100644
index 47bc0b67..00000000
--- a/src/abc8/cnf/cnfMan.c
+++ /dev/null
@@ -1,282 +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"
-
-////////////////////////////////////////////////////////////////////////
-/// 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 = 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] = 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 );
- free( p->pTruths[0] );
- Aig_MmFlexStop( p->pMemCuts, 0 );
- free( p->pSopSizes );
- free( p->pSops[1] );
- free( p->pSops );
- 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 []
-
- 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_DataLift( Cnf_Dat_t * p, int nVarsPlus )
-{
- Aig_Obj_t * pObj;
- int v;
- Aig_ManForEachObj( p->pMan, pObj, v )
- if ( p->pVarNums[pObj->Id] )
- 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_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
-{
- 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 ", 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_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
-{
- sat_solver * pSat;
- int i, f, status;
- assert( nFrames > 0 );
- 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;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 12:46:42 +0000