abc70930: src/sat/fraig/fraig.h Source File

00001 
00019 #ifndef __FRAIG_H__
00020 #define __FRAIG_H__
00021 
00022 #ifdef __cplusplus
00023 extern "C" {
00024 #endif
00025 
00029 
00030 #ifndef SINT64
00031 #define SINT64
00032 
00033 #ifdef _WIN32
00034 typedef signed __int64     sint64;   // compatible with MS VS 6.0
00035 #else
00036 typedef long long          sint64;
00037 #endif
00038 
00039 #endif
00040 
00044 
00048 
00049 typedef struct Fraig_ManStruct_t_         Fraig_Man_t;
00050 typedef struct Fraig_NodeStruct_t_        Fraig_Node_t;
00051 typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
00052 typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
00053 typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;
00054 typedef struct Fraig_PatternsStruct_t_    Fraig_Patterns_t;
00055 typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
00056 
00057 struct Fraig_ParamsStruct_t_
00058 {
00059     int  nPatsRand;     // the number of words of random simulation info
00060     int  nPatsDyna;     // the number of words of dynamic simulation info
00061     int  nBTLimit;      // the max number of backtracks to perform
00062     int  nSeconds;      // the timeout for the final proof
00063     int  fFuncRed;      // performs only one level hashing
00064     int  fFeedBack;     // enables solver feedback
00065     int  fDist1Pats;    // enables distance-1 patterns
00066     int  fDoSparse;     // performs equiv tests for sparse functions 
00067     int  fChoicing;     // enables recording structural choices
00068     int  fTryProve;     // tries to solve the final miter
00069     int  fVerbose;      // the verbosiness flag
00070     int  fVerboseP;     // the verbosiness flag (for proof reporting)
00071     int  fInternal;     // is set to 1 for internal fraig calls
00072     int  nConfLimit;    // the limit on the number of conflicts
00073     sint64 nInspLimit;  // the limit on the number of inspections
00074 };
00075 
00076 struct Prove_ParamsStruct_t_
00077 {
00078     // general parameters
00079     int     fUseFraiging;          // enables fraiging
00080     int     fUseRewriting;         // enables rewriting
00081     int     fUseBdds;              // enables BDD construction when other methods fail
00082     int     fVerbose;              // prints verbose stats
00083     // iterations
00084     int     nItersMax;             // the number of iterations
00085     // mitering 
00086     int     nMiteringLimitStart;   // starting mitering limit
00087     float   nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
00088     // rewriting 
00089     int     nRewritingLimitStart;  // the number of rewriting iterations
00090     float   nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
00091     // fraiging 
00092     int     nFraigingLimitStart;   // starting backtrack(conflict) limit
00093     float   nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
00094     // last-gasp BDD construction
00095     int     nBddSizeLimit;         // the number of BDD nodes when construction is aborted
00096     int     fBddReorder;           // enables dynamic BDD variable reordering
00097     // last-gasp mitering
00098     int     nMiteringLimitLast;    // final mitering limit
00099     // global SAT solver limits
00100     sint64  nTotalBacktrackLimit;  // global limit on the number of backtracks
00101     sint64  nTotalInspectLimit;    // global limit on the number of clause inspects
00102     // global resources applied
00103     sint64  nTotalBacktracksMade;  // the total number of backtracks made
00104     sint64  nTotalInspectsMade;    // the total number of inspects made
00105 };
00106 
00110 
00114  
00115 // macros working with complemented attributes of the nodes
00116 #define Fraig_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
00117 #define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned long)(p) & ~01)) 
00118 #define Fraig_Not(p)             ((Fraig_Node_t *)((unsigned long)(p) ^ 01)) 
00119 #define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))
00120 
00121 // these are currently not used
00122 #define Fraig_Ref(p)              
00123 #define Fraig_Deref(p)            
00124 #define Fraig_RecursiveDeref(p,c)
00125 
00129 
00130 /*=== fraigApi.c =============================================================*/
00131 extern Fraig_NodeVec_t *   Fraig_ManReadVecInputs( Fraig_Man_t * p );
00132 extern Fraig_NodeVec_t *   Fraig_ManReadVecOutputs( Fraig_Man_t * p );    
00133 extern Fraig_NodeVec_t *   Fraig_ManReadVecNodes( Fraig_Man_t * p );      
00134 extern Fraig_Node_t **     Fraig_ManReadInputs ( Fraig_Man_t * p );       
00135 extern Fraig_Node_t **     Fraig_ManReadOutputs( Fraig_Man_t * p );       
00136 extern Fraig_Node_t **     Fraig_ManReadNodes( Fraig_Man_t * p );         
00137 extern int                 Fraig_ManReadInputNum ( Fraig_Man_t * p );     
00138 extern int                 Fraig_ManReadOutputNum( Fraig_Man_t * p );     
00139 extern int                 Fraig_ManReadNodeNum( Fraig_Man_t * p );       
00140 extern Fraig_Node_t *      Fraig_ManReadConst1 ( Fraig_Man_t * p );       
00141 extern Fraig_Node_t *      Fraig_ManReadIthVar( Fraig_Man_t * p, int i ); 
00142 extern Fraig_Node_t *      Fraig_ManReadIthNode( Fraig_Man_t * p, int i );
00143 extern char **             Fraig_ManReadInputNames( Fraig_Man_t * p );    
00144 extern char **             Fraig_ManReadOutputNames( Fraig_Man_t * p );   
00145 extern char *              Fraig_ManReadVarsInt( Fraig_Man_t * p );       
00146 extern char *              Fraig_ManReadSat( Fraig_Man_t * p );           
00147 extern int                 Fraig_ManReadFuncRed( Fraig_Man_t * p );       
00148 extern int                 Fraig_ManReadFeedBack( Fraig_Man_t * p );      
00149 extern int                 Fraig_ManReadDoSparse( Fraig_Man_t * p );      
00150 extern int                 Fraig_ManReadChoicing( Fraig_Man_t * p );      
00151 extern int                 Fraig_ManReadVerbose( Fraig_Man_t * p );       
00152 extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
00153 extern int                 Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
00154 extern int                 Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
00155 extern int                 Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
00156 extern int                 Fraig_ManReadSatFails( Fraig_Man_t * p );      
00157 extern int                 Fraig_ManReadConflicts( Fraig_Man_t * p );      
00158 extern int                 Fraig_ManReadInspects( Fraig_Man_t * p );      
00159 
00160 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
00161 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
00162 extern void                Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse );      
00163 extern void                Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ); 
00164 extern void                Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve );
00165 extern void                Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose );        
00166 extern void                Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time );        
00167 extern void                Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time );          
00168 extern void                Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time );          
00169 extern void                Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ); 
00170 extern void                Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames );  
00171 extern void                Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode );
00172 
00173 extern Fraig_Node_t *      Fraig_NodeReadData0( Fraig_Node_t * p );                     
00174 extern Fraig_Node_t *      Fraig_NodeReadData1( Fraig_Node_t * p );                     
00175 extern int                 Fraig_NodeReadNum( Fraig_Node_t * p );                       
00176 extern Fraig_Node_t *      Fraig_NodeReadOne( Fraig_Node_t * p );                       
00177 extern Fraig_Node_t *      Fraig_NodeReadTwo( Fraig_Node_t * p );                       
00178 extern Fraig_Node_t *      Fraig_NodeReadNextE( Fraig_Node_t * p );                     
00179 extern Fraig_Node_t *      Fraig_NodeReadRepr( Fraig_Node_t * p );                      
00180 extern int                 Fraig_NodeReadNumRefs( Fraig_Node_t * p );                   
00181 extern int                 Fraig_NodeReadNumFanouts( Fraig_Node_t * p );                
00182 extern int                 Fraig_NodeReadSimInv( Fraig_Node_t * p );                    
00183 extern int                 Fraig_NodeReadNumOnes( Fraig_Node_t * p );
00184 extern unsigned *          Fraig_NodeReadPatternsRandom( Fraig_Node_t * p );
00185 extern unsigned *          Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p );
00186 
00187 extern void                Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData );
00188 extern void                Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData );
00189 
00190 extern int                 Fraig_NodeIsConst( Fraig_Node_t * p );
00191 extern int                 Fraig_NodeIsVar( Fraig_Node_t * p );
00192 extern int                 Fraig_NodeIsAnd( Fraig_Node_t * p );
00193 extern int                 Fraig_NodeComparePhase( Fraig_Node_t * p1, Fraig_Node_t * p2 );
00194 
00195 extern Fraig_Node_t *      Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
00196 extern Fraig_Node_t *      Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
00197 extern Fraig_Node_t *      Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
00198 extern Fraig_Node_t *      Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
00199 extern Fraig_Node_t *      Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_Node_t * pNodeT, Fraig_Node_t * pNodeE );
00200 extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );
00201 
00202 /*=== fraigMan.c =============================================================*/
00203 extern void                Prove_ParamsSetDefault( Prove_Params_t * pParams );
00204 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
00205 extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
00206 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
00207 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
00208 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
00209 extern Fraig_NodeVec_t *   Fraig_ManGetSimInfo( Fraig_Man_t * p );
00210 extern int                 Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
00211 extern void                Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
00212 
00213 /*=== fraigDfs.c =============================================================*/
00214 extern Fraig_NodeVec_t *   Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
00215 extern Fraig_NodeVec_t *   Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv );
00216 extern Fraig_NodeVec_t *   Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv );
00217 extern Fraig_NodeVec_t *   Fraig_DfsReverse( Fraig_Man_t * pMan );
00218 extern int                 Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv );
00219 extern int                 Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
00220 extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );
00221 
00222 /*=== fraigSat.c =============================================================*/
00223 extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit );
00224 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
00225 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
00226 extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
00227 extern int                 Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
00228 
00229 /*=== fraigVec.c ===============================================================*/
00230 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
00231 extern void                Fraig_NodeVecFree( Fraig_NodeVec_t * p );
00232 extern Fraig_NodeVec_t *   Fraig_NodeVecDup( Fraig_NodeVec_t * p );
00233 extern Fraig_Node_t **     Fraig_NodeVecReadArray( Fraig_NodeVec_t * p );
00234 extern int                 Fraig_NodeVecReadSize( Fraig_NodeVec_t * p );
00235 extern void                Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin );
00236 extern void                Fraig_NodeVecShrink( Fraig_NodeVec_t * p, int nSizeNew );
00237 extern void                Fraig_NodeVecClear( Fraig_NodeVec_t * p );
00238 extern void                Fraig_NodeVecPush( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
00239 extern int                 Fraig_NodeVecPushUnique( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
00240 extern void                Fraig_NodeVecPushOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
00241 extern int                 Fraig_NodeVecPushUniqueOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
00242 extern void                Fraig_NodeVecPushOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
00243 extern int                 Fraig_NodeVecPushUniqueOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
00244 extern Fraig_Node_t *      Fraig_NodeVecPop( Fraig_NodeVec_t * p );
00245 extern void                Fraig_NodeVecRemove( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
00246 extern void                Fraig_NodeVecWriteEntry( Fraig_NodeVec_t * p, int i, Fraig_Node_t * Entry );
00247 extern Fraig_Node_t *      Fraig_NodeVecReadEntry( Fraig_NodeVec_t * p, int i );
00248 extern void                Fraig_NodeVecSortByLevel( Fraig_NodeVec_t * p, int fIncreasing );
00249 extern void                Fraig_NodeVecSortByNumber( Fraig_NodeVec_t * p );
00250 
00251 /*=== fraigUtil.c ===============================================================*/
00252 extern void                Fraig_ManMarkRealFanouts( Fraig_Man_t * p );
00253 extern int                 Fraig_ManCheckConsistency( Fraig_Man_t * p );
00254 extern int                 Fraig_GetMaxLevel( Fraig_Man_t * pMan );
00255 extern void                Fraig_ManReportChoices( Fraig_Man_t * pMan );
00256 extern void                Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum );
00257 extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );
00258 
00262  
00263 #ifdef __cplusplus
00264 }
00265 #endif
00266 
00267 #endif