summaryrefslogtreecommitdiffstats
path: root/src/aig/dch
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dch')
-rw-r--r--src/aig/dch/dch.h90
-rw-r--r--src/aig/dch/dchAig.c119
-rw-r--r--src/aig/dch/dchChoice.c508
-rw-r--r--src/aig/dch/dchClass.c611
-rw-r--r--src/aig/dch/dchCnf.c334
-rw-r--r--src/aig/dch/dchCore.c158
-rw-r--r--src/aig/dch/dchInt.h170
-rw-r--r--src/aig/dch/dchMan.c191
-rw-r--r--src/aig/dch/dchSat.c166
-rw-r--r--src/aig/dch/dchSim.c297
-rw-r--r--src/aig/dch/dchSimSat.c258
-rw-r--r--src/aig/dch/dchSweep.c146
-rw-r--r--src/aig/dch/module.make10
13 files changed, 0 insertions, 3058 deletions
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
deleted file mode 100644
index 69f340e5..00000000
--- a/src/aig/dch/dch.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dch.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __DCH_H__
-#define __DCH_H__
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-// choicing parameters
-typedef struct Dch_Pars_t_ Dch_Pars_t;
-struct Dch_Pars_t_
-{
- int nWords; // the number of simulation words
- int nBTLimit; // conflict limit at a node
- int nSatVarMax; // the max number of SAT variables
- int fSynthesis; // set to 1 to perform synthesis
- int fPolarFlip; // uses polarity adjustment
- int fSimulateTfo; // uses simulation of TFO classes
- int fPower; // uses power-aware rewriting
- int fUseGia; // uses GIA package
- int fUseCSat; // uses circuit-based solver
- int fLightSynth; // uses lighter version of synthesis
- int fVerbose; // verbose stats
- int timeSynth; // synthesis runtime
- int nNodesAhead; // the lookahead in terms of nodes
- int nCallsRecycle; // calls to perform before recycling SAT solver
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== dchAig.c ==========================================================*/
-extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
-/*=== dchCore.c ==========================================================*/
-extern void Dch_ManSetDefaultParams( Dch_Pars_t * p );
-extern int Dch_ManReadVerbose( Dch_Pars_t * p );
-extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-/*=== dchScript.c ==========================================================*/
-extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c
deleted file mode 100644
index 91a00c63..00000000
--- a/src/aig/dch/dchAig.c
+++ /dev/null
@@ -1,119 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchAig.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [AIG manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Derives the cumulative AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( pObj->pData )
- return;
- Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) );
- Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) );
- pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the cumulative AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
-{
- Aig_Man_t * pAig, * pAig2, * pAigTotal;
- Aig_Obj_t * pObj, * pObjPi, * pObjPo;
- int i, k, nNodes;
- assert( Vec_PtrSize(vAigs) > 0 );
- // make sure they have the same number of PIs/POs
- nNodes = 0;
- pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
- Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
- {
- assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
- assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
- nNodes += Aig_ManNodeNum(pAig2);
- Aig_ManCleanData( pAig2 );
- }
- // map constant nodes
- pAigTotal = Aig_ManStart( nNodes );
- Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
- Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
- // map primary inputs
- Aig_ManForEachPi( pAig, pObj, i )
- {
- pObjPi = Aig_ObjCreatePi( pAigTotal );
- Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
- Aig_ManPi( pAig2, i )->pData = pObjPi;
- }
- // construct the AIG in the order of POs
- Aig_ManForEachPo( pAig, pObj, i )
- {
- Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
- {
- pObjPo = Aig_ManPo( pAig2, i );
- Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
- }
- Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) );
- }
-/*
- // mark the cone of the first AIG
- Aig_ManIncrementTravId( pAigTotal );
- Aig_ManForEachObj( pAig, pObj, i )
- if ( pObj->pData )
- Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
-*/
- // cleanup should not be done
- return pAigTotal;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c
deleted file mode 100644
index 1772f8aa..00000000
--- a/src/aig/dch/dchChoice.c
+++ /dev/null
@@ -1,508 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchChoice.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Contrustion of choices.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
-{
- Aig_Obj_t * pObj, * pRepr;
- int i, nReprs = 0;
- Aig_ManForEachObj( pAig, pObj, i )
- {
- pRepr = Aig_ObjRepr( pAig, pObj );
- if ( pRepr == NULL )
- continue;
- assert( pRepr->Id < pObj->Id );
- nReprs++;
- }
- return nReprs;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of equivalences.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
-{
- Aig_Obj_t * pObj, * pTemp, * pPrev;
- int i, nEquivs = 0, Counter = 0;
- Aig_ManForEachObj( pAig, pObj, i )
- {
- if ( !Aig_ObjIsChoice(pAig, pObj) )
- continue;
- for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp;
- pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
- {
- if ( pTemp->nRefs > 0 )
- {
- // remove referenced node from equivalence class
- assert( pAig->pEquivs[pPrev->Id] == pTemp );
- pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
- pAig->pEquivs[pTemp->Id] = NULL;
- // how about the need to continue iterating over the list?
- // pPrev = pTemp ???
- Counter++;
- }
- nEquivs++;
- }
- }
-// printf( "Removed %d classes.\n", Counter );
-
- if ( Counter )
- Dch_DeriveChoiceCountEquivs( pAig );
-// if ( Counter )
-// printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
- return nEquivs;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- // check the trivial cases
- if ( pObj == NULL )
- return 0;
- if ( Aig_ObjIsPi(pObj) )
- return 0;
- if ( pObj->fMarkA )
- return 1;
- // skip the visited node
- if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
- return 0;
- Aig_ObjSetTravIdCurrent( p, pObj );
- // check the children
- if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
- return 1;
- if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
- return 1;
- // check equivalent nodes
- return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pTemp;
- int RetValue;
- assert( !Aig_IsComplement(pObj) );
- assert( !Aig_IsComplement(pRepr) );
- // mark nodes of the choice node
- for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
- pTemp->fMarkA = 1;
- // traverse the new node
- Aig_ManIncrementTravId( p );
- RetValue = Dch_ObjCheckTfi_rec( p, pObj );
- // unmark nodes of the choice node
- for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
- pTemp->fMarkA = 0;
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns representatives of fanin in approapriate polarity.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pRepr;
- if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
- return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
- return pObj;
-}
-
-static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
-static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
- // get the new node
- pObj->pData = Aig_And( pAigNew,
- Aig_ObjChild0CopyRepr(pAigNew, pObj),
- Aig_ObjChild1CopyRepr(pAigNew, pObj) );
- pRepr = Aig_ObjRepr( pAigOld, pObj );
- if ( pRepr == NULL )
- return;
- // get the corresponding new nodes
- pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData);
- pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
- if ( pObjNew == pReprNew )
- return;
- // skip the earlier nodes
- if ( pReprNew->Id > pObjNew->Id )
- return;
- assert( pReprNew->Id < pObjNew->Id );
- // set the representatives
- Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
- // skip used nodes
- if ( pObjNew->nRefs > 0 )
- return;
- assert( pObjNew->nRefs == 0 );
- // update new nodes of the object
- if ( !Aig_ObjIsNode(pRepr) )
- return;
- // skip choices with combinational loops
- if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
- return;
- // add choice
- pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
- pAigNew->pEquivs[pReprNew->Id] = pObjNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
-{
- Aig_Man_t * pChoices, * pTemp;
- Aig_Obj_t * pObj;
- int i;
- // start recording equivalences
- pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
- pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- pChoices->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- // map constants and PIs
- Aig_ManCleanData( pAig );
- Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
- Aig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pChoices );
- // construct choices for the internal nodes
- assert( pAig->pReprs != NULL );
- Aig_ManForEachNode( pAig, pObj, i )
- Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
- Aig_ManForEachPo( pAig, pObj, i )
- Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
- Dch_DeriveChoiceCountEquivs( pChoices );
- // there is no need for cleanup
- ABC_FREE( pChoices->pReprs );
- pChoices = Aig_ManDupDfs( pTemp = pChoices );
- Aig_ManStop( pTemp );
- return pChoices;
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Checks for combinational loops in the AIG.]
-
- Description [Returns 1 if combinational loop is detected.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
-{
- Aig_Obj_t * pFanin;
- int fAcyclic;
- if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) )
- return 1;
- assert( Aig_ObjIsNode(pNode) );
- // make sure the node is not visited
- assert( !Aig_ObjIsTravIdPrevious(p, pNode) );
- // check if the node is part of the combinational loop
- if ( Aig_ObjIsTravIdCurrent(p, pNode) )
- {
- if ( fVerbose )
- Abc_Print( 1, "Network \"%s\" contains combinational loop!\n", p->pSpec? p->pSpec : NULL );
- if ( fVerbose )
- Abc_Print( 1, "Node \"%d\" is encountered twice on the following path to the COs:\n", Aig_ObjId(pNode) );
- return 0;
- }
- // mark this node as a node on the current path
- Aig_ObjSetTravIdCurrent( p, pNode );
-
- // visit the transitive fanin
- pFanin = Aig_ObjFanin0(pNode);
- // check if the fanin is visited
- if ( !Aig_ObjIsTravIdPrevious(p, pFanin) )
- {
- // traverse the fanin's cone searching for the loop
- if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
- {
- // return as soon as the loop is detected
- if ( fVerbose )
- Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
- return 0;
- }
- }
-
- // visit the transitive fanin
- pFanin = Aig_ObjFanin1(pNode);
- // check if the fanin is visited
- if ( !Aig_ObjIsTravIdPrevious(p, pFanin) )
- {
- // traverse the fanin's cone searching for the loop
- if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
- {
- // return as soon as the loop is detected
- if ( fVerbose )
- Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
- return 0;
- }
- }
-
- // visit choices
- if ( Aig_ObjRepr(p, pNode) == NULL && Aig_ObjEquiv(p, pNode) != NULL )
- {
- for ( pFanin = Aig_ObjEquiv(p, pNode); pFanin; pFanin = Aig_ObjEquiv(p, pFanin) )
- {
- // check if the fanin is visited
- if ( Aig_ObjIsTravIdPrevious(p, pFanin) )
- continue;
- // traverse the fanin's cone searching for the loop
- if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
- continue;
- // return as soon as the loop is detected
- if ( fVerbose )
- Abc_Print( 1, " %d", Aig_ObjId(pFanin) );
- if ( fVerbose )
- Abc_Print( 1, " (choice of %d) -> ", Aig_ObjId(pNode) );
- return 0;
- }
- }
- // mark this node as a visited node
- Aig_ObjSetTravIdPrevious( p, pNode );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks for combinational loops in the AIG.]
-
- Description [Returns 1 if there is no combinational loops.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
-{
- Aig_Obj_t * pNode;
- int fAcyclic;
- int i;
- // set the traversal ID for this DFS ordering
- Aig_ManIncrementTravId( p );
- Aig_ManIncrementTravId( p );
- // pNode->TravId == pNet->nTravIds means "pNode is on the path"
- // pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path"
- // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited"
- // traverse the network to detect cycles
- fAcyclic = 1;
- Aig_ManForEachPo( p, pNode, i )
- {
- pNode = Aig_ObjFanin0(pNode);
- if ( Aig_ObjIsTravIdPrevious(p, pNode) )
- continue;
- // traverse the output logic cone
- if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pNode, fVerbose)) )
- continue;
- // stop as soon as the first loop is detected
- if ( fVerbose )
- Abc_Print( 1, " CO %d\n", i );
- break;
- }
- return fAcyclic;
-}
-
-/**Function*************************************************************
-
- Synopsis [Removes combinational loop.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
-{
- Aig_Obj_t * pObj;
- int i, Counter = 0, Counter2 = 0;
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
- continue;
- Counter2++;
- if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL )
- {
- Aig_ObjSetEquiv(p, pObj, NULL);
- Counter++;
- }
- }
- if ( fVerbose )
- Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
-{
- Aig_Man_t * pChoices;
- Aig_Obj_t * pObj;
- int i;
- // start recording equivalences
- pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
- pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- pChoices->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- // map constants and PIs
- Aig_ManCleanData( pAig );
- Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
- Aig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pChoices );
- // construct choices for the internal nodes
- assert( pAig->pReprs != NULL );
- Aig_ManForEachNode( pAig, pObj, i )
- Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
- Aig_ManForEachPo( pAig, pObj, i )
- Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
- Dch_DeriveChoiceCountEquivs( pChoices );
- Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
- return pChoices;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
-{
- extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose );
- Aig_Man_t * pChoices, * pTemp;
- int fVerbose = 0;
- pChoices = Dch_DeriveChoiceAigInt( pAig );
-// pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices );
-// Aig_ManStop( pTemp );
- // there is no need for cleanup
- ABC_FREE( pChoices->pReprs );
- while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) )
- {
- if ( fVerbose )
- Abc_Print( 1, "There is a loop!\n" );
- Aig_ManFixLoopProblem( pChoices, fVerbose );
- }
- pChoices = Aig_ManDupDfs( pTemp = pChoices );
- Aig_ManStop( pTemp );
- return pChoices;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c
deleted file mode 100644
index 83a3bc2e..00000000
--- a/src/aig/dch/dchClass.c
+++ /dev/null
@@ -1,611 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchClass.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Representation of candidate equivalence classes.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-/*
- The candidate equivalence classes are stored as a vector of pointers
- to the array of pointers to the nodes in each class.
- The first node of the class is its representative node.
- The representative has the smallest topological order among the class nodes.
- The nodes inside each class are ordered according to their topological order.
- The classes are ordered according to the topo order of their representatives.
-*/
-
-// internal representation of candidate equivalence classes
-struct Dch_Cla_t_
-{
- // class information
- Aig_Man_t * pAig; // original AIG manager
- Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node
- int * pClassSizes; // sizes of each equivalence class
- // statistics
- int nClasses; // the total number of non-const classes
- int nCands1; // the total number of const candidates
- int nLits; // the number of literals in all classes
- // memory
- Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
- Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
- // temporary data
- Vec_Ptr_t * vClassOld; // old equivalence class after splitting
- Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
- // procedures used for class refinement
- void * pManData;
- unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
- int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant
- int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
-};
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Obj_t * Dch_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
-static inline void Dch_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
-
-// iterator through the equivalence classes
-#define Dch_ManForEachClass( p, ppClass, i ) \
- for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
- if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
-// iterator through the nodes in one class
-#define Dch_ClassForEachNode( p, pRepr, pNode, i ) \
- for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
- if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates one equivalence class.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Dch_ObjAddClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
-{
- assert( p->pId2Class[pRepr->Id] == NULL );
- p->pId2Class[pRepr->Id] = pClass;
- assert( p->pClassSizes[pRepr->Id] == 0 );
- assert( nSize > 1 );
- p->pClassSizes[pRepr->Id] = nSize;
- p->nClasses++;
- p->nLits += nSize - 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Removes one equivalence class.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Aig_Obj_t ** Dch_ObjRemoveClass( Dch_Cla_t * p, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
- int nSize;
- assert( pClass != NULL );
- p->pId2Class[pRepr->Id] = NULL;
- nSize = p->pClassSizes[pRepr->Id];
- assert( nSize > 1 );
- p->nClasses--;
- p->nLits -= nSize - 1;
- p->pClassSizes[pRepr->Id] = 0;
- return pClass;
-}
-
-/**Function*************************************************************
-
- Synopsis [Starts representation of equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig )
-{
- Dch_Cla_t * p;
- p = ABC_ALLOC( Dch_Cla_t, 1 );
- memset( p, 0, sizeof(Dch_Cla_t) );
- p->pAig = pAig;
- p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
- p->pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
- p->vClassOld = Vec_PtrAlloc( 100 );
- p->vClassNew = Vec_PtrAlloc( 100 );
- assert( pAig->pReprs == NULL );
- Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Starts representation of equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
- unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
- int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
- int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
-{
- p->pManData = pManData;
- p->pFuncNodeHash = pFuncNodeHash;
- p->pFuncNodeIsConst = pFuncNodeIsConst;
- p->pFuncNodesAreEqual = pFuncNodesAreEqual;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stop representation of equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesStop( Dch_Cla_t * p )
-{
- if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
- if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
- ABC_FREE( p->pId2Class );
- ABC_FREE( p->pClassSizes );
- ABC_FREE( p->pMemClasses );
- ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Stop representation of equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ClassesLitNum( Dch_Cla_t * p )
-{
- return p->nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stop representation of equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
-{
- assert( p->pId2Class[pRepr->Id] != NULL );
- assert( p->pClassSizes[pRepr->Id] > 1 );
- *pnSize = p->pClassSizes[pRepr->Id];
- return p->pId2Class[pRepr->Id];
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks candidate equivalence classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesCheck( Dch_Cla_t * p )
-{
- Aig_Obj_t * pObj, * pPrev, ** ppClass;
- int i, k, nLits, nClasses, nCands1;
- nClasses = nLits = 0;
- Dch_ManForEachClass( p, ppClass, k )
- {
- pPrev = NULL;
- Dch_ClassForEachNode( p, ppClass[0], pObj, i )
- {
- if ( i == 0 )
- assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
- else
- {
- assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
- assert( pPrev->Id < pObj->Id );
- nLits++;
- }
- pPrev = pObj;
- }
- nClasses++;
- }
- nCands1 = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
- nCands1 += Dch_ObjIsConst1Cand( p->pAig, pObj );
- assert( p->nLits == nLits );
- assert( p->nCands1 == nCands1 );
- assert( p->nClasses == nClasses );
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints simulation classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesPrintOne( Dch_Cla_t * p, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pObj;
- int i;
- Abc_Print( 1, "{ " );
- Dch_ClassForEachNode( p, pRepr, pObj, i )
- Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
- Abc_Print( 1, "}\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints simulation classes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose )
-{
- Aig_Obj_t ** ppClass;
- Aig_Obj_t * pObj;
- int i;
- Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
- p->nCands1, p->nClasses, p->nLits );
- if ( !fVeryVerbose )
- return;
- Abc_Print( 1, "Constants { " );
- Aig_ManForEachObj( p->pAig, pObj, i )
- if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) )
- Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
- Abc_Print( 1, "}\n" );
- Dch_ManForEachClass( p, ppClass, i )
- {
- Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
- Dch_ClassesPrintOne( p, ppClass[0] );
- }
- Abc_Print( 1, "\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates initial simulation classes.]
-
- Description [Assumes that simulation info is assigned.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
-{
- Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
- Aig_Obj_t * pObj, * pTemp, * pRepr;
- int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
-
- // allocate the hash table hashing simulation info into nodes
- nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
- ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
- ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
-
- // add all the nodes to the hash table
- nEntries = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
- {
- if ( fLatchCorr )
- {
- if ( !Aig_ObjIsPi(pObj) )
- continue;
- }
- else
- {
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
- continue;
- // skip the node with more that the given number of levels
- if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
- continue;
- }
- // check if the node belongs to the class of constant 1
- if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
- {
- Dch_ObjSetConst1Cand( p->pAig, pObj );
- p->nCands1++;
- continue;
- }
- // hash the node by its simulation info
- iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
- // add the node to the class
- if ( ppTable[iEntry] == NULL )
- ppTable[iEntry] = pObj;
- else
- {
- // set the representative of this node
- pRepr = ppTable[iEntry];
- Aig_ObjSetRepr( p->pAig, pObj, pRepr );
- // add node to the table
- if ( Dch_ObjNext( ppNexts, pRepr ) == NULL )
- { // this will be the second entry
- p->pClassSizes[pRepr->Id]++;
- nEntries++;
- }
- // add the entry to the list
- Dch_ObjSetNext( ppNexts, pObj, Dch_ObjNext( ppNexts, pRepr ) );
- Dch_ObjSetNext( ppNexts, pRepr, pObj );
- p->pClassSizes[pRepr->Id]++;
- nEntries++;
- }
- }
-
- // allocate room for classes
- p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
- p->pMemClassesFree = p->pMemClasses + nEntries;
-
- // copy the entries into storage in the topological order
- nEntries2 = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
- {
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
- continue;
- nNodes = p->pClassSizes[pObj->Id];
- // skip the nodes that are not representatives of non-trivial classes
- if ( nNodes == 0 )
- continue;
- assert( nNodes > 1 );
- // add the nodes to the class in the topological order
- ppClassNew = p->pMemClasses + nEntries2;
- ppClassNew[0] = pObj;
- for ( pTemp = Dch_ObjNext(ppNexts, pObj), k = 1; pTemp;
- pTemp = Dch_ObjNext(ppNexts, pTemp), k++ )
- {
- ppClassNew[nNodes-k] = pTemp;
- }
- // add the class of nodes
- p->pClassSizes[pObj->Id] = 0;
- Dch_ObjAddClass( p, pObj, ppClassNew, nNodes );
- // increment the number of entries
- nEntries2 += nNodes;
- }
- assert( nEntries == nEntries2 );
- ABC_FREE( ppTable );
- ABC_FREE( ppNexts );
- // now it is time to refine the classes
- Dch_ClassesRefine( p );
- Dch_ClassesCheck( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Iteratively refines the classes after simulation.]
-
- Description [Returns the number of refinements performed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
-{
- Aig_Obj_t ** pClassOld, ** pClassNew;
- Aig_Obj_t * pObj, * pReprNew;
- int i;
-
- // split the class
- Vec_PtrClear( p->vClassOld );
- Vec_PtrClear( p->vClassNew );
- Dch_ClassForEachNode( p, pReprOld, pObj, i )
- if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
- Vec_PtrPush( p->vClassOld, pObj );
- else
- Vec_PtrPush( p->vClassNew, pObj );
- // check if splitting happened
- if ( Vec_PtrSize(p->vClassNew) == 0 )
- return 0;
-
- // get the new representative
- pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
- assert( Vec_PtrSize(p->vClassOld) > 0 );
- assert( Vec_PtrSize(p->vClassNew) > 0 );
-
- // create old class
- pClassOld = Dch_ObjRemoveClass( p, pReprOld );
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
- {
- pClassOld[i] = pObj;
- Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
- }
- // create new class
- pClassNew = pClassOld + i;
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
- {
- pClassNew[i] = pObj;
- Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
- }
-
- // put classes back
- if ( Vec_PtrSize(p->vClassOld) > 1 )
- Dch_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
- if ( Vec_PtrSize(p->vClassNew) > 1 )
- Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
-
- // check if the class should be recursively refined
- if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
- return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Refines the classes after simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ClassesRefine( Dch_Cla_t * p )
-{
- Aig_Obj_t ** ppClass;
- int i, nRefis = 0;
- Dch_ManForEachClass( p, ppClass, i )
- nRefis += Dch_ClassesRefineOneClass( p, ppClass[0], 0 );
- return nRefis;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Returns equivalence class of the given node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots )
-{
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrClear( vRoots );
- Dch_ClassForEachNode( p, pRepr, pObj, i )
- Vec_PtrPush( vRoots, pObj );
- assert( Vec_PtrSize(vRoots) > 1 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns equivalence class of the given node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots )
-{
- int i, Limit;
- Vec_PtrClear( vRoots );
- Limit = ABC_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
- for ( i = pObj->Id; i < Limit; i++ )
- {
- pObj = Aig_ManObj( p->pAig, i );
- if ( pObj && Dch_ObjIsConst1Cand( p->pAig, pObj ) )
- Vec_PtrPush( vRoots, pObj );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Refine the group of constant 1 nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
-{
- Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
- int i;
- if ( Vec_PtrSize(vRoots) == 0 )
- return 0;
- // collect the nodes to be refined
- Vec_PtrClear( p->vClassNew );
- Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
- if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
- Vec_PtrPush( p->vClassNew, pObj );
- // check if there is a new class
- if ( Vec_PtrSize(p->vClassNew) == 0 )
- return 0;
- p->nCands1 -= Vec_PtrSize(p->vClassNew);
- pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
- Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
- if ( Vec_PtrSize(p->vClassNew) == 1 )
- return 1;
- // create a new class composed of these nodes
- ppClassNew = p->pMemClassesFree;
- p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
- {
- ppClassNew[i] = pObj;
- Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
- }
- Dch_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
- // refine them recursively
- if ( fRecursive )
- return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
- return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchCnf.c b/src/aig/dch/dchCnf.c
deleted file mode 100644
index 4175a123..00000000
--- a/src/aig/dch/dchCnf.c
+++ /dev/null
@@ -1,334 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchCnf.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Computation of CNF.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Addes clauses to the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
-{
- Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
- int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
-
- assert( !Aig_IsComplement( pNode ) );
- assert( Aig_ObjIsMuxType( pNode ) );
- // get nodes (I = if, T = then, E = else)
- pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
- // get the variable numbers
- VarF = Dch_ObjSatNum(p,pNode);
- VarI = Dch_ObjSatNum(p,pNodeI);
- VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT));
- VarE = Dch_ObjSatNum(p,Aig_Regular(pNodeE));
- // 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
- pLits[0] = toLitCond(VarI, 1);
- pLits[1] = toLitCond(VarT, 1^fCompT);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 1);
- pLits[1] = toLitCond(VarT, 0^fCompT);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 0);
- pLits[1] = toLitCond(VarE, 1^fCompE);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 0);
- pLits[1] = toLitCond(VarE, 0^fCompE);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
-
- // two additional clauses
- // t' & e' -> f'
- // t & e -> f
-
- // t + e + f'
- // t' + e' + f
-
- if ( VarT == VarE )
- {
-// assert( fCompT == !fCompE );
- return;
- }
-
- pLits[0] = toLitCond(VarT, 0^fCompT);
- pLits[1] = toLitCond(VarE, 0^fCompE);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarT, 1^fCompT);
- pLits[1] = toLitCond(VarE, 1^fCompE);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
-}
-
-/**Function*************************************************************
-
- Synopsis [Addes clauses to the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
-{
- Aig_Obj_t * pFanin;
- int * pLits, nLits, RetValue, i;
- assert( !Aig_IsComplement(pNode) );
- assert( Aig_ObjIsNode( pNode ) );
- // create storage for literals
- nLits = Vec_PtrSize(vSuper) + 1;
- pLits = ABC_ALLOC( int, nLits );
- // suppose AND-gate is A & B = C
- // add !A => !C or A + !C
- Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
- {
- pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
- pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- }
- // add A & B => C or !A + !B + C
- Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
- {
- pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
- }
- }
- pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
- assert( RetValue );
- ABC_FREE( pLits );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the supergate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
-{
- // if the new node is complemented or a PI, another gate begins
- if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ||
- (!fFirst && Aig_ObjRefs(pObj) > 1) ||
- (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
- {
- Vec_PtrPushUnique( vSuper, pObj );
- return;
- }
- // go through the branches
- Dch_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
- Dch_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the supergate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
-{
- assert( !Aig_IsComplement(pObj) );
- assert( !Aig_ObjIsPi(pObj) );
- Vec_PtrClear( vSuper );
- Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates the solver clause database.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( Dch_ObjSatNum(p,pObj) )
- return;
- assert( Dch_ObjSatNum(p,pObj) == 0 );
- if ( Aig_ObjIsConst1(pObj) )
- return;
- Vec_PtrPush( p->vUsedNodes, pObj );
- Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
- if ( Aig_ObjIsNode(pObj) )
- Vec_PtrPush( vFrontier, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates the solver clause database.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- Vec_Ptr_t * vFrontier;
- Aig_Obj_t * pNode, * pFanin;
- int i, k, fUseMuxes = 1;
- // quit if CNF is ready
- if ( Dch_ObjSatNum(p,pObj) )
- return;
- // start the frontier
- vFrontier = Vec_PtrAlloc( 100 );
- Dch_ObjAddToFrontier( p, pObj, vFrontier );
- // explore nodes in the frontier
- Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
- {
- // create the supergate
- assert( Dch_ObjSatNum(p,pNode) );
- if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
- {
- Vec_PtrClear( p->vFanins );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
- Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
- Dch_AddClausesMux( p, pNode );
- }
- else
- {
- Dch_CollectSuper( pNode, fUseMuxes, p->vFanins );
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
- Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
- Dch_AddClausesSuper( p, pNode, p->vFanins );
- }
- assert( Vec_PtrSize(p->vFanins) > 1 );
- }
- Vec_PtrFree( vFrontier );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
deleted file mode 100644
index bc78682b..00000000
--- a/src/aig/dch/dchCore.c
+++ /dev/null
@@ -1,158 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchCore.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [The core procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManSetDefaultParams( Dch_Pars_t * p )
-{
- memset( p, 0, sizeof(Dch_Pars_t) );
- p->nWords = 8; // the number of simulation words
- p->nBTLimit = 1000; // conflict limit at a node
- p->nSatVarMax = 5000; // the max number of SAT variables
- p->fSynthesis = 1; // derives three snapshots
- p->fPolarFlip = 1; // uses polarity adjustment
- p->fSimulateTfo = 1; // simulate TFO
- p->fPower = 0; // power-aware rewriting
- p->fLightSynth = 0; // uses lighter version of synthesis
- p->fVerbose = 0; // verbose stats
- p->nNodesAhead = 1000; // the lookahead in terms of nodes
- p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns verbose parameter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_ManReadVerbose( Dch_Pars_t * p )
-{
- return p->fVerbose;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs computation of AIGs with choices.]
-
- Description [Takes several AIGs and performs choicing.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
-{
- Dch_Man_t * p;
- Aig_Man_t * pResult;
- int clk, clkTotal = clock();
- // reset random numbers
- Aig_ManRandom(1);
- // start the choicing manager
- p = Dch_ManCreate( pAig, pPars );
- // compute candidate equivalence classes
-clk = clock();
- p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
-p->timeSimInit = clock() - clk;
-// Dch_ClassesPrint( p->ppClasses, 0 );
- p->nLits = Dch_ClassesLitNum( p->ppClasses );
- // perform SAT sweeping
- Dch_ManSweep( p );
- // free memory ahead of time
-p->timeTotal = clock() - clkTotal;
- Dch_ManStop( p );
- // create choices
- ABC_FREE( pAig->pTable );
- pResult = Dch_DeriveChoiceAig( pAig );
- // count the number of representatives
- if ( pPars->fVerbose )
- Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
- Dch_DeriveChoiceCountReprs( pAig ),
- Dch_DeriveChoiceCountEquivs( pResult ),
- Aig_ManChoiceNum( pResult ) );
- return pResult;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs computation of AIGs with choices.]
-
- Description [Takes several AIGs and performs choicing.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
-{
- Dch_Man_t * p;
- int clk, clkTotal = clock();
- // reset random numbers
- Aig_ManRandom(1);
- // start the choicing manager
- p = Dch_ManCreate( pAig, pPars );
- // compute candidate equivalence classes
-clk = clock();
- p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
-p->timeSimInit = clock() - clk;
-// Dch_ClassesPrint( p->ppClasses, 0 );
- p->nLits = Dch_ClassesLitNum( p->ppClasses );
- // perform SAT sweeping
- Dch_ManSweep( p );
- // free memory ahead of time
-p->timeTotal = clock() - clkTotal;
- Dch_ManStop( p );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
deleted file mode 100644
index 6072d97b..00000000
--- a/src/aig/dch/dchInt.h
+++ /dev/null
@@ -1,170 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchInt.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __DCH_INT_H__
-#define __DCH_INT_H__
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include "aig.h"
-#include "satSolver.h"
-#include "dch.h"
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-// equivalence classes
-typedef struct Dch_Cla_t_ Dch_Cla_t;
-
-// choicing manager
-typedef struct Dch_Man_t_ Dch_Man_t;
-struct Dch_Man_t_
-{
- // parameters
- Dch_Pars_t * pPars; // choicing parameters
- // AIGs used in the package
-// Vec_Ptr_t * vAigs; // user-given AIGs
- Aig_Man_t * pAigTotal; // intermediate AIG
- Aig_Man_t * pAigFraig; // final AIG
- // equivalence classes
- Dch_Cla_t * ppClasses; // equivalence classes of nodes
- Aig_Obj_t ** pReprsProved; // equivalences proved
- // SAT solving
- sat_solver * pSat; // recyclable SAT solver
- int nSatVars; // the counter of SAT variables
- int * pSatVars; // mapping of each node into its SAT var
- Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
- int nRecycles; // the number of times SAT solver was recycled
- int nCallsSince; // the number of calls since the last recycle
- Vec_Ptr_t * vFanins; // fanins of the CNF node
- Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
- Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
- // solver cone size
- int nConeThis;
- int nConeMax;
- // SAT calls statistics
- int nSatCalls; // the number of SAT calls
- int nSatProof; // the number of proofs
- int nSatFailsReal; // the number of timeouts
- int nSatCallsUnsat; // the number of unsat SAT calls
- int nSatCallsSat; // the number of sat SAT calls
- // choice node statistics
- int nLits; // the number of lits in the cand equiv classes
- int nReprs; // the number of proved equivalent pairs
- int nEquivs; // the number of final equivalences
- int nChoices; // the number of final choice nodes
- // runtime stats
- int timeSimInit; // simulation and class computation
- int timeSimSat; // simulation of the counter-examples
- int timeSat; // solving SAT
- int timeSatSat; // sat
- int timeSatUnsat; // unsat
- int timeSatUndec; // undecided
- int timeChoice; // choice computation
- int timeOther; // other runtime
- int timeTotal; // total runtime
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
-static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
-
-static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return (Aig_Obj_t *)pObj->pData; }
-static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
-static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
-}
-static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
- Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== dchAig.c ===================================================*/
-/*=== dchChoice.c ===================================================*/
-extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
-extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
-extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig );
-/*=== dchClass.c =================================================*/
-extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig );
-extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
- unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
- int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
- int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
-extern void Dch_ClassesStop( Dch_Cla_t * p );
-extern int Dch_ClassesLitNum( Dch_Cla_t * p );
-extern Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
-extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
-extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
-extern int Dch_ClassesRefine( Dch_Cla_t * p );
-extern int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
-extern void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots );
-extern void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots );
-extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
-/*=== dchCnf.c ===================================================*/
-extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
-/*=== dchMan.c ===================================================*/
-extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-extern void Dch_ManStop( Dch_Man_t * p );
-extern void Dch_ManSatSolverRecycle( Dch_Man_t * p );
-/*=== dchSat.c ===================================================*/
-extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
-/*=== dchSim.c ===================================================*/
-extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
-/*=== dchSimSat.c ===================================================*/
-extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
-extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
-/*=== dchSweep.c ===================================================*/
-extern void Dch_ManSweep( Dch_Man_t * p );
-
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
deleted file mode 100644
index dc856309..00000000
--- a/src/aig/dch/dchMan.c
+++ /dev/null
@@ -1,191 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchMan.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Calls to the SAT solver.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars )
-{
- Dch_Man_t * p;
- // create interpolation manager
- p = ABC_ALLOC( Dch_Man_t, 1 );
- memset( p, 0, sizeof(Dch_Man_t) );
- p->pPars = pPars;
- p->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs );
- Aig_ManFanoutStart( p->pAigTotal );
- // SAT solving
- p->nSatVars = 1;
- p->pSatVars = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
- p->vUsedNodes = Vec_PtrAlloc( 1000 );
- p->vFanins = Vec_PtrAlloc( 100 );
- p->vSimRoots = Vec_PtrAlloc( 1000 );
- p->vSimClasses = Vec_PtrAlloc( 1000 );
- // equivalences proved
- p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints stats of the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManPrintStats( Dch_Man_t * p )
-{
- int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3;
- Abc_Print( 1, "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n",
- p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax );
- Abc_Print( 1, "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n",
- Aig_ManNodeNum(p->pAigTotal),
- Aig_ManNodeNum(p->pAigTotal)-nNodeNum,
- nNodeNum,
- 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) );
- Abc_Print( 1, "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n",
- p->nSatVars, p->nConeMax, p->nRecycles );
- Abc_Print( 1, "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n",
- p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal,
- p->nSatCallsSat, p->nSatFailsReal );
- Abc_Print( 1, "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n",
- p->nLits, p->nReprs, p->nEquivs, p->nChoices );
- Abc_Print( 1, "Choicing runtime statistics:\n" );
- p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice;
- Abc_PrintTimeP( 1, "Sim init ", p->timeSimInit, p->timeTotal );
- Abc_PrintTimeP( 1, "Sim SAT ", p->timeSimSat, p->timeTotal );
- Abc_PrintTimeP( 1, "SAT solving", p->timeSat, p->timeTotal );
- Abc_PrintTimeP( 1, " sat ", p->timeSatSat, p->timeTotal );
- Abc_PrintTimeP( 1, " unsat ", p->timeSatUnsat, p->timeTotal );
- Abc_PrintTimeP( 1, " undecided", p->timeSatUndec, p->timeTotal );
- Abc_PrintTimeP( 1, "Choice ", p->timeChoice, p->timeTotal );
- Abc_PrintTimeP( 1, "Other ", p->timeOther, p->timeTotal );
- Abc_PrintTimeP( 1, "TOTAL ", p->timeTotal, p->timeTotal );
- if ( p->pPars->timeSynth )
- {
- Abc_PrintTime( 1, "Synthesis ", p->pPars->timeSynth );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Frees the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManStop( Dch_Man_t * p )
-{
- Aig_ManFanoutStop( p->pAigTotal );
- if ( p->pPars->fVerbose )
- Dch_ManPrintStats( p );
- if ( p->pAigFraig )
- Aig_ManStop( p->pAigFraig );
- if ( p->ppClasses )
- Dch_ClassesStop( p->ppClasses );
- if ( p->pSat )
- sat_solver_delete( p->pSat );
- Vec_PtrFree( p->vUsedNodes );
- Vec_PtrFree( p->vFanins );
- Vec_PtrFree( p->vSimRoots );
- Vec_PtrFree( p->vSimClasses );
- ABC_FREE( p->pReprsProved );
- ABC_FREE( p->pSatVars );
- ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Recycles the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManSatSolverRecycle( Dch_Man_t * p )
-{
- int Lit;
- if ( p->pSat )
- {
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i )
- Dch_ObjSetSatNum( p, pObj, 0 );
- Vec_PtrClear( p->vUsedNodes );
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
- sat_solver_delete( p->pSat );
- }
- p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 1000 );
- // var 0 is not used
- // var 1 is reserved for const1 node - add the clause
- p->nSatVars = 1;
-// p->nSatVars = 0;
- Lit = toLit( p->nSatVars );
- if ( p->pPars->fPolarFlip )
- Lit = lit_neg( Lit );
- sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );
-
- p->nRecycles++;
- p->nCallsSince = 0;
-}
-
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
deleted file mode 100644
index f5e346ef..00000000
--- a/src/aig/dch/dchSat.c
+++ /dev/null
@@ -1,166 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Calls to the SAT solver.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Runs equivalence test for the two nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
- int nBTLimit = p->pPars->nBTLimit;
- int pLits[2], RetValue, RetValue1, status, clk;
- p->nSatCalls++;
-
- // sanity checks
- assert( !Aig_IsComplement(pNew) );
- assert( !Aig_IsComplement(pOld) );
- assert( pNew != pOld );
-
- p->nCallsSince++; // experiment with this!!!
-
- // check if SAT solver needs recycling
- if ( p->pSat == NULL ||
- (p->pPars->nSatVarMax &&
- p->nSatVars > p->pPars->nSatVarMax &&
- p->nCallsSince > p->pPars->nCallsRecycle) )
- Dch_ManSatSolverRecycle( p );
-
- // if the nodes do not have SAT variables, allocate them
- Dch_CnfNodeAddToSolver( p, pOld );
- Dch_CnfNodeAddToSolver( p, pNew );
-
- // propage unit clauses
- if ( p->pSat->qtail != p->pSat->qhead )
- {
- status = sat_solver_simplify(p->pSat);
- assert( status != 0 );
- assert( p->pSat->qtail == p->pSat->qhead );
- }
-
- // solve under assumptions
- // A = 1; B = 0 OR A = 1; B = 1
- pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
- pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
- if ( p->pPars->fPolarFlip )
- {
- if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
- }
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
- if ( RetValue1 == l_False )
- {
-p->timeSatUnsat += clock() - clk;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- p->nSatCallsUnsat++;
- }
- else if ( RetValue1 == l_True )
- {
-p->timeSatSat += clock() - clk;
- p->nSatCallsSat++;
- return 0;
- }
- else // if ( RetValue1 == l_Undef )
- {
-p->timeSatUndec += clock() - clk;
- p->nSatFailsReal++;
- return -1;
- }
-
- // if the old node was constant 0, we already know the answer
- if ( pOld == Aig_ManConst1(p->pAigFraig) )
- {
- p->nSatProof++;
- return 1;
- }
-
- // solve under assumptions
- // A = 0; B = 1 OR A = 0; B = 0
- pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
- if ( p->pPars->fPolarFlip )
- {
- if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
- }
-clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
- (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
- if ( RetValue1 == l_False )
- {
-p->timeSatUnsat += clock() - clk;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- p->nSatCallsUnsat++;
- }
- else if ( RetValue1 == l_True )
- {
-p->timeSatSat += clock() - clk;
- p->nSatCallsSat++;
- return 0;
- }
- else // if ( RetValue1 == l_Undef )
- {
-p->timeSatUndec += clock() - clk;
- p->nSatFailsReal++;
- return -1;
- }
- // return SAT proof
- p->nSatProof++;
- return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
deleted file mode 100644
index b2d24761..00000000
--- a/src/aig/dch/dchSim.c
+++ /dev/null
@@ -1,297 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchSim.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Performs random simulation at the beginning.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj )
-{
- return (unsigned *)Vec_PtrEntry( vSims, pObj->Id );
-}
-static inline unsigned Dch_ObjRandomSim()
-{
- return Aig_ManRandom(0);
-}
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
-{
- return pObj->fPhase == pObj->fMarkB;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the nodes appear equal.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
- return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes hash value of the node using its simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned Dch_NodeHash( void * p, Aig_Obj_t * pObj )
-{
- Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
- static int s_FPrimes[128] = {
- 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
- 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
- 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
- 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
- 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
- 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
- 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
- 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
- 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
- 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
- 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
- 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
- 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
- };
- unsigned * pSim;
- unsigned uHash;
- int k, nWords;
- nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
- uHash = 0;
- pSim = Dch_ObjSim( vSims, pObj );
- if ( pObj->fPhase )
- {
- for ( k = 0; k < nWords; k++ )
- uHash ^= ~pSim[k] * s_FPrimes[k & 0x7F];
- }
- else
- {
- for ( k = 0; k < nWords; k++ )
- uHash ^= pSim[k] * s_FPrimes[k & 0x7F];
- }
- return uHash;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if simulation info is composed of all zeros.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodeIsConst( void * p, Aig_Obj_t * pObj )
-{
- Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
- unsigned * pSim;
- int k, nWords;
- nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
- pSim = Dch_ObjSim( vSims, pObj );
- if ( pObj->fPhase )
- {
- for ( k = 0; k < nWords; k++ )
- if ( ~pSim[k] )
- return 0;
- }
- else
- {
- for ( k = 0; k < nWords; k++ )
- if ( pSim[k] )
- return 0;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if simulation infos are equal.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodesAreEqual( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
- Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
- unsigned * pSim0, * pSim1;
- int k, nWords;
- nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
- pSim0 = Dch_ObjSim( vSims, pObj0 );
- pSim1 = Dch_ObjSim( vSims, pObj1 );
- if ( pObj0->fPhase != pObj1->fPhase )
- {
- for ( k = 0; k < nWords; k++ )
- if ( pSim0[k] != ~pSim1[k] )
- return 0;
- }
- else
- {
- for ( k = 0; k < nWords; k++ )
- if ( pSim0[k] != pSim1[k] )
- return 0;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Perform random simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims )
-{
- unsigned * pSim, * pSim0, * pSim1;
- Aig_Obj_t * pObj;
- int i, k, nWords;
- nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
-
- // assign const 1 sim info
- pObj = Aig_ManConst1(pAig);
- pSim = Dch_ObjSim( vSims, pObj );
- memset( pSim, 0xff, sizeof(unsigned) * nWords );
-
- // assign primary input random sim info
- Aig_ManForEachPi( pAig, pObj, i )
- {
- pSim = Dch_ObjSim( vSims, pObj );
- for ( k = 0; k < nWords; k++ )
- pSim[k] = Dch_ObjRandomSim();
- pSim[0] <<= 1;
- }
-
- // simulate AIG in the topological order
- Aig_ManForEachNode( pAig, pObj, i )
- {
- pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) );
- pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) );
- pSim = Dch_ObjSim( vSims, pObj );
-
- if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
- {
- for ( k = 0; k < nWords; k++ )
- pSim[k] = ~pSim0[k] & ~pSim1[k];
- }
- else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
- {
- for ( k = 0; k < nWords; k++ )
- pSim[k] = ~pSim0[k] & pSim1[k];
- }
- else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
- {
- for ( k = 0; k < nWords; k++ )
- pSim[k] = pSim0[k] & ~pSim1[k];
- }
- else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
- {
- for ( k = 0; k < nWords; k++ )
- pSim[k] = pSim0[k] & pSim1[k];
- }
- }
- // get simulation information for primary outputs
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives candidate equivalence classes of AIG nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose )
-{
- Dch_Cla_t * pClasses;
- Vec_Ptr_t * vSims;
- int i;
- // allocate simulation information
- vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
- // run random simulation from the primary inputs
- Dch_PerformRandomSimulation( pAig, vSims );
- // start storage for equivalence classes
- pClasses = Dch_ClassesStart( pAig );
- Dch_ClassesSetData( pClasses, vSims, Dch_NodeHash, Dch_NodeIsConst, Dch_NodesAreEqual );
- // hash nodes by sim info
- Dch_ClassesPrepare( pClasses, 0, 0 );
- // iterate random simulation
- for ( i = 0; i < 7; i++ )
- {
- Dch_PerformRandomSimulation( pAig, vSims );
- Dch_ClassesRefine( pClasses );
- }
- // clean up and return
- Vec_PtrFree( vSims );
- // prepare class refinement procedures
- Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
- return pClasses;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
deleted file mode 100644
index 325543d1..00000000
--- a/src/aig/dch/dchSimSat.c
+++ /dev/null
@@ -1,258 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchSimSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [Performs resimulation using counter-examples.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the reverse DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pFanout, * pRepr;
- int iFanout = -1, i;
- assert( !Aig_IsComplement(pObj) );
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- // traverse the fanouts
- Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
- Dch_ManCollectTfoCands_rec( p, pFanout );
- // check if the given node has a representative
- pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
- if ( pRepr == NULL )
- return;
- // pRepr is the constant 1 node
- if ( pRepr == Aig_ManConst1(p->pAigTotal) )
- {
- Vec_PtrPush( p->vSimRoots, pObj );
- return;
- }
- // pRepr is the representative of an equivalence class
- if ( pRepr->fMarkA )
- return;
- pRepr->fMarkA = 1;
- Vec_PtrPush( p->vSimClasses, pRepr );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collect equivalence classes and const1 cands in the TFO.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
-{
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrClear( p->vSimRoots );
- Vec_PtrClear( p->vSimClasses );
- Aig_ManIncrementTravId( p->pAigTotal );
- Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
- Dch_ManCollectTfoCands_rec( p, pObj1 );
- Dch_ManCollectTfoCands_rec( p, pObj2 );
- Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
- Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
- pObj->fMarkA = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the solved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- Aig_Obj_t * pObjFraig;
- int nVarNum;
- pObjFraig = Dch_ObjFraig( pObj );
- assert( !Aig_IsComplement(pObjFraig) );
- nVarNum = Dch_ObjSatNum( p, pObjFraig );
- // get the value from the SAT solver
- // (account for the fact that some vars may be minimized away)
- pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
-// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
- return;
- }
- Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
- Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
- // count the cone size
- if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
- p->nConeThis++;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the other nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- // set random value
- pObj->fMarkB = Aig_ManRandom(0) & 1;
- return;
- }
- Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
- Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pRoot, ** ppClass;
- int i, k, nSize, RetValue1, RetValue2, clk = clock();
- // get the equivalence classes
- Dch_ManCollectTfoCands( p, pObj, pRepr );
- // resimulate the cone of influence of the solved nodes
- p->nConeThis = 0;
- Aig_ManIncrementTravId( p->pAigTotal );
- Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
- Dch_ManResimulateSolved_rec( p, pObj );
- Dch_ManResimulateSolved_rec( p, pRepr );
- p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
- // resimulate the cone of influence of the other nodes
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
- Dch_ManResimulateOther_rec( p, pRoot );
- // refine these nodes
- RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
- // resimulate the cone of influence of the cand classes
- RetValue2 = 0;
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
- {
- ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
- for ( k = 0; k < nSize; k++ )
- Dch_ManResimulateOther_rec( p, ppClass[k] );
- // refine this class
- RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
- }
- // make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
- assert( RetValue1 );
- else
- assert( RetValue2 );
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pRoot;
- int i, RetValue, clk = clock();
- // get the equivalence class
- if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
- Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
- else
- Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
- // resimulate the cone of influence of the solved nodes
- p->nConeThis = 0;
- Aig_ManIncrementTravId( p->pAigTotal );
- Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
- Dch_ManResimulateSolved_rec( p, pObj );
- Dch_ManResimulateSolved_rec( p, pRepr );
- p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
- // resimulate the cone of influence of the other nodes
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
- Dch_ManResimulateOther_rec( p, pRoot );
- // refine this class
- if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
- RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
- else
- RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
- assert( RetValue );
-p->timeSimSat += clock() - clk;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c
deleted file mode 100644
index 4b054be2..00000000
--- a/src/aig/dch/dchSweep.c
+++ /dev/null
@@ -1,146 +0,0 @@
-/**CFile****************************************************************
-
- FileName [dchSweep.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Choice computation for tech-mapping.]
-
- Synopsis [One round of SAT sweeping.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 29, 2008.]
-
- Revision [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dchInt.h"
-#include "bar.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
-static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs fraiging for one node.]
-
- Description [Returns the fraiged node.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
- int RetValue;
- // get representative of this class
- pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj );
- if ( pObjRepr == NULL )
- return;
- // get the fraiged node
- pObjFraig = Dch_ObjFraig( pObj );
- if ( pObjFraig == NULL )
- return;
- // get the fraiged representative
- pObjReprFraig = Dch_ObjFraig( pObjRepr );
- if ( pObjReprFraig == NULL )
- return;
- // if the fraiged nodes are the same, return
- if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
- {
- // remember the proved equivalence
- p->pReprsProved[ pObj->Id ] = pObjRepr;
- return;
- }
- assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
- RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
- if ( RetValue == -1 ) // timed out
- {
- Dch_ObjSetFraig( pObj, NULL );
- return;
- }
- if ( RetValue == 1 ) // proved equivalent
- {
- pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
- Dch_ObjSetFraig( pObj, pObjFraig2 );
- // remember the proved equivalence
- p->pReprsProved[ pObj->Id ] = pObjRepr;
- return;
- }
- // disproved the equivalence
- if ( p->pPars->fSimulateTfo )
- Dch_ManResimulateCex( p, pObj, pObjRepr );
- else
- Dch_ManResimulateCex2( p, pObj, pObjRepr );
- assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs fraiging for the internal nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManSweep( Dch_Man_t * p )
-{
- Bar_Progress_t * pProgress = NULL;
- Aig_Obj_t * pObj, * pObjNew;
- int i;
- // map constants and PIs
- p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
- Aig_ManCleanData( p->pAigTotal );
- Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
- Aig_ManForEachPi( p->pAigTotal, pObj, i )
- pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
- // sweep internal nodes
- pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
- Aig_ManForEachNode( p->pAigTotal, pObj, i )
- {
- Bar_ProgressUpdate( pProgress, i, NULL );
- if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL ||
- Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
- continue;
- pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
- if ( pObjNew == NULL )
- continue;
- Dch_ObjSetFraig( pObj, pObjNew );
- Dch_ManSweepNode( p, pObj );
- }
- Bar_ProgressStop( pProgress );
- // update the representatives of the nodes (makes classes invalid)
- ABC_FREE( p->pAigTotal->pReprs );
- p->pAigTotal->pReprs = p->pReprsProved;
- p->pReprsProved = NULL;
- // clean the mark
- Aig_ManCleanMarkB( p->pAigTotal );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/dch/module.make b/src/aig/dch/module.make
deleted file mode 100644
index 5709f87a..00000000
--- a/src/aig/dch/module.make
+++ /dev/null
@@ -1,10 +0,0 @@
-SRC += src/aig/dch/dchAig.c \
- src/aig/dch/dchChoice.c \
- src/aig/dch/dchClass.c \
- src/aig/dch/dchCnf.c \
- src/aig/dch/dchCore.c \
- src/aig/dch/dchMan.c \
- src/aig/dch/dchSat.c \
- src/aig/dch/dchSim.c \
- src/aig/dch/dchSimSat.c \
- src/aig/dch/dchSweep.c
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-14 07:36:49 +0000