summaryrefslogtreecommitdiffstats
path: root/src/aig/fra/fraInd.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra/fraInd.c')
-rw-r--r--src/aig/fra/fraInd.c135
1 files changed, 85 insertions, 50 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 1bfe1cb4..71e535f7 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -31,6 +31,42 @@
/**Function*************************************************************
+ Synopsis [Performs speculative reduction for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
+{
+ Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+ // skip nodes without representative
+ if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+ return;
+ assert( pObjRepr->Id < pObj->Id );
+ // get the new node
+ pObjNew = Fra_ObjFraig( pObj, iFrame );
+ // get the new node of the representative
+ pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
+ // if this is the same node, no need to add constraints
+ if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+ return;
+ // these are different nodes - perform speculative reduction
+ pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+ // set the new node
+ Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
+ // add the constraint
+ pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+ pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+ pMiter = Aig_Not( pMiter );
+ Aig_ObjCreatePo( pManFraig, pMiter );
+}
+
+/**Function*************************************************************
+
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
@@ -43,77 +79,58 @@
Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
{
Aig_Man_t * pManFraig;
- Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter;
+ Aig_Obj_t * pObj, * pObjNew;
Aig_Obj_t ** pLatches;
int i, k, f;
assert( p->pManFraig == NULL );
- assert( Aig_ManInitNum(p->pManAig) > 0 );
- assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+ assert( Aig_ManRegNum(p->pManAig) > 0 );
+ assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// start the fraig package
- pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames );
- pManFraig->vInits = Vec_IntDup(p->pManAig->vInits);
+ pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
+ pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames
- for ( f = 0; f < p->nFrames; f++ )
- {
+ for ( f = 0; f < p->nFramesAll; f++ )
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
+ for ( f = 0; f < p->nFramesAll; f++ )
Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
- }
// create latches for the first frame
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// add timeframes
- pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) );
- for ( f = 0; f < p->nFrames - 1; f++ )
+ pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
+ for ( f = 0; f < p->nFramesAll - 1; f++ )
{
+ // set the constraints on the latch outputs
+ Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+ Fra_FramesConstrainNode( pManFraig, pObj, f );
// add internal nodes of this frame
Aig_ManForEachNode( p->pManAig, pObj, i )
{
pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
Fra_ObjSetFraig( pObj, f, pObjNew );
- // skip nodes without representative
- if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
- continue;
- assert( pObjRepr->Id < pObj->Id );
- // get the new node of the representative
- pObjReprNew = Fra_ObjFraig( pObjRepr, f );
- // if this is the same node, no need to add constraints
- if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
- continue;
- // these are different nodes
- // perform speculative reduction
- Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) );
- // add the constraint
- pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
- pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
- Aig_ObjCreatePo( pManFraig, pMiter );
+ Fra_FramesConstrainNode( pManFraig, pObj, f );
}
// save the latch input values
k = 0;
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
- assert( k == Aig_ManInitNum(p->pManAig) );
+ assert( k == Aig_ManRegNum(p->pManAig) );
// insert them to the latch output values
k = 0;
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
- assert( k == Aig_ManInitNum(p->pManAig) );
+ assert( k == Aig_ManRegNum(p->pManAig) );
}
free( pLatches );
// mark the asserts
pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
// add the POs for the latch inputs
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
- Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) );
-
- // set the pointer to the manager
- Aig_ManForEachObj( p->pManAig, pObj, i )
- pObj->pData = p;
- // set the pointers to the manager
- Aig_ManForEachObj( pManFraig, pObj, i )
- pObj->pData = p;
+ Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
return pManFraig;
@@ -130,7 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose )
{
Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars;
@@ -142,20 +159,23 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig, 1);
assert( Aig_ManLatchNum(pManAig) == 0 );
- assert( Aig_ManInitNum(pManAig) > 0 );
+ assert( Aig_ManRegNum(pManAig) > 0 );
+ assert( nFramesK > 0 );
// get parameters
Fra_ParamsDefaultSeq( pPars );
- pPars->nTimeFrames = nFrames;
+ pPars->nFramesK = nFramesK;
pPars->fVerbose = fVerbose;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using the 1st init frame
Fra_Simulate( p, 1 );
+// Fra_ClassesTest( p->pCla, 2, 3 );
+//Aig_ManShow( pManAig, 0, NULL );
// refine e-classes using sequential simulation
-
+
// iterate the inductive case
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -165,18 +185,32 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
// derive non-init K-timeframes while implementing e-classes
p->pManFraig = Fra_FramesWithClasses( p );
if ( fVerbose )
- printf( "Iter = %3d. Original = %6d. Reduced = %6d.\n",
- nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
-
+ {
+ printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n",
+ nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
+ Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
+ Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
+ }
// perform AIG rewriting on the speculated frames
// convert the manager to SAT solver (the last nLatches outputs are inputs)
- pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) );
+// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+ pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+
p->pSat = Cnf_DataWriteIntoSolver( pCnf );
- // transfer variable numbers
- Aig_ManForEachPi( p->pManAig, pObj, i )
+ p->nSatVars = pCnf->nVars;
+
+ // set the pointers to the manager
+ Aig_ManForEachObj( p->pManFraig, pObj, i )
+ pObj->pData = p;
+ // transfer PI/LO variable numbers
+ pObj = Aig_ManConst1( p->pManFraig );
+ Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+ Aig_ManForEachPi( p->pManFraig, pObj, i )
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
- Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+ // transfer LI variable numbers
+ Aig_ManForEachLiSeq( p->pManFraig, pObj, i )
{
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Fra_ObjSetFaninVec( pObj, (void *)1 );
@@ -185,9 +219,10 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
// perform sweeping
Fra_FraigSweep( p );
- assert( Vec_PtrSize(p->vTimeouts) == 0 );
- Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
- sat_solver_delete( p->pSat ); p->pSat = NULL;
+ assert( p->vTimeouts == NULL );
+
+ // cleanup
+ Fra_ManClean( p );
}
// move the classes into representatives
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 11:08:38 +0000