summaryrefslogtreecommitdiffstats
path: root/src/aig/fra/fraCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra/fraCore.c')
-rw-r--r--src/aig/fra/fraCore.c132
1 files changed, 54 insertions, 78 deletions
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index ca2d0fb4..977396dd 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -39,24 +39,24 @@
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
+Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObj )
{
- Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+ Aig_Obj_t * pObjRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjReprFraig;
int RetValue;
- assert( !Aig_IsComplement(pObjOld) );
- assert( Aig_ObjIsNode(pObjOld) );
+ assert( !Aig_IsComplement(pObj) );
+ assert( Aig_ObjIsNode(pObj) );
// get the fraiged fanins
- pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
- pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
+ pFanin0Fraig = Fra_ObjChild0Fra(pObj,0);
+ pFanin1Fraig = Fra_ObjChild1Fra(pObj,0);
// get the fraiged node
pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
return pObjFraig;
Aig_Regular(pObjFraig)->pData = p;
// get representative of this class
- pObjOldRepr = Fra_ObjRepr(pObjOld);
- if ( pObjOldRepr == NULL || // this is a unique node
- (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
+ pObjRepr = Fra_ClassObjRepr(pObj);
+ if ( pObjRepr == NULL || // this is a unique node
+ (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
{
assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
@@ -64,58 +64,38 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
return pObjFraig;
}
// get the fraiged representative
- pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
+ pObjReprFraig = Fra_ObjFraig(pObjRepr,0);
// if the fraiged nodes are the same, return
- if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
+ if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return pObjFraig;
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
-// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
+// printf( "Node = %d. Repr = %d.\n", pObj->Id, pObjRepr->Id );
// if they are proved different, the c-ex will be in p->pPatWords
- RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
+ RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
-// pObjOld->fMarkA = 1;
- if ( p->pPars->fChoicing && !Fra_CheckTfi( p, Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) ) )
- {
-// Fra_ObjSetReprFra( Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) );
- Aig_Obj_t * pObjNew = Aig_Regular(pObjFraig);
- Aig_Obj_t * pObjOld = Aig_Regular(pObjOldReprFraig);
- Aig_Obj_t * pTemp;
- assert( pObjNew != pObjOld );
- for ( pTemp = Fra_ObjReprFra(pObjOld); pTemp; pTemp = Fra_ObjReprFra(pTemp) )
- if ( pTemp == pObjNew )
- break;
- if ( pTemp == NULL )
- {
- Fra_ObjSetReprFra( pObjNew, Fra_ObjReprFra(pObjOld) );
- Fra_ObjSetReprFra( pObjOld, pObjNew );
- assert( pObjOld != Fra_ObjReprFra(pObjOld) );
- assert( pObjNew != Fra_ObjReprFra(pObjNew) );
- p->nChoices++;
-
- assert( pObjOld->Id < pObjNew->Id );
- }
- else
- p->nChoicesFake++;
- }
- return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+// pObj->fMarkA = 1;
+// if ( p->pPars->fChoicing )
+// Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+ return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
}
if ( RetValue == -1 ) // failed
{
static int Counter = 0;
char FileName[20];
Aig_Man_t * pTemp;
- Aig_Obj_t * pObj;
+ Aig_Obj_t * pNode;
int i;
- Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
+ Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) };
// Vec_Ptr_t * vNodes;
+ Vec_PtrPush( p->vTimeouts, pObj );
if ( !p->pPars->fSpeculate )
return pObjFraig;
// substitute the node
-// pObjOld->fMarkB = 1;
+// pObj->fMarkB = 1;
p->nSpeculs++;
pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
@@ -124,21 +104,18 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
Aig_ManStop( pTemp );
- Aig_ManForEachObj( p->pManFraig, pObj, i )
- pObj->pData = p;
+ Aig_ManForEachObj( p->pManFraig, pNode, i )
+ pNode->pData = p;
// vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
// printf( "Cone=%d ", Vec_PtrSize(vNodes) );
// Vec_PtrFree( vNodes );
- return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+ return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
}
-// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
// simulate the counter-example and return the Fraig node
-// printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
Fra_Resimulate( p );
-// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
- assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
+ assert( Fra_ClassObjRepr(pObj) != pObjRepr );
return pObjFraig;
}
@@ -153,13 +130,13 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
SeeAlso []
***********************************************************************/
-void Fra_Sweep( Fra_Man_t * p )
+void Fra_FraigSweep( Fra_Man_t * p )
{
ProgressBar * pProgress;
Aig_Obj_t * pObj, * pObjNew;
int i, k = 0;
-p->nClassesZero = Vec_PtrSize(p->vClasses1);
-p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
+p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
+p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
// duplicate internal nodes
pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
Aig_ManForEachNode( p->pManAig, pObj, i )
@@ -167,36 +144,18 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0
Extra_ProgressBarUpdate( pProgress, i, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
- pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+ pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,0), Fra_ObjChild1Fra(pObj,0) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
- Fra_ObjSetFraig( pObj, pObjNew );
- assert( Fra_ObjFraig(pObj) != NULL );
+ Fra_ObjSetFraig( pObj, 0, pObjNew );
}
Extra_ProgressBarStop( pProgress );
-p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
+p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
// try to prove the outputs of the miter
p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
// Fra_MiterProve( p );
- // add the POs
- Aig_ManForEachPo( p->pManAig, pObj, i )
- Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
- // postprocess
- Aig_ManCleanMarkB( p->pManFraig );
- if ( p->pPars->fChoicing )
- {
- // transfer the representative info
- p->pManFraig->pReprs = p->pMemReprFra;
- p->pMemReprFra = NULL;
-// printf( "The number of choices = %d. Fake choices = %d.\n", p->nChoices, p->nChoicesFake );
- }
- else
- {
- // remove dangling nodes
- Aig_ManCleanup( p->pManFraig );
- }
}
/**Function*************************************************************
@@ -210,7 +169,7 @@ p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0)
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
+Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Aig_Man_t * pManAigNew;
@@ -220,9 +179,26 @@ Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
clk = clock();
assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
- Fra_Simulate( p );
- Fra_Sweep( p );
- pManAigNew = p->pManFraig;
+ p->pManFraig = Fra_ManPrepareComb( p );
+ Fra_Simulate( p, 0 );
+ if ( p->pPars->fChoicing )
+ Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
+ Fra_FraigSweep( p );
+ Fra_ManFinalizeComb( p );
+ if ( p->pPars->fChoicing )
+ {
+ Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
+ pManAigNew = Aig_ManDupRepr( p->pManAig );
+ Aig_ManCreateChoices( pManAigNew );
+ Aig_ManStop( p->pManFraig );
+ p->pManFraig = NULL;
+ }
+ else
+ {
+ Aig_ManCleanup( p->pManFraig );
+ pManAigNew = p->pManFraig;
+ p->pManFraig = NULL;
+ }
p->timeTotal = clock() - clk;
Fra_ManStop( p );
return pManAigNew;
@@ -239,7 +215,7 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
@@ -249,7 +225,7 @@ Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig )
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 1;
- return Fra_Perform( pManAig, pPars );
+ return Fra_FraigPerform( pManAig, pPars );
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 05:44:03 +0000