summaryrefslogtreecommitdiffstats
path: root/src/proof/fra/fraImp.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/fra/fraImp.c')
-rw-r--r--src/proof/fra/fraImp.c731
1 files changed, 731 insertions, 0 deletions
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
new file mode 100644
index 00000000..9877ceaa
--- /dev/null
+++ b/src/proof/fra/fraImp.c
@@ -0,0 +1,731 @@
+/**CFile****************************************************************
+
+ FileName [fraImp.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Detecting and proving implications.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in each siminfo of each node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
+{
+ unsigned * pSim;
+ int k, Counter = 0;
+ pSim = Fra_ObjSim( p, Node );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ Counter += Aig_WordCountOnes( pSim[k] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in each siminfo of each node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, * pnBits;
+ pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pnBits[i] = Fra_SmlCountOnesOne( p, i );
+ return pnBits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if implications holds.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
+{
+ unsigned * pSimL, * pSimR;
+ int k;
+ pSimL = Fra_ObjSim( p, Left );
+ pSimR = Fra_ObjSim( p, Right );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ if ( pSimL[k] & ~pSimR[k] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in the complement of the implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
+{
+ unsigned * pSimL, * pSimR;
+ int k, Counter = 0;
+ pSimL = Fra_ObjSim( p, Left );
+ pSimR = Fra_ObjSim( p, Right );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the complement of the implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
+{
+ unsigned * pSimL, * pSimR;
+ int k;
+ pSimL = Fra_ObjSim( p, Left );
+ pSimR = Fra_ObjSim( p, Right );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ pResult[k] |= pSimL[k] & ~pSimR[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes sorted by the number of 1s.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
+{
+ Aig_Obj_t * pObj;
+ Vec_Ptr_t * vNodes;
+ int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
+ assert( p->nWordsTotal > 0 );
+ // count 1s in each node's siminfo
+ pnBits = Fra_SmlCountOnes( p );
+ // count number of nodes having that many 1s
+ nNodes = 0;
+ nBits = p->nWordsTotal * 32;
+ pnNodes = ABC_ALLOC( int, nBits + 1 );
+ memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( i == 0 ) continue;
+ // skip non-PI and non-internal nodes
+ if ( fLatchCorr )
+ {
+ if ( !Aig_ObjIsPi(pObj) )
+ continue;
+ }
+ else
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ }
+ // skip nodes participating in the classes
+// if ( Fra_ClassObjRepr(pObj) )
+// continue;
+ assert( pnBits[i] <= nBits ); // "<" because of normalized info
+ pnNodes[pnBits[i]]++;
+ nNodes++;
+ }
+ // allocate memory for all the nodes
+ pMemory = ABC_ALLOC( int, nNodes + nBits + 1 );
+ // markup the memory for each node
+ vNodes = Vec_PtrAlloc( nBits + 1 );
+ Vec_PtrPush( vNodes, pMemory );
+ for ( i = 1; i <= nBits; i++ )
+ {
+ pMemory += pnNodes[i-1] + 1;
+ Vec_PtrPush( vNodes, pMemory );
+ }
+ // add the nodes
+ memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( i == 0 ) continue;
+ // skip non-PI and non-internal nodes
+ if ( fLatchCorr )
+ {
+ if ( !Aig_ObjIsPi(pObj) )
+ continue;
+ }
+ else
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ }
+ // skip nodes participating in the classes
+// if ( Fra_ClassObjRepr(pObj) )
+// continue;
+ pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] );
+ pMemory[ pnNodes[pnBits[i]]++ ] = i;
+ }
+ // add 0s in the end
+ nTotal = 0;
+ Vec_PtrForEachEntry( int *, vNodes, pMemory, i )
+ {
+ pMemory[ pnNodes[i]++ ] = 0;
+ nTotal += pnNodes[i];
+ }
+ assert( nTotal == nNodes + nBits + 1 );
+ ABC_FREE( pnNodes );
+ ABC_FREE( pnBits );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of implications with the highest cost.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
+{
+ Vec_Int_t * vImpsNew;
+ int * pCostCount, nImpCount, Imp, i, c;
+ assert( Vec_IntSize(vImps) >= nImpLimit );
+ // count how many implications have each cost
+ pCostCount = ABC_ALLOC( int, nCostMax + 1 );
+ memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
+ for ( i = 0; i < Vec_IntSize(vImps); i++ )
+ {
+ assert( pCosts[i] <= nCostMax );
+ pCostCount[ pCosts[i] ]++;
+ }
+ assert( pCostCount[0] == 0 );
+ // select the bound on the cost (above this bound, implication will be included)
+ nImpCount = 0;
+ for ( c = nCostMax; c > 0; c-- )
+ {
+ nImpCount += pCostCount[c];
+ if ( nImpCount >= nImpLimit )
+ break;
+ }
+// printf( "Cost range >= %d.\n", c );
+ // collect implications with the given costs
+ vImpsNew = Vec_IntAlloc( nImpLimit );
+ Vec_IntForEachEntry( vImps, Imp, i )
+ {
+ if ( pCosts[i] < c )
+ continue;
+ Vec_IntPush( vImpsNew, Imp );
+ if ( Vec_IntSize( vImpsNew ) == nImpLimit )
+ break;
+ }
+ ABC_FREE( pCostCount );
+ if ( pCostRange )
+ *pCostRange = c;
+ return vImpsNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares two implications using their largest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
+{
+ int Max1 = Abc_MaxInt( pImp1[0], pImp1[1] );
+ int Max2 = Abc_MaxInt( pImp2[0], pImp2[1] );
+ if ( Max1 < Max2 )
+ return -1;
+ if ( Max1 > Max2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives implication candidates.]
+
+ Description [Implication candidates have the property that
+ (1) they hold using sequential simulation information
+ (2) they do not hold using combinational simulation information
+ (3) they have as high expressive power as possible (heuristically)
+ that is, they are easy to disprove combinationally
+ meaning they cover relatively larger sequential subspace.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
+{
+ int nSimWords = 64;
+ Fra_Sml_t * pSeq, * pComb;
+ Vec_Int_t * vImps, * vTemp;
+ Vec_Ptr_t * vNodes;
+ int * pImpCosts, * pNodesI, * pNodesK;
+ int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
+ int CostMin = ABC_INFINITY, CostMax = 0;
+ int i, k, Imp, CostRange, clk = clock();
+ assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
+ assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
+ // normalize both managers
+ pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
+ // get the nodes sorted by the number of 1s
+ vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
+ // count the total number of implications
+ for ( k = nSimWords * 32; k > 0; k-- )
+ for ( i = k - 1; i > 0; i-- )
+ for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+ for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+ nImpsTotal++;
+
+ // compute implications and their costs
+ pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
+ vImps = Vec_IntAlloc( nImpMaxLimit );
+ for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
+ for ( i = k - 1; i > 0; i-- )
+ {
+ // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
+
+ for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+ for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+ {
+ nImpsTried++;
+ if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
+ {
+ nImpsNonSeq++;
+ continue;
+ }
+ if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
+ {
+ nImpsComb++;
+ continue;
+ }
+ nImpsCollected++;
+ Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
+ pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
+ CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
+ CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
+ Vec_IntPush( vImps, Imp );
+ if ( Vec_IntSize(vImps) == nImpMaxLimit )
+ goto finish;
+ }
+ }
+finish:
+ Fra_SmlStop( pComb );
+ Fra_SmlStop( pSeq );
+
+ // select implications with the highest cost
+ CostRange = CostMin;
+ if ( Vec_IntSize(vImps) > nImpUseLimit )
+ {
+ vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
+ Vec_IntFree( vTemp );
+ }
+
+ // dealloc
+ ABC_FREE( pImpCosts );
+ {
+ void * pTemp = Vec_PtrEntry(vNodes, 0);
+ ABC_FREE( pTemp );
+ }
+ Vec_PtrFree( vNodes );
+ // reorder implications topologically
+ qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int),
+ (int (*)(const void *, const void *)) Sml_CompareMaxId );
+if ( p->pPars->fVerbose )
+{
+printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
+ nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
+printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
+ CostMin, CostRange, CostMax );
+ABC_PRT( "Time", clock() - clk );
+}
+ return vImps;
+}
+
+
+// the following three procedures are called to
+// - add implications to the SAT solver
+// - check implications using the SAT solver
+// - refine implications using after a cex is generated
+
+/**Function*************************************************************
+
+ Synopsis [Add implication clauses to the SAT solver.]
+
+ Description [Note that implications should be checked in the first frame!]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
+{
+ sat_solver * pSat = p->pSat;
+ Aig_Obj_t * pLeft, * pRight;
+ Aig_Obj_t * pLeftF, * pRightF;
+ int pLits[2], Imp, Left, Right, i, f, status;
+ int fComplL, fComplR;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ {
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
+ // check if all the nodes are present
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // map these info fraig
+ pLeftF = Fra_ObjFraig( pLeft, f );
+ pRightF = Fra_ObjFraig( pRight, f );
+ if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
+ {
+ Vec_IntWriteEntry( vImps, i, 0 );
+ break;
+ }
+ }
+ if ( f < p->pPars->nFramesK )
+ continue;
+ // add constraints in each timeframe
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // map these info fraig
+ pLeftF = Fra_ObjFraig( pLeft, f );
+ pRightF = Fra_ObjFraig( pRight, f );
+ // get the corresponding SAT numbers
+ Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
+ Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
+ assert( Left > 0 && Left < p->nSatVars );
+ assert( Right > 0 && Right < p->nSatVars );
+ // get the complemented attributes
+ fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
+ fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
+ // get the constraint
+ // L => R L' v R (complement = L & R')
+ pLits[0] = 2 * Left + !fComplL;
+ pLits[1] = 2 * Right + fComplR;
+ // add constraint to solver
+ if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ p->pSat = NULL;
+ return;
+ }
+ }
+ }
+ status = sat_solver_simplify(pSat);
+ if ( status == 0 )
+ {
+ sat_solver_delete( pSat );
+ p->pSat = NULL;
+ }
+// printf( "Total imps = %d. ", Vec_IntSize(vImps) );
+ Fra_ImpCompactArray( vImps );
+// printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check implications for the node (if they are present).]
+
+ Description [Returns the new position in the array.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
+{
+ Aig_Obj_t * pLeft, * pRight;
+ Aig_Obj_t * pLeftF, * pRightF;
+ int i, Imp, Left, Right, Max, RetValue;
+ int fComplL, fComplR;
+ Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
+ {
+ if ( Imp == 0 )
+ continue;
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ Max = Abc_MaxInt( Left, Right );
+ assert( Max >= pNode->Id );
+ if ( Max > pNode->Id )
+ return i;
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Left );
+ pRight = Aig_ManObj( p->pManAig, Right );
+ // get the corresponding FRAIG nodes
+ pLeftF = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
+ pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
+ // get the complemented attributes
+ fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
+ fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
+ // check equality
+ if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
+ {
+ if ( fComplL == fComplR ) // x => x - always true
+ continue;
+ assert( fComplL != fComplR );
+ // consider 4 possibilities:
+ // NOT(1) => 1 or 0 => 1 - always true
+ // 1 => NOT(1) or 1 => 0 - never true
+ // NOT(x) => x or x - not always true
+ // x => NOT(x) or NOT(x) - not always true
+ if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
+ continue;
+ // disproved implication
+ p->pCla->fRefinement = 1;
+ Vec_IntWriteEntry( vImps, i, 0 );
+ continue;
+ }
+ // check the implication
+ // - if true, a clause is added
+ // - if false, a cex is simulated
+ // make sure the implication is refined
+ RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
+ if ( RetValue != 1 )
+ {
+ p->pCla->fRefinement = 1;
+ if ( RetValue == 0 )
+ Fra_SmlResimulate( p );
+ if ( Vec_IntEntry(vImps, i) != 0 )
+ printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
+ assert( Vec_IntEntry(vImps, i) == 0 );
+ }
+ }
+ return i;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes those implications that no longer hold.]
+
+ Description [Returns 1 if refinement has happened.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
+{
+ Aig_Obj_t * pLeft, * pRight;
+ int Imp, i, RetValue = 0;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ {
+ if ( Imp == 0 )
+ continue;
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
+ // check if implication holds using this simulation info
+ if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
+ {
+ Vec_IntWriteEntry( vImps, i, 0 );
+ RetValue = 1;
+ }
+ }
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes empty implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpCompactArray( Vec_Int_t * vImps )
+{
+ int i, k, Imp;
+ k = 0;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ if ( Imp )
+ Vec_IntWriteEntry( vImps, k++, Imp );
+ Vec_IntShrink( vImps, k );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Determines the ratio of the state space by computed implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
+{
+ int nSimWords = 64;
+ Fra_Sml_t * pComb;
+ unsigned * pResult;
+ double Ratio = 0.0;
+ int Left, Right, Imp, i;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return Ratio;
+ // simulate the AIG manager with combinational patterns
+ pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+ // go through the implications and collect where they do not hold
+ pResult = Fra_ObjSim( pComb, 0 );
+ assert( pResult[0] == 0 );
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
+ }
+ // count the number of ones in this area
+ Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
+ Fra_SmlStop( pComb );
+ return Ratio;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of failed implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
+{
+ int nFrames = 2000;
+ int nSimWords = 8;
+ Fra_Sml_t * pSeq;
+ char * pfFails;
+ int Left, Right, Imp, i, Counter;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return 0;
+ // simulate the AIG manager with combinational patterns
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1 );
+ // go through the implications and check how many of them do not hold
+ pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
+ memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
+ }
+ // count how many has failed
+ Counter = 0;
+ for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
+ Counter += pfFails[i];
+ ABC_FREE( pfFails );
+ Fra_SmlStop( pSeq );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Record proven implications in the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
+{
+ Aig_Obj_t * pLeft, * pRight, * pMiter;
+ int nPosOld, Imp, i;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return;
+ // go through the implication
+ nPosOld = Aig_ManPoNum(pNew);
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
+ // record the implication: L' + R
+ pMiter = Aig_Or( pNew,
+ Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase),
+ Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:56:44 +0000