| /**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 ABC__sat__fraig__fraig_h |
| #define ABC__sat__fraig__fraig_h |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// INCLUDES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// PARAMETERS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| |
| ABC_NAMESPACE_HEADER_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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; |
| typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t; |
| typedef struct Prove_ParamsStruct_t_ Prove_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 nSeconds; // the timeout for the final proof |
| 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) |
| int fInternal; // is set to 1 for internal fraig calls |
| int nConfLimit; // the limit on the number of conflicts |
| ABC_INT64_T nInspLimit; // the limit on the number of inspections |
| }; |
| |
| struct Prove_ParamsStruct_t_ |
| { |
| // general parameters |
| int fUseFraiging; // enables fraiging |
| int fUseRewriting; // enables rewriting |
| int fUseBdds; // enables BDD construction when other methods fail |
| int fVerbose; // prints verbose stats |
| // iterations |
| int nItersMax; // the number of iterations |
| // mitering |
| int nMiteringLimitStart; // starting mitering limit |
| float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration |
| // rewriting |
| int nRewritingLimitStart; // the number of rewriting iterations |
| float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration |
| // fraiging |
| int nFraigingLimitStart; // starting backtrack(conflict) limit |
| float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration |
| // last-gasp BDD construction |
| int nBddSizeLimit; // the number of BDD nodes when construction is aborted |
| int fBddReorder; // enables dynamic BDD variable reordering |
| // last-gasp mitering |
| int nMiteringLimitLast; // final mitering limit |
| // global SAT solver limits |
| ABC_INT64_T nTotalBacktrackLimit; // global limit on the number of backtracks |
| ABC_INT64_T nTotalInspectLimit; // global limit on the number of clause inspects |
| // global resources applied |
| ABC_INT64_T nTotalBacktracksMade; // the total number of backtracks made |
| ABC_INT64_T nTotalInspectsMade; // the total number of inspects made |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// GLOBAL VARIABLES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// MACRO DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // macros working with complemented attributes of the nodes |
| #define Fraig_IsComplement(p) (((int)((ABC_PTRUINT_T) (p) & 01))) |
| #define Fraig_Regular(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) |
| #define Fraig_Not(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) |
| #define Fraig_NotCond(p,c) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c))) |
| |
| // these are currently not used |
| #define Fraig_Ref(p) |
| #define Fraig_Deref(p) |
| #define Fraig_RecursiveDeref(p,c) |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /*=== 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 int * Fraig_ManReadModel( Fraig_Man_t * p ); |
| extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ); |
| extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ); |
| extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ); |
| extern int Fraig_ManReadSatFails( Fraig_Man_t * p ); |
| extern int Fraig_ManReadConflicts( Fraig_Man_t * p ); |
| extern int Fraig_ManReadInspects( 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_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 unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ); |
| extern unsigned * Fraig_NodeReadPatternsDynamic( 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 Prove_ParamsSetDefault( Prove_Params_t * pParams ); |
| extern void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ); |
| extern void Fraig_ParamsSetDefaultFull( 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 ); |
| extern Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p ); |
| extern int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ); |
| extern void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes ); |
| |
| /*=== 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, int nTimeLimit ); |
| extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ); |
| extern void Fraig_ManProveMiter( Fraig_Man_t * p ); |
| extern int Fraig_ManCheckMiter( Fraig_Man_t * p ); |
| extern int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ); |
| |
| /*=== 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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| |
| ABC_NAMESPACE_HEADER_END |
| |
| |
| |
| #endif |
