summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/aig/aig.h377
-rw-r--r--src/sat/aig/aigBalance.c47
-rw-r--r--src/sat/aig/aigCheck.c146
-rw-r--r--src/sat/aig/aigFanout.c423
-rw-r--r--src/sat/aig/aigMan.c157
-rw-r--r--src/sat/aig/aigMem.c246
-rw-r--r--src/sat/aig/aigNode.c316
-rw-r--r--src/sat/aig/aigOper.c175
-rw-r--r--src/sat/aig/aigReplace.c133
-rw-r--r--src/sat/aig/aigTable.c334
-rw-r--r--src/sat/aig/aigUtil.c190
-rw-r--r--src/sat/aig/fraigClass.c320
-rw-r--r--src/sat/aig/fraigCnf.c476
-rw-r--r--src/sat/aig/fraigCore.c129
-rw-r--r--src/sat/aig/fraigEngine.c174
-rw-r--r--src/sat/aig/fraigProve.c47
-rw-r--r--src/sat/aig/fraigSim.c361
-rw-r--r--src/sat/aig/fraigSolver.c47
-rw-r--r--src/sat/aig/fraigTrav.c47
-rw-r--r--src/sat/aig/rwrMffc.c303
-rw-r--r--src/sat/aig/rwrTruth.c456
-rw-r--r--src/sat/aig/rwr_.c48
22 files changed, 0 insertions, 4952 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
deleted file mode 100644
index a0d63ce9..00000000
--- a/src/sat/aig/aig.h
+++ /dev/null
@@ -1,377 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aig.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [And-Inverter Graph package.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: aig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __AIG_H__
-#define __AIG_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-/*
- AIG is an And-Inv Graph with structural hashing.
- It is always structurally hashed. It means that at any time:
- - for each AND gate, there are no other AND gates with the same children
- - the constants are propagated
- - there is no single-input nodes (inverters/buffers)
- Additionally the following invariants are satisfied:
- - there are no dangling nodes (the nodes without fanout)
- - the level of each AND gate reflects the levels of this fanins
- - the AND nodes are in the topological order
- - the constant 1 node has always number 0 in the object list
- The operations that are performed on AIGs:
- - building new nodes (Aig_And)
- - performing elementary Boolean operations (Aig_Or, Aig_Xor, etc)
- - replacing one node by another (Abc_AigReplace)
- - propagating constants (Abc_AigReplace)
- - deleting dangling nodes (Abc_AigDelete)
- When AIG is duplicated, the new graph is structurally hashed too.
- If this repeated hashing leads to fewer nodes, it means the original
- AIG was not strictly hashed (one of the conditions above is violated).
-*/
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-#include "solver.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-//typedef int bool;
-#ifndef __cplusplus
-#ifndef bool
-#define bool int
-#endif
-#endif
-
-typedef struct Aig_Param_t_ Aig_Param_t;
-typedef struct Aig_Man_t_ Aig_Man_t;
-typedef struct Aig_Node_t_ Aig_Node_t;
-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 {
- AIG_NONE = 0, // 0: unknown
- AIG_PI, // 1: primary input
- AIG_PO, // 2: primary output
- 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
-struct Aig_Edge_t_
-{
- unsigned iNode : 31; // the node
- unsigned fComp : 1; // the complemented attribute
-};
-
-// the AIG node
-struct Aig_Node_t_ // 8 words
-{
- // various numbers associated with the node
- int Id; // the unique number (SAT var number) of this node
- int nRefs; // the reference counter
- unsigned Type : 2; // the node type
- unsigned fPhase : 1; // the phase of this node
- unsigned fMarkA : 1; // the mask
- unsigned fMarkB : 1; // the mask
- unsigned fMarkC : 1; // the mask
- unsigned TravId : 26; // the traversal ID
- unsigned Level : 16; // the direct level of the node
- unsigned LevelR : 16; // the reverse level of the node
- Aig_Edge_t Fans[2]; // the fanins
- int NextH; // next node in the hash table
- int Data; // miscelleneous data
- Aig_Man_t * pMan; // the parent manager
-};
-
-// the AIG manager
-struct Aig_Man_t_
-{
- // the AIG parameters
- Aig_Param_t Param; // the full set of AIG parameters
- Aig_Param_t * pParam; // the pointer to the above set
- // the nodes
- Aig_Node_t * pConst1; // the constant 1 node (ID=0)
- Vec_Ptr_t * vNodes; // all nodes by ID
- Vec_Ptr_t * vPis; // all PIs
- 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
- Vec_Ptr_t * vFanFans1; // the next fanout of the second fanin
- // the memory managers
- Aig_MemFixed_t * mmNodes; // the memory manager for nodes
- 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
- Aig_Pattern_t * pPatMask; // the mask which shows what patterns are used
- // simulation patterns
- int nPiWords; // the number of words in the PI info
- int nPatsMax; // the max number of patterns
- Vec_Ptr_t * vPats; // simulation patterns to try
- // equivalence classes
- Vec_Vec_t * vClasses; // the non-trival equivalence classes of nodes
- // temporary data
- Vec_Ptr_t * vFanouts; // temporary storage for fanouts of a node
- Vec_Ptr_t * vToReplace; // the nodes to replace
- Vec_Int_t * vClassTemp; // temporary class representatives
-};
-
-// the simulation patter
-struct Aig_Pattern_t_
-{
- int nBits;
- int nWords;
- unsigned * pData;
-};
-
-// the AIG simulation info
-struct Aig_SimInfo_t_
-{
- int Type; // the type (0 = PI, 1 = all)
- int nNodes; // the number of nodes for which allocated
- int nWords; // the number of words for each node
- int nPatsMax; // the maximum number of patterns
- int nPatsCur; // the current number of patterns
- unsigned * pData; // the simulation data
-};
-
-// iterators over nodes, PIs, POs, ANDs
-#define Aig_ManForEachNode( pMan, pNode, i ) \
- for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ )
-#define Aig_ManForEachPi( pMan, pNode, i ) \
- 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( pMan, pNode, i ) \
- for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \
- if ( !Aig_NodeIsAnd(pNode) ) {} else
-
-// maximum/minimum operators
-#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
-#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 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); }
-
-static inline int Aig_ManNodeNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vNodes); }
-static inline int Aig_ManPiNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPis); }
-static inline int Aig_ManPoNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPos); }
-static inline int Aig_ManAndNum( Aig_Man_t * pMan ) { return Aig_ManNodeNum(pMan)-Aig_ManPiNum(pMan)-Aig_ManPoNum(pMan)-1; }
-
-static inline Aig_Node_t * Aig_Regular( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) & ~01); }
-static inline Aig_Node_t * Aig_Not( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) ^ 01); }
-static inline Aig_Node_t * Aig_NotCond( Aig_Node_t * p, int c ) { return (Aig_Node_t *)((unsigned)(p) ^ (c)); }
-static inline bool Aig_IsComplement( Aig_Node_t * p ) { return (bool)(((unsigned)p) & 01); }
-
-static inline bool Aig_NodeIsConst( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Id == 0; }
-static inline bool Aig_NodeIsPi( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PI; }
-static inline bool Aig_NodeIsPo( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PO; }
-static inline bool Aig_NodeIsAnd( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_AND; }
-
-static inline int Aig_NodeId( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Id; }
-static inline int Aig_NodeRefs( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->nRefs; }
-static inline bool Aig_NodePhase( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->fPhase; }
-static inline int Aig_NodeLevel( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Level; }
-static inline int Aig_NodeLevelR( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->LevelR; }
-static inline int Aig_NodeData( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Data; }
-static inline Aig_Man_t * Aig_NodeMan( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->pMan; }
-static inline int Aig_NodeFaninId0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].iNode; }
-static inline int Aig_NodeFaninId1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].iNode; }
-static inline bool Aig_NodeFaninC0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].fComp; }
-static inline bool Aig_NodeFaninC1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].fComp; }
-static inline Aig_Node_t * Aig_NodeFanin0( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId0(pNode) ); }
-static inline Aig_Node_t * Aig_NodeFanin1( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId1(pNode) ); }
-static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin0(pNode), Aig_NodeFaninC0(pNode) ); }
-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_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
-
-static inline unsigned * Aig_SimInfoForNodeId( Aig_SimInfo_t * p, int NodeId ) { assert( p->Type ); return p->pData + p->nWords * NodeId; }
-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; }
-
-static inline void Aig_NodeSetTravId( Aig_Node_t * pNode, int TravId ) { pNode->TravId = TravId; }
-static inline void Aig_NodeSetTravIdCurrent( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds; }
-static inline void Aig_NodeSetTravIdPrevious( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds - 1; }
-static inline bool Aig_NodeIsTravIdCurrent( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds); }
-static inline bool Aig_NodeIsTravIdPrevious( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds - 1); }
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== aigCheck.c ==========================================================*/
-extern bool Aig_ManCheck( Aig_Man_t * pMan );
-extern bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot );
-/*=== aigFanout.c ==========================================================*/
-extern void Aig_ManCreateFanouts( Aig_Man_t * p );
-extern void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout );
-extern void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove );
-extern int Aig_NodeGetFanoutNum( Aig_Node_t * pNode );
-extern Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode );
-extern int Aig_NodeGetLevelRNew( Aig_Node_t * pNode );
-extern int Aig_ManSetLevelR( Aig_Man_t * pMan );
-extern int Aig_ManGetLevelMax( Aig_Man_t * pMan );
-extern int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode );
-extern int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode );
-/*=== aigMem.c =============================================================*/
-extern Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize );
-extern void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose );
-extern char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p );
-extern void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry );
-extern void Aig_MemFixedRestart( Aig_MemFixed_t * p );
-extern int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p );
-/*=== aigMan.c =============================================================*/
-extern void Aig_ManSetDefaultParams( Aig_Param_t * pParam );
-extern Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam );
-extern int Aig_ManCleanup( Aig_Man_t * pMan );
-extern void Aig_ManStop( Aig_Man_t * p );
-/*=== aigNode.c =============================================================*/
-extern Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p );
-extern Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p );
-extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p );
-extern Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
-extern Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin );
-extern void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode );
-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 );
-extern Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
-extern Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 );
-extern Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs );
-/*=== aigReplace.c ==========================================================*/
-extern void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel );
-/*=== aigTable.c ==========================================================*/
-extern Aig_Table_t * Aig_TableCreate( int nSize );
-extern void Aig_TableFree( Aig_Table_t * p );
-extern int Aig_TableNumNodes( Aig_Table_t * p );
-extern Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
-extern Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd );
-extern void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis );
-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 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 int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask );
-extern void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats );
-/*=== fraigCnf.c ==========================================================*/
-extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan );
-/*=== fraigEngine.c ==========================================================*/
-extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
-extern void Aig_EngineSimulateFirst( Aig_Man_t * p );
-extern int Aig_EngineSimulate( Aig_Man_t * p );
-/*=== fraigSim.c ==========================================================*/
-extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, 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 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_PatternFill( Aig_Pattern_t * pPat );
-extern int Aig_PatternCount( Aig_Pattern_t * pPat );
-extern void Aig_PatternRandom( Aig_Pattern_t * pPat );
-extern void Aig_PatternFree( Aig_Pattern_t * pPat );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/aig/aigBalance.c b/src/sat/aig/aigBalance.c
deleted file mode 100644
index 1dd8ab01..00000000
--- a/src/sat/aig/aigBalance.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigBalance.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: aigBalance.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/aigCheck.c b/src/sat/aig/aigCheck.c
deleted file mode 100644
index a9facef3..00000000
--- a/src/sat/aig/aigCheck.c
+++ /dev/null
@@ -1,146 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigCheck.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: aigCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Makes sure that every node in the table is in the network and vice versa.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Aig_ManCheck( Aig_Man_t * pMan )
-{
- Aig_Node_t * pObj, * pAnd;
- int i;
- Aig_ManForEachNode( pMan, pObj, i )
- {
- if ( pObj == pMan->pConst1 || Aig_NodeIsPi(pObj) )
- {
- if ( pObj->Fans[0].iNode || pObj->Fans[1].iNode || pObj->Level )
- {
- printf( "Aig_ManCheck: The AIG has non-standard constant or PI node \"%d\".\n", pObj->Id );
- return 0;
- }
- continue;
- }
- if ( Aig_NodeIsPo(pObj) )
- {
- if ( pObj->Fans[1].iNode )
- {
- printf( "Aig_ManCheck: The AIG has non-standard PO node \"%d\".\n", pObj->Id );
- return 0;
- }
- continue;
- }
- // consider the AND node
- if ( !pObj->Fans[0].iNode || !pObj->Fans[1].iNode )
- {
- printf( "Aig_ManCheck: The AIG has node \"%d\" with a constant fanin.\n", pObj->Id );
- return 0;
- }
- if ( pObj->Fans[0].iNode > pObj->Fans[1].iNode )
- {
- printf( "Aig_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
- return 0;
- }
- if ( pObj->Level != 1 + AIG_MAX(Aig_NodeFanin0(pObj)->Level, Aig_NodeFanin1(pObj)->Level) )
- printf( "Aig_ManCheck: Node \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
- pAnd = Aig_TableLookupNode( pMan, Aig_NodeChild0(pObj), Aig_NodeChild1(pObj) );
- if ( pAnd != pObj )
- printf( "Aig_ManCheck: Node \"%d\" is not in the structural hashing table.\n", pObj->Id );
- }
- // count the number of nodes in the table
- if ( Aig_TableNumNodes(pMan->pTable) != Aig_ManAndNum(pMan) )
- {
- printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
- return 0;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Check if the node has a combination loop of depth 1 or 2.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot )
-{
- Aig_Node_t * pFanin0, * pFanin1;
- Aig_Node_t * pChild00, * pChild01;
- Aig_Node_t * pChild10, * pChild11;
- if ( !Aig_NodeIsAnd(pNode) )
- return 1;
- pFanin0 = Aig_NodeFanin0(pNode);
- pFanin1 = Aig_NodeFanin1(pNode);
- if ( pRoot == pFanin0 || pRoot == pFanin1 )
- return 0;
- if ( Aig_NodeIsPi(pFanin0) )
- {
- pChild00 = NULL;
- pChild01 = NULL;
- }
- else
- {
- pChild00 = Aig_NodeFanin0(pFanin0);
- pChild01 = Aig_NodeFanin1(pFanin0);
- if ( pRoot == pChild00 || pRoot == pChild01 )
- return 0;
- }
- if ( Aig_NodeIsPi(pFanin1) )
- {
- pChild10 = NULL;
- pChild11 = NULL;
- }
- else
- {
- pChild10 = Aig_NodeFanin0(pFanin1);
- pChild11 = Aig_NodeFanin1(pFanin1);
- if ( pRoot == pChild10 || pRoot == pChild11 )
- return 0;
- }
- return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigFanout.c b/src/sat/aig/aigFanout.c
deleted file mode 100644
index aed38426..00000000
--- a/src/sat/aig/aigFanout.c
+++ /dev/null
@@ -1,423 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigFanout.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: aigFanout.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Node_t * Aig_NodeFanPivot( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanPivots, pNode->Id); }
-static inline Aig_Node_t * Aig_NodeFanFan0( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanFans0, pNode->Id); }
-static inline Aig_Node_t * Aig_NodeFanFan1( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanFans1, pNode->Id); }
-static inline Aig_Node_t ** Aig_NodeFanPivotPlace( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanPivots->pArray) + pNode->Id; }
-static inline Aig_Node_t ** Aig_NodeFanFan0Place( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanFans0->pArray) + pNode->Id; }
-static inline Aig_Node_t ** Aig_NodeFanFan1Place( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanFans1->pArray) + pNode->Id; }
-static inline void Aig_NodeSetFanPivot( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanPivots, pNode->Id, pNode2); }
-static inline void Aig_NodeSetFanFan0( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanFans0, pNode->Id, pNode2); }
-static inline void Aig_NodeSetFanFan1( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanFans1, pNode->Id, pNode2); }
-static inline Aig_Node_t * Aig_NodeNextFanout( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { if ( pFanout == NULL ) return NULL; return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0(pFanout) : Aig_NodeFanFan1(pFanout); }
-static inline Aig_Node_t ** Aig_NodeNextFanoutPlace( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0Place(pFanout) : Aig_NodeFanFan1Place(pFanout); }
-
-// iterator through the fanouts of the node
-#define Aig_NodeForEachFanout( pNode, pFanout ) \
- for ( pFanout = Aig_NodeFanPivot(pNode); pFanout; \
- pFanout = Aig_NodeNextFanout(pNode, pFanout) )
-// safe iterator through the fanouts of the node
-#define Aig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 ) \
- for ( pFanout = Aig_NodeFanPivot(pNode), \
- pFanout2 = Aig_NodeNextFanout(pNode, pFanout); \
- pFanout; \
- pFanout = pFanout2, \
- pFanout2 = Aig_NodeNextFanout(pNode, pFanout) )
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the fanouts for all nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManCreateFanouts( Aig_Man_t * p )
-{
- Aig_Node_t * pNode;
- int i;
- assert( p->vFanPivots == NULL );
- p->vFanPivots = Vec_PtrStart( Aig_ManNodeNum(p) );
- p->vFanFans0 = Vec_PtrStart( Aig_ManNodeNum(p) );
- p->vFanFans1 = Vec_PtrStart( Aig_ManNodeNum(p) );
- Aig_ManForEachNode( p, pNode, i )
- {
- if ( Aig_NodeIsPi(pNode) || i == 0 )
- continue;
- Aig_NodeAddFaninFanout( Aig_NodeFanin0(pNode), pNode );
- if ( Aig_NodeIsPo(pNode) )
- continue;
- Aig_NodeAddFaninFanout( Aig_NodeFanin1(pNode), pNode );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the fanouts for all nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Aig_ManResizeFanouts( Aig_Man_t * p, int nSizeNew )
-{
- assert( p->vFanPivots );
- if ( Vec_PtrSize(p->vFanPivots) < nSizeNew )
- {
- Vec_PtrFillExtra( p->vFanPivots, nSizeNew + 1000, NULL );
- Vec_PtrFillExtra( p->vFanFans0, nSizeNew + 1000, NULL );
- Vec_PtrFillExtra( p->vFanFans1, nSizeNew + 1000, NULL );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Add the fanout to the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout )
-{
- Aig_Node_t * pPivot;
-
- // check that they are not complemented
- assert( !Aig_IsComplement(pFanin) );
- assert( !Aig_IsComplement(pFanout) );
- // check that pFanins is a fanin of pFanout
- assert( Aig_NodeFaninId0(pFanout) == pFanin->Id || Aig_NodeFaninId1(pFanout) == pFanin->Id );
-
- // resize the fanout manager
- Aig_ManResizeFanouts( pFanin->pMan, 1 + AIG_MAX(pFanin->Id, pFanout->Id) );
-
- // consider the case of the first fanout
- pPivot = Aig_NodeFanPivot(pFanin);
- if ( pPivot == NULL )
- {
- Aig_NodeSetFanPivot( pFanin, pFanout );
- return;
- }
-
- // consider the case of more than one fanouts
- if ( Aig_NodeFaninId0(pPivot) == pFanin->Id )
- {
- if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
- {
- Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan0(pPivot) );
- Aig_NodeSetFanFan0( pPivot, pFanout );
- }
- else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
- {
- Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan0(pPivot) );
- Aig_NodeSetFanFan0( pPivot, pFanout );
- }
- }
- else // if ( Aig_NodeFaninId1(pPivot) == pFanin->Id )
- {
- assert( Aig_NodeFaninId1(pPivot) == pFanin->Id );
- if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
- {
- Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan1(pPivot) );
- Aig_NodeSetFanFan1( pPivot, pFanout );
- }
- else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
- {
- Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan1(pPivot) );
- Aig_NodeSetFanFan1( pPivot, pFanout );
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Add the fanout to the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove )
-{
- Aig_Node_t * pFanout, * pFanout2, ** ppFanList;
- // start the linked list of fanouts
- ppFanList = Aig_NodeFanPivotPlace(pFanin);
- // go through the fanouts
- Aig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 )
- {
- // skip the fanout-to-remove
- if ( pFanout == pFanoutToRemove )
- continue;
- // add useful fanouts to the list
- *ppFanList = pFanout;
- ppFanList = Aig_NodeNextFanoutPlace( pFanin, pFanout );
- }
- *ppFanList = NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of fanouts of a node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeGetFanoutNum( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- int Counter = 0;
- Aig_NodeForEachFanout( pNode, pFanout )
- Counter++;
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collect fanouts.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- Vec_PtrClear( pNode->pMan->vFanouts );
- Aig_NodeForEachFanout( pNode, pFanout )
- Vec_PtrPush( pNode->pMan->vFanouts, pFanout );
- return pNode->pMan->vFanouts;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the node has at least one complemented fanout.]
-
- Description [A fanout is complemented if the fanout's fanin edge pointing
- to the given node is complemented.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Aig_NodeHasComplFanoutEdge( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- int iFanin;
- Aig_NodeForEachFanout( pNode, pFanout )
- {
- iFanin = Aig_NodeWhatFanin( pFanout, pNode );
- assert( iFanin >= 0 );
- if ( iFanin && Aig_NodeFaninC1(pFanout) || !iFanin && Aig_NodeFaninC0(pFanout) )
- return 1;
- }
- return 0;
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Recursively computes and assigns the reverse level of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static int Aig_NodeSetLevelR_rec( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- int LevelR = 0;
- if ( Aig_NodeIsPo(pNode) )
- return pNode->LevelR = 0;
- Aig_NodeForEachFanout( pNode, pFanout )
- if ( LevelR < Aig_NodeSetLevelR_rec(pFanout) )
- LevelR = pFanout->LevelR;
- return pNode->LevelR = 1 + LevelR;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the reverse level of all nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManSetLevelR( Aig_Man_t * pMan )
-{
- Aig_Node_t * pNode;
- int i, LevelR = 0;
- Aig_ManForEachPi( pMan, pNode, i )
- if ( LevelR < Aig_NodeSetLevelR_rec(pNode) )
- LevelR = pNode->LevelR;
- return LevelR;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the global number of logic levels.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManGetLevelMax( Aig_Man_t * pMan )
-{
- Aig_Node_t * pNode;
- int i, LevelsMax = 0;
- Aig_ManForEachPo( pMan, pNode, i )
- if ( LevelsMax < (int)pNode->Level )
- LevelsMax = (int)pNode->Level;
- return LevelsMax;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes but does not assign the reverse level of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeGetLevelRNew( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- unsigned LevelR = 0;
- Aig_NodeForEachFanout( pNode, pFanout )
- LevelR = AIG_MAX( LevelR, pFanout->LevelR );
- return LevelR + !Aig_NodeIsPi(pNode);
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Updates the direct level of one node.]
-
- Description [Returns 1 if direct level of at least one CO was changed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanout;
- unsigned LevelNew, fStatus = 0;
- Aig_NodeForEachFanout( pNode, pFanout )
- {
- LevelNew = Aig_NodeGetLevelNew( pFanout );
- if ( pFanout->Level == LevelNew )
- continue;
- // the level has changed
- pFanout->Level = LevelNew;
- if ( Aig_NodeIsPo(pNode) )
- fStatus = 1;
- else
- fStatus |= Aig_NodeUpdateLevel_int( pFanout );
- }
- return fStatus;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Updates the reverse level of one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanin;
- unsigned LevelNew;
- assert( !Aig_NodeIsPo(pNode) );
- pFanin = Aig_NodeFanin0(pNode);
- LevelNew = Aig_NodeGetLevelRNew(pFanin);
- if ( pFanin->LevelR != LevelNew )
- {
- pFanin->LevelR = LevelNew;
- if ( Aig_NodeIsAnd(pFanin) )
- Aig_NodeUpdateLevelR_int( pFanin );
- }
- pFanin = Aig_NodeFanin1(pNode);
- LevelNew = Aig_NodeGetLevelRNew(pFanin);
- if ( pFanin->LevelR != LevelNew )
- {
- pFanin->LevelR = LevelNew;
- if ( Aig_NodeIsAnd(pFanin) )
- Aig_NodeUpdateLevelR_int( pFanin );
- }
- return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
deleted file mode 100644
index 4c64c897..00000000
--- a/src/sat/aig/aigMan.c
+++ /dev/null
@@ -1,157 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigMan.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: aigMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Sets the default parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSetDefaultParams( Aig_Param_t * pParam )
-{
- memset( pParam, 0, sizeof(Aig_Param_t) );
- pParam->nPatsRand = 4096; // the number of random patterns
- pParam->nBTLimit = 99; // backtrack limit at the intermediate nodes
- pParam->nSeconds = 1; // the timeout for the final miter in seconds
-}
-
-/**Function*************************************************************
-
- Synopsis [Starts the AIG manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
-{
- Aig_Man_t * p;
- // set the random seed for simulation
- srand( 0xDEADCAFE );
- // start the manager
- p = ALLOC( Aig_Man_t, 1 );
- memset( p, 0, sizeof(Aig_Man_t) );
- p->pParam = &p->Param;
- p->nTravIds = 1;
- p->nPatsMax = 25;
- // set the defaults
- *p->pParam = *pParam;
- // start memory managers
- p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) );
- // allocate node arrays
- p->vPis = Vec_PtrAlloc( 1000 ); // the array of primary inputs
- p->vPos = Vec_PtrAlloc( 1000 ); // the array of primary outputs
- p->vNodes = Vec_PtrAlloc( 1000 ); // the array of internal nodes
- // start the table
- p->pTable = Aig_TableCreate( 1000 );
- // create the constant node
- p->pConst1 = Aig_NodeCreateConst( p );
- // initialize other variables
- p->vFanouts = Vec_PtrAlloc( 10 );
- p->vToReplace = Vec_PtrAlloc( 10 );
- p->vClassTemp = Vec_IntAlloc( 10 );
- p->vPats = Vec_PtrAlloc( p->nPatsMax );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of dangling nodes removed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManCleanup( Aig_Man_t * pMan )
-{
- Aig_Node_t * pAnd;
- int i, nNodesOld;
- nNodesOld = Aig_ManAndNum(pMan);
- Aig_ManForEachAnd( pMan, pAnd, i )
- if ( pAnd->nRefs == 0 )
- Aig_NodeDeleteAnd_rec( pMan, pAnd );
- return nNodesOld - Aig_ManAndNum(pMan);
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the AIG manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-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 );
- // patterns
- if ( p->vPats ) Vec_PtrFree( p->vPats );
- if ( p->pPatMask ) Aig_PatternFree( p->pPatMask );
- // 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 );
- Vec_IntFree( p->vClassTemp );
- Aig_TableFree( p->pTable );
- free( p );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
deleted file mode 100644
index 32709bf6..00000000
--- a/src/sat/aig/aigMem.c
+++ /dev/null
@@ -1,246 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigMem.c]
-
- PackageName [ABC: Logic synthesis and verification system.]
-
- Synopsis [Fixed-size-entry memory manager for the AIG package.]
-
- Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 2.0. Started - October 1, 2004]
-
- Revision [$Id: aigMem.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-struct Aig_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 []
-
-***********************************************************************/
-Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize )
-{
- Aig_MemFixed_t * p;
-
- p = ALLOC( Aig_MemFixed_t, 1 );
- memset( p, 0, sizeof(Aig_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 Aig_MemFixedStop( Aig_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 * Aig_MemFixedEntryFetch( Aig_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 Aig_MemFixedEntryRecycle( Aig_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 Aig_MemFixedRestart( Aig_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 Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p )
-{
- return p->nMemoryAlloc;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
deleted file mode 100644
index ce458353..00000000
--- a/src/sat/aig/aigNode.c
+++ /dev/null
@@ -1,316 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigNode.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: aigNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
-{
- Aig_Node_t * pNode;
- // create the node
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the constant 1 node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates a primary input node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
-{
- Aig_Node_t * pNode;
- pNode = Aig_NodeCreate( p );
- Vec_PtrPush( p->vPis, pNode );
- pNode->Type = AIG_PI;
- pNode->fPhase = 0; // sim value for 000... pattern
- return pNode;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates a primary output node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p )
-{
- Aig_Node_t * pNode;
- pNode = Aig_NodeCreate( p );
- pNode->Type = AIG_PO;
- Vec_PtrPush( p->vPos, pNode );
- return pNode;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates a primary output node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin )
-{
- assert( Aig_NodeIsPo(pNode) );
- assert( !Aig_IsComplement(pNode) );
- // connect to the fanin
- pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
- pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id;
- pNode->fPhase = pNode->Fans[0].fComp ^ Aig_Regular(pFanin)->fPhase; // sim value for 000... pattern
- pNode->Level = Aig_Regular(pFanin)->Level;
- Aig_Regular(pFanin)->nRefs++;
- if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin, pNode );
- // update global level if needed
- if ( p->nLevelMax < (int)pNode->Level )
- p->nLevelMax = pNode->Level;
- return pNode;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates a new node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 )
-{
- Aig_Node_t * pNode;
- pNode = Aig_NodeCreate( p );
- pNode->Type = AIG_AND;
- Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
- return pNode;
-}
-
-/**Function*************************************************************
-
- Synopsis [Connects the nodes to the AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode )
-{
- assert( !Aig_IsComplement(pNode) );
- assert( Aig_NodeIsAnd(pNode) );
- // add the fanins
- pNode->Fans[0].fComp = Aig_IsComplement(pFanin0);
- pNode->Fans[0].iNode = Aig_Regular(pFanin0)->Id;
- pNode->Fans[1].fComp = Aig_IsComplement(pFanin1);
- pNode->Fans[1].iNode = Aig_Regular(pFanin1)->Id;
- // compute the phase (sim value for 000... pattern)
- pNode->fPhase = (pNode->Fans[0].fComp ^ Aig_Regular(pFanin0)->fPhase) &
- (pNode->Fans[1].fComp ^ Aig_Regular(pFanin1)->fPhase);
- pNode->Level = Aig_NodeGetLevelNew(pNode);
- // reference the fanins
- Aig_Regular(pFanin0)->nRefs++;
- Aig_Regular(pFanin1)->nRefs++;
- // add the fanouts
- if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin0, pNode );
- if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin1, pNode );
- // add the node to the structural hash table
- Aig_TableInsertNode( pNode->pMan, pFanin0, pFanin1, pNode );
-}
-
-/**Function*************************************************************
-
- Synopsis [Connects the nodes to the AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeDisconnectAnd( Aig_Node_t * pNode )
-{
- Aig_Node_t * pFanin0, * pFanin1;
- assert( !Aig_IsComplement(pNode) );
- assert( Aig_NodeIsAnd(pNode) );
- // get the fanins
- pFanin0 = Aig_NodeFanin0(pNode);
- pFanin1 = Aig_NodeFanin1(pNode);
- // dereference the fanins
- pFanin0->nRefs--;
- pFanin0->nRefs--;
- // remove the fanouts
- if ( pNode->pMan->vFanPivots ) Aig_NodeRemoveFaninFanout( pFanin0, pNode );
- if ( pNode->pMan->vFanPivots ) Aig_NodeRemoveFaninFanout( pFanin1, pNode );
- // remove the node from the structural hash table
- Aig_TableDeleteNode( pNode->pMan, pNode );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs internal deletion step.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot )
-{
- Aig_Node_t * pNode0, * pNode1;
- // make sure the node is regular and dangling
- assert( !Aig_IsComplement(pRoot) );
- assert( pRoot->nRefs == 0 );
- assert( Aig_NodeIsAnd(pRoot) );
- // remember the children
- pNode0 = Aig_NodeFanin0(pRoot);
- pNode1 = Aig_NodeFanin1(pRoot);
- // disconnect the node
- Aig_NodeDisconnectAnd( pRoot );
- // recycle the node
- Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL );
- memset( pRoot, 0, sizeof(Aig_Node_t) ); // this is a temporary hack to skip dead children below!!!
- Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot );
- // call recursively
- if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 )
- Aig_NodeDeleteAnd_rec( pMan, pNode0 );
- if ( Aig_NodeIsAnd(pNode1) && pNode1->nRefs == 0 )
- Aig_NodeDeleteAnd_rec( pMan, pNode1 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints the AIG node for debugging purposes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodePrint( Aig_Node_t * pNode )
-{
- Aig_Node_t * pNodeR = Aig_Regular(pNode);
- if ( Aig_NodeIsPi(pNode) )
- {
- printf( "PI %4s%s.\n", Aig_NodeName(pNode), Aig_IsComplement(pNode)? "\'" : "" );
- return;
- }
- if ( Aig_NodeIsConst(pNode) )
- {
- printf( "Constant 1 %s.\n", Aig_IsComplement(pNode)? "(complemented)" : "" );
- return;
- }
- // print the node's function
- printf( "%7s%s", Aig_NodeName(pNodeR), Aig_IsComplement(pNode)? "\'" : "" );
- printf( " = " );
- printf( "%7s%s", Aig_NodeName(Aig_NodeFanin0(pNodeR)), Aig_NodeFaninC0(pNodeR)? "\'" : "" );
- printf( " * " );
- printf( "%7s%s", Aig_NodeName(Aig_NodeFanin1(pNodeR)), Aig_NodeFaninC1(pNodeR)? "\'" : "" );
- printf( "\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the name of the node.]
-
- Description [The name should be used before this procedure is called again.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Aig_NodeName( Aig_Node_t * pNode )
-{
- static char Buffer[100];
- sprintf( Buffer, "%d", Aig_Regular(pNode)->Id );
- return Buffer;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigOper.c b/src/sat/aig/aigOper.c
deleted file mode 100644
index a10cc7ff..00000000
--- a/src/sat/aig/aigOper.c
+++ /dev/null
@@ -1,175 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigOper.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: aigOper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs canonicization step.]
-
- Description [The argument nodes can be complemented.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
-{
- Aig_Node_t * pAnd;
- // check for trivial cases
- if ( p0 == p1 )
- return p0;
- if ( p0 == Aig_Not(p1) )
- return Aig_Not(pMan->pConst1);
- if ( Aig_Regular(p0) == pMan->pConst1 )
- {
- if ( p0 == pMan->pConst1 )
- return p1;
- return Aig_Not(pMan->pConst1);
- }
- if ( Aig_Regular(p1) == pMan->pConst1 )
- {
- if ( p1 == pMan->pConst1 )
- return p0;
- return Aig_Not(pMan->pConst1);
- }
- // order the arguments
- if ( Aig_Regular(p0)->Id > Aig_Regular(p1)->Id )
- {
- if ( pAnd = Aig_TableLookupNode( pMan, p1, p0 ) )
- return pAnd;
- return Aig_NodeCreateAnd( pMan, p1, p0 );
- }
- else
- {
- if ( pAnd = Aig_TableLookupNode( pMan, p0, p1 ) )
- return pAnd;
- return Aig_NodeCreateAnd( pMan, p0, p1 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements Boolean OR.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
-{
- return Aig_Not( Aig_And( pMan, Aig_Not(p0), Aig_Not(p1) ) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements Boolean XOR.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
-{
- return Aig_Or( pMan, Aig_And(pMan, p0, Aig_Not(p1)),
- Aig_And(pMan, p1, Aig_Not(p0)) );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 )
-{
- return Aig_Or( pMan, Aig_And(pMan, pC, p1), Aig_And(pMan, Aig_Not(pC), p0) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements the miter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_Miter_rec( Aig_Man_t * pMan, Aig_Node_t ** ppObjs, int nObjs )
-{
- Aig_Node_t * pObj1, * pObj2;
- if ( nObjs == 1 )
- return ppObjs[0];
- pObj1 = Aig_Miter_rec( pMan, ppObjs, nObjs/2 );
- pObj2 = Aig_Miter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
- return Aig_Or( pMan, pObj1, pObj2 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements the miter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs )
-{
- int i;
- if ( vPairs->nSize == 0 )
- return Aig_Not( pMan->pConst1 );
- assert( vPairs->nSize % 2 == 0 );
- // go through the cubes of the node's SOP
- for ( i = 0; i < vPairs->nSize; i += 2 )
- vPairs->pArray[i/2] = Aig_Xor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
- vPairs->nSize = vPairs->nSize/2;
- return Aig_Miter_rec( pMan, (Aig_Node_t **)vPairs->pArray, vPairs->nSize );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigReplace.c b/src/sat/aig/aigReplace.c
deleted file mode 100644
index d928fdf8..00000000
--- a/src/sat/aig/aigReplace.c
+++ /dev/null
@@ -1,133 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigUpdate.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: aigUpdate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs internal replacement step.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static void Abc_AigReplace_int( Aig_Man_t * pMan, int fUpdateLevel )
-{
- Vec_Ptr_t * vFanouts;
- Aig_Node_t * pOld, * pNew, * pFanin0, * pFanin1, * pFanout, * pTemp, * pFanoutNew;
- int k, iFanin;
- // get the pair of nodes to replace
- assert( Vec_PtrSize(pMan->vToReplace) > 0 );
- pNew = Vec_PtrPop( pMan->vToReplace );
- pOld = Vec_PtrPop( pMan->vToReplace );
- // make sure the old node is internal, regular, and has fanouts
- // (the new node can be PI or internal, is complemented, and can have fanouts)
- assert( !Aig_IsComplement(pOld) );
- assert( pOld->nRefs > 0 );
- assert( Aig_NodeIsAnd(pOld) );
- assert( Aig_NodeIsPo(pNew) );
- // look at the fanouts of old node
- vFanouts = Aig_NodeGetFanouts( pOld );
- Vec_PtrForEachEntry( vFanouts, pFanout, k )
- {
- if ( Aig_NodeIsPo(pFanout) )
- {
- // patch the first fanin of the PO
- pFanout->Fans[0].iNode = Aig_Regular(pNew)->Id;
- pFanout->Fans[0].fComp ^= Aig_IsComplement(pNew);
- continue;
- }
- // find the old node as a fanin of this fanout
- iFanin = Aig_NodeWhatFanin( pFanout, pOld );
- assert( iFanin == 0 || iFanin == 1 );
- // get the new fanin
- pFanin0 = Aig_NotCond( pNew, pFanout->Fans[iFanin].fComp );
- assert( Aig_Regular(pFanin0) != pFanout );
- // get another fanin
- pFanin1 = iFanin? Aig_NodeChild0(pFanout) : Aig_NodeChild1(pFanout);
- assert( Aig_Regular(pFanin1) != pFanout );
- assert( Aig_Regular(pFanin0) != Aig_Regular(pFanin1) );
- // order them
- if ( Aig_Regular(pFanin0)->Id > Aig_Regular(pFanin1)->Id )
- pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
- // check if the node with these fanins exists
- if ( pFanoutNew = Aig_TableLookupNode( pMan, pFanin0, pFanin1 ) )
- { // such node exists (it may be a constant)
- // schedule replacement of the old fanout by the new fanout
- Vec_PtrPush( pMan->vToReplace, pFanout );
- Vec_PtrPush( pMan->vToReplace, pFanoutNew );
- continue;
- }
- // such node does not exist - modify the old fanout node
- // (this way the change will not propagate all the way to the COs)
- Aig_NodeDisconnectAnd( pFanout );
- Aig_NodeConnectAnd( pFanin0, pFanin1, pFanout );
- // recreate the old fanout with new fanins and add it to the table
- assert( Aig_NodeIsAcyclic(pFanout, pFanout) );
- // update the level if requested
- if ( fUpdateLevel )
- {
- if ( Aig_NodeUpdateLevel_int(pFanout) )
- pMan->nLevelMax = Aig_ManGetLevelMax( pMan );
- //Aig_NodeGetLevelRNew( pFanout );
- Aig_NodeUpdateLevelR_int( pFanout );
- }
- }
- // if the node has no fanouts left, remove its MFFC
- if ( pOld->nRefs == 0 )
- Aig_NodeDeleteAnd_rec( pMan, pOld );
-}
-
-/**Function*************************************************************
-
- Synopsis [Replaces one AIG node by the other.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel )
-{
- assert( Vec_PtrSize(pMan->vToReplace) == 0 );
- Vec_PtrPush( pMan->vToReplace, pOld );
- Vec_PtrPush( pMan->vToReplace, pNew );
- while ( Vec_PtrSize(pMan->vToReplace) )
- Abc_AigReplace_int( pMan, fUpdateLevel );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
deleted file mode 100644
index e6fe87d6..00000000
--- a/src/sat/aig/aigTable.c
+++ /dev/null
@@ -1,334 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigTable.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: aigTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// the hash table
-struct Aig_Table_t_
-{
- Aig_Node_t ** pBins; // the table bins
- int nBins; // the size of the table
- int nEntries; // the total number of entries in the table
-};
-
-// iterators through the entries in the linked lists of nodes
-#define Aig_TableBinForEachEntry( pBin, pEnt ) \
- for ( pEnt = pBin; \
- pEnt; \
- pEnt = Aig_NodeNextH(pEnt) )
-#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \
- for ( pEnt = pBin, \
- pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \
- pEnt; \
- pEnt = pEnt2, \
- pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL )
-
-// hash key for the structural hash table
-static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
-//static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
-
-static unsigned int Cudd_PrimeAig( unsigned int p );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Allocates the hash table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Table_t * Aig_TableCreate( int nSize )
-{
- Aig_Table_t * p;
- // allocate the table
- p = ALLOC( Aig_Table_t, 1 );
- memset( p, 0, sizeof(Aig_Table_t) );
- // allocate and clean the bins
- p->nBins = Cudd_PrimeAig(nSize);
- p->pBins = ALLOC( Aig_Node_t *, p->nBins );
- memset( p->pBins, 0, sizeof(Aig_Node_t *) * p->nBins );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Deallocates the supergate hash table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TableFree( Aig_Table_t * p )
-{
- FREE( p->pBins );
- FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of nodes in the table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_TableNumNodes( Aig_Table_t * p )
-{
- return p->nEntries;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs canonicization step.]
-
- Description [The argument nodes can be complemented.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
-{
- Aig_Node_t * pAnd;
- unsigned Key;
- assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
- // get the hash key for these two nodes
- 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) )
- return pAnd;
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs canonicization step.]
-
- Description [The argument nodes can be complemented.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd )
-{
- unsigned Key;
- assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
- // check if it is a good time for table resizing
- if ( pMan->pTable->nEntries > 2 * pMan->pTable->nBins )
- 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]? pMan->pTable->pBins[Key]->Id : 0;
- pMan->pTable->pBins[Key] = pAnd;
- pMan->pTable->nEntries++;
- return pAnd;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Deletes an AIG node from the hash table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
-{
- Aig_Node_t * pAnd, * pPlace = NULL;
- unsigned Key;
- assert( !Aig_IsComplement(pThis) );
- assert( Aig_NodeIsAnd(pThis) );
- assert( pMan == pThis->pMan );
- // get the hash key for these two nodes
- Key = Abc_HashKey2( Aig_NodeChild0(pThis), Aig_NodeChild1(pThis), pMan->pTable->nBins );
- // find the matching node in the table
- Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
- {
- if ( pThis != pAnd )
- {
- pPlace = pAnd;
- continue;
- }
- if ( pPlace == NULL )
- pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
- else
- pPlace->NextH = pThis->NextH;
- break;
- }
- assert( pThis == pAnd );
- pMan->pTable->nEntries--;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resizes the hash table of AIG nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TableResize( Aig_Man_t * pMan )
-{
- Aig_Node_t ** pBinsNew;
- Aig_Node_t * pEnt, * pEnt2;
- int nBinsNew, Counter, i, clk;
- unsigned Key;
-
-clk = clock();
- // get the new table size
- nBinsNew = Cudd_PrimeCopy( 3 * pMan->pTable->nBins );
- // allocate a new array
- pBinsNew = ALLOC( Aig_Node_t *, nBinsNew );
- memset( pBinsNew, 0, sizeof(Aig_Node_t *) * nBinsNew );
- // rehash the entries from the old table
- Counter = 0;
- for ( i = 0; i < pMan->pTable->nBins; i++ )
- Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
- {
- Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
- pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
- pBinsNew[Key] = pEnt;
- Counter++;
- }
- assert( Counter == pMan->pTable->nEntries );
-// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
-// PRT( "Time", clock() - clk );
- // replace the table and the parameters
- free( pMan->pTable->pBins );
- pMan->pTable->pBins = pBinsNew;
- pMan->pTable->nBins = nBinsNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resizes the hash table of AIG nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TableRehash( Aig_Man_t * pMan )
-{
- Aig_Node_t ** pBinsNew;
- Aig_Node_t * pEnt, * pEnt2;
- unsigned Key;
- int Counter, Temp, i;
- // allocate a new array
- pBinsNew = ALLOC( Aig_Node_t *, pMan->pTable->nBins );
- memset( pBinsNew, 0, sizeof(Aig_Node_t *) * pMan->pTable->nBins );
- // rehash the entries from the old table
- Counter = 0;
- for ( i = 0; i < pMan->pTable->nBins; i++ )
- Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
- {
- // swap the fanins if needed
- if ( pEnt->Fans[0].iNode > pEnt->Fans[1].iNode )
- {
- Temp = pEnt->Fans[0].iNode;
- pEnt->Fans[0].iNode = pEnt->Fans[1].iNode;
- pEnt->Fans[1].iNode = Temp;
- Temp = pEnt->Fans[0].fComp;
- pEnt->Fans[0].fComp = pEnt->Fans[1].fComp;
- pEnt->Fans[1].fComp = Temp;
- }
- // rehash the node
- Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
- pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
- pBinsNew[Key] = pEnt;
- Counter++;
- }
- assert( Counter == pMan->pTable->nEntries );
- // replace the table and the parameters
- free( pMan->pTable->pBins );
- pMan->pTable->pBins = pBinsNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the smallest prime larger than the number.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned int Cudd_PrimeAig( 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/aig/aigUtil.c b/src/sat/aig/aigUtil.c
deleted file mode 100644
index 40f7aba1..00000000
--- a/src/sat/aig/aigUtil.c
+++ /dev/null
@@ -1,190 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigUtil.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: aigUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Increments the current traversal ID of the network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManIncrementTravId( Aig_Man_t * pMan )
-{
- Aig_Node_t * pObj;
- int i;
- if ( pMan->nTravIds == (1<<24)-1 )
- {
- pMan->nTravIds = 0;
- Aig_ManForEachNode( pMan, pObj, i )
- pObj->TravId = 0;
- }
- pMan->nTravIds++;
-}
-
-
-/**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
deleted file mode 100644
index a8df9a72..00000000
--- a/src/sat/aig/fraigClass.c
+++ /dev/null
@@ -1,320 +0,0 @@
-/**CFile****************************************************************
-
- FileName [fraigClass.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: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-#include "stmm.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the equivalence classes of patterns.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
-{
- 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, Entry, ClassNum;
- assert( pInfo->Type == 1 );
- // fill in the hash table
- tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
- vClasses = Vec_VecAlloc( 100 );
- // 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, 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
- {
- // create the class
- ClassNum = Vec_VecSize( vClasses );
- Vec_VecPush( vClasses, ClassNum, (void *)((*pSpot) >> 1) );
- Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
- // save the class
- *pSpot = (ClassNum << 1);
- }
- else // this is a class
- {
- 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" );
- }
-*/
- printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) );
- return vClasses;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the hash key of the simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-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;
- if ( fPhase )
- for ( i = 0; i < nWords; i++ )
- uKey ^= i * Primes[i%10] * pData[i];
- else
- for ( i = 0; i < nWords; i++ )
- uKey ^= i * Primes[i%10] * ~pData[i];
- return uKey;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Splits the equivalence class.]
-
- Description [Given an equivalence class (vClass) and the simulation info,
- split the class into two based on the info.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSplitClass( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Int_t * vClass, Vec_Int_t * vClass2, Aig_Pattern_t * pPat )
-{
- int NodeId, i, k, w;
- Aig_Node_t * pRoot, * pTemp;
- unsigned * pRootData, * pTempData;
- assert( Vec_IntSize(vClass) > 1 );
- assert( pInfo->nPatsCur == pPat->nBits );
-// printf( "Class = %5d. --> ", Vec_IntSize(vClass) );
- // clear storage for the new classes
- Vec_IntClear( vClass2 );
- // get the root member of the class
- pRoot = Aig_ManNode( p, Vec_IntEntry(vClass, 0) );
- pRootData = Aig_SimInfoForNode( pInfo, pRoot );
- // sort the class members:
- // (1) with the same siminfo as pRoot remain in vClass
- // (2) nodes with other siminfo go to vClass2
- k = 1;
- Vec_IntForEachEntryStart( vClass, NodeId, i, 1 )
- {
- NodeId = Vec_IntEntry(vClass, i);
- pTemp = Aig_ManNode( p, NodeId );
- pTempData = Aig_SimInfoForNode( pInfo, pTemp );
- if ( pRoot->fPhase == pTemp->fPhase )
- {
- for ( w = 0; w < pInfo->nWords; w++ )
- if ( pRootData[w] != pTempData[w] )
- break;
- if ( w == pInfo->nWords ) // the same info
- Vec_IntWriteEntry( vClass, k++, NodeId );
- else
- {
- Vec_IntPush( vClass2, NodeId );
- // record the diffs if they are not distinguished by the first pattern
- if ( ((pRootData[0] ^ pTempData[0]) & 1) == 0 )
- for ( w = 0; w < pInfo->nWords; w++ )
- pPat->pData[w] |= (pRootData[w] ^ pTempData[w]);
- }
- }
- else
- {
- for ( w = 0; w < pInfo->nWords; w++ )
- if ( pRootData[w] != ~pTempData[w] )
- break;
- if ( w == pInfo->nWords ) // the same info
- Vec_IntWriteEntry( vClass, k++, NodeId );
- else
- {
- Vec_IntPush( vClass2, NodeId );
- // record the diffs if they are not distinguished by the first pattern
- if ( ((pRootData[0] ^ ~pTempData[0]) & 1) == 0 )
- for ( w = 0; w < pInfo->nWords; w++ )
- pPat->pData[w] |= (pRootData[w] ^ ~pTempData[w]);
- }
- }
- }
- Vec_IntShrink( vClass, k );
-// printf( "Class1 = %5d. Class2 = %5d.\n", Vec_IntSize(vClass), Vec_IntSize(vClass2) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates the equivalence classes using the simulation info.]
-
- Description [Records successful simulation patterns into the pattern
- storage.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask )
-{
- Vec_Ptr_t * vClass;
- int i, k, fSplit = 0;
- assert( Vec_VecSize(vClasses) > 0 );
- // collect patterns that lead to changes
- Aig_PatternClean( pPatMask );
- // split the classes using the new symmetry info
- Vec_VecForEachLevel( vClasses, vClass, i )
- {
- if ( i == 0 )
- continue;
- // split vClass into two parts (vClass and vClassTemp)
- Aig_ManSplitClass( p, pInfo, (Vec_Int_t *)vClass, p->vClassTemp, pPatMask );
- // check if there is any splitting
- if ( Vec_IntSize(p->vClassTemp) > 0 )
- fSplit = 1;
- // skip the new class if it is empty or trivial
- if ( Vec_IntSize(p->vClassTemp) < 2 )
- continue;
- // consider replacing the current class with the new one
- if ( Vec_PtrSize(vClass) == 1 )
- {
- assert( vClasses->pArray[i] == vClass );
- vClasses->pArray[i] = p->vClassTemp;
- p->vClassTemp = (Vec_Int_t *)vClass;
- i--;
- continue;
- }
- // add the new non-trival class in the end
- Vec_PtrPush( (Vec_Ptr_t *)vClasses, p->vClassTemp );
- p->vClassTemp = Vec_IntAlloc( 10 );
- }
- // free trivial classes
- k = 0;
- Vec_VecForEachLevel( vClasses, vClass, i )
- {
- assert( Vec_PtrSize(vClass) > 0 );
- if ( Vec_PtrSize(vClass) == 1 )
- Vec_PtrFree(vClass);
- else
- vClasses->pArray[k++] = vClass;
- }
- Vec_PtrShrink( (Vec_Ptr_t *)vClasses, k );
- // catch the patterns which led to splitting
- printf( "Classes = %6d. Pairs = %6d. Patterns = %3d.\n",
- Vec_VecSize(vClasses),
- Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses),
- Vec_PtrSize(p->vPats) );
- return fSplit;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects useful patterns.]
-
- Description [If the flag fAddToVector is 1, creates and adds new patterns
- to the internal storage of patterns.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats )
-{
- Aig_SimInfo_t * pInfoRes = p->pInfo;
- Aig_Pattern_t * pPatNew;
- Aig_Node_t * pNode;
- int i, k;
-
- assert( Aig_InfoHasBit(pMask->pData, 0) == 0 );
- for ( i = 0; i < pMask->nBits; i++ )
- {
- if ( vPats && Vec_PtrSize(vPats) >= p->nPatsMax )
- break;
- if ( i == 0 || Aig_InfoHasBit(pMask->pData, i) )
- {
- // expand storage if needed
- if ( pInfoRes->nPatsCur == pInfoRes->nPatsMax )
- Aig_SimInfoResize( pInfoRes );
- // create a new pattern
- if ( vPats )
- {
- pPatNew = Aig_PatternAlloc( Aig_ManPiNum(p) );
- Aig_PatternClean( pPatNew );
- }
- // go through the PIs
- Aig_ManForEachPi( p, pNode, k )
- {
- if ( Aig_InfoHasBit( Aig_SimInfoForNode(pInfo, pNode), i ) )
- {
- Aig_InfoSetBit( Aig_SimInfoForPi(pInfoRes, k), pInfoRes->nPatsCur );
- if ( vPats ) Aig_InfoSetBit( pPatNew->pData, k );
- }
- }
- // store the new pattern
- if ( vPats ) Vec_PtrPush( vPats, pPatNew );
- // increment the number of patterns stored
- pInfoRes->nPatsCur++;
- }
- }
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c
deleted file mode 100644
index 913165b2..00000000
--- a/src/sat/aig/fraigCnf.c
+++ /dev/null
@@ -1,476 +0,0 @@
-/**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
deleted file mode 100644
index 03781180..00000000
--- a/src/sat/aig/fraigCore.c
+++ /dev/null
@@ -1,129 +0,0 @@
-/**CFile****************************************************************
-
- FileName [fraigCore.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: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- 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 );
- // reduce equivalence classes using simulation
- Aig_EngineSimulateFirst( pMan );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Top-level equivalence checking procedure.]
-
- Description []
-
- SideEffects []
-
- 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, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit );
- 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
deleted file mode 100644
index 17468e8f..00000000
--- a/src/sat/aig/fraigEngine.c
+++ /dev/null
@@ -1,174 +0,0 @@
-/**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 [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( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 );
- Aig_SimInfoRandom( pInfoPi );
- // allocate sim info for all nodes
- pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 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( Aig_ManPiNum(p), Aig_ManPiNum(p)+1, 0 );
- p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1, 1 );
- p->pPatMask = Aig_PatternAlloc( Aig_ManPiNum(p)+1 );
-}
-
-/**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, Counter;
-
- // simulate the pattern of all zeros
- pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
- Aig_PatternClean( pPat );
- Vec_PtrPush( p->vPats, pPat );
- if ( !Aig_EngineSimulate( p ) )
- return;
-
- // simulate the pattern of all ones
- pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
- Aig_PatternFill( pPat );
- Vec_PtrPush( p->vPats, pPat );
- if ( !Aig_EngineSimulate( p ) )
- return;
-
- // simulate random until the number of new patterns is reasonable
- do {
- // generate random PI siminfo
- Aig_SimInfoRandom( p->pInfoPi );
- // simulate this info
- Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
- // split the classes and collect the new patterns
- if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
- Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL );
- if ( Vec_VecSize(p->vClasses) == 0 )
- return;
- // count the number of useful patterns
- Counter = Aig_PatternCount(p->pPatMask);
- }
- while ( Counter > p->nPatsMax/2 );
-
- // perform targetted simulation
- for ( i = 0; i < 3; i++ )
- {
- assert( Vec_PtrSize(p->vPats) == 0 );
- // generate random PI siminfo
- Aig_SimInfoRandom( p->pInfoPi );
- // simulate this info
- Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
- // split the classes and collect the new patterns
- if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
- Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
- if ( Vec_VecSize(p->vClasses) == 0 )
- return;
- // simulate the remaining patters
- if ( Vec_PtrSize(p->vPats) > 0 )
- 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);
- assert( pPat->nBits == Aig_ManPiNum(p) );
- // create the new siminfo
- Aig_SimInfoFromPattern( p->pInfoPi, pPat );
- // free the pattern
- Aig_PatternFree( pPat );
-
- // simulate this info
- Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
- // split the classes and collect the new patterns
- if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
- Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
- }
- return Vec_VecSize(p->vClasses) > 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
deleted file mode 100644
index 901f2fe2..00000000
--- a/src/sat/aig/fraigProve.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
- FileName [fraigProve.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: fraigProve.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/fraigSim.c b/src/sat/aig/fraigSim.c
deleted file mode 100644
index 6d4f214c..00000000
--- a/src/sat/aig/fraigSim.c
+++ /dev/null
@@ -1,361 +0,0 @@
-/**CFile****************************************************************
-
- FileName [fraigSim.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: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Simulates all nodes using the given simulation info.]
-
- Description [Returns the simulation info for all nodes.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
-{
- Aig_Node_t * pNode;
- unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
- int i, k, fComp0, fComp1;
-
- assert( !pInfoPi->Type ); // PI siminfo
- // set the constant sim info
- pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pData1[k] = ~((unsigned)0);
- // set the PI siminfo
- Aig_ManForEachPi( p, pNode, i )
- {
- pDataPi = Aig_SimInfoForPi( pInfoPi, i );
- pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pDataAnd[k] = pDataPi[k];
- }
- // simulate the nodes
- Aig_ManForEachAnd( p, pNode, i )
- {
- pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
- pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
- pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
- fComp0 = Aig_NodeFaninC0(pNode);
- fComp1 = Aig_NodeFaninC1(pNode);
- if ( fComp0 && fComp1 )
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pDataAnd[k] = ~pData0[k] & ~pData1[k];
- else if ( fComp0 )
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pDataAnd[k] = ~pData0[k] & pData1[k];
- else if ( fComp1 )
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pDataAnd[k] = pData0[k] & ~pData1[k];
- else
- for ( k = 0; k < pInfoPi->nWords; k++ )
- pDataAnd[k] = pData0[k] & pData1[k];
- }
- // derive the PO siminfo
- Aig_ManForEachPo( 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 [Allocates the simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, int Type )
-{
- Aig_SimInfo_t * p;
- p = ALLOC( Aig_SimInfo_t, 1 );
- memset( p, 0, sizeof(Aig_SimInfo_t) );
- p->Type = Type;
- p->nNodes = nNodes;
- p->nWords = Aig_BitWordNum(nBits);
- p->nPatsCur = nBits;
- p->nPatsMax = p->nWords * sizeof(unsigned) * 8;
- p->pData = ALLOC( unsigned, nNodes * p->nWords );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets the simulation info to zero.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_SimInfoClean( Aig_SimInfo_t * p )
-{
- int i, Size = p->nNodes * p->nWords;
- p->nPatsCur = 0;
- for ( i = 0; i < Size; i++ )
- p->pData[i] = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets the random simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_SimInfoRandom( Aig_SimInfo_t * p )
-{
- int i, Size = p->nNodes * p->nWords;
- unsigned * pData;
- for ( i = 0; i < Size; i++ )
- p->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
- // make sure the first bit of all nodes is 0
- for ( i = 0; i < p->nNodes; i++ )
- {
- pData = p->pData + p->nWords * i;
- *pData <<= 1;
- }
-}
-
-/**Function*************************************************************
-
- 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->nPatsCur == pPat->nBits+1 );
- for ( i = 0; i < p->nPatsCur; 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, starting from the first pattern
- if ( i ) Aig_InfoXorBit( pData, i-1 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Resizes the simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_SimInfoResize( Aig_SimInfo_t * p )
-{
- unsigned * pData;
- int i, k;
- assert( p->nPatsCur == p->nPatsMax );
- pData = ALLOC( unsigned, 2 * p->nNodes * p->nWords );
- for ( i = 0; i < p->nNodes; i++ )
- {
- for ( k = 0; k < p->nWords; k++ )
- pData[2 * p->nWords * i + k] = p->pData[p->nWords * i + k];
- for ( k = 0; k < p->nWords; k++ )
- pData[2 * p->nWords * i + k + p->nWords] = 0;
- }
- p->nWords *= 2;
- p->nPatsMax *= 2;
- free( p->pData );
- p->pData = pData;
-}
-
-/**Function*************************************************************
-
- Synopsis [Deallocates the simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_SimInfoFree( Aig_SimInfo_t * p )
-{
- free( p->pData );
- free( 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 [Cleans the pattern.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_PatternFill( Aig_Pattern_t * pPat )
-{
- memset( pPat->pData, 0xff, 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 [Counts the number of 1s in the pattern.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_PatternCount( Aig_Pattern_t * pPat )
-{
- int i, Counter = 0;
- for ( i = 0; i < pPat->nBits; i++ )
- Counter += Aig_InfoHasBit( pPat->pData, i );
- return Counter;
-}
-
-/**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
deleted file mode 100644
index 12502951..00000000
--- a/src/sat/aig/fraigSolver.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**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
deleted file mode 100644
index d5a09259..00000000
--- a/src/sat/aig/fraigTrav.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/rwrMffc.c b/src/sat/aig/rwrMffc.c
deleted file mode 100644
index 663534b3..00000000
--- a/src/sat/aig/rwrMffc.c
+++ /dev/null
@@ -1,303 +0,0 @@
-/**CFile****************************************************************
-
- FileName [rwrMffc.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [And-Inverter Graph package.]
-
- Synopsis [Procedures working with Maximum Fanout-Free Cones.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: rwrMffc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-extern int Aig_NodeDeref_rec( Aig_Node_t * pNode );
-extern int Aig_NodeRef_rec( Aig_Node_t * pNode );
-extern void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-extern void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_MffcTest( Aig_Man_t * pMan )
-{
- Aig_Node_t * pNode, * pNodeA, * pNodeB, * pNodeC, * pLeaf;
- Vec_Ptr_t * vCone, * vSupp;
- int i, k;//, nNodes1, nNodes2;
- int nSizes = 0;
- int nCones = 0;
- int nMuxes = 0;
- int nExors = 0;
-
- vCone = Vec_PtrAlloc( 100 );
- vSupp = Vec_PtrAlloc( 100 );
-
- // mark the multiple-fanout nodes
- Aig_ManForEachAnd( pMan, pNode, i )
- if ( pNode->nRefs > 1 )
- pNode->fMarkA = 1;
- // unmark the control inputs of MUXes and inputs of EXOR gates
- Aig_ManForEachAnd( pMan, pNode, i )
- {
- if ( !Aig_NodeIsMuxType(pNode) )
- continue;
-
- pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
- // if real children are used, skip
- if ( Aig_NodeFanin0(pNode)->nRefs > 1 || Aig_NodeFanin1(pNode)->nRefs > 1 )
- continue;
-/*
-
- if ( pNodeC->nRefs == 2 )
- pNodeC->fMarkA = 0;
- if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) && Aig_Regular(pNodeA)->nRefs == 2 )
- Aig_Regular(pNodeA)->fMarkA = 0;
-*/
-
- if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) )
- nExors++;
- else
- nMuxes++;
- }
- // mark the PO drivers
- Aig_ManForEachPo( pMan, pNode, i )
- {
- Aig_NodeFanin0(pNode)->fMarkA = 1;
- Aig_NodeFanin0(pNode)->fMarkB = 1;
- }
-
-
- // print sizes of MFFCs
- Aig_ManForEachAnd( pMan, pNode, i )
- {
- if ( !pNode->fMarkA )
- continue;
-
-// nNodes1 = Aig_NodeDeref_rec( pNode );
-// Aig_NodeMffsConeSupp( pNode, vCone, vSupp );
-// nNodes2 = Aig_NodeRef_rec( pNode );
-// assert( nNodes1 == nNodes2 );
-
- Aig_NodeFactorConeSupp( pNode, vCone, vSupp );
-
- printf( "%6d : Fan = %4d. Co = %5d. Su = %5d. %s ",
- pNode->Id, pNode->nRefs, Vec_PtrSize(vCone), Vec_PtrSize(vSupp), pNode->fMarkB? "po" : " " );
-
- Vec_PtrForEachEntry( vSupp, pLeaf, k )
- printf( " %d", pLeaf->Id );
-
- printf( "\n" );
-
- nSizes += Vec_PtrSize(vCone);
- nCones++;
- }
- printf( "Nodes = %6d. MFFC sizes = %6d. Cones = %6d. nExors = %6d. Muxes = %6d.\n",
- Aig_ManAndNum(pMan), nSizes, nCones, nExors, nMuxes );
-
- // unmark the nodes
- Aig_ManForEachNode( pMan, pNode, i )
- {
- pNode->fMarkA = 0;
- pNode->fMarkB = 0;
- pNode->fMarkC = 0;
- }
-
- Vec_PtrFree( vCone );
- Vec_PtrFree( vSupp );
-}
-
-/**Function*************************************************************
-
- Synopsis [Dereferences the node's MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeDeref_rec( Aig_Node_t * pNode )
-{
- Aig_Node_t * pNode0, * pNode1;
- int Counter = 1;
- if ( Aig_NodeIsPi(pNode) )
- return 0;
- pNode0 = Aig_NodeFanin0(pNode);
- pNode1 = Aig_NodeFanin1(pNode);
- assert( pNode0->nRefs > 0 );
- assert( pNode1->nRefs > 0 );
- if ( --pNode0->nRefs == 0 )
- Counter += Aig_NodeDeref_rec( pNode0 );
- if ( --pNode1->nRefs == 0 )
- Counter += Aig_NodeDeref_rec( pNode1 );
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [References the node's MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeRef_rec( Aig_Node_t * pNode )
-{
- Aig_Node_t * pNode0, * pNode1;
- int Counter = 1;
- if ( Aig_NodeIsPi(pNode) )
- return 0;
- pNode0 = Aig_NodeFanin0(pNode);
- pNode1 = Aig_NodeFanin1(pNode);
- if ( pNode0->nRefs++ == 0 )
- Counter += Aig_NodeRef_rec( pNode0 );
- if ( pNode1->nRefs++ == 0 )
- Counter += Aig_NodeRef_rec( pNode1 );
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the internal and leaf nodes in the derefed MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeMffsConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
-{
- // skip visited nodes
- if ( Aig_NodeIsTravIdCurrent(pNode) )
- return;
- Aig_NodeSetTravIdCurrent(pNode);
- // add to the new support nodes
- if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->nRefs > 0) )
- {
- Vec_PtrPush( vSupp, pNode );
- return;
- }
- // recur on the children
- Aig_NodeMffsConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
- Aig_NodeMffsConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
- // collect the internal node
- Vec_PtrPush( vCone, pNode );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the support of the derefed MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
-{
- assert( Aig_NodeIsAnd(pNode) );
- assert( !Aig_IsComplement(pNode) );
- Vec_PtrClear( vCone );
- Vec_PtrClear( vSupp );
- Aig_ManIncrementTravId( pNode->pMan );
- Aig_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
-}
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Collects the internal and leaf nodes of the factor-cut of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeFactorConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
-{
- // skip visited nodes
- if ( Aig_NodeIsTravIdCurrent(pNode) )
- return;
- Aig_NodeSetTravIdCurrent(pNode);
- // add to the new support nodes
- if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->fMarkA) )
- {
- Vec_PtrPush( vSupp, pNode );
- return;
- }
- // recur on the children
- Aig_NodeFactorConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
- Aig_NodeFactorConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
- // collect the internal node
- assert( fTopmost || !pNode->fMarkA );
- Vec_PtrPush( vCone, pNode );
-
- assert( pNode->fMarkC == 0 );
- pNode->fMarkC = 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the support of the derefed MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
-{
- assert( Aig_NodeIsAnd(pNode) );
- assert( !Aig_IsComplement(pNode) );
- Vec_PtrClear( vCone );
- Vec_PtrClear( vSupp );
- Aig_ManIncrementTravId( pNode->pMan );
- Aig_NodeFactorConeSupp_rec( pNode, vCone, vSupp, 1 );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
deleted file mode 100644
index cb8d03e0..00000000
--- a/src/sat/aig/rwrTruth.c
+++ /dev/null
@@ -1,456 +0,0 @@
-/**CFile****************************************************************
-
- FileName [rwrTruth.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: rwrTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-/* The code in this file was written with portability to 64-bits in mind.
- The type "unsigned" is assumed to be 32-bit on any platform.
-*/
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-#define ABCTMAX 8 // the max number of vars
-
-typedef struct Aig_Truth_t_ Aig_Truth_t;
-struct Aig_Truth_t_
-{
- short nVars; // the number of variables
- short nWords; // the number of 32-bit words
- unsigned Truth[1<<(ABCTMAX-5)]; // the truth table
- unsigned Cofs[2][1<<(ABCTMAX-6)]; // the truth table of cofactors
- unsigned Data[4][1<<(ABCTMAX-7)]; // the truth table of cofactors
- short Counts[ABCTMAX][2]; // the minterm counters
- Aig_Node_t * pLeaves[ABCTMAX]; // the pointers to leaves
- Aig_Man_t * pMan; // the AIG manager
-};
-
-static void Aig_TruthCount( Aig_Truth_t * p );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the function given the truth table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Truth_t * Aig_TruthCreate( int nVars, unsigned * pTruth, Aig_Node_t ** pLeaves )
-{
- Aig_Truth_t * p;
- int i;
- p = ALLOC( Aig_Truth_t, 1 );
- memset( p, 0, sizeof(Aig_Truth_t) );
- p->nVars = nVars;
- p->nWords = (nVars < 5)? 1 : (1 << (nVars-5));
- for ( i = 0; i < p->nWords; i++ )
- p->Truth[i] = pTruth[i];
- if ( nVars < 5 )
- p->Truth[0] &= (~0u >> (32-(1<<nVars)));
- for ( i = 0; i < p->nVars; i++ )
- p->pLeaves[i] = pLeaves[i];
- Aig_TruthCount( p );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of miterms in the cofactors.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Aig_WordCountOnes( unsigned val )
-{
- val = (val & 0x55555555) + ((val>>1) & 0x55555555);
- val = (val & 0x33333333) + ((val>>2) & 0x33333333);
- val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F);
- val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF);
- return (val & 0x0000FFFF) + (val>>16);
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of miterms in the cofactors.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TruthCount( Aig_Truth_t * p )
-{
- static unsigned Masks[5][2] = {
- { 0x33333333, 0xAAAAAAAA },
- { 0x55555555, 0xCCCCCCCC },
- { 0x0F0F0F0F, 0xF0F0F0F0 },
- { 0x00FF00FF, 0xFF00FF00 },
- { 0x0000FFFF, 0xFFFF0000 }
- };
-
- int i, k;
- assert( p->Counts[0][0] == 0 && p->Counts[0][1] == 0 );
- for ( i = 0; i < p->nVars; i++ )
- {
- p->Counts[i][0] = p->Counts[i][1] = 0;
- if ( i < 5 )
- {
- for ( k = 0; k < p->nWords; k++ )
- {
- p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] & Masks[i][0] );
- p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] & Masks[i][1] );
- }
- }
- else
- {
- for ( k = 0; k < p->nWords; k++ )
- if ( i & (1 << (k-5)) )
- p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] );
- else
- p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] );
- }
- }
-/*
- // normalize the variables
- for ( i = 0; i < p->nVars; i++ )
- if ( p->Counts[i][0] > p->Counts[i][1] )
- {
- k = p->Counts[i][0];
- p->Counts[i][0] = p->Counts[i][1];
- p->Counts[i][1] = k;
- p->pLeaves[i] = Aig_Not( p->pLeaves[i] );
- }
-*/
-}
-
-/**Function*************************************************************
-
- Synopsis [Extracts one part of the bitstring.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
-{
- return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size));
-}
-
-/**Function*************************************************************
-
- Synopsis [Inserts one part of the bitstring.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
-{
- p[Start/5] |= (Part << (Start&31));
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the cofactor with respect to one variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TruthCofactor( int Var, int Pol, int nVars, unsigned * pTruth, unsigned * pResult )
-{
- if ( Var < 5 )
- {
- int nPartSize = ( 1 << Var );
- int nParts = ( 1 << (nVars-Var-1) );
- unsigned uPart;
- int i;
- for ( i = 0; i < nParts; i++ )
- {
- uPart = Aig_WordGetPart( pTruth, (2*i+Pol)*nPartSize, nPartSize );
- Aig_WordSetPart( pResult, i*nPartSize, uPart );
- }
- if ( nVars <= 5 )
- pResult[0] &= (~0u >> (32-(1<<(nVars-1))));
- }
- else
- {
- int nWords = (1 << (nVars-5));
- int i, k = 0;
- for ( i = 0; i < nWords; i++ )
- if ( (i & (1 << (Var-5))) == Pol )
- pResult[k++] = pTruth[i];
- assert( k == nWords/2 );
- }
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Computes the BDD of the truth table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int nVars, int iVar )
-{
- DdNode * bCof0, * bCof1, * bRes;
- if ( nVars == 1 )
- return Cudd_NotCond( Cudd_ReadOne(dd), !Aig_WordGetPart(pTruth, Shift, 1) );
- if ( nVars == 3 )
- {
- unsigned char * pChar = ((char *)pTruth) + Shift/8;
- assert( Shift % 8 == 0 );
- if ( *pChar == 0 )
- return Cudd_ReadLogicZero(dd);
- if ( *pChar == 0xFF )
- return Cudd_ReadOne(dd);
- }
- if ( nVars == 5 )
- {
- unsigned * pWord = pTruth + (Shift>>5);
- assert( Shift % 32 == 0 );
- if ( *pWord == 0 )
- return Cudd_ReadLogicZero(dd);
- if ( *pWord == 0xFFFFFFFF )
- return Cudd_ReadOne(dd);
- }
- bCof0 = Aig_TruthToBdd_rec( dd, pTruth, Shift, nVars-1, iVar+1 ); Cudd_Ref( bCof0 );
- bCof1 = Aig_TruthToBdd_rec( dd, pTruth, Shift + (1 << (nVars-1)), nVars-1, iVar+1 ); Cudd_Ref( bCof1 );
- bRes = Cudd_bddIte( dd, Cudd_bddIthVar(dd, iVar), bCof1, bCof0 ); Cudd_Ref( bRes );
- Cudd_RecursiveDeref( dd, bCof0 );
- Cudd_RecursiveDeref( dd, bCof1 );
- Cudd_Deref( bRes );
- return bRes;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the BDD of the truth table.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-DdNode * Aig_TruthToBdd( DdManager * dd, Aig_Truth_t * p )
-{
- return Aig_TruthToBdd_rec( dd, p->Truth, 0, p->nVars, 0 );
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Compare bistrings.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Aig_WordCompare( unsigned * p0, unsigned * p1, int nWords )
-{
- int i;
- for ( i = 0; i < nWords; i++ )
- if ( p0[i] != p1[i] )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Compare bistrings.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Aig_WordCompareCompl( unsigned * p0, unsigned * p1, int nWords )
-{
- int i;
- for ( i = 0; i < nWords; i++ )
- if ( p0[i] != ~p1[i] )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the cofactor with respect to one variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_TruthReplaceByCofactor( Aig_Truth_t * p, int iVar, unsigned * pTruth )
-{
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Computes the cofactor with respect to one variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p )
-{
- Aig_Node_t * pVar;
- int nOnesCof = ( 1 << (p->nVars-1) );
- int nWordsCof = (p->nWords == 1 ? 1 : p->nWords/2);
- int i;
-
- // check for constant function
- if ( p->nVars == 0 )
- return Aig_NotCond( Aig_ManConst1(p->pMan), (p->Truth[0]&1)==0 );
-
- // count the number of minterms in the cofactors
- Aig_TruthCount( p );
-
- // remove redundant variables and EXORs
- for ( i = p->nVars - 1; i >= 0; i-- )
- {
- if ( p->Counts[i][0] == p->Counts[i][1] )
- {
- // compute cofactors
- Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
- Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
- if ( Aig_WordCompare( p->Cofs[0], p->Cofs[1], nWordsCof ) )
- { // equal
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
- return Aig_TruthDecompose( p );
- }
- }
- // check the case of EXOR
- if ( p->Counts[i][0] == nOnesCof - p->Counts[i][1] )
- {
- // compute cofactors
- Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
- Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
- if ( Aig_WordCompareCompl( p->Cofs[0], p->Cofs[1], nWordsCof ) )
- { // equal
- pVar = p->pLeaves[i];
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
- // F = x' * F0 + x * F1 = x <+> F0 assuming that F0 == ~F1
- return Aig_Xor( p->pMan, pVar, Aig_TruthDecompose( p ) );
- }
- }
- }
-
- // process variables with constant cofactors
- for ( i = p->nVars - 1; i >= 0; i-- )
- {
- if ( p->Counts[i][0] != 0 && p->Counts[i][1] != 0 &&
- p->Counts[i][0] != nOnesCof && p->Counts[i][1] != nOnesCof )
- continue;
- pVar = p->pLeaves[i];
- if ( p->Counts[i][0] == 0 )
- {
- Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
- // F = x' * 0 + x * F1 = x * F1
- return Aig_And( p->pMan, pVar, Aig_TruthDecompose( p ) );
- }
- if ( p->Counts[i][1] == 0 )
- {
- Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
- // F = x' * F0 + x * 0 = x' * F0
- return Aig_And( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
- }
- if ( p->Counts[i][0] == nOnesCof )
- {
- Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
- // F = x' * 1 + x * F1 = x' + F1
- return Aig_Or( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
- }
- if ( p->Counts[i][1] == nOnesCof )
- {
- Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
- // remove redundant variable
- Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
- // F = x' * F0 + x * 1 = x + F0
- return Aig_Or( p->pMan, pVar, Aig_TruthDecompose( p ) );
- }
- assert( 0 );
- }
-
-
- return NULL;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/rwr_.c b/src/sat/aig/rwr_.c
deleted file mode 100644
index 45e76f75..00000000
--- a/src/sat/aig/rwr_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
- FileName [rwr_.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: rwr_.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-02 17:28:25 +0000