summaryrefslogtreecommitdiffstats
path: root/src/aig/dch/dchInt.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dch/dchInt.h')
-rw-r--r--src/aig/dch/dchInt.h170
1 files changed, 0 insertions, 170 deletions
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
deleted file mode 100644
index 6072d97b..00000000
--- a/src/aig/dch/dchInt.h
+++ /dev/null
@@ -1,170 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchInt.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __DCH_INT_H__
-#define __DCH_INT_H__
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include "aig.h"
-#include "satSolver.h"
-#include "dch.h"
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-// equivalence classes
-typedef struct Dch_Cla_t_ Dch_Cla_t;
-
-// choicing manager
-typedef struct Dch_Man_t_ Dch_Man_t;
-struct Dch_Man_t_
-{
- // parameters
- Dch_Pars_t * pPars; // choicing parameters
- // AIGs used in the package
-// Vec_Ptr_t * vAigs; // user-given AIGs
- Aig_Man_t * pAigTotal; // intermediate AIG
- Aig_Man_t * pAigFraig; // final AIG
- // equivalence classes
- Dch_Cla_t * ppClasses; // equivalence classes of nodes
- Aig_Obj_t ** pReprsProved; // equivalences proved
- // SAT solving
- sat_solver * pSat; // recyclable SAT solver
- int nSatVars; // the counter of SAT variables
- int * pSatVars; // mapping of each node into its SAT var
- Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
- int nRecycles; // the number of times SAT solver was recycled
- int nCallsSince; // the number of calls since the last recycle
- Vec_Ptr_t * vFanins; // fanins of the CNF node
- Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
- Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
- // solver cone size
- int nConeThis;
- int nConeMax;
- // SAT calls statistics
- int nSatCalls; // the number of SAT calls
- int nSatProof; // the number of proofs
- int nSatFailsReal; // the number of timeouts
- int nSatCallsUnsat; // the number of unsat SAT calls
- int nSatCallsSat; // the number of sat SAT calls
- // choice node statistics
- int nLits; // the number of lits in the cand equiv classes
- int nReprs; // the number of proved equivalent pairs
- int nEquivs; // the number of final equivalences
- int nChoices; // the number of final choice nodes
- // runtime stats
- int timeSimInit; // simulation and class computation
- int timeSimSat; // simulation of the counter-examples
- int timeSat; // solving SAT
- int timeSatSat; // sat
- int timeSatUnsat; // unsat
- int timeSatUndec; // undecided
- int timeChoice; // choice computation
- int timeOther; // other runtime
- int timeTotal; // total runtime
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
-static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
-
-static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return (Aig_Obj_t *)pObj->pData; }
-static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
-static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
-}
-static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
- Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== dchAig.c ===================================================*/
-/*=== dchChoice.c ===================================================*/
-extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
-extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
-extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig );
-/*=== dchClass.c =================================================*/
-extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig );
-extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
- unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
- int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
- int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
-extern void Dch_ClassesStop( Dch_Cla_t * p );
-extern int Dch_ClassesLitNum( Dch_Cla_t * p );
-extern Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
-extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
-extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
-extern int Dch_ClassesRefine( Dch_Cla_t * p );
-extern int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
-extern void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots );
-extern void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots );
-extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
-/*=== dchCnf.c ===================================================*/
-extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
-/*=== dchMan.c ===================================================*/
-extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-extern void Dch_ManStop( Dch_Man_t * p );
-extern void Dch_ManSatSolverRecycle( Dch_Man_t * p );
-/*=== dchSat.c ===================================================*/
-extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
-/*=== dchSim.c ===================================================*/
-extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
-/*=== dchSimSat.c ===================================================*/
-extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
-extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
-/*=== dchSweep.c ===================================================*/
-extern void Dch_ManSweep( Dch_Man_t * p );
-
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 18:11:57 +0000