summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig/fraig.h
blob: 53a46584eb0675c0897c5a976c4be88062ae4e33 (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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
/**CFile****************************************************************

  FileName    [fraig.h]

  PackageName [FRAIG: Functionally reduced AND-INV graphs.]

  Synopsis    [External declarations of the FRAIG package.]

  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 2.0. Started - October 1, 2004]

  Revision    [$Id: fraig.h,v 1.18 2005/07/08 01:01:30 alanmi Exp $]

***********************************************************************/

#ifndef __FRAIG_H__
#define __FRAIG_H__
 
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

typedef struct Fraig_ManStruct_t_         Fraig_Man_t;
typedef struct Fraig_NodeStruct_t_        Fraig_Node_t;
typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;

struct Fraig_ParamsStruct_t_
{
    int  nPatsRand;     // the number of words of random simulation info
    int  nPatsDyna;     // the number of words of dynamic simulation info
    int  nBTLimit;      // the max number of backtracks to perform
    int  fFuncRed;      // performs only one level hashing
    int  fFeedBack;     // enables solver feedback
    int  fDist1Pats;    // enables distance-1 patterns
    int  fDoSparse;     // performs equiv tests for sparse functions 
    int  fChoicing;     // enables recording structural choices
    int  fTryProve;     // tries to solve the final miter
    int  fVerbose;      // the verbosiness flag
    int  fVerboseP;     // the verbosiness flag (for proof reporting)
};

////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                       MACRO DEFITIONS                            ///
////////////////////////////////////////////////////////////////////////
 
// macros working with complemented attributes of the nodes
#define Fraig_IsComplement(p)    (((int)((long) (p) & 01)))
#define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned)(p) & ~01)) 
#define Fraig_Not(p)             ((Fraig_Node_t *)((long)(p) ^ 01)) 
#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((long)(p) ^ (c)))

// these are currently not used
#define Fraig_Ref(p)              
#define Fraig_Deref(p)            
#define Fraig_RecursiveDeref(p,c)

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFITIONS                           ///
////////////////////////////////////////////////////////////////////////

/*=== fraigApi.c =============================================================*/
extern Fraig_NodeVec_t *   Fraig_ManReadVecInputs( Fraig_Man_t * p );
extern Fraig_NodeVec_t *   Fraig_ManReadVecOutputs( Fraig_Man_t * p );    
extern Fraig_NodeVec_t *   Fraig_ManReadVecNodes( Fraig_Man_t * p );      
extern Fraig_Node_t **     Fraig_ManReadInputs ( Fraig_Man_t * p );       
extern Fraig_Node_t **     Fraig_ManReadOutputs( Fraig_Man_t * p );       
extern Fraig_Node_t **     Fraig_ManReadNodes( Fraig_Man_t * p );         
extern int                 Fraig_ManReadInputNum ( Fraig_Man_t * p );     
extern int                 Fraig_ManReadOutputNum( Fraig_Man_t * p );     
extern int                 Fraig_ManReadNodeNum( Fraig_Man_t * p );       
extern Fraig_Node_t *      Fraig_ManReadConst1 ( Fraig_Man_t * p );       
extern Fraig_Node_t *      Fraig_ManReadIthVar( Fraig_Man_t * p, int i ); 
extern Fraig_Node_t *      Fraig_ManReadIthNode( Fraig_Man_t * p, int i );
extern char **             Fraig_ManReadInputNames( Fraig_Man_t * p );    
extern char **             Fraig_ManReadOutputNames( Fraig_Man_t * p );   
extern char *              Fraig_ManReadVarsInt( Fraig_Man_t * p );       
extern char *              Fraig_ManReadSat( Fraig_Man_t * p );           
extern int                 Fraig_ManReadFuncRed( Fraig_Man_t * p );       
extern int                 Fraig_ManReadFeedBack( Fraig_Man_t * p );      
extern int                 Fraig_ManReadDoSparse( Fraig_Man_t * p );      
extern int                 Fraig_ManReadChoicing( Fraig_Man_t * p );      
extern int                 Fraig_ManReadVerbose( Fraig_Man_t * p );       

extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
extern void                Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse );      
extern void                Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ); 
extern void                Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve );
extern void                Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose );        
extern void                Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time );        
extern void                Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time );          
extern void                Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time );          
extern void                Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ); 
extern void                Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames );  
extern void                Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode );

extern Fraig_Node_t *      Fraig_NodeReadData0( Fraig_Node_t * p );                     
extern Fraig_Node_t *      Fraig_NodeReadData1( Fraig_Node_t * p );                     
extern int                 Fraig_NodeReadNum( Fraig_Node_t * p );                       
extern Fraig_Node_t *      Fraig_NodeReadOne( Fraig_Node_t * p );                       
extern Fraig_Node_t *      Fraig_NodeReadTwo( Fraig_Node_t * p );                       
extern Fraig_Node_t *      Fraig_NodeReadNextE( Fraig_Node_t * p );                     
extern Fraig_Node_t *      Fraig_NodeReadRepr( Fraig_Node_t * p );                      
extern int                 Fraig_NodeReadNumRefs( Fraig_Node_t * p );                   
extern int                 Fraig_NodeReadNumFanouts( Fraig_Node_t * p );                
extern int                 Fraig_NodeReadSimInv( Fraig_Node_t * p );                    
extern int                 Fraig_NodeReadNumOnes( Fraig_Node_t * p );

extern void                Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData );
extern void                Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData );

extern int                 Fraig_NodeIsConst( Fraig_Node_t * p );
extern int                 Fraig_NodeIsVar( Fraig_Node_t * p );
extern int                 Fraig_NodeIsAnd( Fraig_Node_t * p );
extern int                 Fraig_NodeComparePhase( Fraig_Node_t * p1, Fraig_Node_t * p2 );

extern Fraig_Node_t *      Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t *      Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t *      Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t *      Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t *      Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_Node_t * pNodeT, Fraig_Node_t * pNodeE );
extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );

/*=== fraigMan.c =============================================================*/
extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
extern void                Fraig_ManFree( Fraig_Man_t * pMan );
extern void                Fraig_ManPrintStats( Fraig_Man_t * p );

/*=== fraigDfs.c =============================================================*/
extern Fraig_NodeVec_t *   Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
extern Fraig_NodeVec_t *   Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv );
extern Fraig_NodeVec_t *   Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv );
extern Fraig_NodeVec_t *   Fraig_DfsReverse( Fraig_Man_t * pMan );
extern int                 Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv );
extern int                 Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );

/*=== fraigSat.c =============================================================*/
extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
extern void                Fraig_ManProveMiter( Fraig_Man_t * p );

/*=== fraigVec.c ===============================================================*/
extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
extern void                Fraig_NodeVecFree( Fraig_NodeVec_t * p );
extern Fraig_NodeVec_t *   Fraig_NodeVecDup( Fraig_NodeVec_t * p );
extern Fraig_Node_t **     Fraig_NodeVecReadArray( Fraig_NodeVec_t * p );
extern int                 Fraig_NodeVecReadSize( Fraig_NodeVec_t * p );
extern void                Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin );
extern void                Fraig_NodeVecShrink( Fraig_NodeVec_t * p, int nSizeNew );
extern void                Fraig_NodeVecClear( Fraig_NodeVec_t * p );
extern void                Fraig_NodeVecPush( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern int                 Fraig_NodeVecPushUnique( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern void                Fraig_NodeVecPushOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern int                 Fraig_NodeVecPushUniqueOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern void                Fraig_NodeVecPushOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern int                 Fraig_NodeVecPushUniqueOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern Fraig_Node_t *      Fraig_NodeVecPop( Fraig_NodeVec_t * p );
extern void                Fraig_NodeVecRemove( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern void                Fraig_NodeVecWriteEntry( Fraig_NodeVec_t * p, int i, Fraig_Node_t * Entry );
extern Fraig_Node_t *      Fraig_NodeVecReadEntry( Fraig_NodeVec_t * p, int i );
extern void                Fraig_NodeVecSortByLevel( Fraig_NodeVec_t * p, int fIncreasing );
extern void                Fraig_NodeVecSortByNumber( Fraig_NodeVec_t * p );

/*=== fraigUtil.c ===============================================================*/
extern void                Fraig_ManMarkRealFanouts( Fraig_Man_t * p );
extern int                 Fraig_ManCheckConsistency( Fraig_Man_t * p );
extern int                 Fraig_GetMaxLevel( Fraig_Man_t * pMan );
extern void                Fraig_ManReportChoices( Fraig_Man_t * pMan );
extern void                Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum );
extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////
#endif