summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw_old/sswAig.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw_old/sswAig.c')
-rw-r--r--src/aig/ssw_old/sswAig.c205
1 files changed, 0 insertions, 205 deletions
diff --git a/src/aig/ssw_old/sswAig.c b/src/aig/ssw_old/sswAig.c
deleted file mode 100644
index 7b6d1bb0..00000000
--- a/src/aig/ssw_old/sswAig.c
+++ /dev/null
@@ -1,205 +0,0 @@
-/**CFile****************************************************************
-
- FileName [sswAig.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Inductive prover with constraints.]
-
- Synopsis [AIG manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - September 1, 2008.]
-
- Revision [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sswInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs speculative reduction for one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame, int fTwoPos )
-{
- Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
- // skip nodes without representative
- pObjRepr = Aig_ObjRepr(pAig, pObj);
- if ( pObjRepr == NULL )
- return;
- p->nConstrTotal++;
- assert( pObjRepr->Id < pObj->Id );
- // get the new node
- pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
- // get the new node of the representative
- pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
- // if this is the same node, no need to add constraints
- if ( pObj->fPhase == pObjRepr->fPhase )
- {
- assert( pObjNew != Aig_Not(pObjReprNew) );
- if ( pObjNew == pObjReprNew )
- return;
- }
- else
- {
- assert( pObjNew != pObjReprNew );
- if ( pObjNew == Aig_Not(pObjReprNew) )
- return;
- }
- p->nConstrReduced++;
- // these are different nodes - perform speculative reduction
- pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
- // set the new node
- Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
- // add the constraint
- if ( fTwoPos )
- {
- Aig_ObjCreatePo( pFrames, pObjNew2 );
- Aig_ObjCreatePo( pFrames, pObjNew );
- }
- else
- {
- pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
- Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Prepares the inductive case with speculative reduction.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
-{
- Aig_Man_t * pFrames;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
- int i, f;
- assert( p->pFrames == NULL );
- assert( Aig_ManRegNum(p->pAig) > 0 );
- assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
- p->nConstrTotal = p->nConstrReduced = 0;
-
- // start the fraig package
- pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
- // create latches for the first frame
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
- // add timeframes
- for ( f = 0; f < p->pPars->nFramesK; f++ )
- {
- // map constants and PIs
- Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
- Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
- // set the constraints on the latch outputs
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
- // add internal nodes of this frame
- Aig_ManForEachNode( p->pAig, pObj, i )
- {
- pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
- }
- // transfer latch input to the latch outputs
- Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
- }
- // add the POs for the latch outputs of the last frame
-// Saig_ManForEachLo( p->pAig, pObj, i )
-// Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
- for ( f = 0; f <= p->pPars->nFramesK; f++ )
- Saig_ManForEachLo( p->pAig, pObj, i )
- Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, f ) );
-
- // remove dangling nodes
- Aig_ManCleanup( pFrames );
- // make sure the satisfying assignment is node assigned
- assert( pFrames->pData == NULL );
-//Aig_ManShow( pFrames, 0, NULL );
- return pFrames;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Prepares the inductive case with speculative reduction.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
-{
- Aig_Man_t * pFrames;
- Aig_Obj_t * pObj, * pObjNew;
- int i;
- assert( p->pFrames == NULL );
- assert( Aig_ManRegNum(p->pAig) > 0 );
- assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
- p->nConstrTotal = p->nConstrReduced = 0;
-
- // start the fraig package
- pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
- // map constants and PIs
- Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
- Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
- // create latches for the first frame
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
- // set the constraints on the latch outputs
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
- // add internal nodes of this frame
- Aig_ManForEachNode( p->pAig, pObj, i )
- {
- pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
- Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
- Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
- }
- // add the POs for the latch outputs of the last frame
- Saig_ManForEachLi( p->pAig, pObj, i )
- Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
- // remove dangling nodes
- Aig_ManCleanup( pFrames );
- Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
- printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
- p->nConstrTotal, p->nConstrReduced );
- return pFrames;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 02:15:30 +0000