summaryrefslogtreecommitdiffstats
path: root/src/sat/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/aig')
-rw-r--r--src/sat/aig/aig.h64
-rw-r--r--src/sat/aig/aigMan.c15
-rw-r--r--src/sat/aig/aigMem.c2
-rw-r--r--src/sat/aig/aigNode.c7
-rw-r--r--src/sat/aig/aigTable.c19
-rw-r--r--src/sat/aig/aigUtil.c130
-rw-r--r--src/sat/aig/fraigClass.c60
-rw-r--r--src/sat/aig/fraigCnf.c476
-rw-r--r--src/sat/aig/fraigCore.c86
-rw-r--r--src/sat/aig/fraigEngine.c131
-rw-r--r--src/sat/aig/fraigProve.c4
-rw-r--r--src/sat/aig/fraigSim.c184
-rw-r--r--src/sat/aig/fraigSolver.c47
-rw-r--r--src/sat/aig/fraigTrav.c47
14 files changed, 1187 insertions, 85 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 009a17bb..55a75cf5 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -48,6 +48,7 @@
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
+#include "solver.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
@@ -70,6 +71,7 @@ typedef struct Aig_Edge_t_ Aig_Edge_t;
typedef struct Aig_MemFixed_t_ Aig_MemFixed_t;
typedef struct Aig_SimInfo_t_ Aig_SimInfo_t;
typedef struct Aig_Table_t_ Aig_Table_t;
+typedef struct Aig_Pattern_t_ Aig_Pattern_t;
// network types
typedef enum {
@@ -79,12 +81,25 @@ typedef enum {
AIG_AND // 3: internal node
} Aig_NodeType_t;
+// proof outcomes
+typedef enum {
+ AIG_PROOF_NONE = 0, // 0: unknown
+ AIG_PROOF_SAT, // 1: primary input
+ AIG_PROOF_UNSAT, // 2: primary output
+ AIG_PROOF_TIMEOUT, // 3: primary output
+ AIG_PROOF_FAIL // 4: internal node
+} Aig_ProofType_t;
+
+
+
// the AIG parameters
struct Aig_Param_t_
{
int nPatsRand; // the number of random patterns
int nBTLimit; // backtrack limit at the intermediate nodes
int nSeconds; // the runtime limit at the final miter
+ int fVerbose; // verbosity
+ int fSatVerbose; // verbosity of SAT
};
// the AIG edge
@@ -127,6 +142,13 @@ struct Aig_Man_t_
Vec_Ptr_t * vPos; // all POs
Aig_Table_t * pTable; // structural hash table
int nLevelMax; // the maximum level
+ // SAT solver and related structures
+ solver * pSat;
+ Vec_Int_t * vVar2Sat; // mapping of nodes into their SAT var numbers (for each node num)
+ Vec_Int_t * vSat2Var; // mapping of the SAT var numbers into nodes (for each SAT var)
+ Vec_Int_t * vPiSatNums; // the SAT variable numbers (for each PI)
+ int * pModel; // the satisfying assignment (for each PI)
+ int nMuxes; // the number of MUXes
// fanout representation
Vec_Ptr_t * vFanPivots; // fanout pivots
Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin
@@ -136,6 +158,7 @@ struct Aig_Man_t_
int nTravIds; // the traversal ID
// simulation info
Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs
+ Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes
Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes
// simulation patterns
int nPiWords; // the number of words in the PI info
@@ -148,6 +171,14 @@ struct Aig_Man_t_
Vec_Ptr_t * vToReplace; // the nodes to replace
};
+// the simulation patter
+struct Aig_Pattern_t_
+{
+ int nBits;
+ int nWords;
+ unsigned * pData;
+};
+
// the AIG simulation info
struct Aig_SimInfo_t_
{
@@ -166,9 +197,9 @@ struct Aig_SimInfo_t_
for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
#define Aig_ManForEachPo( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
-#define Aig_ManForEachAnd( pNtk, pNode, i ) \
+#define Aig_ManForEachAnd( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \
- if ( Aig_NodeIsAnd(pNode) ) {} else
+ if ( !Aig_NodeIsAnd(pNode) ) {} else
// maximum/minimum operators
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
@@ -178,8 +209,12 @@ struct Aig_SimInfo_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
+static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
+static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
+static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan ) { return pMan->pConst1; }
static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); }
static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); }
static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); }
@@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_N
static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); }
static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; }
static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; }
-static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; }
static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; }
@@ -268,6 +304,7 @@ extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
extern void Aig_NodePrint( Aig_Node_t * pNode );
extern char * Aig_NodeName( Aig_Node_t * pNode );
+extern void Aig_PrintNode( Aig_Node_t * pNode );
/*=== aigOper.c ==========================================================*/
extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
@@ -287,18 +324,33 @@ extern void Aig_TableResize( Aig_Man_t * pMan );
extern void Aig_TableRehash( Aig_Man_t * pMan );
/*=== aigUtil.c ==========================================================*/
extern void Aig_ManIncrementTravId( Aig_Man_t * pMan );
-extern void Aig_PrintNode( Aig_Node_t * pNode );
+extern bool Aig_NodeIsMuxType( Aig_Node_t * pNode );
+extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE );
+/*=== fraigCore.c ==========================================================*/
+extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan );
/*=== fraigClasses.c ==========================================================*/
extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
+extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses );
+/*=== fraigCnf.c ==========================================================*/
+extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan );
+/*=== fraigEngine.c ==========================================================*/
+extern void Aig_EngineSimulateFirst( Aig_Man_t * p );
+extern int Aig_EngineSimulate( Aig_Man_t * p );
+extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
/*=== fraigSim.c ==========================================================*/
extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
extern void Aig_SimInfoClean( Aig_SimInfo_t * p );
extern void Aig_SimInfoRandom( Aig_SimInfo_t * p );
+extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat );
extern void Aig_SimInfoResize( Aig_SimInfo_t * p );
extern void Aig_SimInfoFree( Aig_SimInfo_t * p );
-extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
+extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll );
+extern Aig_Pattern_t * Aig_PatternAlloc( int nBits );
+extern void Aig_PatternClean( Aig_Pattern_t * pPat );
+extern void Aig_PatternRandom( Aig_Pattern_t * pPat );
+extern void Aig_PatternFree( Aig_Pattern_t * pPat );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
index 2058f6b0..3807d28a 100644
--- a/src/sat/aig/aigMan.c
+++ b/src/sat/aig/aigMan.c
@@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
// start the manager
p = ALLOC( Aig_Man_t, 1 );
memset( p, 0, sizeof(Aig_Man_t) );
- p->pParam = &p->Param;
- p->nTravIds = 1;
+ p->pParam = &p->Param;
+ p->nTravIds = 1;
+ p->nPatsMax = 20;
// set the defaults
- *p->pParam = *pParam;
+ *p->pParam = *pParam;
// start memory managers
p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) );
// allocate node arrays
@@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan )
***********************************************************************/
void Aig_ManStop( Aig_Man_t * p )
{
+ // SAT solver
+ if ( p->pSat ) solver_delete( p->pSat );
+ if ( p->vVar2Sat ) Vec_IntFree( p->vVar2Sat );
+ if ( p->vSat2Var ) Vec_IntFree( p->vSat2Var );
+ if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums );
+ // fanouts
if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots );
if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 );
if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 );
if ( p->vClasses ) Vec_VecFree( p->vClasses );
+ // nodes
Aig_MemFixedStop( p->mmNodes, 0 );
Vec_PtrFree( p->vNodes );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
+ // temporary
Vec_PtrFree( p->vFanouts );
Vec_PtrFree( p->vToReplace );
Aig_TableFree( p->pTable );
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
index 280cf98b..32709bf6 100644
--- a/src/sat/aig/aigMem.c
+++ b/src/sat/aig/aigMem.c
@@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p )
int i;
char * pTemp;
- // delocate all chunks except the first one
+ // deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
index afccd985..991cc7e5 100644
--- a/src/sat/aig/aigNode.c
+++ b/src/sat/aig/aigNode.c
@@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes );
memset( pNode, 0, sizeof(Aig_Node_t) );
// assign the number and add to the array of nodes
+ pNode->pMan = p;
pNode->Id = p->vNodes->nSize;
Vec_PtrPush( p->vNodes, pNode );
return pNode;
@@ -66,6 +67,7 @@ Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_NONE;
pNode->fPhase = 1; // sim value for 000... pattern
return pNode;
}
@@ -86,7 +88,8 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
Vec_PtrPush( p->vPis, pNode );
- pNode->fPhase = 0; // sim value for 000... pattern
+ pNode->Type = AIG_PI;
+ pNode->fPhase = 0; // sim value for 000... pattern
return pNode;
}
@@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_PO;
Vec_PtrPush( p->vPos, pNode );
// connect to the fanin
pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
@@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_AND;
Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
return pNode;
}
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
index cfc94f6b..e6fe87d6 100644
--- a/src/sat/aig/aigTable.c
+++ b/src/sat/aig/aigTable.c
@@ -36,7 +36,7 @@ struct Aig_Table_t_
#define Aig_TableBinForEachEntry( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
- pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
+ pEnt = Aig_NodeNextH(pEnt) )
#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \
@@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_Node_t * pAnd;
unsigned Key;
assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
- assert( p0->pMan == p1->pMan );
// get the hash key for these two nodes
- Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+ Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
// find the matching node in the table
Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) )
@@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_TableResize( pMan );
// add the node to the corresponding linked list in the table
Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
- pAnd->NextH = pMan->pTable->pBins[Key]->Id;
- pMan->pTable->pBins[Key]->NextH = pAnd->Id;
+ pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0;
+ pMan->pTable->pBins[Key] = pAnd;
pMan->pTable->nEntries++;
return pAnd;
}
@@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
if ( pPlace == NULL )
pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
else
- pPlace->NextH = pThis->Id;
+ pPlace->NextH = pThis->NextH;
break;
}
assert( pThis == pAnd );
@@ -232,8 +231,8 @@ clk = clock();
Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
{
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
- pEnt->NextH = pBinsNew[Key]->Id;
- pBinsNew[Key]->NextH = pEnt->Id;
+ pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+ pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
@@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan )
}
// rehash the node
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
- pEnt->NextH = pBinsNew[Key]->Id;
- pBinsNew[Key]->NextH = pEnt->Id;
+ pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+ pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c
index a1c9ca44..40f7aba1 100644
--- a/src/sat/aig/aigUtil.c
+++ b/src/sat/aig/aigUtil.c
@@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan )
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Aig_NodeIsMuxType( Aig_Node_t * pNode )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ // check that the node is regular
+ assert( !Aig_IsComplement(pNode) );
+ // if the node is not AND, this is not MUX
+ if ( !Aig_NodeIsAnd(pNode) )
+ return 0;
+ // if the children are not complemented, this is not MUX
+ if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) )
+ return 0;
+ // get children
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ // if the children are not ANDs, this is not MUX
+ if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) )
+ return 0;
+ // otherwise the node is MUX iff it has a pair of equal grandchildren
+ return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
+ (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) ||
+ (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
+ (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)));
+}
+
+/**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 []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_NodeIsMuxType(pNode) );
+ // get children
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ // find the control variable
+// if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
+ if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p1) )
+ if ( Aig_NodeFaninC0(pNode0) )
+ { // pNode2->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ return Aig_NodeChild0(pNode1);//pNode2->p1;
+ }
+ else
+ { // pNode1->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ return Aig_NodeChild0(pNode0);//pNode1->p1;
+ }
+ }
+// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
+ else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p1) )
+ if ( Aig_NodeFaninC0(pNode0) )
+ { // pNode2->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ return Aig_NodeChild1(pNode1);//pNode2->p2;
+ }
+ else
+ { // pNode1->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ return Aig_NodeChild0(pNode0);//pNode1->p1;
+ }
+ }
+// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
+ else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p2) )
+ if ( Aig_NodeFaninC1(pNode0) )
+ { // pNode2->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ return Aig_NodeChild0(pNode1);//pNode2->p1;
+ }
+ else
+ { // pNode1->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ return Aig_NodeChild1(pNode0);//pNode1->p2;
+ }
+ }
+// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
+ else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p2) )
+ if ( Aig_NodeFaninC1(pNode0) )
+ { // pNode2->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ return Aig_NodeChild1(pNode1);//pNode2->p2;
+ }
+ else
+ { // pNode1->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ return Aig_NodeChild1(pNode0);//pNode1->p2;
+ }
+ }
+ assert( 0 ); // this is not MUX
+ return NULL;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
index b3040e2a..2f2d3e0c 100644
--- a/src/sat/aig/fraigClass.c
+++ b/src/sat/aig/fraigClass.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigFraig.c]
+ FileName [fraigClass.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -25,7 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
+static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
***********************************************************************/
Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
{
- Vec_Vec_t * vClasses; // equivalence classes
+ Vec_Vec_t * vClasses; // equivalence classes
stmm_table * tSim2Node; // temporary hash table hashing key into the class number
Aig_Node_t * pNode;
unsigned uKey;
- int i, * pSpot, ClassNum;
+ int i, * pSpot, Entry, ClassNum;
assert( pInfo->Type == 1 );
// fill in the hash table
tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
vClasses = Vec_VecAlloc( 100 );
- Aig_ManForEachNode( p, pNode, i )
+ // enumerate the nodes considered in the equivalence classes
+// Aig_ManForEachNode( p, pNode, i )
+ Vec_IntForEachEntry( p->vSat2Var, Entry, i )
{
+ pNode = Aig_ManNode( p, Entry );
+
if ( Aig_NodeIsPo(pNode) )
continue;
- uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords );
+ uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase );
if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist
*pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing
else if ( (*pSpot) & 1 ) // this is a node
@@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
}
else // this is a class
{
- ClassNum = (*pSpot) >> 1;
+ ClassNum = ((*pSpot) >> 1);
Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
}
}
stmm_free_table( tSim2Node );
+
+ // print the classes
+ {
+ Vec_Ptr_t * vVec;
+ printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n",
+ Aig_ManPiNum(p), Aig_ManPoNum(p),
+ Aig_ManNodeNum(p) - Aig_ManPoNum(p),
+ Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) );
+
+ Vec_VecForEachLevel( vClasses, vVec, i )
+ printf( "%d ", Vec_PtrSize(vVec) );
+ printf( "\n" );
+ }
return vClasses;
}
@@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
SeeAlso []
***********************************************************************/
-unsigned Aig_ManHashKey( unsigned * pData, int nWords )
+unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
{
static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
unsigned uKey;
int i;
uKey = 0;
- for ( i = 0; i < nWords; i++ )
- uKey ^= pData[i] * Primes[i%10];
+ if ( fPhase )
+ for ( i = 0; i < nWords; i++ )
+ uKey ^= Primes[i%10] * pData[i];
+ else
+ for ( i = 0; i < nWords; i++ )
+ uKey ^= Primes[i%10] * ~pData[i];
return uKey;
}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the equivalence classes using the simulation info.]
+
+ Description [Records successful simulation patterns into the pattern
+ storage.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses )
+{
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c
new file mode 100644
index 00000000..913165b2
--- /dev/null
+++ b/src/sat/aig/fraigCnf.c
@@ -0,0 +1,476 @@
+/**CFile****************************************************************
+
+ FileName [fraigCnf.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: fraigCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseTriv( solver * pSat, Aig_Node_t * pNode, Vec_Int_t * vVars )
+{
+//printf( "Adding triv %d. %d\n", Aig_Regular(pNode)->Id, (int)pSat->solver_stats.clauses );
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond( Aig_Regular(pNode)->Data, Aig_IsComplement(pNode) ) );
+// Vec_IntPush( vVars, toLitCond( (int)Aig_Regular(pNode)->Id, Aig_IsComplement(pNode) ) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseAnd( solver * pSat, Aig_Node_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
+{
+ int fComp1, Var, Var1, i;
+//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses );
+
+ assert( !Aig_IsComplement( pNode ) );
+ assert( Aig_NodeIsAnd( pNode ) );
+
+// nVars = solver_nvars(pSat);
+ Var = pNode->Data;
+// Var = pNode->Id;
+
+// assert( Var < nVars );
+ for ( i = 0; i < vSuper->nSize; i++ )
+ {
+ // get the predecessor nodes
+ // get the complemented attributes of the nodes
+ fComp1 = Aig_IsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = Aig_Regular(vSuper->pArray[i])->Data;
+// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
+
+ // 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 );
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
+ Vec_IntPush( vVars, toLitCond(Var, 1 ) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ }
+
+ // add A & B => C or !A + !B + C
+// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
+ vVars->nSize = 0;
+ for ( i = 0; i < vSuper->nSize; i++ )
+ {
+ // get the predecessor nodes
+ // get the complemented attributes of the nodes
+ fComp1 = Aig_IsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = Aig_Regular(vSuper->pArray[i])->Data;
+// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
+ // add this variable to the array
+ Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
+ }
+ Vec_IntPush( vVars, toLitCond(Var, 0) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseMux( solver * pSat, Aig_Node_t * pNode, Aig_Node_t * pNodeC, Aig_Node_t * pNodeT, Aig_Node_t * pNodeE, Vec_Int_t * vVars )
+{
+ int VarF, VarI, VarT, VarE, fCompT, fCompE;
+//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses );
+
+ assert( !Aig_IsComplement( pNode ) );
+ assert( Aig_NodeIsMuxType( pNode ) );
+ // get the variable numbers
+ VarF = pNode->Data;
+ VarI = pNodeC->Data;
+ VarT = Aig_Regular(pNodeT)->Data;
+ VarE = Aig_Regular(pNodeE)->Data;
+// VarF = (int)pNode->Id;
+// VarI = (int)pNodeC->Id;
+// VarT = (int)Aig_Regular(pNodeT)->Id;
+// VarE = (int)Aig_Regular(pNodeE)->Id;
+
+ // get the complementation flags
+ fCompT = Aig_IsComplement(pNodeT);
+ fCompE = Aig_IsComplement(pNodeE);
+
+ // f = ITE(i, t, e)
+ // i' + t' + f
+ // i' + t + f'
+ // i + e' + f
+ // i + e + f'
+ // create four clauses
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 1) );
+ Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 1) );
+ Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 0) );
+ Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 0) );
+ Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return 1;
+ }
+
+ // two additional clauses
+ // t' & e' -> f' t + e + f'
+ // t & e -> f t' + e' + f
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseCollectSupergate_rec( Aig_Node_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
+{
+ int RetValue1, RetValue2, i;
+ // check if the node is visited
+ if ( Aig_Regular(pNode)->fMarkB )
+ {
+ // check if the node occurs in the same polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == pNode )
+ return 1;
+ // check if the node is present in the opposite polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == Aig_Not(pNode) )
+ return -1;
+ assert( 0 );
+ return 0;
+ }
+ // if the new node is complemented or a PI, another gate begins
+ if ( !fFirst )
+ if ( Aig_IsComplement(pNode) || !Aig_NodeIsAnd(pNode) || Aig_NodeRefs(pNode) > 1 || fStopAtMux && Aig_NodeIsMuxType(pNode) )
+ {
+ Vec_PtrPush( vSuper, pNode );
+ Aig_Regular(pNode)->fMarkB = 1;
+ return 0;
+ }
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_NodeIsAnd(pNode) );
+ // go through the branches
+ RetValue1 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild0(pNode), vSuper, 0, fStopAtMux );
+ RetValue2 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild1(pNode), vSuper, 0, fStopAtMux );
+ if ( RetValue1 == -1 || RetValue2 == -1 )
+ return -1;
+ // return 1 if at least one branch has a duplicate
+ return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ClauseCollectSupergate( Aig_Node_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
+{
+ int RetValue, i;
+ assert( !Aig_IsComplement(pNode) );
+ // collect the nodes in the implication supergate
+ Vec_PtrClear( vNodes );
+ RetValue = Aig_ClauseCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
+ assert( vNodes->nSize > 1 );
+ // unmark the visited nodes
+ for ( i = 0; i < vNodes->nSize; i++ )
+ Aig_Regular((Aig_Node_t *)vNodes->pArray[i])->fMarkB = 0;
+ // if we found the node and its complement in the same implication supergate,
+ // return empty set of nodes (meaning that we should use constant-0 node)
+ if ( RetValue == -1 )
+ vNodes->nSize = 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Sets up the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseCreateCnfInt( solver * pSat, Aig_Man_t * pNtk )
+{
+ Aig_Node_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
+ Vec_Ptr_t * vNodes, * vSuper;
+ Vec_Int_t * vVars;
+ int i, k, fUseMuxes = 1;
+
+ // start the data structures
+ vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver
+ vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate
+ vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause
+
+ // add the clause for the constant node
+ pNode = Aig_ManConst1(pNtk);
+ pNode->fMarkA = 1;
+ pNode->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pNode );
+ Aig_ClauseTriv( pSat, pNode, vVars );
+
+ // collect the nodes that need clauses and top-level assignments
+ Aig_ManForEachPo( pNtk, pNode, i )
+ {
+ // get the fanin
+ pFanin = Aig_NodeFanin0(pNode);
+ // create the node's variable
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ // add the trivial clause
+ if ( !Aig_ClauseTriv( pSat, Aig_NodeChild0(pNode), vVars ) )
+ return 0;
+ }
+
+ // add the clauses
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ assert( !Aig_IsComplement(pNode) );
+ if ( !Aig_NodeIsAnd(pNode) )
+ continue;
+//printf( "%d ", pNode->Id );
+
+ // add the clauses
+ if ( fUseMuxes && Aig_NodeIsMuxType(pNode) )
+ {
+ pNode->pMan->nMuxes++;
+ pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
+ Vec_PtrClear( vSuper );
+ Vec_PtrPush( vSuper, pNodeC );
+ Vec_PtrPush( vSuper, pNodeT );
+ Vec_PtrPush( vSuper, pNodeE );
+ // add the fanin nodes to explore
+ Vec_PtrForEachEntry( vSuper, pFanin, k )
+ {
+ pFanin = Aig_Regular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( !Aig_ClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
+ return 0;
+ }
+ else
+ {
+ // get the supergate
+ Aig_ClauseCollectSupergate( pNode, fUseMuxes, vSuper );
+ // add the fanin nodes to explore
+ Vec_PtrForEachEntry( vSuper, pFanin, k )
+ {
+ pFanin = Aig_Regular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( vSuper->nSize == 0 )
+ {
+ if ( !Aig_ClauseTriv( pSat, Aig_Not(pNode), vVars ) )
+ return 0;
+ }
+ else
+ {
+ if ( !Aig_ClauseAnd( pSat, pNode, vSuper, vVars ) )
+ return 0;
+ }
+ }
+ }
+
+ // delete
+ Vec_IntFree( vVars );
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vSuper );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets up the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+solver * Aig_ClauseCreateCnf( Aig_Man_t * pMan )
+{
+ solver * pSat;
+ Aig_Node_t * pNode;
+ int RetValue, i, clk = clock();
+ // clean the marks
+ Aig_ManForEachNode( pMan, pNode, i )
+ pNode->fMarkA = 0, pNode->Data = -1;
+ // create the solver
+ pMan->nMuxes = 0;
+ pSat = solver_new();
+ RetValue = Aig_ClauseCreateCnfInt( pSat, pMan );
+// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+ if ( RetValue == 0 )
+ {
+ solver_delete(pSat);
+ Aig_ManForEachNode( pMan, pNode, i )
+ pNode->fMarkA = 0;
+ return NULL;
+ }
+ printf( "The number of MUXes detected = %d (%5.2f %% of logic). ",
+ pNode->pMan->nMuxes, 300.0*pNode->pMan->nMuxes/Aig_ManNodeNum(pMan) );
+ PRT( "Creating solver", clock() - clk );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan )
+{
+ Aig_Node_t * pNode;
+ int i;
+
+ // make sure it has one PO
+ if ( Aig_ManPoNum(pMan) != 1 )
+ {
+ printf( "The miter has other than 1 output.\n" );
+ return AIG_PROOF_FAIL;
+ }
+
+ // get the solver
+ assert( pMan->pSat == NULL );
+ pMan->pSat = Aig_ClauseCreateCnf( pMan );
+ if ( pMan->pSat == NULL )
+ return AIG_PROOF_UNSAT;
+
+ // get the variable mappings
+ pMan->vVar2Sat = Vec_IntStart( Aig_ManNodeNum(pMan) );
+ pMan->vSat2Var = Vec_IntStart( solver_nvars(pMan->pSat) );
+ Aig_ManForEachNode( pMan, pNode, i )
+ {
+ Vec_IntWriteEntry( pMan->vVar2Sat, i, pNode->Data );
+ if ( pNode->Data >= 0 ) Vec_IntWriteEntry( pMan->vSat2Var, pNode->Data, i );
+ }
+ // get the SAT var numbers of the primary inputs
+ pMan->vPiSatNums = Vec_IntAlloc( Aig_ManPiNum(pMan) );
+ Aig_ManForEachPi( pMan, pNode, i )
+ Vec_IntPush( pMan->vPiSatNums, (pNode->Data >= 0)? pNode->Data : 0 );
+ return AIG_PROOF_NONE;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index 6187538b..e7df1335 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigFraig.c]
+ FileName [fraigCore.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -24,13 +24,56 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis []
+ Synopsis [Top-level equivalence checking procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
+{
+ Aig_ProofType_t RetValue;
+ int clk, status;
+
+ // create the solver
+ RetValue = Aig_ClauseSolverStart( pMan );
+ if ( RetValue != AIG_PROOF_NONE )
+ return RetValue;
+ // perform solving
+
+ // simplify the problem
+ clk = clock();
+ status = solver_simplify(pMan->pSat);
+ if ( status == 0 )
+ {
+// printf( "The problem is UNSATISFIABLE after simplification.\n" );
+ return AIG_PROOF_UNSAT;
+ }
+
+ // try to prove the output
+ RetValue = Aig_FraigProveOutput( pMan );
+ if ( RetValue != AIG_PROOF_TIMEOUT )
+ return RetValue;
+
+ // create equivalence classes
+ Aig_EngineSimulateRandomFirst( pMan );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Top-level equivalence checking procedure.]
Description []
@@ -39,6 +82,43 @@
SeeAlso []
***********************************************************************/
+Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
+{
+ Aig_ProofType_t RetValue;
+ int clk, status;
+
+ // solve the miter
+ clk = clock();
+ pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
+ status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
+ if ( status == l_Undef )
+ {
+// printf( "The problem timed out.\n" );
+ RetValue = AIG_PROOF_TIMEOUT;
+ }
+ else if ( status == l_True )
+ {
+// printf( "The problem is SATISFIABLE.\n" );
+ RetValue = AIG_PROOF_SAT;
+ }
+ else if ( status == l_False )
+ {
+// printf( "The problem is UNSATISFIABLE.\n" );
+ RetValue = AIG_PROOF_UNSAT;
+ }
+ else
+ assert( 0 );
+// PRT( "SAT solver time", clock() - clk );
+
+ // if the problem is SAT, get the counterexample
+ if ( status == l_True )
+ {
+ if ( pMan->pModel ) free( pMan->pModel );
+ pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize );
+ printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] );
+ }
+ return RetValue;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c
new file mode 100644
index 00000000..6214bf3b
--- /dev/null
+++ b/src/sat/aig/fraigEngine.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+ FileName [fraigEngine.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: fraigEngine.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the simulation engine for the first time.]
+
+ Description [Tries several random patterns and their distance-1
+ minterms hoping to get simulation started.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_EngineSimulateFirst( Aig_Man_t * p )
+{
+ Aig_Pattern_t * pPat;
+ int i;
+ assert( Vec_PtrSize(p->vPats) == 0 );
+ for ( i = 0; i < p->nPatsMax; i++ )
+ {
+ pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
+ Aig_PatternRandom( pPat );
+ Vec_PtrPush( p->vPats, pPat );
+ if ( !Aig_EngineSimulate( p ) )
+ return;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements intelligent simulation engine.]
+
+ Description [Assumes that the good simulation patterns have been
+ assigned (p->vPats). Simulates until all of them are gone. Returns 1
+ if some classes are left. Returns 0 if there is no more classes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_EngineSimulate( Aig_Man_t * p )
+{
+ Aig_Pattern_t * pPat;
+ if ( Vec_VecSize(p->vClasses) == 0 )
+ return 0;
+ assert( Vec_PtrSize(p->vPats) > 0 );
+ // process patterns
+ while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 )
+ {
+ // get the pattern and create new siminfo
+ pPat = Vec_PtrPop(p->vPats);
+ // create the new siminfo
+ Aig_SimInfoFromPattern( p->pInfoPi, pPat );
+ // free the patter
+ Aig_PatternFree( pPat );
+
+ // simulate this info
+ Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+ // split the classes and collect the new patterns
+ Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
+ }
+ return Vec_VecSize(p->vClasses) > 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates all nodes using random simulation for the first time.]
+
+ Description [Assigns the original simulation info and the storage for the
+ future simulation info.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
+{
+ Aig_SimInfo_t * pInfoPi, * pInfoAll;
+ assert( !p->pInfo && !p->pInfoTemp );
+ // create random PI info
+ pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
+ Aig_SimInfoRandom( pInfoPi );
+ // allocate sim info for all nodes
+ pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
+ // simulate though the circuit
+ Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
+ // detect classes
+ p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+ Aig_SimInfoFree( pInfoAll );
+ // save simulation info
+ p->pInfo = pInfoPi;
+ p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 );
+ p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
index b5cce582..901f2fe2 100644
--- a/src/sat/aig/fraigProve.c
+++ b/src/sat/aig/fraigProve.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigProve.c]
+ FileName [fraigProve.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
index 1d547621..415b6918 100644
--- a/src/sat/aig/fraigSim.c
+++ b/src/sat/aig/fraigSim.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigSim.c]
+ FileName [fraigSim.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -30,59 +30,28 @@
/**Function*************************************************************
- Synopsis [Simulates all nodes using random simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
-{
- Aig_SimInfo_t * pInfoPi, * pInfoAll;
- assert( p->pInfo && p->pInfoTemp );
- // create random PI info
- pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
- Aig_SimInfoRandom( pInfoPi );
- // simulate it though the circuit
- pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
- // detect classes
- p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
- Aig_SimInfoFree( pInfoAll );
- // save simulation info
- p->pInfo = pInfoPi;
- p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
-}
-
-/**Function*************************************************************
-
Synopsis [Simulates all nodes using the given simulation info.]
- Description []
+ Description [Returns the simulation info for all nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
-Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
+void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
{
- Aig_SimInfo_t * pInfoAll;
Aig_Node_t * pNode;
- unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
+ unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
int i, k, fComp0, fComp1;
assert( !pInfoPi->Type ); // PI siminfo
- // allocate sim info for all nodes
- pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
// set the constant sim info
pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
for ( k = 0; k < pInfoPi->nWords; k++ )
pData1[k] = ~((unsigned)0);
- // copy the PI siminfo
- Vec_PtrForEachEntry( p->vPis, pNode, i )
+ // set the PI siminfo
+ Aig_ManForEachPi( p, pNode, i )
{
pDataPi = Aig_SimInfoForPi( pInfoPi, i );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
@@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
pDataAnd[k] = pDataPi[k];
}
// simulate the nodes
- Vec_PtrForEachEntry( p->vNodes, pNode, i )
+ Aig_ManForEachAnd( p, pNode, i )
{
- if ( !Aig_NodeIsAnd(pNode) )
- continue;
pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
@@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
for ( k = 0; k < pInfoPi->nWords; k++ )
pDataAnd[k] = pData0[k] & pData1[k];
}
- return pInfoAll;
+ // derive the PO siminfo
+ Aig_ManForEachPi( p, pNode, i )
+ {
+ pDataPo = Aig_SimInfoForNode( pInfoAll, pNode );
+ pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
+ if ( Aig_NodeFaninC0(pNode) )
+ for ( k = 0; k < pInfoPi->nWords; k++ )
+ pDataPo[k] = ~pDataAnd[k];
+ else
+ for ( k = 0; k < pInfoPi->nWords; k++ )
+ pDataPo[k] = pDataAnd[k];
+ }
}
+
/**Function*************************************************************
- Synopsis []
+ Synopsis [Allocates the simulation info.]
Description []
@@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the simulation info to zero.]
Description []
@@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the random simulation info.]
Description []
@@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the random simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
+{
+ unsigned * pData;
+ int i, k;
+ assert( p->Type == 0 );
+ assert( p->nNodes == pPat->nBits );
+ for ( i = 0; i < p->nNodes; i++ )
+ {
+ // get the pointer to the bitdata for node i
+ pData = p->pData + p->nWords * i;
+ // fill in the bit data according to the pattern
+ if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1
+ for ( k = 0; k < p->nWords; k++ )
+ pData[k] = ~((unsigned)0);
+ else
+ for ( k = 0; k < p->nWords; k++ )
+ pData[k] = 0;
+ // flip one bit
+ Aig_InfoXorBit( pData, i );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resizes the simulation info.]
Description []
@@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p )
for ( k = 0; k < p->nWords; k++ )
pData[2 * p->nWords * i + k + p->nWords] = 0;
}
- p->nPatsMax *= 2;
p->nWords *= 2;
+ p->nPatsMax *= 2;
+ free( p->pData );
+ p->pData = pData;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Deallocates the simulation info.]
Description []
@@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * p )
}
+/**Function*************************************************************
+
+ Synopsis [Allocates the simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Pattern_t * Aig_PatternAlloc( int nBits )
+{
+ Aig_Pattern_t * pPat;
+ pPat = ALLOC( Aig_Pattern_t, 1 );
+ memset( pPat, 0, sizeof(Aig_Pattern_t) );
+ pPat->nBits = nBits;
+ pPat->nWords = Aig_BitWordNum(nBits);
+ pPat->pData = ALLOC( unsigned, pPat->nWords );
+ return pPat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cleans the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternClean( Aig_Pattern_t * pPat )
+{
+ memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the random pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternRandom( Aig_Pattern_t * pPat )
+{
+ int i;
+ for ( i = 0; i < pPat->nWords; i++ )
+ pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternFree( Aig_Pattern_t * pPat )
+{
+ free( pPat->pData );
+ free( pPat );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigSolver.c b/src/sat/aig/fraigSolver.c
new file mode 100644
index 00000000..12502951
--- /dev/null
+++ b/src/sat/aig/fraigSolver.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [fraigSolver.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: fraigSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigTrav.c b/src/sat/aig/fraigTrav.c
new file mode 100644
index 00000000..d5a09259
--- /dev/null
+++ b/src/sat/aig/fraigTrav.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [fraigTrav.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: fraigTrav.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 07:34:33 +0000