Version abc70930

1 files changed, 0 insertions, 428 deletions

diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
deleted file mode 100644
index b390edbe..00000000
--- a/src/aig/fra/fraCore.c
+++ /dev/null
@@ -1,428 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-/* 
-    Speculating reduction in the sequential case leads to an interesting 
-    situation when a counter-ex may not refine any classes. This happens
-    for non-constant equivalence classes. In such cases the representative
-    of the class (proved by simulation to be non-constant) may be reduced 
-    to a constant during the speculative reduction. The fraig-representative 
-    of this representative node is a constant node, even though this is a 
-    non-constant class. Experiments have shown that this situation happens 
-    very often at the beginning of the refinement iteration when there are 
-    many spurious candidate equivalence classes (especially if heavy-duty 
-    simulatation of BMC was node used at the beginning). As a result, the 
-    SAT solver run may return a counter-ex that  distinguishes the given 
-    representative node from the constant-1 node but this counter-ex
-    does not distinguish the nodes in the non-costant class... This is why 
-    there is no check of refinment after a counter-ex in the sequential case.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Reports the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_FraigMiterStatus( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
-    if ( p->pData )
-        return 0;
-    Aig_ManForEachPoSeq( p, pObj, i )
-    {
-        pObjNew = Aig_ObjChild0(pObj);
-        // check if the output is constant 0
-        if ( pObjNew == Aig_ManConst0(p) )
-        {
-            CountConst0++;
-            continue;
-        }
-        // check if the output is constant 1
-        if ( pObjNew == Aig_ManConst1(p) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        // check if the output can be constant 0
-        if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        CountUndecided++;
-    }
-/*
-    if ( p->pParams->fVerbose )
-    {
-        printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
-        printf( "Const0 = %d.  ", CountConst0 );
-        printf( "NonConst0 = %d.  ", CountNonConst0 );
-        printf( "Undecided = %d.  ", CountUndecided );
-        printf( "\n" );
-    }
-*/
-    if ( CountNonConst0 )
-        return 0;
-    if ( CountUndecided )
-        return -1;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Write speculative miter for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
-{ 
-    static int Counter = 0;
-    char FileName[20];
-    Aig_Man_t * pTemp;
-    Aig_Obj_t * pNode;
-    int i;
-    // create manager with the logic for these two nodes
-    pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
-    // dump the logic into a file
-    sprintf( FileName, "aig\\%03d.blif", ++Counter );
-    Aig_ManDumpBlif( pTemp, FileName );
-    printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
-    // clean up
-    Aig_ManStop( pTemp );
-    Aig_ManForEachObj( p->pManFraig, pNode, i )
-        pNode->pData = p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies the generated counter-ex.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, c;
-    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
-    // make sure the input pattern is not used
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        assert( !pObj->fMarkB );
-    // simulate the cex through the AIG
-    Aig_ManConst1(p->pManAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        pObj->fMarkB = Vec_IntEntry(vCex, i);
-    Aig_ManForEachNode( p->pManAig, pObj, i )
-        pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
-                       (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
-    // check if the classes hold
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
-    {
-        if ( pObj->fPhase != pObj->fMarkB )
-            printf( "The node %d is not constant under cex!\n", pObj->Id );
-    }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
-    {
-        for ( c = 1; ppClass[c]; c++ )
-            if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
-                printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
-//        for ( c = 0; ppClass[c]; c++ )
-//            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
-//                printf( "A member of non-constant class has a constant repr!\n" );
-    }
-    // clean the simulation pattern
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        pObj->fMarkB = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for one node.]
-
-  Description [Returns the fraiged node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
-{ 
-    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
-    int RetValue;
-    assert( !Aig_IsComplement(pObj) );
-    // get representative of this class
-    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
-        return;
-    // get the fraiged node
-    pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK );
-    // get the fraiged representative
-    pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
-    // if the fraiged nodes are the same, return
-    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-    {
-        p->nSatCallsSkipped++;
-        return;
-    }
-    assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
-    // if they are proved different, the c-ex will be in p->pPatWords
-    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-    if ( RetValue == 1 )  // proved equivalent
-    {
-//        if ( p->pPars->fChoicing )
-//            Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-        // the nodes proved equal
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
-        return;
-    }
-    if ( RetValue == -1 ) // failed
-    {
-        if ( p->vTimeouts == NULL )
-            p->vTimeouts = Vec_PtrAlloc( 100 );
-        Vec_PtrPush( p->vTimeouts, pObj );
-        if ( !p->pPars->fSpeculate )
-            return;
-        assert( 0 );
-        // speculate
-        p->nSpeculs++;
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
-        Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
-        return;
-    }
-    // disprove the nodes
-    p->pCla->fRefinement = 1;
-    // if we do not include the node into those disproved, we may end up 
-    // merging this node with another representative, for which proof has timed out
-    if ( p->vTimeouts )
-        Vec_PtrPush( p->vTimeouts, pObj );
-    // verify that the counter-example satisfies all the constraints
-//    if ( p->vCex )
-//        Fra_FraigVerifyCounterEx( p, p->vCex );
-    // simulate the counter-example and return the Fraig node
-    Fra_SmlResimulate( p );
-    if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
-        printf( "Fra_FraigNode(): Error in class refinement!\n" );
-    assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for the internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigSweep( Fra_Man_t * p )
-{
-    Bar_Progress_t * pProgress;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, k = 0, Pos = 0;
-    // fraig latch outputs
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-    {
-        Fra_FraigNode( p, pObj );
-        if ( p->pPars->fUseImps )
-            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
-    }
-    if ( p->pPars->fLatchCorr )
-        return;
-    // fraig internal nodes
-    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
-    Aig_ManForEachNode( p->pManAig, pObj, i )
-    {
-        Bar_ProgressUpdate( pProgress, i, NULL );
-        // derive and remember the new fraig node
-        pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
-        Aig_Regular(pObjNew)->pData = p;
-        // quit if simulation detected a counter-example for a PO
-        if ( p->pManFraig->pData )
-            continue;
-        // perform fraiging
-        Fra_FraigNode( p, pObj );
-        if ( p->pPars->fUseImps )
-            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
-    }
-    Bar_ProgressStop( pProgress );
-    // 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 );
-    // compress implications after processing all of them
-    if ( p->pPars->fUseImps )
-        Fra_ImpCompactArray( p->pCla->vImps );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
-{
-    Fra_Man_t * p;
-    Aig_Man_t * pManAigNew;
-    int clk;
-    if ( Aig_ManNodeNum(pManAig) == 0 )
-        return Aig_ManDup(pManAig, 1);
-clk = clock();
-    assert( Aig_ManLatchNum(pManAig) == 0 );
-    p = Fra_ManStart( pManAig, pPars );
-    p->pManFraig = Fra_ManPrepareComb( p );
-    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
-    Fra_SmlSimulate( p, 0 );
-//    if ( p->pPars->fChoicing )
-//        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
-    // collect initial states
-    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesBeg = Aig_ManNodeNum(pManAig);
-    p->nRegsBeg  = Aig_ManRegNum(pManAig);
-    // perform fraig sweep
-    Fra_FraigSweep( p );
-    // call back the procedure to check implications
-    if ( pManAig->pImpFunc )
-        pManAig->pImpFunc( p, pManAig->pImpData );
-    // finalize the fraiged manager
-    Fra_ManFinalizeComb( p );
-    if ( p->pPars->fChoicing )
-    {
-int clk2 = clock();
-        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-        pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
-        Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
-        Aig_ManTransferRepr( pManAigNew, p->pManAig );
-        Aig_ManMarkValidChoices( pManAigNew );
-        Aig_ManStop( p->pManFraig );
-        p->pManFraig = NULL;
-p->timeTrav += clock() - clk2;
-    }
-    else
-    {
-        Aig_ManCleanup( p->pManFraig );
-        pManAigNew = p->pManFraig;
-        p->pManFraig = NULL;
-    }
-p->timeTotal = clock() - clk;
-    // collect final stats
-    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
-    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
-    Fra_ManStop( p );
-    return pManAigNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs choicing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
-{
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = nConfMax;
-    pPars->fChoicing    = 1;
-    pPars->fDoSparse    = 1;
-    pPars->fSpeculate   = 0;
-    pPars->fProve       = 0;
-    pPars->fVerbose     = 0;
-    return Fra_FraigPerform( pManAig, pPars );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
-{
-    Aig_Man_t * pFraig;
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = nConfMax;
-    pPars->fChoicing    = 0;
-    pPars->fDoSparse    = 1;
-    pPars->fSpeculate   = 0;
-    pPars->fProve       = 0;
-    pPars->fVerbose     = 0;
-    pFraig = Fra_FraigPerform( pManAig, pPars );
-    return pFraig;
-} 
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-