From 888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2005 08:01:00 -0700 Subject: Version abc50729 --- src/sat/fraig/fraig.h | 194 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) create mode 100644 src/sat/fraig/fraig.h (limited to 'src/sat/fraig/fraig.h') diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h new file mode 100644 index 00000000..53a46584 --- /dev/null +++ b/src/sat/fraig/fraig.h @@ -0,0 +1,194 @@ +/**CFile**************************************************************** + + FileName [fraig.h] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [External declarations of the FRAIG package.] + + Author [Alan Mishchenko ] + + 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 -- cgit v1.2.3