summaryrefslogtreecommitdiffstats
path: root/src/aig/dch/dchInt.h
blob: 6072d97beb1cdccee1bb6d7382345203152476a4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
/**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                                ///
////////////////////////////////////////////////////////////////////////