diff options
Diffstat (limited to 'src/sat/fraig')
| -rw-r--r-- | src/sat/fraig/fraig.h | 267 | ||||
| -rw-r--r-- | src/sat/fraig/fraigApi.c | 297 | ||||
| -rw-r--r-- | src/sat/fraig/fraigCanon.c | 218 | ||||
| -rw-r--r-- | src/sat/fraig/fraigChoice.c | 241 | ||||
| -rw-r--r-- | src/sat/fraig/fraigFanout.c | 175 | ||||
| -rw-r--r-- | src/sat/fraig/fraigFeed.c | 909 | ||||
| -rw-r--r-- | src/sat/fraig/fraigInt.h | 451 | ||||
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 540 | ||||
| -rw-r--r-- | src/sat/fraig/fraigMem.c | 246 | ||||
| -rw-r--r-- | src/sat/fraig/fraigNode.c | 313 | ||||
| -rw-r--r-- | src/sat/fraig/fraigPrime.c | 144 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 1455 | ||||
| -rw-r--r-- | src/sat/fraig/fraigTable.c | 657 | ||||
| -rw-r--r-- | src/sat/fraig/fraigUtil.c | 1034 | ||||
| -rw-r--r-- | src/sat/fraig/fraigVec.c | 545 | ||||
| -rw-r--r-- | src/sat/fraig/module.make | 12 |
16 files changed, 7504 insertions, 0 deletions
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h new file mode 100644 index 00000000..1dad21e2 --- /dev/null +++ b/src/sat/fraig/fraig.h @@ -0,0 +1,267 @@ +/**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__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#ifndef SINT64 +#define SINT64 + +#ifdef _WIN32 +typedef signed __int64 sint64; // compatible with MS VS 6.0 +#else +typedef long long sint64; +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// 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; +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 + sint64 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 + sint64 nTotalBacktrackLimit; // global limit on the number of backtracks + sint64 nTotalInspectLimit; // global limit on the number of clause inspects + // global resources applied + sint64 nTotalBacktracksMade; // the total number of backtracks made + sint64 nTotalInspectsMade; // the total number of inspects made +}; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// macros working with complemented attributes of the nodes +#define Fraig_IsComplement(p) (((int)((unsigned long) (p) & 01))) +#define Fraig_Regular(p) ((Fraig_Node_t *)((unsigned long)(p) & ~01)) +#define Fraig_Not(p) ((Fraig_Node_t *)((unsigned long)(p) ^ 01)) +#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((unsigned long)(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_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 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 /// +//////////////////////////////////////////////////////////////////////// + +#ifdef __cplusplus +} +#endif + +#endif diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c new file mode 100644 index 00000000..79a7c224 --- /dev/null +++ b/src/sat/fraig/fraigApi.c @@ -0,0 +1,297 @@ +/**CFile**************************************************************** + + FileName [fraigApi.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Access APIs for the FRAIG manager and node.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigApi.c,v 1.2 2005/07/08 01:01:30 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Access functions to read the data members of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_ManReadVecInputs( Fraig_Man_t * p ) { return p->vInputs; } +Fraig_NodeVec_t * Fraig_ManReadVecOutputs( Fraig_Man_t * p ) { return p->vOutputs; } +Fraig_NodeVec_t * Fraig_ManReadVecNodes( Fraig_Man_t * p ) { return p->vNodes; } +Fraig_Node_t ** Fraig_ManReadInputs ( Fraig_Man_t * p ) { return p->vInputs->pArray; } +Fraig_Node_t ** Fraig_ManReadOutputs( Fraig_Man_t * p ) { return p->vOutputs->pArray; } +Fraig_Node_t ** Fraig_ManReadNodes( Fraig_Man_t * p ) { return p->vNodes->pArray; } +int Fraig_ManReadInputNum ( Fraig_Man_t * p ) { return p->vInputs->nSize; } +int Fraig_ManReadOutputNum( Fraig_Man_t * p ) { return p->vOutputs->nSize; } +int Fraig_ManReadNodeNum( Fraig_Man_t * p ) { return p->vNodes->nSize; } +Fraig_Node_t * Fraig_ManReadConst1 ( Fraig_Man_t * p ) { return p->pConst1; } +Fraig_Node_t * Fraig_ManReadIthNode( Fraig_Man_t * p, int i ) { assert ( i < p->vNodes->nSize ); return p->vNodes->pArray[i]; } +char ** Fraig_ManReadInputNames( Fraig_Man_t * p ) { return p->ppInputNames; } +char ** Fraig_ManReadOutputNames( Fraig_Man_t * p ) { return p->ppOutputNames; } +char * Fraig_ManReadVarsInt( Fraig_Man_t * p ) { return (char *)p->vVarsInt; } +char * Fraig_ManReadSat( Fraig_Man_t * p ) { return (char *)p->pSat; } +int Fraig_ManReadFuncRed( Fraig_Man_t * p ) { return p->fFuncRed; } +int Fraig_ManReadFeedBack( Fraig_Man_t * p ) { return p->fFeedBack; } +int Fraig_ManReadDoSparse( Fraig_Man_t * p ) { return p->fDoSparse; } +int Fraig_ManReadChoicing( Fraig_Man_t * p ) { return p->fChoicing; } +int Fraig_ManReadVerbose( Fraig_Man_t * p ) { return p->fVerbose; } +int * Fraig_ManReadModel( Fraig_Man_t * p ) { return p->pModel; } +// returns the number of patterns used for random simulation (this number is fixed for the FRAIG run) +int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ) { return p->nWordsRand * 32; } +// returns the number of dynamic patterns accumulated at runtime (include SAT solver counter-examples and distance-1 patterns derived from them) +int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { return p->iWordStart * 32; } +// returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns) +int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } +// returns the number of times FRAIG package timed out +int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFailsReal; } +// returns the number of conflicts in the SAT solver +int Fraig_ManReadConflicts( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; } +// returns the number of inspections in the SAT solver +int Fraig_ManReadInspects( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadInspects(p->pSat) : 0; } + +/**Function************************************************************* + + Synopsis [Access functions to set the data members of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed ) { p->fFuncRed = fFuncRed; } +void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack ) { p->fFeedBack = fFeedBack; } +void Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse ) { p->fDoSparse = fDoSparse; } +void Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ) { p->fChoicing = fChoicing; } +void Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve ) { p->fTryProve = fTryProve; } +void Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose ) { p->fVerbose = fVerbose; } +void Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time ) { p->timeToAig = Time; } +void Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time ) { p->timeToNet = Time; } +void Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time ) { p->timeTotal = Time; } +void Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppOutputNames = ppNames; } +void Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppInputNames = ppNames; } + +/**Function************************************************************* + + Synopsis [Access functions to read the data members of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeReadData0( Fraig_Node_t * p ) { return p->pData0; } +Fraig_Node_t * Fraig_NodeReadData1( Fraig_Node_t * p ) { return p->pData1; } +int Fraig_NodeReadNum( Fraig_Node_t * p ) { return p->Num; } +Fraig_Node_t * Fraig_NodeReadOne( Fraig_Node_t * p ) { assert (!Fraig_IsComplement(p)); return p->p1; } +Fraig_Node_t * Fraig_NodeReadTwo( Fraig_Node_t * p ) { assert (!Fraig_IsComplement(p)); return p->p2; } +Fraig_Node_t * Fraig_NodeReadNextE( Fraig_Node_t * p ) { return p->pNextE; } +Fraig_Node_t * Fraig_NodeReadRepr( Fraig_Node_t * p ) { return p->pRepr; } +int Fraig_NodeReadNumRefs( Fraig_Node_t * p ) { return p->nRefs; } +int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ) { return p->nFanouts; } +int Fraig_NodeReadSimInv( Fraig_Node_t * p ) { return p->fInv; } +int Fraig_NodeReadNumOnes( Fraig_Node_t * p ) { return p->nOnes; } +// returns the pointer to the random simulation patterns (their number is returned by Fraig_ManReadPatternNumRandom) +// memory pointed to by this and the following procedure is maintained by the FRAIG package and exists as long as the package runs +unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ) { return p->puSimR; } +// returns the pointer to the dynamic simulation patterns (their number is returned by Fraig_ManReadPatternNumDynamic or Fraig_ManReadPatternNumDynamicFiltered) +// if the number of patterns is not evenly divisible by 32, the patterns beyond the given number contain garbage +unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ) { return p->puSimD; } + +/**Function************************************************************* + + Synopsis [Access functions to set the data members of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData ) { p->pData0 = pData; } +void Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData ) { p->pData1 = pData; } + +/**Function************************************************************* + + Synopsis [Checks the type of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsConst( Fraig_Node_t * p ) { return (Fraig_Regular(p))->Num == 0; } +int Fraig_NodeIsVar( Fraig_Node_t * p ) { return (Fraig_Regular(p))->NumPi >= 0; } +int Fraig_NodeIsAnd( Fraig_Node_t * p ) { return (Fraig_Regular(p))->NumPi < 0 && (Fraig_Regular(p))->Num > 0; } +int Fraig_NodeComparePhase( Fraig_Node_t * p1, Fraig_Node_t * p2 ) { assert( !Fraig_IsComplement(p1) ); assert( !Fraig_IsComplement(p2) ); return p1->fInv ^ p2->fInv; } + +/**Function************************************************************* + + Synopsis [Returns a new primary input node.] + + Description [If the node with this number does not exist, + create a new PI node with this number.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i ) +{ + int k; + if ( i < 0 ) + { + printf( "Requesting a PI with a negative number\n" ); + return NULL; + } + // create the PIs to fill in the interval + if ( i >= p->vInputs->nSize ) + for ( k = p->vInputs->nSize; k <= i; k++ ) + Fraig_NodeCreatePi( p ); + return p->vInputs->pArray[i]; +} + +/**Function************************************************************* + + Synopsis [Creates a new PO node.] + + Description [This procedure may take a complemented node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + // internal node may be a PO two times + Fraig_Regular(pNode)->fNodePo = 1; + Fraig_NodeVecPush( p->vOutputs, pNode ); +} + +/**Function************************************************************* + + Synopsis [Perfoms the AND operation with functional hashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ) +{ + return Fraig_NodeAndCanon( p, p1, p2 ); +} + +/**Function************************************************************* + + Synopsis [Perfoms the OR operation with functional hashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ) +{ + return Fraig_Not( Fraig_NodeAndCanon( p, Fraig_Not(p1), Fraig_Not(p2) ) ); +} + +/**Function************************************************************* + + Synopsis [Perfoms the EXOR operation with functional hashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ) +{ + return Fraig_NodeMux( p, p1, Fraig_Not(p2), p2 ); +} + +/**Function************************************************************* + + Synopsis [Perfoms the MUX operation with functional hashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pC, Fraig_Node_t * pT, Fraig_Node_t * pE ) +{ + Fraig_Node_t * pAnd1, * pAnd2, * pRes; + pAnd1 = Fraig_NodeAndCanon( p, pC, pT ); Fraig_Ref( pAnd1 ); + pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE ); Fraig_Ref( pAnd2 ); + pRes = Fraig_NodeOr( p, pAnd1, pAnd2 ); + Fraig_RecursiveDeref( p, pAnd1 ); + Fraig_RecursiveDeref( p, pAnd2 ); + Fraig_Deref( pRes ); + return pRes; +} + + +/**Function************************************************************* + + Synopsis [Sets the node to be equivalent to the given one.] + + Description [This procedure is a work-around for the equivalence check. + Does not verify the equivalence. Use at the user's risk.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew ) +{ +// assert( pMan->fChoicing ); + pNodeNew->pNextE = pNodeOld->pNextE; + pNodeOld->pNextE = pNodeNew; + pNodeNew->pRepr = pNodeOld; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c new file mode 100644 index 00000000..89bc924f --- /dev/null +++ b/src/sat/fraig/fraigCanon.c @@ -0,0 +1,218 @@ +/**CFile**************************************************************** + + FileName [fraigCanon.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [AND-node creation and elementary AND-operation.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigCanon.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include <limits.h> +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [The internal AND operation for the two FRAIG nodes.] + + Description [This procedure is the core of the FRAIG package, because + it performs the two-step canonicization of FRAIG nodes. The first step + involves the lookup in the structural hash table (which hashes two ANDs + into a node that has them as fanins, if such a node exists). If the node + is not found in the structural hash table, an attempt is made to find a + functionally equivalent node in another hash table (which hashes the + simulation info into the nodes, which has this simulation info). Some + tricks used on the way are described in the comments to the code and + in the paper "FRAIGs: Functionally reduced AND-INV graphs".] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 ) +{ + Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr; + int fUseSatCheck; +// int RetValue; + + // check for trivial cases + if ( p1 == p2 ) + return p1; + if ( p1 == Fraig_Not(p2) ) + return Fraig_Not(pMan->pConst1); + if ( Fraig_NodeIsConst(p1) ) + { + if ( p1 == pMan->pConst1 ) + return p2; + return Fraig_Not(pMan->pConst1); + } + if ( Fraig_NodeIsConst(p2) ) + { + if ( p2 == pMan->pConst1 ) + return p1; + return Fraig_Not(pMan->pConst1); + } +/* + // check for less trivial cases + if ( Fraig_IsComplement(p1) ) + { + if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p1), p2 ) ) + { + if ( RetValue == -1 ) + pMan->nImplies0++; + else + pMan->nImplies1++; + + if ( RetValue == -1 ) + return p2; + } + } + else + { + if ( RetValue = Fraig_NodeIsInSupergate( p1, p2 ) ) + { + if ( RetValue == 1 ) + pMan->nSimplifies1++; + else + pMan->nSimplifies0++; + + if ( RetValue == 1 ) + return p1; + return Fraig_Not(pMan->pConst1); + } + } + + if ( Fraig_IsComplement(p2) ) + { + if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p2), p1 ) ) + { + if ( RetValue == -1 ) + pMan->nImplies0++; + else + pMan->nImplies1++; + + if ( RetValue == -1 ) + return p1; + } + } + else + { + if ( RetValue = Fraig_NodeIsInSupergate( p2, p1 ) ) + { + if ( RetValue == 1 ) + pMan->nSimplifies1++; + else + pMan->nSimplifies0++; + + if ( RetValue == 1 ) + return p2; + return Fraig_Not(pMan->pConst1); + } + } +*/ + // perform level-one structural hashing + if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found + { + // if the existent node is part of the cone of unused logic + // (that is logic feeding the node which is equivalent to the given node) + // return the canonical representative of this node + // determine the phase of the given node, with respect to its canonical form + pNodeRepr = Fraig_Regular(pNodeNew)->pRepr; + if ( pMan->fFuncRed && pNodeRepr ) + return Fraig_NotCond( pNodeRepr, Fraig_IsComplement(pNodeNew) ^ Fraig_NodeComparePhase(Fraig_Regular(pNodeNew), pNodeRepr) ); + // otherwise, the node is itself a canonical representative, return it + return pNodeNew; + } + // the same node is not found, but the new one is created + + // if one level hashing is requested (without functionality hashing), return + if ( !pMan->fFuncRed ) + return pNodeNew; + + // check if the new node is unique using the simulation info + if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 ) + { + pMan->nSatZeros++; + if ( !pMan->fDoSparse ) // if we do not do sparse functions, skip + return pNodeNew; + // check the sparse function simulation hash table + pNodeOld = Fraig_HashTableLookupF0( pMan, pNodeNew ); + if ( pNodeOld == NULL ) // the node is unique (it is added to the table) + return pNodeNew; + } + else + { + // check the simulation hash table + pNodeOld = Fraig_HashTableLookupF( pMan, pNodeNew ); + if ( pNodeOld == NULL ) // the node is unique + return pNodeNew; + } + assert( pNodeOld->pRepr == 0 ); + // there is another node which looks the same according to simulation + + // use SAT to resolve the ambiguity + fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); + if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) ) + { + // set the node to be equivalent with this node + // to prevent loops, only set if the old node is not in the TFI of the new node + // the loop may happen in the following case: suppose + // NodeC = AND(NodeA, NodeB) and at the same time NodeA => NodeB + // in this case, NodeA and NodeC are functionally equivalent + // however, NodeA is a fanin of node NodeC (this leads to the loop) + // add the node to the list of equivalent nodes or dereference it + if ( pMan->fChoicing && !Fraig_CheckTfi( pMan, pNodeOld, pNodeNew ) ) + { + // if the old node is not in the TFI of the new node and choicing + // is enabled, add the new node to the list of equivalent ones + pNodeNew->pNextE = pNodeOld->pNextE; + pNodeOld->pNextE = pNodeNew; + } + // set the canonical representative of this node + pNodeNew->pRepr = pNodeOld; + // return the equivalent node + return Fraig_NotCond( pNodeOld, Fraig_NodeComparePhase(pNodeOld, pNodeNew) ); + } + + // now we add another member to this simulation class + if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 ) + { + Fraig_Node_t * pNodeTemp; + assert( pMan->fDoSparse ); + pNodeTemp = Fraig_HashTableLookupF0( pMan, pNodeNew ); +// assert( pNodeTemp == NULL ); +// Fraig_HashTableInsertF0( pMan, pNodeNew ); + } + else + { + pNodeNew->pNextD = pNodeOld->pNextD; + pNodeOld->pNextD = pNodeNew; + } + // return the new node + assert( pNodeNew->pRepr == 0 ); + return pNodeNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigChoice.c b/src/sat/fraig/fraigChoice.c new file mode 100644 index 00000000..896e5d2d --- /dev/null +++ b/src/sat/fraig/fraigChoice.c @@ -0,0 +1,241 @@ +/**CFile**************************************************************** + + FileName [fraigTrans.c] + + PackageName [MVSIS 1.3: Multi-valued logic synthesis system.] + + Synopsis [Adds the additive and distributive choices to the AIG.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: fraigTrans.c,v 1.1 2005/02/28 05:34:34 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds choice nodes based on associativity.] + + Description [Make nLimit big AND gates and add all decompositions + to the Fraig.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit ) +{ +// ProgressBar * pProgress; + char Buffer[100]; + int clkTotal = clock(); + int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes; + int /*nMaxLevel,*/ nDistributive; + Fraig_Node_t *pNode, *pRepr; + Fraig_Node_t *pX, *pA, *pB, *pC, /* *pD,*/ *pN, /* *pQ, *pR,*/ *pT; + int fShortCut = 0; + + nDistributive = 0; + +// Fraig_ManSetApprox( pMan, 1 ); + + // NO functional reduction + if (fShortCut) Fraig_ManSetFuncRed( pMan, 0 ); + + // First we mark critical functions i.e. compute those + // nodes which lie on the critical path. Note that this + // doesn't update the required times on any choice nodes + // which are not the representatives +/* + nMaxLevel = Fraig_GetMaxLevel( pMan ); + for ( i = 0; i < pMan->nOutputs; i++ ) + { + Fraig_SetNodeRequired( pMan, pMan->pOutputs[i], nMaxLevel ); + } +*/ + nNodesBefore = Fraig_ManReadNodeNum( pMan ); + nInputs = Fraig_ManReadInputNum( pMan ); + nMaxNodes = nInputs + nLimit * ( nNodesBefore - nInputs ); + + printf ("Limit = %d, Before = %d\n", nMaxNodes, nNodesBefore ); + + if (0) + { + char buffer[128]; + sprintf (buffer, "test" ); +// Fraig_MappingShow( pMan, buffer ); + } + +// pProgress = Extra_ProgressBarStart( stdout, nMaxNodes ); +Fraig_ManCheckConsistency( pMan ); + + for ( i = nInputs+1; (i < Fraig_ManReadNodeNum( pMan )) + && (nMaxNodes > Fraig_ManReadNodeNum( pMan )); ++i ) + { +// if ( i == nNodesBefore ) +// break; + + pNode = Fraig_ManReadIthNode( pMan, i ); + assert ( pNode ); + + pRepr = pNode->pRepr ? pNode->pRepr : pNode; + //printf ("Slack: %d\n", Fraig_NodeReadSlack( pRepr )); + + // All the new associative choices we add will have huge slack + // since we do not redo timing, and timing doesnt handle choices + // well anyway. However every newly added node is a choice of an + // existing critical node, so they are considered critical. +// if ( (Fraig_NodeReadSlack( pRepr ) > 3) && (i < nNodesBefore) ) +// continue; + +// if ( pNode->pRepr ) +// continue; + + // Try ((ab)c), x = ab -> (a(bc)) and (b(ac)) + pX = Fraig_NodeReadOne(pNode); + pC = Fraig_NodeReadTwo(pNode); + if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX)) + { + pA = Fraig_NodeReadOne(Fraig_Regular(pX)); + pB = Fraig_NodeReadTwo(Fraig_Regular(pX)); + +// pA = Fraig_NodeGetRepr( pA ); +// pB = Fraig_NodeGetRepr( pB ); +// pC = Fraig_NodeGetRepr( pC ); + + if (fShortCut) + { + pT = Fraig_NodeAnd(pMan, pB, pC); + if ( !pT->pRepr ) + { + pN = Fraig_NodeAnd(pMan, pA, pT); +// Fraig_NodeAddChoice( pMan, pNode, pN ); + } + } + else + pN = Fraig_NodeAnd(pMan, pA, Fraig_NodeAnd(pMan, pB, pC)); + // assert ( Fraig_NodesEqual(pN, pNode) ); + + + if (fShortCut) + { + pT = Fraig_NodeAnd(pMan, pA, pC); + if ( !pT->pRepr ) + { + pN = Fraig_NodeAnd(pMan, pB, pT); +// Fraig_NodeAddChoice( pMan, pNode, pN ); + } + } + else + pN = Fraig_NodeAnd(pMan, pB, Fraig_NodeAnd(pMan, pA, pC)); + // assert ( Fraig_NodesEqual(pN, pNode) ); + } + + + // Try (a(bc)), x = bc -> ((ab)c) and ((ac)b) + pA = Fraig_NodeReadOne(pNode); + pX = Fraig_NodeReadTwo(pNode); + if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX)) + { + pB = Fraig_NodeReadOne(Fraig_Regular(pX)); + pC = Fraig_NodeReadTwo(Fraig_Regular(pX)); + +// pA = Fraig_NodeGetRepr( pA ); +// pB = Fraig_NodeGetRepr( pB ); +// pC = Fraig_NodeGetRepr( pC ); + + if (fShortCut) + { + pT = Fraig_NodeAnd(pMan, pA, pB); + if ( !pT->pRepr ) + { + pN = Fraig_NodeAnd(pMan, pC, pT); +// Fraig_NodeAddChoice( pMan, pNode, pN ); + } + } + else + pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pB), pC); + // assert ( Fraig_NodesEqual(pN, pNode) ); + + if (fShortCut) + { + pT = Fraig_NodeAnd(pMan, pA, pC); + if ( !pT->pRepr ) + { + pN = Fraig_NodeAnd(pMan, pB, pT); +// Fraig_NodeAddChoice( pMan, pNode, pN ); + } + } + else + pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pC), pB); + // assert ( Fraig_NodesEqual(pN, pNode) ); + } + + +/* + // Try distributive transform + pQ = Fraig_NodeReadOne(pNode); + pR = Fraig_NodeReadTwo(pNode); + if ( (Fraig_IsComplement(pQ) && Fraig_NodeIsAnd(pQ)) + && (Fraig_IsComplement(pR) && Fraig_NodeIsAnd(pR)) ) + { + pA = Fraig_NodeReadOne(Fraig_Regular(pQ)); + pB = Fraig_NodeReadTwo(Fraig_Regular(pQ)); + pC = Fraig_NodeReadOne(Fraig_Regular(pR)); + pD = Fraig_NodeReadTwo(Fraig_Regular(pR)); + + // Now detect the !(xy + xz) pattern, store + // x in pA, y in pB and z in pC and set pD = 0 to indicate + // pattern was found + assert (pD != 0); + if (pA == pC) { pC = pD; pD = 0; } + if (pA == pD) { pD = 0; } + if (pB == pC) { pB = pA; pA = pC; pC = pD; pD = 0; } + if (pB == pD) { pB = pA; pA = pD; pD = 0; } + if (pD == 0) + { + nDistributive++; + pN = Fraig_Not(Fraig_NodeAnd(pMan, pA, + Fraig_NodeOr(pMan, pB, pC))); + if (fShortCut) Fraig_NodeAddChoice( pMan, pNode, pN ); + // assert ( Fraig_NodesEqual(pN, pNode) ); + } + } +*/ + if ( i % 1000 == 0 ) + { + sprintf( Buffer, "Adding choice %6d...", i - nNodesBefore ); +// Extra_ProgressBarUpdate( pProgress, i, Buffer ); + } + } + +// Extra_ProgressBarStop( pProgress ); + +Fraig_ManCheckConsistency( pMan ); + + nNodesAfter = Fraig_ManReadNodeNum( pMan ); + printf ( "Nodes before = %6d. Nodes with associative choices = %6d. Increase = %4.2f %%.\n", + nNodesBefore, nNodesAfter, ((float)(nNodesAfter - nNodesBefore)) * 100.0/(nNodesBefore - nInputs) ); + printf ( "Distributive = %d\n", nDistributive ); + +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigFanout.c b/src/sat/fraig/fraigFanout.c new file mode 100644 index 00000000..789bffca --- /dev/null +++ b/src/sat/fraig/fraigFanout.c @@ -0,0 +1,175 @@ +/**CFile**************************************************************** + + FileName [fraigFanout.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Procedures to manipulate fanouts of the FRAIG nodes.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigFanout.c,v 1.5 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +#ifdef FRAIG_ENABLE_FANOUTS + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Add the fanout to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeAddFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanout ) +{ + Fraig_Node_t * pPivot; + + // pFanins is a fanin of pFanout + assert( !Fraig_IsComplement(pFanin) ); + assert( !Fraig_IsComplement(pFanout) ); + assert( Fraig_Regular(pFanout->p1) == pFanin || Fraig_Regular(pFanout->p2) == pFanin ); + + pPivot = pFanin->pFanPivot; + if ( pPivot == NULL ) + { + pFanin->pFanPivot = pFanout; + return; + } + + if ( Fraig_Regular(pPivot->p1) == pFanin ) + { + if ( Fraig_Regular(pFanout->p1) == pFanin ) + { + pFanout->pFanFanin1 = pPivot->pFanFanin1; + pPivot->pFanFanin1 = pFanout; + } + else // if ( Fraig_Regular(pFanout->p2) == pFanin ) + { + pFanout->pFanFanin2 = pPivot->pFanFanin1; + pPivot->pFanFanin1 = pFanout; + } + } + else // if ( Fraig_Regular(pPivot->p2) == pFanin ) + { + assert( Fraig_Regular(pPivot->p2) == pFanin ); + if ( Fraig_Regular(pFanout->p1) == pFanin ) + { + pFanout->pFanFanin1 = pPivot->pFanFanin2; + pPivot->pFanFanin2 = pFanout; + } + else // if ( Fraig_Regular(pFanout->p2) == pFanin ) + { + pFanout->pFanFanin2 = pPivot->pFanFanin2; + pPivot->pFanFanin2 = pFanout; + } + } +} + +/**Function************************************************************* + + Synopsis [Add the fanout to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeRemoveFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanoutToRemove ) +{ + Fraig_Node_t * pFanout, * pFanout2, ** ppFanList; + // start the linked list of fanouts + ppFanList = &pFanin->pFanPivot; + // go through the fanouts + Fraig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 ) + { + // skip the fanout-to-remove + if ( pFanout == pFanoutToRemove ) + continue; + // add useful fanouts to the list + *ppFanList = pFanout; + ppFanList = Fraig_NodeReadNextFanoutPlace( pFanin, pFanout ); + } + *ppFanList = NULL; +} + +/**Function************************************************************* + + Synopsis [Transfers fanout to a different node.] + + Description [Assumes that the other node currently has no fanouts.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeTransferFanout( Fraig_Node_t * pNodeFrom, Fraig_Node_t * pNodeTo ) +{ + Fraig_Node_t * pFanout; + assert( pNodeTo->pFanPivot == NULL ); + assert( pNodeTo->pFanFanin1 == NULL ); + assert( pNodeTo->pFanFanin2 == NULL ); + // go through the fanouts and update their fanins + Fraig_NodeForEachFanout( pNodeFrom, pFanout ) + { + if ( Fraig_Regular(pFanout->p1) == pNodeFrom ) + pFanout->p1 = Fraig_NotCond( pNodeTo, Fraig_IsComplement(pFanout->p1) ); + else if ( Fraig_Regular(pFanout->p2) == pNodeFrom ) + pFanout->p2 = Fraig_NotCond( pNodeTo, Fraig_IsComplement(pFanout->p2) ); + } + // move the pointers + pNodeTo->pFanPivot = pNodeFrom->pFanPivot; + pNodeTo->pFanFanin1 = pNodeFrom->pFanFanin1; + pNodeTo->pFanFanin2 = pNodeFrom->pFanFanin2; + pNodeFrom->pFanPivot = NULL; + pNodeFrom->pFanFanin1 = NULL; + pNodeFrom->pFanFanin2 = NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the number of fanouts of a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeGetFanoutNum( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pFanout; + int Counter = 0; + Fraig_NodeForEachFanout( pNode, pFanout ) + Counter++; + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c new file mode 100644 index 00000000..8a3cc6c7 --- /dev/null +++ b/src/sat/fraig/fraigFeed.c @@ -0,0 +1,909 @@ +/**CFile**************************************************************** + + FileName [fraigFeed.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Procedures to support the solver feedback.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigFeed.c,v 1.8 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Fraig_FeedBackPrepare( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars ); +static int Fraig_FeedBackInsert( Fraig_Man_t * p, int nVarsPi ); +static void Fraig_FeedBackVerify( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); + +static void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ); +static Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * pMan ); +static int Fraig_GetSmallestColumn( int * pHits, int nHits ); +static int Fraig_GetHittingPattern( unsigned * pSims, int nWords ); +static void Fraig_CancelCoveredColumns( Fraig_NodeVec_t * vColumns, int * pHits, int iPat ); +static void Fraig_FeedBackCheckTable( Fraig_Man_t * p ); +static void Fraig_FeedBackCheckTableF0( Fraig_Man_t * p ); +static void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Initializes the feedback information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBackInit( Fraig_Man_t * p ) +{ + p->vCones = Fraig_NodeVecAlloc( 500 ); + p->vPatsReal = Msat_IntVecAlloc( 1000 ); + p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna ); + p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); +} + +/**Function************************************************************* + + Synopsis [Processes the feedback from teh solver.] + + Description [Array pModel gives the value of each variable in the SAT + solver. Array vVars is the array of integer numbers of variables + involves in this conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int nVarsPi, nWords; + int i, clk = clock(); + + // get the number of PI vars in the feedback (also sets the PI values) + nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars ); + + // set the PI values + nWords = Fraig_FeedBackInsert( p, nVarsPi ); + assert( p->iWordStart + nWords <= p->nWordsDyna ); + + // resimulates the words from p->iWordStart to iWordStop + for ( i = 1; i < p->vNodes->nSize; i++ ) + if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) ) + Fraig_NodeSimulate( p->vNodes->pArray[i], p->iWordStart, p->iWordStart + nWords, 0 ); + + if ( p->fDoSparse ) + Fraig_TableRehashF0( p, 0 ); + + if ( !p->fChoicing ) + Fraig_FeedBackVerify( p, pOld, pNew ); + + // if there is no room left, compress the patterns + if ( p->iWordStart + nWords == p->nWordsDyna ) + p->iWordStart = Fraig_FeedBackCompress( p ); + else // otherwise, update the starting word + p->iWordStart += nWords; + +p->timeFeed += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Get the number and values of the PI variables.] + + Description [Returns the number of PI variables involved in this feedback. + Fills in the internal presence and value data for the primary inputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_FeedBackPrepare( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars ) +{ + Fraig_Node_t * pNode; + int i, nVars, nVarsPis, * pVars; + + // clean the presence flag for all PIs + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + pNode = p->vInputs->pArray[i]; + pNode->fFeedUse = 0; + } + + // get the variables involved in the feedback + nVars = Msat_IntVecReadSize(vVars); + pVars = Msat_IntVecReadArray(vVars); + + // set the values for the present variables + nVarsPis = 0; + for ( i = 0; i < nVars; i++ ) + { + pNode = p->vNodes->pArray[ pVars[i] ]; + if ( !Fraig_NodeIsVar(pNode) ) + continue; + // set its value + pNode->fFeedUse = 1; + pNode->fFeedVal = !MSAT_LITSIGN(pModel[pVars[i]]); + nVarsPis++; + } + return nVarsPis; +} + +/**Function************************************************************* + + Synopsis [Inserts the new simulation patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_FeedBackInsert( Fraig_Man_t * p, int nVarsPi ) +{ + Fraig_Node_t * pNode; + int nWords, iPatFlip, nPatFlipLimit, i, w; + int fUseNoPats = 0; + int fUse2Pats = 0; + + // get the number of words + if ( fUse2Pats ) + nWords = FRAIG_NUM_WORDS( 2 * nVarsPi + 1 ); + else if ( fUseNoPats ) + nWords = 1; + else + nWords = FRAIG_NUM_WORDS( nVarsPi + 1 ); + // update the number of words if they do not fit into the simulation info + if ( nWords > p->nWordsDyna - p->iWordStart ) + nWords = p->nWordsDyna - p->iWordStart; + // determine the bound on the flipping bit + nPatFlipLimit = nWords * 32 - 2; + + // mark the real pattern + Msat_IntVecPush( p->vPatsReal, p->iWordStart * 32 ); + // record the real pattern + Fraig_BitStringSetBit( p->pSimsReal, p->iWordStart * 32 ); + + // set the values at the PIs + iPatFlip = 1; + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + pNode = p->vInputs->pArray[i]; + for ( w = p->iWordStart; w < p->iWordStart + nWords; w++ ) + if ( !pNode->fFeedUse ) + pNode->puSimD[w] = FRAIG_RANDOM_UNSIGNED; + else if ( pNode->fFeedVal ) + pNode->puSimD[w] = FRAIG_FULL; + else // if ( !pNode->fFeedVal ) + pNode->puSimD[w] = 0; + + if ( fUse2Pats ) + { + // flip two patterns + if ( pNode->fFeedUse && 2 * iPatFlip < nPatFlipLimit ) + { + Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip - 1 ); + Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip ); + Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip + 1 ); + iPatFlip++; + } + } + else if ( fUseNoPats ) + { + } + else + { + // flip the diagonal + if ( pNode->fFeedUse && iPatFlip < nPatFlipLimit ) + { + Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, iPatFlip ); + iPatFlip++; + // Extra_PrintBinary( stdout, &pNode->puSimD, 45 ); printf( "\n" ); + } + } + // clean the use mask + pNode->fFeedUse = 0; + + // add the info to the D hash value of the PIs + for ( w = p->iWordStart; w < p->iWordStart + nWords; w++ ) + pNode->uHashD ^= pNode->puSimD[w] * s_FraigPrimes[w]; + + } + return nWords; +} + + +/**Function************************************************************* + + Synopsis [Checks that the SAT solver pattern indeed distinquishes the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBackVerify( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int fValue1, fValue2, iPat; + iPat = Msat_IntVecReadEntry( p->vPatsReal, Msat_IntVecReadSize(p->vPatsReal)-1 ); + fValue1 = (Fraig_BitStringHasBit( pOld->puSimD, iPat )); + fValue2 = (Fraig_BitStringHasBit( pNew->puSimD, iPat )); +/* +Fraig_PrintNode( p, pOld ); +printf( "\n" ); +Fraig_PrintNode( p, pNew ); +printf( "\n" ); +*/ +// assert( fValue1 != fValue2 ); +} + +/**Function************************************************************* + + Synopsis [Compress the simulation patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_FeedBackCompress( Fraig_Man_t * p ) +{ + unsigned * pSims; + unsigned uHash; + int i, w, t, nPats, * pPats; + int fPerformChecks = (p->nBTLimit == -1); + + // solve the covering problem + if ( fPerformChecks ) + { + Fraig_FeedBackCheckTable( p ); + if ( p->fDoSparse ) + Fraig_FeedBackCheckTableF0( p ); + } + + // solve the covering problem + Fraig_FeedBackCovering( p, p->vPatsReal ); + + + // get the number of additional patterns + nPats = Msat_IntVecReadSize( p->vPatsReal ); + pPats = Msat_IntVecReadArray( p->vPatsReal ); + // get the new starting word + p->iWordStart = FRAIG_NUM_WORDS( p->iPatsPerm + nPats ); + + // set the simulation info for the PIs + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + // get hold of the simulation info for this PI + pSims = p->vInputs->pArray[i]->puSimD; + // clean the storage for the new patterns + for ( w = p->iWordPerm; w < p->iWordStart; w++ ) + p->pSimsTemp[w] = 0; + // set the patterns + for ( t = 0; t < nPats; t++ ) + if ( Fraig_BitStringHasBit( pSims, pPats[t] ) ) + { + // check if this pattern falls into temporary storage + if ( p->iPatsPerm + t < p->iWordPerm * 32 ) + Fraig_BitStringSetBit( pSims, p->iPatsPerm + t ); + else + Fraig_BitStringSetBit( p->pSimsTemp, p->iPatsPerm + t ); + } + // copy the pattern + for ( w = p->iWordPerm; w < p->iWordStart; w++ ) + pSims[w] = p->pSimsTemp[w]; + // recompute the hashing info + uHash = 0; + for ( w = 0; w < p->iWordStart; w++ ) + uHash ^= pSims[w] * s_FraigPrimes[w]; + p->vInputs->pArray[i]->uHashD = uHash; + } + + // update info about the permanently stored patterns + p->iWordPerm = p->iWordStart; + p->iPatsPerm += nPats; + assert( p->iWordPerm == FRAIG_NUM_WORDS( p->iPatsPerm ) ); + + // resimulate and recompute the hash values + for ( i = 1; i < p->vNodes->nSize; i++ ) + if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) ) + { + p->vNodes->pArray[i]->uHashD = 0; + Fraig_NodeSimulate( p->vNodes->pArray[i], 0, p->iWordPerm, 0 ); + } + + // double-check that the nodes are still distinguished + if ( fPerformChecks ) + Fraig_FeedBackCheckTable( p ); + + // rehash the values in the F0 table + if ( p->fDoSparse ) + { + Fraig_TableRehashF0( p, 0 ); + if ( fPerformChecks ) + Fraig_FeedBackCheckTableF0( p ); + } + + // check if we need to resize the simulation info + // if less than FRAIG_WORDS_STORE words are left, reallocate simulation info + if ( p->iWordPerm + FRAIG_WORDS_STORE > p->nWordsDyna ) + Fraig_ReallocateSimulationInfo( p ); + + // set the real patterns + Msat_IntVecClear( p->vPatsReal ); + memset( p->pSimsReal, 0, sizeof(unsigned)*p->nWordsDyna ); + for ( w = 0; w < p->iWordPerm; w++ ) + p->pSimsReal[w] = FRAIG_FULL; + if ( p->iPatsPerm % 32 > 0 ) + p->pSimsReal[p->iWordPerm-1] = FRAIG_MASK( p->iPatsPerm % 32 ); +// printf( "The number of permanent words = %d.\n", p->iWordPerm ); + return p->iWordStart; +} + + + + +/**Function************************************************************* + + Synopsis [Checks the correctness of the functional simulation table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ) +{ + Fraig_NodeVec_t * vColumns; + unsigned * pSims; + int * pHits, iPat, iCol, i; + int nOnesTotal, nSolStarting; + int fVeryVerbose = 0; + + // collect the pairs to be distinguished + vColumns = Fraig_FeedBackCoveringStart( p ); + // collect the number of 1s in each simulation vector + nOnesTotal = 0; + pHits = ALLOC( int, vColumns->nSize ); + for ( i = 0; i < vColumns->nSize; i++ ) + { + pSims = (unsigned *)vColumns->pArray[i]; + pHits[i] = Fraig_BitStringCountOnes( pSims, p->iWordStart ); + nOnesTotal += pHits[i]; +// assert( pHits[i] > 0 ); + } + + // go through the patterns + nSolStarting = Msat_IntVecReadSize(vPats); + while ( (iCol = Fraig_GetSmallestColumn( pHits, vColumns->nSize )) != -1 ) + { + // find the pattern, which hits this column + iPat = Fraig_GetHittingPattern( (unsigned *)vColumns->pArray[iCol], p->iWordStart ); + // cancel the columns covered by this pattern + Fraig_CancelCoveredColumns( vColumns, pHits, iPat ); + // save the pattern + Msat_IntVecPush( vPats, iPat ); + } + + // free the set of columns + for ( i = 0; i < vColumns->nSize; i++ ) + Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] ); + + // print stats related to the covering problem + if ( p->fVerbose && fVeryVerbose ) + { + printf( "%3d\\%3d\\%3d ", p->nWordsRand, p->nWordsDyna, p->iWordPerm ); + printf( "Col (pairs) = %5d. ", vColumns->nSize ); + printf( "Row (pats) = %5d. ", p->iWordStart * 32 ); + printf( "Dns = %6.2f %%. ", vColumns->nSize==0? 0.0 : 100.0 * nOnesTotal / vColumns->nSize / p->iWordStart / 32 ); + printf( "Sol = %3d (%3d). ", Msat_IntVecReadSize(vPats), nSolStarting ); + printf( "\n" ); + } + Fraig_NodeVecFree( vColumns ); + free( pHits ); +} + + +/**Function************************************************************* + + Synopsis [Checks the correctness of the functional simulation table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p ) +{ + Fraig_NodeVec_t * vColumns; + Fraig_HashTable_t * pT = p->pTableF; + Fraig_Node_t * pEntF, * pEntD; + unsigned * pSims; + unsigned * pUnsigned1, * pUnsigned2; + int i, k, m, w;//, nOnes; + + // start the set of columns + vColumns = Fraig_NodeVecAlloc( 100 ); + + // go through the pairs of nodes to be distinguished + for ( i = 0; i < pT->nBins; i++ ) + Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) + { + p->vCones->nSize = 0; + Fraig_TableBinForEachEntryD( pEntF, pEntD ) + Fraig_NodeVecPush( p->vCones, pEntD ); + if ( p->vCones->nSize == 1 ) + continue; + //////////////////////////////// bug fix by alanmi, September 14, 2006 + if ( p->vCones->nSize > 20 ) + continue; + //////////////////////////////// + + for ( k = 0; k < p->vCones->nSize; k++ ) + for ( m = k+1; m < p->vCones->nSize; m++ ) + { + if ( !Fraig_CompareSimInfoUnderMask( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0, p->pSimsReal ) ) + continue; + + // primary simulation patterns (counter-examples) cannot distinguish this pair + // get memory to store the feasible simulation patterns + pSims = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + // find the pattern that distinguish this column, exept the primary ones + pUnsigned1 = p->vCones->pArray[k]->puSimD; + pUnsigned2 = p->vCones->pArray[m]->puSimD; + for ( w = 0; w < p->iWordStart; w++ ) + pSims[w] = (pUnsigned1[w] ^ pUnsigned2[w]) & ~p->pSimsReal[w]; + // store the pattern + Fraig_NodeVecPush( vColumns, (Fraig_Node_t *)pSims ); +// nOnes = Fraig_BitStringCountOnes(pSims, p->iWordStart); +// assert( nOnes > 0 ); + } + } + + // if the flag is not set, do not consider sparse nodes in p->pTableF0 + if ( !p->fDoSparse ) + return vColumns; + + // recalculate their hash values based on p->pSimsReal + pT = p->pTableF0; + for ( i = 0; i < pT->nBins; i++ ) + Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) + { + pSims = pEntF->puSimD; + pEntF->uHashD = 0; + for ( w = 0; w < p->iWordStart; w++ ) + pEntF->uHashD ^= (pSims[w] & p->pSimsReal[w]) * s_FraigPrimes[w]; + } + + // rehash the table using these values + Fraig_TableRehashF0( p, 1 ); + + // collect the classes of equivalent node pairs + for ( i = 0; i < pT->nBins; i++ ) + Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) + { + p->vCones->nSize = 0; + Fraig_TableBinForEachEntryD( pEntF, pEntD ) + Fraig_NodeVecPush( p->vCones, pEntD ); + if ( p->vCones->nSize == 1 ) + continue; + + // primary simulation patterns (counter-examples) cannot distinguish all these pairs + for ( k = 0; k < p->vCones->nSize; k++ ) + for ( m = k+1; m < p->vCones->nSize; m++ ) + { + // get memory to store the feasible simulation patterns + pSims = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + // find the patterns that are not distinquished + pUnsigned1 = p->vCones->pArray[k]->puSimD; + pUnsigned2 = p->vCones->pArray[m]->puSimD; + for ( w = 0; w < p->iWordStart; w++ ) + pSims[w] = (pUnsigned1[w] ^ pUnsigned2[w]) & ~p->pSimsReal[w]; + // store the pattern + Fraig_NodeVecPush( vColumns, (Fraig_Node_t *)pSims ); +// nOnes = Fraig_BitStringCountOnes(pSims, p->iWordStart); +// assert( nOnes > 0 ); + } + } + return vColumns; +} + +/**Function************************************************************* + + Synopsis [Selects the column, which has the smallest number of hits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_GetSmallestColumn( int * pHits, int nHits ) +{ + int i, iColMin = -1, nHitsMin = 1000000; + for ( i = 0; i < nHits; i++ ) + { + // skip covered columns + if ( pHits[i] == 0 ) + continue; + // take the column if it can only be covered by one pattern + if ( pHits[i] == 1 ) + return i; + // find the column, which requires the smallest number of patterns + if ( nHitsMin > pHits[i] ) + { + nHitsMin = pHits[i]; + iColMin = i; + } + } + return iColMin; +} + +/**Function************************************************************* + + Synopsis [Select the pattern, which hits this column.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_GetHittingPattern( unsigned * pSims, int nWords ) +{ + int i, b; + for ( i = 0; i < nWords; i++ ) + { + if ( pSims[i] == 0 ) + continue; + for ( b = 0; b < 32; b++ ) + if ( pSims[i] & (1 << b) ) + return i * 32 + b; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Cancel covered patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_CancelCoveredColumns( Fraig_NodeVec_t * vColumns, int * pHits, int iPat ) +{ + unsigned * pSims; + int i; + for ( i = 0; i < vColumns->nSize; i++ ) + { + pSims = (unsigned *)vColumns->pArray[i]; + if ( Fraig_BitStringHasBit( pSims, iPat ) ) + pHits[i] = 0; + } +} + + +/**Function************************************************************* + + Synopsis [Checks the correctness of the functional simulation table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBackCheckTable( Fraig_Man_t * p ) +{ + Fraig_HashTable_t * pT = p->pTableF; + Fraig_Node_t * pEntF, * pEntD; + int i, k, m, nPairs; + int clk = clock(); + + nPairs = 0; + for ( i = 0; i < pT->nBins; i++ ) + Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) + { + p->vCones->nSize = 0; + Fraig_TableBinForEachEntryD( pEntF, pEntD ) + Fraig_NodeVecPush( p->vCones, pEntD ); + if ( p->vCones->nSize == 1 ) + continue; + for ( k = 0; k < p->vCones->nSize; k++ ) + for ( m = k+1; m < p->vCones->nSize; m++ ) + { + if ( Fraig_CompareSimInfo( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0 ) ) + printf( "Nodes %d and %d have the same D simulation info.\n", + p->vCones->pArray[k]->Num, p->vCones->pArray[m]->Num ); + nPairs++; + } + } +// printf( "\nThe total of %d node pairs have been verified.\n", nPairs ); +} + +/**Function************************************************************* + + Synopsis [Checks the correctness of the functional simulation table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_FeedBackCheckTableF0( Fraig_Man_t * p ) +{ + Fraig_HashTable_t * pT = p->pTableF0; + Fraig_Node_t * pEntF; + int i, k, m, nPairs; + + nPairs = 0; + for ( i = 0; i < pT->nBins; i++ ) + { + p->vCones->nSize = 0; + Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) + Fraig_NodeVecPush( p->vCones, pEntF ); + if ( p->vCones->nSize == 1 ) + continue; + for ( k = 0; k < p->vCones->nSize; k++ ) + for ( m = k+1; m < p->vCones->nSize; m++ ) + { + if ( Fraig_CompareSimInfo( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0 ) ) + printf( "Nodes %d and %d have the same D simulation info.\n", + p->vCones->pArray[k]->Num, p->vCones->pArray[m]->Num ); + nPairs++; + } + } +// printf( "\nThe total of %d node pairs have been verified.\n", nPairs ); +} + +/**Function************************************************************* + + Synopsis [Doubles the size of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) +{ + Fraig_MemFixed_t * mmSimsNew; // new memory manager for simulation info + Fraig_Node_t * pNode; + unsigned * pSimsNew; + unsigned uSignOld; + int i; + + // allocate a new memory manager + p->nWordsDyna *= 2; + mmSimsNew = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) ); + + // set the new data for the constant node + pNode = p->pConst1; + pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); + pNode->puSimD = pNode->puSimR + p->nWordsRand; + memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand ); + memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna ); + + // copy the simulation info of the PIs + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + pNode = p->vInputs->pArray[i]; + // copy the simulation info + pSimsNew = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); + memmove( pSimsNew, pNode->puSimR, sizeof(unsigned) * (p->nWordsRand + p->iWordStart) ); + // attach the new info + pNode->puSimR = pSimsNew; + pNode->puSimD = pNode->puSimR + p->nWordsRand; + // signatures remain without changes + } + + // replace the manager to free up some memory + Fraig_MemFixedStop( p->mmSims, 0 ); + p->mmSims = mmSimsNew; + + // resimulate the internal nodes (this should lead to the same signatures) + for ( i = 1; i < p->vNodes->nSize; i++ ) + { + pNode = p->vNodes->pArray[i]; + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + // allocate memory for the simulation info + pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); + pNode->puSimD = pNode->puSimR + p->nWordsRand; + // derive random simulation info + uSignOld = pNode->uHashR; + pNode->uHashR = 0; + Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 ); + assert( uSignOld == pNode->uHashR ); + // derive dynamic simulation info + uSignOld = pNode->uHashD; + pNode->uHashD = 0; + Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 ); + assert( uSignOld == pNode->uHashD ); + } + + // realloc temporary storage + p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); + memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna ); + p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); + p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); +} + + +/**Function************************************************************* + + Synopsis [Generated trivial counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ) +{ + int * pModel; + pModel = ALLOC( int, p->vInputs->nSize ); + memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); + return pModel; +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManSimulateBitNode_rec( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + int Value0, Value1; + if ( Fraig_NodeIsTravIdCurrent( p, pNode ) ) + return pNode->fMark3; + Fraig_NodeSetTravIdCurrent( p, pNode ); + Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) ); + Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) ); + Value0 ^= Fraig_IsComplement(pNode->p1); + Value1 ^= Fraig_IsComplement(pNode->p2); + pNode->fMark3 = Value0 & Value1; + return pNode->fMark3; +} + +/**Function************************************************************* + + Synopsis [Simulates one bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManSimulateBitNode( Fraig_Man_t * p, Fraig_Node_t * pNode, int * pModel ) +{ + int fCompl, RetValue, i; + // set the PI values + Fraig_ManIncrementTravId( p ); + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] ); + p->vInputs->pArray[i]->fMark3 = pModel[i]; + } + // perform the traversal + fCompl = Fraig_IsComplement(pNode); + RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) ); + return fCompl ^ RetValue; +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + int * pModel; + int iPattern; + int i, fCompl; + + // the node can be complemented + fCompl = Fraig_IsComplement(pNode); + // because we compare with constant 0, p->pConst1 should also be complemented + fCompl = !fCompl; + + // derive the model + pModel = Fraig_ManAllocCounterExample( p ); + iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 ); + if ( iPattern >= 0 ) + { + for ( i = 0; i < p->vInputs->nSize; i++ ) + if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) ) + pModel[i] = 1; +/* +printf( "SAT solver's pattern:\n" ); +for ( i = 0; i < p->vInputs->nSize; i++ ) + printf( "%d", pModel[i] ); +printf( "\n" ); +*/ + assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); + return pModel; + } + iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 ); + if ( iPattern >= 0 ) + { + for ( i = 0; i < p->vInputs->nSize; i++ ) + if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) ) + pModel[i] = 1; +/* +printf( "SAT solver's pattern:\n" ); +for ( i = 0; i < p->vInputs->nSize; i++ ) + printf( "%d", pModel[i] ); +printf( "\n" ); +*/ + assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); + return pModel; + } + FREE( pModel ); + return NULL; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h new file mode 100644 index 00000000..9c6e0d47 --- /dev/null +++ b/src/sat/fraig/fraigInt.h @@ -0,0 +1,451 @@ +/**CFile**************************************************************** + + FileName [fraigInt.h] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Internal 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: fraigInt.h,v 1.15 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#ifndef __FRAIG_INT_H__ +#define __FRAIG_INT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//#include "leaks.h" +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> + +#include "fraig.h" +#include "msat.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +/* + The AIG node policy: + - Each node has its main number (pNode->Num) + This is the number of this node in the array of all nodes and its SAT variable number + - The PI nodes are stored along with other nodes + Additionally, PI nodes have a PI number, by which they are stored in the PI node array + - The constant node is has number 0 and is also stored in the array +*/ + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// enable this macro to support the fanouts +#define FRAIG_ENABLE_FANOUTS +#define FRAIG_PATTERNS_RANDOM 2048 // should not be less than 128 and more than 32768 (2^15) +#define FRAIG_PATTERNS_DYNAMIC 2048 // should not be less than 256 and more than 32768 (2^15) +#define FRAIG_MAX_PRIMES 1024 // the maximum number of primes used for hashing + +// this parameter determines when simulation info is extended +// it will be extended when the free storage in the dynamic simulation +// info is less or equal to this number of words (FRAIG_WORDS_STORE) +// this is done because if the free storage for dynamic simulation info +// is not sufficient, computation becomes inefficient +#define FRAIG_WORDS_STORE 5 + +// the bit masks +#define FRAIG_MASK(n) ((~((unsigned)0)) >> (32-(n))) +#define FRAIG_FULL (~((unsigned)0)) +#define FRAIG_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0)) + +// maximum/minimum operators +#define FRAIG_MIN(a,b) (((a) < (b))? (a) : (b)) +#define FRAIG_MAX(a,b) (((a) > (b))? (a) : (b)) + +// generating random unsigned (#define RAND_MAX 0x7fff) +#define FRAIG_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())) + +// macros to get hold of the bits in a bit string +#define Fraig_BitStringSetBit(p,i) ((p)[(i)>>5] |= (1<<((i) & 31))) +#define Fraig_BitStringXorBit(p,i) ((p)[(i)>>5] ^= (1<<((i) & 31))) +#define Fraig_BitStringHasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0) + +// macros to get hold of the bits in the support info +//#define Fraig_NodeSetVarStr(p,i) (Fraig_Regular(p)->pSuppStr[((i)%FRAIG_SUPP_SIGN)>>5] |= (1<<(((i)%FRAIG_SUPP_SIGN) & 31))) +//#define Fraig_NodeHasVarStr(p,i) ((Fraig_Regular(p)->pSuppStr[((i)%FRAIG_SUPP_SIGN)>>5] & (1<<(((i)%FRAIG_SUPP_SIGN) & 31))) > 0) +#define Fraig_NodeSetVarStr(p,i) Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i) +#define Fraig_NodeHasVarStr(p,i) Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i) + +// copied from "util.h" for standaloneness +#ifndef ALLOC +# define ALLOC(type, num) \ + ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef REALLOC +# define REALLOC(type, obj, num) \ + (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \ + ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef FREE +# define FREE(obj) \ + ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif + +// copied from "extra.h" for stand-aloneness +#define Fraig_PrintTime(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) + +#define Fraig_HashKey2(a,b,TSIZE) (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE) +//#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE) +//#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE) +// the other two hash functions give bad distribution of hash chain lengths (not clear why) + +#ifndef PRT +#define PRT(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) +#endif + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Fraig_MemFixed_t_ Fraig_MemFixed_t; + +// the mapping manager +struct Fraig_ManStruct_t_ +{ + // the AIG nodes + Fraig_NodeVec_t * vInputs; // the array of primary inputs + Fraig_NodeVec_t * vNodes; // the array of all nodes, including primary inputs + Fraig_NodeVec_t * vOutputs; // the array of primary outputs (some internal nodes) + Fraig_Node_t * pConst1; // the pointer to the constant node (vNodes->pArray[0]) + + // info about the original circuit + char ** ppInputNames; // the primary input names + char ** ppOutputNames; // the primary output names + + // various hash-tables + Fraig_HashTable_t * pTableS; // hashing by structure + Fraig_HashTable_t * pTableF; // hashing by simulation info + Fraig_HashTable_t * pTableF0; // hashing by simulation info (sparse functions) + + // parameters + int nWordsRand; // the number of words of random simulation info + int nWordsDyna; // the number of words of dynamic simulation info + int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the runtime limit for the miter proof + int fFuncRed; // performs only one level hashing + int fFeedBack; // enables solver feedback + int fDist1Pats; // enables solver feedback + 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 + sint64 nInspLimit; // the inspection limit + + int nTravIds; // the traversal counter + int nTravIds2; // the traversal counter + + // info related to the solver feedback + int iWordStart; // the first word to use for simulation + int iWordPerm; // the number of words stored permanently + int iPatsPerm; // the number of patterns stored permanently + Fraig_NodeVec_t * vCones; // the temporary array of internal variables + Msat_IntVec_t * vPatsReal; // the array of real pattern numbers + unsigned * pSimsReal; // used for simulation patterns + unsigned * pSimsDiff; // used for simulation patterns + unsigned * pSimsTemp; // used for simulation patterns + + // the support information + int nSuppWords; + unsigned ** pSuppS; + unsigned ** pSuppF; + + // the memory managers + Fraig_MemFixed_t * mmNodes; // the memory manager for nodes + Fraig_MemFixed_t * mmSims; // the memory manager for simulation info + + // solving the SAT problem + Msat_Solver_t * pSat; // the SAT solver + Msat_IntVec_t * vProj; // the temporary array of projection vars + int nSatNums; // the counter of SAT variables + int * pModel; // the assignment, which satisfies the miter + // these arrays belong to the solver + Msat_IntVec_t * vVarsInt; // the temporary array of variables + Msat_ClauseVec_t * vAdjacents; // the temporary storage for connectivity + Msat_IntVec_t * vVarsUsed; // the array marking vars appearing in the cone + + // various statistic variables + int nSatCalls; // the number of times equivalence checking was called + int nSatProof; // the number of times a proof was found + int nSatCounter; // the number of times a counter example was found + int nSatFails; // the number of times the SAT solver failed to complete due to resource limit or prediction + int nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit + + int nSatCallsImp; // the number of times equivalence checking was called + int nSatProofImp; // the number of times a proof was found + int nSatCounterImp;// the number of times a counter example was found + int nSatFailsImp; // the number of times the SAT solver failed to complete + + int nSatZeros; // the number of times the simulation vector is zero + int nSatSupps; // the number of times the support info was useful + int nRefErrors; // the number of ref counting errors + int nImplies; // the number of implication cases + int nSatImpls; // the number of implication SAT calls + int nVarsClauses; // the number of variables with clauses + int nSimplifies0; + int nSimplifies1; + int nImplies0; + int nImplies1; + + // runtime statistics + int timeToAig; // time to transfer to the mapping structure + int timeSims; // time to compute k-feasible cuts + int timeTrav; // time to traverse the network + int timeFeed; // time for solver feedback (recording and resimulating) + int timeImply; // time to analyze implications + int timeSat; // time to compute the truth table for each cut + int timeToNet; // time to transfer back to the network + int timeTotal; // the total mapping time + int time1; // time to perform one task + int time2; // time to perform another task + int time3; // time to perform another task + int time4; // time to perform another task +}; + +// the mapping node +struct Fraig_NodeStruct_t_ +{ + // various numbers associated with the node + int Num; // the unique number (SAT var number) of this node + int NumPi; // if the node is a PI, this is its variable number + int Level; // the level of the node + int nRefs; // the number of references of the node + int TravId; // the traversal ID (use to avoid cleaning marks) + int TravId2; // the traversal ID (use to avoid cleaning marks) + + // general information about the node + unsigned fInv : 1; // the mark to show that simulation info is complemented + unsigned fNodePo : 1; // the mark used for primary outputs + unsigned fClauses : 1; // the clauses for this node are loaded + unsigned fMark0 : 1; // the mark used for traversals + unsigned fMark1 : 1; // the mark used for traversals + unsigned fMark2 : 1; // the mark used for traversals + unsigned fMark3 : 1; // the mark used for traversals + unsigned fFeedUse : 1; // the presence of the variable in the feedback + unsigned fFeedVal : 1; // the value of the variable in the feedback + unsigned fFailTfo : 1; // the node is in the TFO of the failed SAT run + unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many) + unsigned nOnes : 20; // the number of 1's in the random sim info + + // the children of the node + Fraig_Node_t * p1; // the first child + Fraig_Node_t * p2; // the second child + Fraig_NodeVec_t * vFanins; // the fanins of the supergate rooted at this node +// Fraig_NodeVec_t * vFanouts; // the fanouts of the supergate rooted at this node + + // various linked lists + Fraig_Node_t * pNextS; // the next node in the structural hash table + Fraig_Node_t * pNextF; // the next node in the functional (simulation) hash table + Fraig_Node_t * pNextD; // the next node in the list of nodes based on dynamic simulation + Fraig_Node_t * pNextE; // the next structural choice (functionally-equivalent node) + Fraig_Node_t * pRepr; // the canonical functional representative of the node + + // simulation data + unsigned uHashR; // the hash value for random information + unsigned uHashD; // the hash value for dynamic information + unsigned * puSimR; // the simulation information (random) + unsigned * puSimD; // the simulation information (dynamic) + + // misc information + Fraig_Node_t * pData0; // temporary storage for the corresponding network node + Fraig_Node_t * pData1; // temporary storage for the corresponding network node + +#ifdef FRAIG_ENABLE_FANOUTS + // representation of node's fanouts + Fraig_Node_t * pFanPivot; // the first fanout of this node + Fraig_Node_t * pFanFanin1; // the next fanout of p1 + Fraig_Node_t * pFanFanin2; // the next fanout of p2 +#endif +}; + +// the vector of nodes +struct Fraig_NodeVecStruct_t_ +{ + int nCap; // the number of allocated entries + int nSize; // the number of entries in the array + Fraig_Node_t ** pArray; // the array of nodes +}; + +// the hash table +struct Fraig_HashTableStruct_t_ +{ + Fraig_Node_t ** pBins; // the table bins + int nBins; // the size of the table + int nEntries; // the total number of entries in the table +}; + +// getting hold of the next fanout of the node +#define Fraig_NodeReadNextFanout( pNode, pFanout ) \ + ( ( pFanout == NULL )? NULL : \ + ((Fraig_Regular((pFanout)->p1) == (pNode))? \ + (pFanout)->pFanFanin1 : (pFanout)->pFanFanin2) ) +// getting hold of the place where the next fanout will be attached +#define Fraig_NodeReadNextFanoutPlace( pNode, pFanout ) \ + ( (Fraig_Regular((pFanout)->p1) == (pNode))? \ + &(pFanout)->pFanFanin1 : &(pFanout)->pFanFanin2 ) +// iterator through the fanouts of the node +#define Fraig_NodeForEachFanout( pNode, pFanout ) \ + for ( pFanout = (pNode)->pFanPivot; pFanout; \ + pFanout = Fraig_NodeReadNextFanout(pNode, pFanout) ) +// safe iterator through the fanouts of the node +#define Fraig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 ) \ + for ( pFanout = (pNode)->pFanPivot, \ + pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout); \ + pFanout; \ + pFanout = pFanout2, \ + pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout) ) + +// iterators through the entries in the linked lists of nodes +// the list of nodes in the structural hash table +#define Fraig_TableBinForEachEntryS( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = pEnt->pNextS ) +#define Fraig_TableBinForEachEntrySafeS( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? pEnt->pNextS: NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? pEnt->pNextS: NULL ) +// the list of nodes in the functional (simulation) hash table +#define Fraig_TableBinForEachEntryF( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = pEnt->pNextF ) +#define Fraig_TableBinForEachEntrySafeF( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? pEnt->pNextF: NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? pEnt->pNextF: NULL ) +// the list of nodes with the same simulation and different functionality +#define Fraig_TableBinForEachEntryD( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = pEnt->pNextD ) +#define Fraig_TableBinForEachEntrySafeD( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? pEnt->pNextD: NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? pEnt->pNextD: NULL ) +// the list of nodes with the same functionality +#define Fraig_TableBinForEachEntryE( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = pEnt->pNextE ) +#define Fraig_TableBinForEachEntrySafeE( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? pEnt->pNextE: NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? pEnt->pNextE: NULL ) + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== fraigCanon.c =============================================================*/ +extern Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 ); +/*=== fraigFanout.c =============================================================*/ +extern void Fraig_NodeAddFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanout ); +extern void Fraig_NodeRemoveFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanoutToRemove ); +extern int Fraig_NodeGetFanoutNum( Fraig_Node_t * pNode ); +/*=== fraigFeed.c =============================================================*/ +extern void Fraig_FeedBackInit( Fraig_Man_t * p ); +extern void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +extern void Fraig_FeedBackTest( Fraig_Man_t * p ); +extern int Fraig_FeedBackCompress( Fraig_Man_t * p ); +extern int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ); +extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ); +/*=== fraigMan.c =============================================================*/ +extern void Fraig_ManCreateSolver( Fraig_Man_t * p ); +/*=== fraigMem.c =============================================================*/ +extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ); +extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose ); +extern char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ); +extern void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry ); +extern void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ); +extern int Fraig_MemFixedReadMemUsage( Fraig_MemFixed_t * p ); +/*=== fraigNode.c =============================================================*/ +extern Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p ); +extern Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p ); +extern Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ); +extern void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, int fUseRand ); +/*=== fraigPrime.c =============================================================*/ +extern int s_FraigPrimes[FRAIG_MAX_PRIMES]; +extern unsigned int Cudd_PrimeFraig( unsigned int p ); +/*=== fraigSat.c ===============================================================*/ +extern int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); +/*=== fraigTable.c =============================================================*/ +extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize ); +extern void Fraig_HashTableFree( Fraig_HashTable_t * p ); +extern int Fraig_HashTableLookupS( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, Fraig_Node_t ** ppNodeRes ); +extern Fraig_Node_t * Fraig_HashTableLookupF( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ); +extern int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); +extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand ); +extern void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); +extern void Fraig_TablePrintStatsS( Fraig_Man_t * pMan ); +extern void Fraig_TablePrintStatsF( Fraig_Man_t * pMan ); +extern void Fraig_TablePrintStatsF0( Fraig_Man_t * pMan ); +extern int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv ); +/*=== fraigUtil.c ===============================================================*/ +extern int Fraig_NodeCountPis( Msat_IntVec_t * vVars, int nVarsPi ); +extern int Fraig_NodeCountSuppVars( Fraig_Man_t * p, Fraig_Node_t * pNode, int fSuppStr ); +extern int Fraig_NodesCompareSupps( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +extern int Fraig_NodeAndSimpleCase_rec( Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +extern int Fraig_NodeIsExorType( Fraig_Node_t * pNode ); +extern void Fraig_ManSelectBestChoice( Fraig_Man_t * p ); +extern int Fraig_BitStringCountOnes( unsigned * pString, int nWords ); +extern void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits ); +extern int Fraig_NodeIsExorType( Fraig_Node_t * pNode ); +extern int Fraig_NodeIsExor( Fraig_Node_t * pNode ); +extern int Fraig_NodeIsMuxType( Fraig_Node_t * pNode ); +extern Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE ); +extern int Fraig_ManCountExors( Fraig_Man_t * pMan ); +extern int Fraig_ManCountMuxes( Fraig_Man_t * pMan ); +extern int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ); +extern int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux ); +extern int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums ); +extern void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ); +extern void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +/*=== fraigVec.c ===============================================================*/ +extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ); + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c new file mode 100644 index 00000000..7fd937d5 --- /dev/null +++ b/src/sat/fraig/fraigMan.c @@ -0,0 +1,540 @@ +/**CFile**************************************************************** + + FileName [fraigMan.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Implementation of the FRAIG manager.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +int timeSelect; +int timeAssign; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for equivalence checking.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prove_ParamsSetDefault( Prove_Params_t * pParams ) +{ + // clean the parameter structure + memset( pParams, 0, sizeof(Prove_Params_t) ); + // general parameters + pParams->fUseFraiging = 1; // enables fraiging + pParams->fUseRewriting = 1; // enables rewriting + pParams->fUseBdds = 0; // enables BDD construction when other methods fail + pParams->fVerbose = 0; // prints verbose stats + // iterations + pParams->nItersMax = 6; // the number of iterations + // mitering + pParams->nMiteringLimitStart = 300; // starting mitering limit + pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration + // rewriting (currently not used) + pParams->nRewritingLimitStart = 3; // the number of rewriting iterations + pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration + // fraiging + pParams->nFraigingLimitStart = 2; // starting backtrack(conflict) limit + pParams->nFraigingLimitMulti = 8.0; // multiplicative coefficient to increase the limit in each iteration + // last-gasp BDD construction + pParams->nBddSizeLimit = 1000000; // the number of BDD nodes when construction is aborted + pParams->fBddReorder = 1; // enables dynamic BDD variable reordering + // last-gasp mitering +// pParams->nMiteringLimitLast = 1000000; // final mitering limit + pParams->nMiteringLimitLast = 0; // final mitering limit + // global SAT solver limits + pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks + pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects +// pParams->nTotalInspectLimit = 100000000; // global limit on the number of clause inspects +} + +/**Function************************************************************* + + Synopsis [Prints out the current values of CEC engine parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prove_ParamsPrint( Prove_Params_t * pParams ) +{ + printf( "CEC enging parameters:\n" ); + printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" ); + printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" ); + printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" ); + printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" ); + printf( "Solver iterations: %d\n", pParams->nItersMax ); + printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart ); + printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti ); + printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart ); + printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti ); + printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit ); + printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" ); + printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast ); + printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit ); + printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit ); + printf( "Parameter dump complete.\n" ); +} + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for equivalence checking.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) +{ + memset( pParams, 0, sizeof(Fraig_Params_t) ); + pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info + pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info + pParams->nBTLimit = 99; // the max number of backtracks to perform + pParams->nSeconds = 20; // the max number of seconds to solve the miter + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 1; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections +} + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for complete FRAIGing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ) +{ + memset( pParams, 0, sizeof(Fraig_Params_t) ); + pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info + pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info + pParams->nBTLimit = -1; // the max number of backtracks to perform + pParams->nSeconds = 20; // the max number of seconds to solve the miter + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 1; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 0; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections +} + +/**Function************************************************************* + + Synopsis [Creates the new FRAIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) +{ + Fraig_Params_t Params; + Fraig_Man_t * p; + + // set the random seed for simulation +// srand( 0xFEEDDEAF ); + srand( 0xDEADCAFE ); + + // set parameters for equivalence checking + if ( pParams == NULL ) + Fraig_ParamsSetDefault( pParams = &Params ); + // adjust the amount of simulation info + if ( pParams->nPatsRand < 128 ) + pParams->nPatsRand = 128; + if ( pParams->nPatsRand > 32768 ) + pParams->nPatsRand = 32768; + if ( pParams->nPatsDyna < 128 ) + pParams->nPatsDyna = 128; + if ( pParams->nPatsDyna > 32768 ) + pParams->nPatsDyna = 32768; + // if reduction is not performed, allocate minimum simulation info + if ( !pParams->fFuncRed ) + pParams->nPatsRand = pParams->nPatsDyna = 128; + + // start the manager + p = ALLOC( Fraig_Man_t, 1 ); + memset( p, 0, sizeof(Fraig_Man_t) ); + + // set the default parameters + p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info + p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info + p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit + p->nSeconds = pParams->nSeconds; // the timeout for the final miter + p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed) + p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation) + p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation) + p->fDoSparse = pParams->fDoSparse; // performs equivalence checking for sparse functions (whose sim-info is 0) + p->fChoicing = pParams->fChoicing; // disable accumulation of structural choices (keeps only the first choice) + p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice) + p->fVerbose = pParams->fVerbose; // disable verbose output + p->fVerboseP = pParams->fVerboseP; // disable verbose output + p->nInspLimit = pParams->nInspLimit; // the limit on the number of inspections + + // start memory managers + p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) ); + p->mmSims = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) ); + // allocate node arrays + p->vInputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary inputs + p->vOutputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary outputs + p->vNodes = Fraig_NodeVecAlloc( 1000 ); // the array of internal nodes + // start the tables + p->pTableS = Fraig_HashTableCreate( 1000 ); // hashing by structure + p->pTableF = Fraig_HashTableCreate( 1000 ); // hashing by function + p->pTableF0 = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions) + // create the constant node + p->pConst1 = Fraig_NodeCreateConst( p ); + // initialize SAT solver feedback data structures + Fraig_FeedBackInit( p ); + // initialize other variables + p->vProj = Msat_IntVecAlloc( 10 ); + p->nTravIds = 1; + p->nTravIds2 = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManFree( Fraig_Man_t * p ) +{ + int i; + if ( p->fVerbose ) + { + if ( p->fChoicing ) Fraig_ManReportChoices( p ); + Fraig_ManPrintStats( p ); +// Fraig_TablePrintStatsS( p ); +// Fraig_TablePrintStatsF( p ); +// Fraig_TablePrintStatsF0( p ); + } + + for ( i = 0; i < p->vNodes->nSize; i++ ) + if ( p->vNodes->pArray[i]->vFanins ) + { + Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins ); + p->vNodes->pArray[i]->vFanins = NULL; + } + + if ( p->vInputs ) Fraig_NodeVecFree( p->vInputs ); + if ( p->vNodes ) Fraig_NodeVecFree( p->vNodes ); + if ( p->vOutputs ) Fraig_NodeVecFree( p->vOutputs ); + + if ( p->pTableS ) Fraig_HashTableFree( p->pTableS ); + if ( p->pTableF ) Fraig_HashTableFree( p->pTableF ); + if ( p->pTableF0 ) Fraig_HashTableFree( p->pTableF0 ); + + if ( p->pSat ) Msat_SolverFree( p->pSat ); + if ( p->vProj ) Msat_IntVecFree( p->vProj ); + if ( p->vCones ) Fraig_NodeVecFree( p->vCones ); + if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal ); + if ( p->pModel ) free( p->pModel ); + + Fraig_MemFixedStop( p->mmNodes, 0 ); + Fraig_MemFixedStop( p->mmSims, 0 ); + + if ( p->pSuppS ) + { + FREE( p->pSuppS[0] ); + FREE( p->pSuppS ); + } + if ( p->pSuppF ) + { + FREE( p->pSuppF[0] ); + FREE( p->pSuppF ); + } + + FREE( p->ppOutputNames ); + FREE( p->ppInputNames ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Prepares the SAT solver to run on the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManCreateSolver( Fraig_Man_t * p ) +{ + extern int timeSelect; + extern int timeAssign; + assert( p->pSat == NULL ); + // allocate data for SAT solving + p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 ); + p->vVarsInt = Msat_SolverReadConeVars( p->pSat ); + p->vAdjacents = Msat_SolverReadAdjacents( p->pSat ); + p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat ); + timeSelect = 0; + timeAssign = 0; +} + + +/**Function************************************************************* + + Synopsis [Deallocates the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManPrintStats( Fraig_Man_t * p ) +{ + double nMemory; + int clk = clock(); + nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * + (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20); + printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", + p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory ); + printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", + p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros ); + printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", + Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses ); + if ( p->pSat ) Msat_SolverPrintStats( p->pSat ); + Fraig_PrintTime( "AIG simulation ", p->timeSims ); + Fraig_PrintTime( "AIG traversal ", p->timeTrav ); + Fraig_PrintTime( "Solver feedback ", p->timeFeed ); + Fraig_PrintTime( "SAT solving ", p->timeSat ); + Fraig_PrintTime( "Network update ", p->timeToNet ); + Fraig_PrintTime( "TOTAL RUNTIME ", p->timeTotal ); + if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); } + if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); } + if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); } + if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); } +// PRT( "Selection ", timeSelect ); +// PRT( "Assignment", timeAssign ); +} + +/**Function************************************************************* + + Synopsis [Allocates simulation information for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean ) +{ + Fraig_NodeVec_t * vInfo; + unsigned * pUnsigned; + int i; + assert( nSize > 0 && nWords > 0 ); + vInfo = Fraig_NodeVecAlloc( nSize ); + pUnsigned = ALLOC( unsigned, nSize * nWords ); + vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned; + if ( fClean ) + memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords ); + for ( i = 1; i < nSize; i++ ) + vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords); + vInfo->nSize = nSize; + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Returns simulation info of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p ) +{ + Fraig_NodeVec_t * vInfo; + Fraig_Node_t * pNode; + unsigned * pUnsigned; + int nRandom, nDynamic; + int i, k, nWords; + + nRandom = Fraig_ManReadPatternNumRandom( p ); + nDynamic = Fraig_ManReadPatternNumDynamic( p ); + nWords = nRandom / 32 + nDynamic / 32; + + vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 ); + for ( i = 0; i < p->vNodes->nSize; i++ ) + { + pNode = p->vNodes->pArray[i]; + assert( i == pNode->Num ); + pUnsigned = (unsigned *)vInfo->pArray[i]; + for ( k = 0; k < nRandom / 32; k++ ) + pUnsigned[k] = pNode->puSimR[k]; + for ( k = 0; k < nDynamic / 32; k++ ) + pUnsigned[nRandom / 32 + k] = pNode->puSimD[k]; + } + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if A v B is always true based on the siminfo.] + + Description [A v B is always true iff A' * B' is always false.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ) +{ + int fCompl1, fCompl2, i; + + fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv; + fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv; + + pNode1 = Fraig_Regular(pNode1); + pNode2 = Fraig_Regular(pNode2); + assert( pNode1 != pNode2 ); + + // check the simulation info + if ( fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] ) + return 0; + return 1; + } + if ( !fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] ) + return 0; + return 1; + } + if ( fCompl1 && !fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] ) + return 0; + return 1; + } +// if ( fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( pNode1->puSimR[i] & pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( pNode1->puSimD[i] & pNode2->puSimD[i] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [This procedure is used to add external clauses to the solver. + The clauses are given by sets of nodes. Each node stands for one literal. + If the node is complemented, the literal is negated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes ) +{ + Fraig_Node_t * pNode; + int i, fComp, RetValue; + if ( p->pSat == NULL ) + Fraig_ManCreateSolver( p ); + // create four clauses + Msat_IntVecClear( p->vProj ); + for ( i = 0; i < nNodes; i++ ) + { + pNode = Fraig_Regular(ppNodes[i]); + fComp = Fraig_IsComplement(ppNodes[i]); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); +// printf( "%d(%d) ", pNode->Num, fComp ); + } +// printf( "\n" ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c new file mode 100644 index 00000000..500431c6 --- /dev/null +++ b/src/sat/fraig/fraigMem.c @@ -0,0 +1,246 @@ +/**CFile**************************************************************** + + FileName [fraigMem.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Fixed-size-entry memory manager for the FRAIG package.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigMem.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Fraig_MemFixed_t_ +{ + // information about individual entries + int nEntrySize; // the size of one entry + int nEntriesAlloc; // the total number of entries allocated + int nEntriesUsed; // the number of entries in use + int nEntriesMax; // the max number of entries in use + char * pEntriesFree; // the linked list of free entries + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the internal memory manager.] + + Description [Can only work with entry size at least 4 byte long.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ) +{ + Fraig_MemFixed_t * p; + + p = ALLOC( Fraig_MemFixed_t, 1 ); + memset( p, 0, sizeof(Fraig_MemFixed_t) ); + + p->nEntrySize = nEntrySize; + p->nEntriesAlloc = 0; + p->nEntriesUsed = 0; + p->pEntriesFree = NULL; + + if ( nEntrySize * (1 << 10) < (1<<16) ) + p->nChunkSize = (1 << 10); + else + p->nChunkSize = (1<<16) / nEntrySize; + if ( p->nChunkSize < 8 ) + p->nChunkSize = 8; + + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); + + p->nMemoryUsed = 0; + p->nMemoryAlloc = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose ) +{ + int i; + if ( p == NULL ) + return; + if ( fVerbose ) + { + printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", + p->nEntrySize, p->nChunkSize, p->nChunks ); + printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", + p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); + } + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Extracts one entry from the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ) +{ + char * pTemp; + int i; + + // check if there are still free entries + if ( p->nEntriesUsed == p->nEntriesAlloc ) + { // need to allocate more entries + assert( p->pEntriesFree == NULL ); + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; + // transform these entries into a linked list + pTemp = p->pEntriesFree; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // add the chunk to the chunk storage + p->pChunks[ p->nChunks++ ] = p->pEntriesFree; + // add to the number of entries allocated + p->nEntriesAlloc += p->nChunkSize; + } + // incrememt the counter of used entries + p->nEntriesUsed++; + if ( p->nEntriesMax < p->nEntriesUsed ) + p->nEntriesMax = p->nEntriesUsed; + // return the first entry in the free entry list + pTemp = p->pEntriesFree; + p->pEntriesFree = *((char **)pTemp); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Returns one entry into the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry ) +{ + // decrement the counter of used entries + p->nEntriesUsed--; + // add the entry to the linked list of free entries + *((char **)pEntry) = p->pEntriesFree; + p->pEntriesFree = pEntry; +} + +/**Function************************************************************* + + Synopsis [Frees all associated memory and resets the manager.] + + Description [Relocates all the memory except the first chunk.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) +{ + int i; + char * pTemp; + + // deallocate all chunks except the first one + for ( i = 1; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + p->nChunks = 1; + // transform these entries into a linked list + pTemp = p->pChunks[0]; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // set the free entry list + p->pEntriesFree = p->pChunks[0]; + // set the correct statistics + p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; + p->nMemoryUsed = 0; + p->nEntriesAlloc = p->nChunkSize; + p->nEntriesUsed = 0; +} + +/**Function************************************************************* + + Synopsis [Reports the memory usage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MemFixedReadMemUsage( Fraig_MemFixed_t * p ) +{ + return p->nMemoryAlloc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c new file mode 100644 index 00000000..6e3d3c7d --- /dev/null +++ b/src/sat/fraig/fraigNode.c @@ -0,0 +1,313 @@ +/**CFile**************************************************************** + + FileName [fraigNode.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Implementation of the FRAIG node.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigNode.c,v 1.3 2005/07/08 01:01:32 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// returns the complemented attribute of the node +#define Fraig_NodeIsSimComplement(p) (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode; + + // create the node + pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes ); + memset( pNode, 0, sizeof(Fraig_Node_t) ); + + // assign the number and add to the array of nodes + pNode->Num = p->vNodes->nSize; + Fraig_NodeVecPush( p->vNodes, pNode ); + pNode->NumPi = -1; // this is not a PI, so its number is -1 + pNode->Level = 0; // just like a PI, it has 0 level + pNode->nRefs = 1; // it is a persistent node, which comes referenced + pNode->fInv = 1; // the simulation info is complemented + + // create the simulation info + pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + pNode->puSimD = pNode->puSimR + p->nWordsRand; + memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand ); + memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna ); + + // count the number of ones in the simulation vector + pNode->nOnes = p->nWordsRand * sizeof(unsigned) * 8; + + // insert it into the hash table + Fraig_HashTableLookupF0( p, pNode ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a primary input node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode, * pNodeRes; + int i, clk; + + // create the node + pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes ); + memset( pNode, 0, sizeof(Fraig_Node_t) ); + pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + pNode->puSimD = pNode->puSimR + p->nWordsRand; + memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna ); + + // assign the number and add to the array of nodes + pNode->Num = p->vNodes->nSize; + Fraig_NodeVecPush( p->vNodes, pNode ); + + // assign the PI number and add to the array of primary inputs + pNode->NumPi = p->vInputs->nSize; + Fraig_NodeVecPush( p->vInputs, pNode ); + + pNode->Level = 0; // PI has 0 level + pNode->nRefs = 1; // it is a persistent node, which comes referenced + pNode->fInv = 0; // the simulation info of the PI is not complemented + + // derive the simulation info for the new node +clk = clock(); + // set the random simulation info for the primary input + pNode->uHashR = 0; + for ( i = 0; i < p->nWordsRand; i++ ) + { + // generate the simulation info + pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED; + // for reasons that take very long to explain, it makes sense to have (0000000...) + // pattern in the set (this helps if we need to return the counter-examples) + if ( i == 0 ) + pNode->puSimR[i] <<= 1; + // compute the hash key + pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i]; + } + // count the number of ones in the simulation vector + pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand ); + + // set the systematic simulation info for the primary input + pNode->uHashD = 0; + for ( i = 0; i < p->iWordStart; i++ ) + { + // generate the simulation info + pNode->puSimD[i] = FRAIG_RANDOM_UNSIGNED; + // compute the hash key + pNode->uHashD ^= pNode->puSimD[i] * s_FraigPrimes[i]; + } +p->timeSims += clock() - clk; + + // insert it into the hash table + pNodeRes = Fraig_HashTableLookupF( p, pNode ); + assert( pNodeRes == NULL ); + // add to the runtime of simulation + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a new node.] + + Description [This procedure should be called to create the constant + node and the PI nodes first.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ) +{ + Fraig_Node_t * pNode; + int clk; + + // create the node + pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes ); + memset( pNode, 0, sizeof(Fraig_Node_t) ); + + // assign the children + pNode->p1 = p1; Fraig_Ref(p1); Fraig_Regular(p1)->nRefs++; + pNode->p2 = p2; Fraig_Ref(p2); Fraig_Regular(p2)->nRefs++; + + // assign the number and add to the array of nodes + pNode->Num = p->vNodes->nSize; + Fraig_NodeVecPush( p->vNodes, pNode ); + + // assign the PI number + pNode->NumPi = -1; + + // compute the level of this node + pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level); + pNode->fInv = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2); + pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo; + + // derive the simulation info +clk = clock(); + // allocate memory for the simulation info + pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); + pNode->puSimD = pNode->puSimR + p->nWordsRand; + // derive random simulation info + pNode->uHashR = 0; + Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 ); + // derive dynamic simulation info + pNode->uHashD = 0; + Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 ); + // count the number of ones in the random simulation info + pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand ); + if ( pNode->fInv ) + pNode->nOnes = p->nWordsRand * 32 - pNode->nOnes; + // add to the runtime of simulation +p->timeSims += clock() - clk; + +#ifdef FRAIG_ENABLE_FANOUTS + // create the fanout info + Fraig_NodeAddFaninFanout( Fraig_Regular(p1), pNode ); + Fraig_NodeAddFaninFanout( Fraig_Regular(p2), pNode ); +#endif + return pNode; +} + + +/**Function************************************************************* + + Synopsis [Simulates the node.] + + Description [Simulates the random or dynamic simulation info through + the node. Uses phases of the children to determine their real simulation + info. Uses phase of the node to determine the way its simulation info + is stored. The resulting info is guaranteed to be 0 for the first pattern.] + + SideEffects [This procedure modified the hash value of the simulation info.] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, int fUseRand ) +{ + unsigned * pSims, * pSims1, * pSims2; + unsigned uHash; + int fCompl, fCompl1, fCompl2, i; + + assert( !Fraig_IsComplement(pNode) ); + + // get hold of the simulation information + pSims = fUseRand? pNode->puSimR : pNode->puSimD; + pSims1 = fUseRand? Fraig_Regular(pNode->p1)->puSimR : Fraig_Regular(pNode->p1)->puSimD; + pSims2 = fUseRand? Fraig_Regular(pNode->p2)->puSimR : Fraig_Regular(pNode->p2)->puSimD; + + // get complemented attributes of the children using their random info + fCompl = pNode->fInv; + fCompl1 = Fraig_NodeIsSimComplement(pNode->p1); + fCompl2 = Fraig_NodeIsSimComplement(pNode->p2); + + // simulate + uHash = 0; + if ( fCompl1 && fCompl2 ) + { + if ( fCompl ) + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (pSims1[i] | pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + else + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = ~(pSims1[i] | pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + } + else if ( fCompl1 && !fCompl2 ) + { + if ( fCompl ) + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (pSims1[i] | ~pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + else + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (~pSims1[i] & pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + } + else if ( !fCompl1 && fCompl2 ) + { + if ( fCompl ) + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (~pSims1[i] | pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + else + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (pSims1[i] & ~pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + } + else // if ( !fCompl1 && !fCompl2 ) + { + if ( fCompl ) + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = ~(pSims1[i] & pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + else + for ( i = iWordStart; i < iWordStop; i++ ) + { + pSims[i] = (pSims1[i] & pSims2[i]); + uHash ^= pSims[i] * s_FraigPrimes[i]; + } + } + + if ( fUseRand ) + pNode->uHashR ^= uHash; + else + pNode->uHashD ^= uHash; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c new file mode 100644 index 00000000..127ad478 --- /dev/null +++ b/src/sat/fraig/fraigPrime.c @@ -0,0 +1,144 @@ +/**CFile**************************************************************** + + FileName [fraigPrime.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [The table of the first 1000 primes.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigPrime.c,v 1.4 2005/07/08 01:01:32 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// The 1,024 smallest prime numbers used to compute the hash value +// http://www.math.utah.edu/~alfeld/math/primelist.html +int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, +7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, +101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, +193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, +293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, +409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, +521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, +641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, +757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, +881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, +1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091, +1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193, +1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291, +1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, +1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, +1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, +1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699, +1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811, +1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931, +1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029, +2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137, +2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267, +2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357, +2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459, +2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593, +2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693, +2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791, +2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903, +2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023, +3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167, +3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271, +3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373, +3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511, +3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607, +3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709, +3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833, +3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931, +3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057, +4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177, +4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283, +4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423, +4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547, +4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657, +4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789, +4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931, +4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011, +5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147, +5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279, +5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413, +5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507, +5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647, +5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743, +5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857, +5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007, +6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121, +6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247, +6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343, +6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473, +6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607, +6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733, +6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857, +6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971, +6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103, +7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229, +7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369, +7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517, +7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, +7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, +7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, +7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, +8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, +8147, 8161 }; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function******************************************************************** + + Synopsis [Returns the next prime >= p.] + + Description [Copied from CUDD, for stand-aloneness.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +unsigned int Cudd_PrimeFraig( unsigned int p) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c new file mode 100644 index 00000000..53057fc3 --- /dev/null +++ b/src/sat/fraig/fraigSat.c @@ -0,0 +1,1455 @@ +/**CFile**************************************************************** + + FileName [fraigSat.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Proving functional equivalence using SAT.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigSat.c,v 1.10 2005/07/08 01:01:32 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" +#include "math.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +static void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ); +static void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ); +static void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); +static void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); + +static void Fraig_SupergateAddClauses( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper ); +static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +//static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); + +extern void * Msat_ClauseVecReadEntry( void * p, int i ); + +// The lesson learned seems to be that variable should be in reverse topological order +// from the output of the miter. The ordering of adjacency lists is very important. +// The best way seems to be fanins followed by fanouts. Slight changes to this order +// leads to big degradation in quality. + +static int nMuxes; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks equivalence of two nodes.] + + Description [Returns 1 iff the nodes are equivalent.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ) +{ + if ( pNode1 == pNode2 ) + return 1; + if ( pNode1 == Fraig_Not(pNode2) ) + return 0; + return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit ); +} + +/**Function************************************************************* + + Synopsis [Tries to prove the final miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManProveMiter( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode; + int i, clk; + + if ( !p->fTryProve ) + return; + + clk = clock(); + // consider all outputs of the multi-output miter + for ( i = 0; i < p->vOutputs->nSize; i++ ) + { + pNode = Fraig_Regular(p->vOutputs->pArray[i]); + // skip already constant nodes + if ( pNode == p->pConst1 ) + continue; + // skip nodes that are different according to simulation + if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) ) + continue; + if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) ) + { + if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) ) + p->vOutputs->pArray[i] = Fraig_Not(p->pConst1); + else + p->vOutputs->pArray[i] = p->pConst1; + } + } + if ( p->fVerboseP ) + { +// PRT( "Final miter proof time", clock() - clk ); + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckMiter( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode; + int i; + FREE( p->pModel ); + for ( i = 0; i < p->vOutputs->nSize; i++ ) + { + // get the output node (it can be complemented!) + pNode = p->vOutputs->pArray[i]; + // if the miter is constant 0, the problem is UNSAT + if ( pNode == Fraig_Not(p->pConst1) ) + continue; + // consider the special case when the miter is constant 1 + if ( pNode == p->pConst1 ) + { + // in this case, any counter example will do to distinquish it from constant 0 + // here we pick the counter example composed of all zeros + p->pModel = Fraig_ManAllocCounterExample( p ); + return 0; + } + // save the counter example + p->pModel = Fraig_ManSaveCounterExample( p, pNode ); + // if the model is not found, return undecided + if ( p->pModel == NULL ) + return -1; + else + return 0; + } + return 1; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 1; + // check the children + return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) + + Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi2_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + // skip the boundary node + if ( pNode->TravId == pMan->nTravIds-1 ) + { + pNode->TravId = pMan->nTravIds; + return 1; + } + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 1; + // check the children + return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) + + Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi3_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 1; + // skip the boundary node + if ( pNode->TravId == pMan->nTravIds-1 ) + { + pNode->TravId = pMan->nTravIds; + return 1; + } + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 0; + // check the children + return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) * + Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int NumPis, NumCut, fContain; + + // mark the TFI of pNew + p->nTravIds++; + NumPis = Fraig_MarkTfi_rec( p, pNew ); + printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level ); + + // check if the old is in the TFI + if ( pOld->TravId == p->nTravIds ) + { + printf( "* " ); + return; + } + + // count the boundary of nodes in pOld + p->nTravIds++; + NumCut = Fraig_MarkTfi2_rec( p, pOld ); + printf( "%d", NumCut ); + + // check if the new is contained in the old's support + p->nTravIds++; + fContain = Fraig_MarkTfi3_rec( p, pNew ); + printf( "%c ", fContain? '+':'-' ); +} + + +/**Function************************************************************* + + Synopsis [Checks whether two nodes are functinally equivalent.] + + Description [The flag (fComp) tells whether the nodes to be checked + are in the opposite polarity. The second flag (fSkipZeros) tells whether + the checking should be performed if the simulation vectors are zeros. + Returns 1 if the nodes are equivalent; 0 othewise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) +{ + int RetValue, RetValue1, i, fComp, clk; + int fVerbose = 0; + int fSwitch = 0; + + // make sure the nodes are not complemented + assert( !Fraig_IsComplement(pNew) ); + assert( !Fraig_IsComplement(pOld) ); + assert( pNew != pOld ); + + // if at least one of the nodes is a failed node, perform adjustments: + // if the backtrack limit is small, simply skip this node + // if the backtrack limit is > 10, take the quare root of the limit + if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) + { + p->nSatFails++; +// return 0; +// if ( nBTLimit > 10 ) +// nBTLimit /= 10; + if ( nBTLimit <= 10 ) + return 0; + nBTLimit = (int)sqrt(nBTLimit); +// fSwitch = 1; + } + + p->nSatCalls++; + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + Fraig_ManCreateSolver( p ); + // make sure the SAT solver has enough variables + for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); + + + +/* + { + Fraig_Node_t * ppNodes[2] = { pOld, pNew }; + extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName ); + Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" ); + } +*/ + + nMuxes = 0; + + + // get the logic cone +clk = clock(); +// Fraig_VarsStudy( p, pOld, pNew ); + Fraig_OrderVariables( p, pOld, pNew ); +// Fraig_PrepareCones( p, pOld, pNew ); +p->timeTrav += clock() - clk; + +// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); +// PRT( "Time", clock() - clk ); + +if ( fVerbose ) + printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); + + + // prepare variable activity + Fraig_SetActivity( p, pOld, pNew ); + + // get the complemented attribute + fComp = Fraig_NodeComparePhase( pOld, pNew ); +//Msat_SolverPrintClauses( p->pSat ); + + //////////////////////////////////////////// + // prepare the solver to run incrementally on these variables +//clk = clock(); + Msat_SolverPrepare( p->pSat, p->vVarsInt ); +//p->time3 += clock() - clk; + + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); + +//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); + + // run the solver +clk = clock(); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); +p->timeSat += clock() - clk; + + if ( RetValue1 == MSAT_FALSE ) + { +//p->time1 += clock() - clk; + +if ( fVerbose ) +{ + printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // add the clause + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + // continue solving the other implication + } + else if ( RetValue1 == MSAT_TRUE ) + { +//p->time2 += clock() - clk; + +if ( fVerbose ) +{ + printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // record the counter example + Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "s(%d)", pNew->Level ); + if ( fSwitch ) + printf( "s(%d)", pNew->Level ); + p->nSatCounter++; + return 0; + } + else // if ( RetValue1 == MSAT_UNKNOWN ) + { +p->time3 += clock() - clk; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "T(%d)", pNew->Level ); + + // mark the node as the failed node + if ( pOld != p->pConst1 ) + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; +// p->nSatFails++; + if ( fSwitch ) + printf( "T(%d)", pNew->Level ); + p->nSatFailsReal++; + return 0; + } + + // if the old node was constant 0, we already know the answer + if ( pOld == p->pConst1 ) + return 1; + + //////////////////////////////////////////// + // prepare the solver to run incrementally +//clk = clock(); + Msat_SolverPrepare( p->pSat, p->vVarsInt ); +//p->time3 += clock() - clk; + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); + // run the solver +clk = clock(); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); +p->timeSat += clock() - clk; + + if ( RetValue1 == MSAT_FALSE ) + { +//p->time1 += clock() - clk; + +if ( fVerbose ) +{ + printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // add the clause + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + // continue solving the other implication + } + else if ( RetValue1 == MSAT_TRUE ) + { +//p->time2 += clock() - clk; + +if ( fVerbose ) +{ + printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // record the counter example + Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); + p->nSatCounter++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "s(%d)", pNew->Level ); + if ( fSwitch ) + printf( "s(%d)", pNew->Level ); + return 0; + } + else // if ( RetValue1 == MSAT_UNKNOWN ) + { +p->time3 += clock() - clk; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "T(%d)", pNew->Level ); + if ( fSwitch ) + printf( "T(%d)", pNew->Level ); + + // mark the node as the failed node + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; +// p->nSatFails++; + p->nSatFailsReal++; + return 0; + } + + // return SAT proof + p->nSatProof++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "u(%d)", pNew->Level ); + + if ( fSwitch ) + printf( "u(%d)", pNew->Level ); + + return 1; +} + + +/**Function************************************************************* + + Synopsis [Checks whether pOld => pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) +{ + int RetValue, RetValue1, i, fComp, clk; + int fVerbose = 0; + + // make sure the nodes are not complemented + assert( !Fraig_IsComplement(pNew) ); + assert( !Fraig_IsComplement(pOld) ); + assert( pNew != pOld ); + + p->nSatCallsImp++; + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + Fraig_ManCreateSolver( p ); + // make sure the SAT solver has enough variables + for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); + + // get the logic cone +clk = clock(); + Fraig_OrderVariables( p, pOld, pNew ); +// Fraig_PrepareCones( p, pOld, pNew ); +p->timeTrav += clock() - clk; + +if ( fVerbose ) + printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); + + + // get the complemented attribute + fComp = Fraig_NodeComparePhase( pOld, pNew ); +//Msat_SolverPrintClauses( p->pSat ); + + //////////////////////////////////////////// + // prepare the solver to run incrementally on these variables +//clk = clock(); + Msat_SolverPrepare( p->pSat, p->vVarsInt ); +//p->time3 += clock() - clk; + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); + // run the solver +clk = clock(); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); +p->timeSat += clock() - clk; + + if ( RetValue1 == MSAT_FALSE ) + { +//p->time1 += clock() - clk; + +if ( fVerbose ) +{ + printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // add the clause + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +// p->nSatProofImp++; + return 1; + } + else if ( RetValue1 == MSAT_TRUE ) + { +//p->time2 += clock() - clk; + +if ( fVerbose ) +{ + printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + // record the counter example + Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); + p->nSatCounterImp++; + return 0; + } + else // if ( RetValue1 == MSAT_UNKNOWN ) + { +p->time3 += clock() - clk; + p->nSatFailsImp++; + return 0; + } +} + +/**Function************************************************************* + + Synopsis [Prepares the SAT solver to run on the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) +{ + Fraig_Node_t * pNode1R, * pNode2R; + int RetValue, RetValue1, i, clk; + int fVerbose = 0; + + pNode1R = Fraig_Regular(pNode1); + pNode2R = Fraig_Regular(pNode2); + assert( pNode1R != pNode2R ); + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + Fraig_ManCreateSolver( p ); + // make sure the SAT solver has enough variables + for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); + + // get the logic cone +clk = clock(); + Fraig_OrderVariables( p, pNode1R, pNode2R ); +// Fraig_PrepareCones( p, pNode1R, pNode2R ); +p->timeTrav += clock() - clk; + + //////////////////////////////////////////// + // prepare the solver to run incrementally on these variables +//clk = clock(); + Msat_SolverPrepare( p->pSat, p->vVarsInt ); +//p->time3 += clock() - clk; + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) ); + // run the solver +clk = clock(); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); +p->timeSat += clock() - clk; + + if ( RetValue1 == MSAT_FALSE ) + { +//p->time1 += clock() - clk; + +if ( fVerbose ) +{ + printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + + // add the clause + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +// p->nSatProofImp++; + return 1; + } + else if ( RetValue1 == MSAT_TRUE ) + { +//p->time2 += clock() - clk; + +if ( fVerbose ) +{ + printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +PRT( "time", clock() - clk ); +} + // record the counter example +// Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R ); + p->nSatCounterImp++; + return 0; + } + else // if ( RetValue1 == MSAT_UNKNOWN ) + { +p->time3 += clock() - clk; + p->nSatFailsImp++; + return 0; + } +} + + +/**Function************************************************************* + + Synopsis [Prepares the SAT solver to run on the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ +// Msat_IntVec_t * vAdjs; +// int * pVars, nVars, i, k; + int nVarsAlloc; + + assert( pOld != pNew ); + assert( !Fraig_IsComplement(pOld) ); + assert( !Fraig_IsComplement(pNew) ); + // clean the variables + nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); + Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); + Msat_IntVecClear( pMan->vVarsInt ); + + pMan->nTravIds++; + Fraig_PrepareCones_rec( pMan, pNew ); + Fraig_PrepareCones_rec( pMan, pOld ); + + +/* + nVars = Msat_IntVecReadSize( pMan->vVarsInt ); + pVars = Msat_IntVecReadArray( pMan->vVarsInt ); + for ( i = 0; i < nVars; i++ ) + { + // process its connections + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); + printf( "%d=%d { ", pVars[i], Msat_IntVecReadSize(vAdjs) ); + for ( k = 0; k < Msat_IntVecReadSize(vAdjs); k++ ) + printf( "%d ", Msat_IntVecReadEntry(vAdjs,k) ); + printf( "}\n" ); + + } + i = 0; +*/ +} + +/**Function************************************************************* + + Synopsis [Traverses the cone, collects the numbers and adds the clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pFanin; + Msat_IntVec_t * vAdjs; + int fUseMuxes = 1, i; + int fItIsTime; + + // skip if the node is aleady visited + assert( !Fraig_IsComplement(pNode) ); + if ( pNode->TravId == pMan->nTravIds ) + return; + pNode->TravId = pMan->nTravIds; + + // collect the node's number (closer to reverse topological order) + Msat_IntVecPush( pMan->vVarsInt, pNode->Num ); + Msat_IntVecWriteEntry( pMan->vVarsUsed, pNode->Num, 1 ); + if ( !Fraig_NodeIsAnd( pNode ) ) + return; + + // if the node does not have fanins, create them + fItIsTime = 0; + if ( pNode->vFanins == NULL ) + { + fItIsTime = 1; + // create the fanins of the supergate + assert( pNode->fClauses == 0 ); + if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) + { + pNode->vFanins = Fraig_NodeVecAlloc( 4 ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); + Fraig_SupergateAddClausesMux( pMan, pNode ); + } + else + { + pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes ); + Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins ); + } + assert( pNode->vFanins->nSize > 1 ); + pNode->fClauses = 1; + pMan->nVarsClauses++; + + // add fanins + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pNode->Num ); + assert( Msat_IntVecReadSize( vAdjs ) == 0 ); + for ( i = 0; i < pNode->vFanins->nSize; i++ ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[i]); + Msat_IntVecPush( vAdjs, pFanin->Num ); + } + } + + // recursively visit the fanins + for ( i = 0; i < pNode->vFanins->nSize; i++ ) + Fraig_PrepareCones_rec( pMan, Fraig_Regular(pNode->vFanins->pArray[i]) ); + + if ( fItIsTime ) + { + // recursively visit the fanins + for ( i = 0; i < pNode->vFanins->nSize; i++ ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[i]); + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); + Msat_IntVecPush( vAdjs, pNode->Num ); + } + } +} + +/**Function************************************************************* + + Synopsis [Collect variables using their proximity from the nodes.] + + Description [This procedure creates a variable order based on collecting + first the nodes that are the closest to the given two target nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + Fraig_Node_t * pNode, * pFanin; + int i, k, Number, fUseMuxes = 1; + int nVarsAlloc; + + assert( pOld != pNew ); + assert( !Fraig_IsComplement(pOld) ); + assert( !Fraig_IsComplement(pNew) ); + + pMan->nTravIds++; + + // clean the variables + nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); + Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); + Msat_IntVecClear( pMan->vVarsInt ); + + // add the first node + Msat_IntVecPush( pMan->vVarsInt, pOld->Num ); + Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 ); + pOld->TravId = pMan->nTravIds; + + // add the second node + Msat_IntVecPush( pMan->vVarsInt, pNew->Num ); + Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 ); + pNew->TravId = pMan->nTravIds; + + // create the variable order + for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ ) + { + // get the new node on the frontier + Number = Msat_IntVecReadEntry(pMan->vVarsInt, i); + pNode = pMan->vNodes->pArray[Number]; + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + + // if the node does not have fanins, create them + if ( pNode->vFanins == NULL ) + { + // create the fanins of the supergate + assert( pNode->fClauses == 0 ); + // detecting a fanout-free cone (experiment only) +// Fraig_DetectFanoutFreeCone( pMan, pNode ); + + if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) + { + pNode->vFanins = Fraig_NodeVecAlloc( 4 ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) ); + Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); + Fraig_SupergateAddClausesMux( pMan, pNode ); +// Fraig_DetectFanoutFreeConeMux( pMan, pNode ); + + nMuxes++; + } + else + { + pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes ); + Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins ); + } + assert( pNode->vFanins->nSize > 1 ); + pNode->fClauses = 1; + pMan->nVarsClauses++; + + pNode->fMark2 = 1; // goes together with Fraig_SetupAdjacentMark() + } + + // explore the implication fanins of pNode + for ( k = 0; k < pNode->vFanins->nSize; k++ ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); + if ( pFanin->TravId == pMan->nTravIds ) // already collected + continue; + // collect and mark + Msat_IntVecPush( pMan->vVarsInt, pFanin->Num ); + Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 ); + pFanin->TravId = pMan->nTravIds; + } + } + + // set up the adjacent variable information +// Fraig_SetupAdjacent( pMan, pMan->vVarsInt ); + Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt ); +} + + + +/**Function************************************************************* + + Synopsis [Set up the adjacent variable information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ) +{ + Fraig_Node_t * pNode, * pFanin; + Msat_IntVec_t * vAdjs; + int * pVars, nVars, i, k; + + // clean the adjacents for the variables + nVars = Msat_IntVecReadSize( vConeVars ); + pVars = Msat_IntVecReadArray( vConeVars ); + for ( i = 0; i < nVars; i++ ) + { + // process its connections + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); + Msat_IntVecClear( vAdjs ); + + pNode = pMan->vNodes->pArray[pVars[i]]; + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + + // add fanins + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); + for ( k = 0; k < pNode->vFanins->nSize; k++ ) +// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); + Msat_IntVecPush( vAdjs, pFanin->Num ); +// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); + } + } + // add the fanouts + for ( i = 0; i < nVars; i++ ) + { + pNode = pMan->vNodes->pArray[pVars[i]]; + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + + // add the edges + for ( k = 0; k < pNode->vFanins->nSize; k++ ) +// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); + Msat_IntVecPush( vAdjs, pNode->Num ); +// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); + } + } +} + + +/**Function************************************************************* + + Synopsis [Set up the adjacent variable information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ) +{ + Fraig_Node_t * pNode, * pFanin; + Msat_IntVec_t * vAdjs; + int * pVars, nVars, i, k; + + // clean the adjacents for the variables + nVars = Msat_IntVecReadSize( vConeVars ); + pVars = Msat_IntVecReadArray( vConeVars ); + for ( i = 0; i < nVars; i++ ) + { + pNode = pMan->vNodes->pArray[pVars[i]]; + if ( pNode->fMark2 == 0 ) + continue; +// pNode->fMark2 = 0; + + // process its connections +// vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); +// Msat_IntVecClear( vAdjs ); + + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + + // add fanins + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); + for ( k = 0; k < pNode->vFanins->nSize; k++ ) +// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); + Msat_IntVecPush( vAdjs, pFanin->Num ); +// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); + } + } + // add the fanouts + for ( i = 0; i < nVars; i++ ) + { + pNode = pMan->vNodes->pArray[pVars[i]]; + if ( pNode->fMark2 == 0 ) + continue; + pNode->fMark2 = 0; + + if ( !Fraig_NodeIsAnd(pNode) ) + continue; + + // add the edges + for ( k = 0; k < pNode->vFanins->nSize; k++ ) +// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) + { + pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); + vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); + Msat_IntVecPush( vAdjs, pNode->Num ); +// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); + } + } +} + + + + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SupergateAddClauses( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper ) +{ + int fComp1, RetValue, nVars, Var, Var1, i; + + assert( Fraig_NodeIsAnd( pNode ) ); + nVars = Msat_SolverReadVarNum(p->pSat); + + Var = pNode->Num; + assert( Var < nVars ); + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Fraig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Fraig_Regular(vSuper->pArray[i])->Num; + // check that the variables are in the SAT manager + assert( Var1 < nVars ); + + // suppose the AND-gate is A * B = C + // add !A => !C or A + !C + // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, fComp1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + } + + // add A & B => C or !A + !B + C +// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 ); + Msat_IntVecClear( p->vProj ); + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Fraig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Fraig_Regular(vSuper->pArray[i])->Num; + + // add this variable to the array + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, !fComp1) ); + } + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SupergateAddClausesExor( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + int fComp, RetValue; + + assert( !Fraig_IsComplement( pNode ) ); + assert( Fraig_NodeIsExorType( pNode ) ); + // get nodes + pNode1 = Fraig_Regular(Fraig_Regular(pNode->p1)->p1); + pNode2 = Fraig_Regular(Fraig_Regular(pNode->p1)->p2); + // get the complemented attribute of the EXOR/NEXOR gate + fComp = Fraig_NodeIsExor( pNode ); // 1 if EXOR, 0 if NEXOR + + // create four clauses + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNodeI, * pNodeT, * pNodeE; + int RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Fraig_IsComplement( pNode ) ); + assert( Fraig_NodeIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = pNode->Num; + VarI = pNodeI->Num; + VarT = Fraig_Regular(pNodeT)->Num; + VarE = Fraig_Regular(pNodeE)->Num; + // get the complementation flags + fCompT = Fraig_IsComplement(pNodeT); + fCompE = Fraig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + +} + + + + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_DetectFanoutFreeCone_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst ) +{ + // make the pointer regular + pNode = Fraig_Regular(pNode); + // if the new node is complemented or a PI, another gate begins + if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) ) + { + Fraig_NodeVecPushUnique( vSuper, pNode ); + return; + } + // go through the branches + Fraig_DetectFanoutFreeCone_rec( pNode->p1, vSuper, vInside, 0 ); + Fraig_DetectFanoutFreeCone_rec( pNode->p2, vSuper, vInside, 0 ); + // add the node + Fraig_NodeVecPushUnique( vInside, pNode ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_NodeVec_t * vFanins; + Fraig_NodeVec_t * vInside; + int nCubes; + extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside ); + + vFanins = Fraig_NodeVecAlloc( 8 ); + vInside = Fraig_NodeVecAlloc( 8 ); + + Fraig_DetectFanoutFreeCone_rec( pNode, vFanins, vInside, 1 ); + assert( vInside->pArray[vInside->nSize-1] == pNode ); + + nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside ); + +printf( "%d(%d)", vFanins->nSize, nCubes ); + Fraig_NodeVecFree( vFanins ); + Fraig_NodeVecFree( vInside ); +} +*/ + + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_DetectFanoutFreeConeMux_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst ) +{ + // make the pointer regular + pNode = Fraig_Regular(pNode); + // if the new node is complemented or a PI, another gate begins + if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) || !Fraig_NodeIsMuxType(pNode) ) + { + Fraig_NodeVecPushUnique( vSuper, pNode ); + return; + } + // go through the branches + Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p1, vSuper, vInside, 0 ); + Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p2, vSuper, vInside, 0 ); + Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p1, vSuper, vInside, 0 ); + Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p2, vSuper, vInside, 0 ); + // add the node + Fraig_NodeVecPushUnique( vInside, pNode ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_NodeVec_t * vFanins; + Fraig_NodeVec_t * vInside; + int nCubes; + extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside ); + + vFanins = Fraig_NodeVecAlloc( 8 ); + vInside = Fraig_NodeVecAlloc( 8 ); + + Fraig_DetectFanoutFreeConeMux_rec( pNode, vFanins, vInside, 1 ); + assert( vInside->pArray[vInside->nSize-1] == pNode ); + +// nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside ); + nCubes = 0; + +printf( "%d(%d)", vFanins->nSize, nCubes ); + Fraig_NodeVecFree( vFanins ); + Fraig_NodeVecFree( vInside ); +} + + + +/**Function************************************************************* + + Synopsis [Collect variables using their proximity from the nodes.] + + Description [This procedure creates a variable order based on collecting + first the nodes that are the closest to the given two target nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + Fraig_Node_t * pNode; + int i, Number, MaxLevel; + float * pFactors = Msat_SolverReadFactors(pMan->pSat); + if ( pFactors == NULL ) + return; + MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level ); + // create the variable order + for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ ) + { + // get the new node on the frontier + Number = Msat_IntVecReadEntry(pMan->vVarsInt, i); + pNode = pMan->vNodes->pArray[Number]; + pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level ); +// if ( pNode->Num % 50 == 0 ) +// printf( "(%d) %.2f ", MaxLevel - pNode->Level, pFactors[pNode->Num] ); + } +// printf( "\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c new file mode 100644 index 00000000..b68bbe0e --- /dev/null +++ b/src/sat/fraig/fraigTable.c @@ -0,0 +1,657 @@ +/**CFile**************************************************************** + + FileName [fraigTable.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Structural and functional hash tables.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigTable.c,v 1.7 2005/07/08 01:01:34 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Fraig_TableResizeS( Fraig_HashTable_t * p ); +static void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_HashTable_t * Fraig_HashTableCreate( int nSize ) +{ + Fraig_HashTable_t * p; + // allocate the table + p = ALLOC( Fraig_HashTable_t, 1 ); + memset( p, 0, sizeof(Fraig_HashTable_t) ); + // allocate and clean the bins + p->nBins = Cudd_PrimeFraig(nSize); + p->pBins = ALLOC( Fraig_Node_t *, p->nBins ); + memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates the supergate hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_HashTableFree( Fraig_HashTable_t * p ) +{ + FREE( p->pBins ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Looks up an entry in the structural hash table.] + + Description [If the entry with the same children does not exists, + creates it, inserts it into the table, and returns 0. If the entry + with the same children exists, finds it, and return 1. In both cases, + the new/old entry is returned in ppNodeRes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_HashTableLookupS( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, Fraig_Node_t ** ppNodeRes ) +{ + Fraig_HashTable_t * p = pMan->pTableS; + Fraig_Node_t * pEnt; + unsigned Key; + + // order the arguments + if ( Fraig_Regular(p1)->Num > Fraig_Regular(p2)->Num ) + pEnt = p1, p1 = p2, p2 = pEnt; + + Key = Fraig_HashKey2( p1, p2, p->nBins ); + Fraig_TableBinForEachEntryS( p->pBins[Key], pEnt ) + if ( pEnt->p1 == p1 && pEnt->p2 == p2 ) + { + *ppNodeRes = pEnt; + return 1; + } + // check if it is a good time for table resizing + if ( p->nEntries >= 2 * p->nBins ) + { + Fraig_TableResizeS( p ); + Key = Fraig_HashKey2( p1, p2, p->nBins ); + } + // create the new node + pEnt = Fraig_NodeCreate( pMan, p1, p2 ); + // add the node to the corresponding linked list in the table + pEnt->pNextS = p->pBins[Key]; + p->pBins[Key] = pEnt; + *ppNodeRes = pEnt; + p->nEntries++; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Insert the entry in the functional hash table.] + + Description [If the entry with the same key exists, return it right away. + If the entry with the same key does not exists, inserts it and returns NULL. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_HashTableLookupF( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_HashTable_t * p = pMan->pTableF; + Fraig_Node_t * pEnt, * pEntD; + unsigned Key; + + // go through the hash table entries + Key = pNode->uHashR % p->nBins; + Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt ) + { + // if their simulation info differs, skip + if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->nWordsRand, 1 ) ) + continue; + // equivalent up to the complement + Fraig_TableBinForEachEntryD( pEnt, pEntD ) + { + // if their simulation info differs, skip + if ( !Fraig_CompareSimInfo( pNode, pEntD, pMan->iWordStart, 0 ) ) + continue; + // found a simulation-equivalent node + return pEntD; + } + // did not find a simulation equivalent node + // add the node to the corresponding linked list + pNode->pNextD = pEnt->pNextD; + pEnt->pNextD = pNode; + // return NULL, because there is no functional equivalence in this case + return NULL; + } + + // check if it is a good time for table resizing + if ( p->nEntries >= 2 * p->nBins ) + { + Fraig_TableResizeF( p, 1 ); + Key = pNode->uHashR % p->nBins; + } + + // add the node to the corresponding linked list in the table + pNode->pNextF = p->pBins[Key]; + p->pBins[Key] = pNode; + p->nEntries++; + // return NULL, because there is no functional equivalence in this case + return NULL; +} + +/**Function************************************************************* + + Synopsis [Insert the entry in the functional hash table.] + + Description [If the entry with the same key exists, return it right away. + If the entry with the same key does not exists, inserts it and returns NULL. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_HashTable_t * p = pMan->pTableF0; + Fraig_Node_t * pEnt; + unsigned Key; + + // go through the hash table entries + Key = pNode->uHashD % p->nBins; + Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt ) + { + // if their simulation info differs, skip + if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->iWordStart, 0 ) ) + continue; + // found a simulation-equivalent node + return pEnt; + } + + // check if it is a good time for table resizing + if ( p->nEntries >= 2 * p->nBins ) + { + Fraig_TableResizeF( p, 0 ); + Key = pNode->uHashD % p->nBins; + } + + // add the node to the corresponding linked list in the table + pNode->pNextF = p->pBins[Key]; + p->pBins[Key] = pNode; + p->nEntries++; + // return NULL, because there is no functional equivalence in this case + return NULL; +} + +/**Function************************************************************* + + Synopsis [Insert the entry in the functional hash table.] + + Description [Unconditionally add the node to the corresponding + linked list in the table.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + Fraig_HashTable_t * p = pMan->pTableF0; + unsigned Key = pNode->uHashD % p->nBins; + + pNode->pNextF = p->pBins[Key]; + p->pBins[Key] = pNode; + p->nEntries++; +} + + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_TableResizeS( Fraig_HashTable_t * p ) +{ + Fraig_Node_t ** pBinsNew; + Fraig_Node_t * pEnt, * pEnt2; + int nBinsNew, Counter, i, clk; + unsigned Key; + +clk = clock(); + // get the new table size + nBinsNew = Cudd_PrimeFraig(2 * p->nBins); + // allocate a new array + pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew ); + memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < p->nBins; i++ ) + Fraig_TableBinForEachEntrySafeS( p->pBins[i], pEnt, pEnt2 ) + { + Key = Fraig_HashKey2( pEnt->p1, pEnt->p2, nBinsNew ); + pEnt->pNextS = pBinsNew[Key]; + pBinsNew[Key] = pEnt; + Counter++; + } + assert( Counter == p->nEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pBins ); + p->pBins = pBinsNew; + p->nBins = nBinsNew; +} + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR ) +{ + Fraig_Node_t ** pBinsNew; + Fraig_Node_t * pEnt, * pEnt2; + int nBinsNew, Counter, i, clk; + unsigned Key; + +clk = clock(); + // get the new table size + nBinsNew = Cudd_PrimeFraig(2 * p->nBins); + // allocate a new array + pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew ); + memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < p->nBins; i++ ) + Fraig_TableBinForEachEntrySafeF( p->pBins[i], pEnt, pEnt2 ) + { + if ( fUseSimR ) + Key = pEnt->uHashR % nBinsNew; + else + Key = pEnt->uHashD % nBinsNew; + pEnt->pNextF = pBinsNew[Key]; + pBinsNew[Key] = pEnt; + Counter++; + } + assert( Counter == p->nEntries ); +// printf( "Increasing the functional table size from %6d to %6d. ", p->nBins, nBinsNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pBins ); + p->pBins = pBinsNew; + p->nBins = nBinsNew; +} + + +/**Function************************************************************* + + Synopsis [Compares two pieces of simulation info.] + + Description [Returns 1 if they are equal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ) +{ + int i; + assert( !Fraig_IsComplement(pNode1) ); + assert( !Fraig_IsComplement(pNode2) ); + if ( fUseRand ) + { + // if their signatures differ, skip + if ( pNode1->uHashR != pNode2->uHashR ) + return 0; + // check the simulation info + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) + return 0; + } + else + { + // if their signatures differ, skip + if ( pNode1->uHashD != pNode2->uHashD ) + return 0; + // check the simulation info + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Find the number of the different pattern.] + + Description [Returns -1 if there is no such pattern] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand ) +{ + int i, v; + assert( !Fraig_IsComplement(pNode1) ); + assert( !Fraig_IsComplement(pNode2) ); + // take into account possible internal complementation + fCompl ^= pNode1->fInv; + fCompl ^= pNode2->fInv; + // find the pattern + if ( fCompl ) + { + if ( fUseRand ) + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) ) + return i * 32 + v; + } + else + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimD[i] != ~pNode2->puSimD[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) ) + return i * 32 + v; + } + } + else + { + if ( fUseRand ) + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) ) + return i * 32 + v; + } + else + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) ) + return i * 32 + v; + } + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Compares two pieces of simulation info.] + + Description [Returns 1 if they are equal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ) +{ + unsigned * pSims1, * pSims2; + int i; + assert( !Fraig_IsComplement(pNode1) ); + assert( !Fraig_IsComplement(pNode2) ); + // get hold of simulation info + pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD; + pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD; + // check the simulation info + for ( i = 0; i < iWordLast; i++ ) + if ( (pSims1[i] & puMask[i]) != (pSims2[i] & puMask[i]) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Compares two pieces of simulation info.] + + Description [Returns 1 if they are equal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ) +{ + unsigned * pSims1, * pSims2; + int i; + assert( !Fraig_IsComplement(pNode1) ); + assert( !Fraig_IsComplement(pNode2) ); + // get hold of simulation info + pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD; + pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD; + // check the simulation info + for ( i = 0; i < iWordLast; i++ ) + puMask[i] = ( pSims1[i] ^ pSims2[i] ); +} + + +/**Function************************************************************* + + Synopsis [Prints stats of the structural table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_TablePrintStatsS( Fraig_Man_t * pMan ) +{ + Fraig_HashTable_t * pT = pMan->pTableS; + Fraig_Node_t * pNode; + int i, Counter; + + printf( "Structural table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries ); + for ( i = 0; i < pT->nBins; i++ ) + { + Counter = 0; + Fraig_TableBinForEachEntryS( pT->pBins[i], pNode ) + Counter++; + if ( Counter > 1 ) + { + printf( "%d ", Counter ); + if ( Counter > 50 ) + printf( "{%d} ", i ); + } + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints stats of the structural table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_TablePrintStatsF( Fraig_Man_t * pMan ) +{ + Fraig_HashTable_t * pT = pMan->pTableF; + Fraig_Node_t * pNode; + int i, Counter; + + printf( "Functional table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries ); + for ( i = 0; i < pT->nBins; i++ ) + { + Counter = 0; + Fraig_TableBinForEachEntryF( pT->pBins[i], pNode ) + Counter++; + if ( Counter > 1 ) + printf( "{%d} ", Counter ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints stats of the structural table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_TablePrintStatsF0( Fraig_Man_t * pMan ) +{ + Fraig_HashTable_t * pT = pMan->pTableF0; + Fraig_Node_t * pNode; + int i, Counter; + + printf( "Zero-node table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries ); + for ( i = 0; i < pT->nBins; i++ ) + { + Counter = 0; + Fraig_TableBinForEachEntryF( pT->pBins[i], pNode ) + Counter++; + if ( Counter == 0 ) + continue; +/* + printf( "\nBin = %4d : Number of entries = %4d\n", i, Counter ); + Fraig_TableBinForEachEntryF( pT->pBins[i], pNode ) + printf( "Node %5d. Hash = %10d.\n", pNode->Num, pNode->uHashD ); +*/ + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Rehashes the table after the simulation info has changed.] + + Description [Assumes that the hash values have been updated after performing + additional simulation. Rehashes the table using the new hash values. + Uses pNextF to link the entries in the bins. Uses pNextD to link the entries + with identical hash values. Returns 1 if the identical entries have been found. + Note that identical hash values may mean that the simulation data is different.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv ) +{ + Fraig_HashTable_t * pT = pMan->pTableF0; + Fraig_Node_t ** pBinsNew; + Fraig_Node_t * pEntF, * pEntF2, * pEnt, * pEntD2, * pEntN; + int ReturnValue, Counter, i; + unsigned Key; + + // allocate a new array of bins + pBinsNew = ALLOC( Fraig_Node_t *, pT->nBins ); + memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins ); + + // rehash the entries in the table + // go through all the nodes in the F-lists (and possible in D-lists, if used) + Counter = 0; + ReturnValue = 0; + for ( i = 0; i < pT->nBins; i++ ) + Fraig_TableBinForEachEntrySafeF( pT->pBins[i], pEntF, pEntF2 ) + Fraig_TableBinForEachEntrySafeD( pEntF, pEnt, pEntD2 ) + { + // decide where to put entry pEnt + Key = pEnt->uHashD % pT->nBins; + if ( fLinkEquiv ) + { + // go through the entries in the new bin + Fraig_TableBinForEachEntryF( pBinsNew[Key], pEntN ) + { + // if they have different values skip + if ( pEnt->uHashD != pEntN->uHashD ) + continue; + // they have the same hash value, add pEnt to the D-list pEnt3 + pEnt->pNextD = pEntN->pNextD; + pEntN->pNextD = pEnt; + ReturnValue = 1; + Counter++; + break; + } + if ( pEntN != NULL ) // already linked + continue; + // we did not find equal entry + } + // link the new entry + pEnt->pNextF = pBinsNew[Key]; + pBinsNew[Key] = pEnt; + pEnt->pNextD = NULL; + Counter++; + } + assert( Counter == pT->nEntries ); + // replace the table and the parameters + free( pT->pBins ); + pT->pBins = pBinsNew; + return ReturnValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c new file mode 100644 index 00000000..342a7111 --- /dev/null +++ b/src/sat/fraig/fraigUtil.c @@ -0,0 +1,1034 @@ +/**CFile**************************************************************** + + FileName [fraigUtil.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigUtil.c,v 1.15 2005/07/08 01:01:34 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" +#include <limits.h> + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + +static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv ); +static int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int i; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int i; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + for ( i = 0; i < nNodes; i++ ) + Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Recursively computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv ) +{ + assert( !Fraig_IsComplement(pNode) ); + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return; + pNode->TravId = pMan->nTravIds; + // visit the transitive fanin + if ( Fraig_NodeIsAnd(pNode) ) + { + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p1), vNodes, fEquiv ); + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p2), vNodes, fEquiv ); + } + if ( fEquiv && pNode->pNextE ) + Fraig_Dfs_rec( pMan, pNode->pNextE, vNodes, fEquiv ); + // save the node + Fraig_NodeVecPush( vNodes, pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int RetValue; + vNodes = Fraig_Dfs( pMan, fEquiv ); + RetValue = vNodes->nSize; + Fraig_NodeVecFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + assert( !Fraig_IsComplement(pOld) ); + assert( !Fraig_IsComplement(pNew) ); + pMan->nTravIds++; + return Fraig_CheckTfi_rec( pMan, pNew, pOld ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld ) +{ + // check the trivial cases + if ( pNode == NULL ) + return 0; + if ( pNode->Num < pOld->Num && !pMan->fChoicing ) + return 0; + if ( pNode == pOld ) + return 1; + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + pNode->TravId = pMan->nTravIds; + // check the children + if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p1), pOld ) ) + return 1; + if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p2), pOld ) ) + return 1; + // check equivalent nodes + return Fraig_CheckTfi_rec( pMan, pNode->pNextE, pOld ); +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + Fraig_NodeVec_t * vNodes; + int RetValue; + vNodes = Fraig_DfsOne( pMan, pNew, 1 ); + RetValue = (pOld->TravId == pMan->nTravIds); + Fraig_NodeVecFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Sets the number of fanouts (none, one, or many).] + + Description [This procedure collects the nodes reachable from + the POs of the AIG and sets the type of fanout counter (none, one, + or many) for each node. This procedure is useful to determine + fanout-free cones of AND-nodes, which is helpful for rebalancing + the AIG (see procedure Fraig_ManRebalance, or something like that).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManMarkRealFanouts( Fraig_Man_t * p ) +{ + Fraig_NodeVec_t * vNodes; + Fraig_Node_t * pNodeR; + int i; + // collect the nodes reachable + vNodes = Fraig_Dfs( p, 0 ); + // clean the fanouts field + for ( i = 0; i < vNodes->nSize; i++ ) + { + vNodes->pArray[i]->nFanouts = 0; + vNodes->pArray[i]->pData0 = NULL; + } + // mark reachable nodes by setting the two-bit counter pNode->nFans + for ( i = 0; i < vNodes->nSize; i++ ) + { + pNodeR = Fraig_Regular(vNodes->pArray[i]->p1); + if ( pNodeR && ++pNodeR->nFanouts == 3 ) + pNodeR->nFanouts = 2; + pNodeR = Fraig_Regular(vNodes->pArray[i]->p2); + if ( pNodeR && ++pNodeR->nFanouts == 3 ) + pNodeR->nFanouts = 2; + } + Fraig_NodeVecFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Creates the constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_BitStringCountOnes( unsigned * pString, int nWords ) +{ + unsigned char * pSuppBytes = (unsigned char *)pString; + int i, nOnes, nBytes = sizeof(unsigned) * nWords; + // count the number of ones in the simulation vector + for ( i = nOnes = 0; i < nBytes; i++ ) + nOnes += bit_count[pSuppBytes[i]]; + return nOnes; +} + +/**Function************************************************************* + + Synopsis [Verify one useful property.] + + Description [This procedure verifies one useful property. After + the FRAIG construction with choice nodes is over, each primary node + should have fanins that are primary nodes. The primary nodes is the + one that does not have pNode->pRepr set to point to another node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckConsistency( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode; + Fraig_NodeVec_t * pVec; + int i; + pVec = Fraig_Dfs( p, 0 ); + for ( i = 0; i < pVec->nSize; i++ ) + { + pNode = pVec->pArray[i]; + if ( Fraig_NodeIsVar(pNode) ) + { + if ( pNode->pRepr ) + printf( "Primary input %d is a secondary node.\n", pNode->Num ); + } + else if ( Fraig_NodeIsConst(pNode) ) + { + if ( pNode->pRepr ) + printf( "Constant 1 %d is a secondary node.\n", pNode->Num ); + } + else + { + if ( pNode->pRepr ) + printf( "Internal node %d is a secondary node.\n", pNode->Num ); + if ( Fraig_Regular(pNode->p1)->pRepr ) + printf( "Internal node %d has first fanin %d that is a secondary node.\n", + pNode->Num, Fraig_Regular(pNode->p1)->Num ); + if ( Fraig_Regular(pNode->p2)->pRepr ) + printf( "Internal node %d has second fanin %d that is a secondary node.\n", + pNode->Num, Fraig_Regular(pNode->p2)->Num ); + } + } + Fraig_NodeVecFree( pVec ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Prints the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrintNode( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + Fraig_NodeVec_t * vNodes; + Fraig_Node_t * pTemp; + int fCompl1, fCompl2, i; + + vNodes = Fraig_DfsOne( p, pNode, 0 ); + for ( i = 0; i < vNodes->nSize; i++ ) + { + pTemp = vNodes->pArray[i]; + if ( Fraig_NodeIsVar(pTemp) ) + { + printf( "%3d : PI ", pTemp->Num ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 ); + printf( " " ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 ); + printf( " %d\n", pTemp->fInv ); + continue; + } + + fCompl1 = Fraig_IsComplement(pTemp->p1); + fCompl2 = Fraig_IsComplement(pTemp->p2); + printf( "%3d : %c%3d %c%3d ", pTemp->Num, + (fCompl1? '-':'+'), Fraig_Regular(pTemp->p1)->Num, + (fCompl2? '-':'+'), Fraig_Regular(pTemp->p2)->Num ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 ); + printf( " " ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 ); + printf( " %d\n", pTemp->fInv ); + } + Fraig_NodeVecFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Prints the bit string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits ) +{ + int Remainder, nWords; + int w, i; + + Remainder = (nBits%(sizeof(unsigned)*8)); + nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); + + for ( w = nWords-1; w >= 0; w-- ) + for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) + fprintf( pFile, "%c", '0' + (int)((pSign[w] & (1<<i)) > 0) ); + +// fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Sets up the mask.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_GetMaxLevel( Fraig_Man_t * pMan ) +{ + int nLevelMax, i; + nLevelMax = 0; + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? + nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level; + return nLevelMax; +} + +/**Function************************************************************* + + Synopsis [Analyses choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fMaximum ) +{ + Fraig_Node_t * pTemp; + int Level1, Level2, LevelE; + assert( !Fraig_IsComplement(pNode) ); + if ( !Fraig_NodeIsAnd(pNode) ) + return pNode->Level; + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return pNode->Level; + pNode->TravId = pMan->nTravIds; + // compute levels of the children nodes + Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum ); + Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum ); + pNode->Level = 1 + FRAIG_MAX( Level1, Level2 ); + if ( pNode->pNextE ) + { + LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum ); + if ( fMaximum ) + { + if ( pNode->Level < LevelE ) + pNode->Level = LevelE; + } + else + { + if ( pNode->Level > LevelE ) + pNode->Level = LevelE; + } + // set the level of all equivalent nodes to be the same minimum + if ( pNode->pRepr == NULL ) // the primary node + for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE ) + pTemp->Level = pNode->Level; + } + return pNode->Level; +} + +/**Function************************************************************* + + Synopsis [Resets the levels of the nodes in the choice graph.] + + Description [Makes the level of the choice nodes to be equal to the + maximum of the level of the nodes in the equivalence class. This way + sorting by level leads to the reverse topological order, which is + needed for the required time computation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum ) +{ + int i; + pMan->nTravIds++; + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum ); +} + +/**Function************************************************************* + + Synopsis [Reports statistics on choice nodes.] + + Description [The number of choice nodes is the number of primary nodes, + which has pNextE set to a pointer. The number of choices is the number + of entries in the equivalent-node lists of the primary nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManReportChoices( Fraig_Man_t * pMan ) +{ + Fraig_Node_t * pNode, * pTemp; + int nChoiceNodes, nChoices; + int i, LevelMax1, LevelMax2; + + // report the number of levels + LevelMax1 = Fraig_GetMaxLevel( pMan ); + Fraig_MappingSetChoiceLevels( pMan, 0 ); + LevelMax2 = Fraig_GetMaxLevel( pMan ); + + // report statistics about choices + nChoiceNodes = nChoices = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + { + pNode = pMan->vNodes->pArray[i]; + if ( pNode->pRepr == NULL && pNode->pNextE != NULL ) + { // this is a choice node = the primary node that has equivalent nodes + nChoiceNodes++; + for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE ) + nChoices++; + } + } + printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 ); + printf( "Choice stats: Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of EXOR/NEXOR gate.] + + Description [The node can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsExorType( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + // make the node regular (it does not matter for EXOR/NEXOR) + pNode = Fraig_Regular(pNode); + // if the node or its children are not ANDs or not compl, this cannot be EXOR type + if ( !Fraig_NodeIsAnd(pNode) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) ) + return 0; + + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + assert( pNode1->Num < pNode2->Num ); + + // compare grandchildren + return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [The node can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsMuxType( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + + // make the node regular (it does not matter for EXOR/NEXOR) + pNode = Fraig_Regular(pNode); + // if the node or its children are not ANDs or not compl, this cannot be EXOR type + if ( !Fraig_NodeIsAnd(pNode) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) ) + return 0; + + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + assert( pNode1->Num < pNode2->Num ); + + // compare grandchildren + // node is an EXOR/NEXOR + if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) ) + return 1; + + // otherwise the node is MUX iff it has a pair of equal grandchildren + return pNode1->p1 == Fraig_Not(pNode2->p1) || + pNode1->p1 == Fraig_Not(pNode2->p2) || + pNode1->p2 == Fraig_Not(pNode2->p1) || + pNode1->p2 == Fraig_Not(pNode2->p2); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is EXOR, 0 if it is NEXOR.] + + Description [The node should be EXOR type and not complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsExor( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1; + assert( !Fraig_IsComplement(pNode) ); + assert( Fraig_NodeIsExorType(pNode) ); + assert( Fraig_IsComplement(pNode->p1) ); + // get children + pNode1 = Fraig_Regular(pNode->p1); + return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE ) +{ + Fraig_Node_t * pNode1, * pNode2; + assert( !Fraig_IsComplement(pNode) ); + assert( Fraig_NodeIsMuxType(pNode) ); + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + // find the control variable + if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + { + if ( Fraig_IsComplement(pNode1->p1) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p2); + *ppNodeE = Fraig_Not(pNode1->p2); + return pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p2); + *ppNodeE = Fraig_Not(pNode2->p2); + return pNode1->p1; + } + } + else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + { + if ( Fraig_IsComplement(pNode1->p1) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p1); + *ppNodeE = Fraig_Not(pNode1->p2); + return pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p2); + *ppNodeE = Fraig_Not(pNode2->p1); + return pNode1->p1; + } + } + else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + { + if ( Fraig_IsComplement(pNode1->p2) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p2); + *ppNodeE = Fraig_Not(pNode1->p1); + return pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p1); + *ppNodeE = Fraig_Not(pNode2->p2); + return pNode1->p2; + } + } + else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + { + if ( Fraig_IsComplement(pNode1->p2) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p1); + *ppNodeE = Fraig_Not(pNode1->p1); + return pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p1); + *ppNodeE = Fraig_Not(pNode2->p1); + return pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCountExors( Fraig_Man_t * pMan ) +{ + int i, nExors; + nExors = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] ); + return nExors; + +} + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCountMuxes( Fraig_Man_t * pMan ) +{ + int i, nMuxes; + nMuxes = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] ); + return nMuxes; + +} + +/**Function************************************************************* + + Synopsis [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ) +{ + unsigned * pUnsigned1, * pUnsigned2; + int i; + + // compare random siminfo + pUnsigned1 = pNode1->puSimR; + pUnsigned2 = pNode2->puSimR; + for ( i = 0; i < pMan->nWordsRand; i++ ) + if ( pUnsigned1[i] & ~pUnsigned2[i] ) + return 0; + + // compare systematic siminfo + pUnsigned1 = pNode1->puSimD; + pUnsigned2 = pNode2->puSimD; + for ( i = 0; i < pMan->iWordStart; i++ ) + if ( pUnsigned1[i] & ~pUnsigned2[i] ) + return 0; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Count the number of PI variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums ) +{ + int * pVars, nVars, i, Counter; + + nVars = Msat_IntVecReadSize(vVarNums); + pVars = Msat_IntVecReadArray(vVarNums); + Counter = 0; + for ( i = 0; i < nVars; i++ ) + Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] ); + return Counter; +} + + + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManPrintRefs( Fraig_Man_t * pMan ) +{ + Fraig_NodeVec_t * vPivots; + Fraig_Node_t * pNode, * pNode2; + int i, k, Counter, nProved; + int clk; + + vPivots = Fraig_NodeVecAlloc( 1000 ); + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + { + pNode = pMan->vNodes->pArray[i]; + + if ( pNode->nOnes == 0 || pNode->nOnes == (unsigned)pMan->nWordsRand * 32 ) + continue; + + if ( pNode->nRefs > 5 ) + { + Fraig_NodeVecPush( vPivots, pNode ); +// printf( "Node %6d : nRefs = %2d Level = %3d.\n", pNode->Num, pNode->nRefs, pNode->Level ); + } + } + printf( "Total nodes = %d. Referenced nodes = %d.\n", pMan->vNodes->nSize, vPivots->nSize ); + +clk = clock(); + // count implications + Counter = nProved = 0; + for ( i = 0; i < vPivots->nSize; i++ ) + for ( k = i+1; k < vPivots->nSize; k++ ) + { + pNode = vPivots->pArray[i]; + pNode2 = vPivots->pArray[k]; + if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) ) + { + if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) ) + nProved++; + Counter++; + } + else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) ) + { + if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) ) + nProved++; + Counter++; + } + } + printf( "Number of candidate pairs = %d. Proved = %d.\n", Counter, nProved ); +PRT( "Time", clock() - clk ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Checks if pNew exists among the implication fanins of pOld.] + + Description [If pNew is an implication fanin of pOld, returns 1. + If Fraig_Not(pNew) is an implication fanin of pOld, return -1. + Otherwise returns 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int RetValue1, RetValue2; + if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) ) + return (pOld == pNew)? 1 : -1; + if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) ) + return 0; + RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew ); + RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + if ( RetValue1 == 1 || RetValue2 == 1 ) + return 1; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_CollectSupergate_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, int fFirst, int fStopAtMux ) +{ + // if the new node is complemented or a PI, another gate begins +// if ( Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || Fraig_NodeIsMuxType(pNode) ) + if ( (!fFirst && Fraig_Regular(pNode)->nRefs > 1) || + Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || + (fStopAtMux && Fraig_NodeIsMuxType(pNode)) ) + { + Fraig_NodeVecPushUnique( vSuper, pNode ); + return; + } + // go through the branches + Fraig_CollectSupergate_rec( pNode->p1, vSuper, 0, fStopAtMux ); + Fraig_CollectSupergate_rec( pNode->p2, vSuper, 0, fStopAtMux ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux ) +{ + Fraig_NodeVec_t * vSuper; + vSuper = Fraig_NodeVecAlloc( 8 ); + Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux ); + return vSuper; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ) +{ + pMan->nTravIds2++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + pNode->TravId2 = pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2 - 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c new file mode 100644 index 00000000..ba3feecd --- /dev/null +++ b/src/sat/fraig/fraigVec.c @@ -0,0 +1,545 @@ +/**CFile**************************************************************** + + FileName [fraigVec.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Vector of FRAIG nodes.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigVec.c,v 1.7 2005/07/08 01:01:34 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates a vector with the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap ) +{ + Fraig_NodeVec_t * p; + p = ALLOC( Fraig_NodeVec_t, 1 ); + if ( nCap > 0 && nCap < 8 ) + nCap = 8; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecFree( Fraig_NodeVec_t * p ) +{ + FREE( p->pArray ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Duplicates the integer array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_NodeVecDup( Fraig_NodeVec_t * pVec ) +{ + Fraig_NodeVec_t * p; + p = ALLOC( Fraig_NodeVec_t, 1 ); + p->nSize = pVec->nSize; + p->nCap = pVec->nCap; + p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL; + memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t ** Fraig_NodeVecReadArray( Fraig_NodeVec_t * p ) +{ + return p->pArray; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecReadSize( Fraig_NodeVec_t * p ) +{ + return p->nSize; +} + +/**Function************************************************************* + + Synopsis [Resizes the vector to the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); + p->nCap = nCapMin; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecShrink( Fraig_NodeVec_t * p, int nSizeNew ) +{ + assert( p->nSize >= nSizeNew ); + p->nSize = nSizeNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecClear( Fraig_NodeVec_t * p ) +{ + p->nSize = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecPush( Fraig_NodeVec_t * p, Fraig_Node_t * Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Fraig_NodeVecGrow( p, 16 ); + else + Fraig_NodeVecGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} + +/**Function************************************************************* + + Synopsis [Add the element while ensuring uniqueness.] + + Description [Returns 1 if the element was found, and 0 if it was new. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecPushUnique( Fraig_NodeVec_t * p, Fraig_Node_t * Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + return 1; + Fraig_NodeVecPush( p, Entry ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by arrival times.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecPushOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + int i; + Fraig_NodeVecPush( p, pNode ); + // find the p of the node + for ( i = p->nSize-1; i > 0; i-- ) + { + pNode1 = p->pArray[i ]; + pNode2 = p->pArray[i-1]; + if ( pNode1 >= pNode2 ) + break; + p->pArray[i ] = pNode2; + p->pArray[i-1] = pNode1; + } +} + +/**Function************************************************************* + + Synopsis [Add the element while ensuring uniqueness in the order.] + + Description [Returns 1 if the element was found, and 0 if it was new. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecPushUniqueOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == pNode ) + return 1; + Fraig_NodeVecPushOrder( p, pNode ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by arrival times.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecPushOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + int i; + Fraig_NodeVecPush( p, pNode ); + // find the p of the node + for ( i = p->nSize-1; i > 0; i-- ) + { + pNode1 = p->pArray[i ]; + pNode2 = p->pArray[i-1]; + if ( Fraig_Regular(pNode1)->Level <= Fraig_Regular(pNode2)->Level ) + break; + p->pArray[i ] = pNode2; + p->pArray[i-1] = pNode1; + } +} + +/**Function************************************************************* + + Synopsis [Add the element while ensuring uniqueness in the order.] + + Description [Returns 1 if the element was found, and 0 if it was new. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecPushUniqueOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == pNode ) + return 1; + Fraig_NodeVecPushOrderByLevel( p, pNode ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeVecPop( Fraig_NodeVec_t * p ) +{ + return p->pArray[--p->nSize]; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecRemove( Fraig_NodeVec_t * p, Fraig_Node_t * Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + break; + assert( i < p->nSize ); + for ( i++; i < p->nSize; i++ ) + p->pArray[i-1] = p->pArray[i]; + p->nSize--; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecWriteEntry( Fraig_NodeVec_t * p, int i, Fraig_Node_t * Entry ) +{ + assert( i >= 0 && i < p->nSize ); + p->pArray[i] = Entry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeVecReadEntry( Fraig_NodeVec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i]; +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecCompareLevelsIncreasing( Fraig_Node_t ** pp1, Fraig_Node_t ** pp2 ) +{ + int Level1 = Fraig_Regular(*pp1)->Level; + int Level2 = Fraig_Regular(*pp2)->Level; + if ( Level1 < Level2 ) + return -1; + if ( Level1 > Level2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecCompareLevelsDecreasing( Fraig_Node_t ** pp1, Fraig_Node_t ** pp2 ) +{ + int Level1 = Fraig_Regular(*pp1)->Level; + int Level2 = Fraig_Regular(*pp2)->Level; + if ( Level1 > Level2 ) + return -1; + if ( Level1 < Level2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecCompareNumbers( Fraig_Node_t ** pp1, Fraig_Node_t ** pp2 ) +{ + int Num1 = Fraig_Regular(*pp1)->Num; + int Num2 = Fraig_Regular(*pp2)->Num; + if ( Num1 < Num2 ) + return -1; + if ( Num1 > Num2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeVecCompareRefCounts( Fraig_Node_t ** pp1, Fraig_Node_t ** pp2 ) +{ + int nRefs1 = Fraig_Regular(*pp1)->nRefs; + int nRefs2 = Fraig_Regular(*pp2)->nRefs; + + if ( nRefs1 < nRefs2 ) + return -1; + if ( nRefs1 > nRefs2 ) + return 1; + + nRefs1 = Fraig_Regular(*pp1)->Level; + nRefs2 = Fraig_Regular(*pp2)->Level; + + if ( nRefs1 < nRefs2 ) + return -1; + if ( nRefs1 > nRefs2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Sorting the entries by their integer value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecSortByLevel( Fraig_NodeVec_t * p, int fIncreasing ) +{ + if ( fIncreasing ) + qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), + (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsIncreasing ); + else + qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), + (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsDecreasing ); +} + +/**Function************************************************************* + + Synopsis [Sorting the entries by their integer value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecSortByNumber( Fraig_NodeVec_t * p ) +{ + qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), + (int (*)(const void *, const void *)) Fraig_NodeVecCompareNumbers ); +} + +/**Function************************************************************* + + Synopsis [Sorting the entries by their integer value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ) +{ + qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), + (int (*)(const void *, const void *)) Fraig_NodeVecCompareRefCounts ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/fraig/module.make b/src/sat/fraig/module.make new file mode 100644 index 00000000..cc6eb9d3 --- /dev/null +++ b/src/sat/fraig/module.make @@ -0,0 +1,12 @@ +SRC += src/sat/fraig/fraigApi.c \ + src/sat/fraig/fraigCanon.c \ + src/sat/fraig/fraigFanout.c \ + src/sat/fraig/fraigFeed.c \ + src/sat/fraig/fraigMan.c \ + src/sat/fraig/fraigMem.c \ + src/sat/fraig/fraigNode.c \ + src/sat/fraig/fraigPrime.c \ + src/sat/fraig/fraigSat.c \ + src/sat/fraig/fraigTable.c \ + src/sat/fraig/fraigUtil.c \ + src/sat/fraig/fraigVec.c |