1 files changed, 489 insertions, 0 deletions

diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
new file mode 100644
index 00000000..d9a16e22
--- /dev/null
+++ b/src/proof/ssw/sswDyn.c
@@ -0,0 +1,489 @@
+/**CFile****************************************************************
+
+  FileName    [sswDyn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Dynamic loading of constraints.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "src/misc/bar/bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Label PIs nodes of the frames corresponding to PIs of AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjFrames;
+    int f, i;
+    Aig_ManConst1( p->pFrames )->fMarkA = 1;
+    Aig_ManConst1( p->pFrames )->fMarkB = 1;
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pObjFrames = Ssw_ObjFrame( p, pObj, f );
+            assert( Aig_ObjIsPi(pObjFrames) );
+            assert( pObjFrames->fMarkB == 0 );
+            pObjFrames->fMarkA = 1;
+            pObjFrames->fMarkB = 1;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects new POs in p->vNewPos.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( pObj->fMarkA )
+        return;
+    pObj->fMarkA = 1;
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_PtrPush( vNewPis, pObj );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
+    Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects new POs in p->vNewPos.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
+{
+    Aig_Obj_t * pFanout;
+    int iFanout = -1, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( pObj->fMarkB )
+        return;
+    pObj->fMarkB = 1;
+    if ( pObj->Id > p->nSRMiterMaxId )
+        return;
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        // skip if it is a register input PO
+        if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+            return;
+        // add the number of this constraint
+        Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
+        return;
+    }
+    // visit the fanouts
+    assert( p->pFrames->pFanData != NULL );
+    Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
+        Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads logic cones and relevant constraints.]
+
+  Description [Both pRepr and pObj are objects of the AIG. 
+  The result is the current SAT solver loaded with the logic cones
+  for pRepr and pObj corresponding to them in the frames, 
+  as well as all the relevant constraints.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjFrames, * pReprFrames;
+    Aig_Obj_t * pTemp, * pObj0, * pObj1;
+    int i, iConstr, RetValue;
+
+    assert( pRepr != pObj );
+    // get the corresponding frames nodes
+    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
+    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
+    assert( pReprFrames != pObjFrames );
+ /*
+    // compute the AIG support 
+    Vec_PtrClear( p->vNewLos );
+    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
+    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
+    // add logic cones for register outputs
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
+    {
+        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
+        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
+    }
+*/
+    // add cones for the nodes
+    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
+    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
+
+    // compute the frames support 
+    Vec_PtrClear( p->vNewLos );
+    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
+    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
+    // these nodes include both nodes corresponding to PIs and LOs
+    // (the nodes corresponding to PIs should be labeled with fMarkB!)
+
+    // collect the related constraint POs
+    Vec_IntClear( p->vNewPos );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
+        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
+    // check if the corresponding pairs are added
+    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
+    {
+        pObj0 = Aig_ManPo( p->pFrames, 2*iConstr   );
+        pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
+//        if ( pObj0->fMarkB && pObj1->fMarkB )
+        if ( pObj0->fMarkB || pObj1->fMarkB )
+        {
+            pObj0->fMarkB = 1;
+            pObj1->fMarkB = 1;
+            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
+        }
+    }
+    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pMSat->pSat);
+        assert( RetValue != 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tranfers simulation information from FRAIG to AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjFraig;
+    unsigned * pInfo;
+    int i, f, nFrames;
+
+    // transfer simulation information
+    Aig_ManForEachPi( p->pAig, pObj, i )
+    {
+        pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
+        if ( pObjFraig == Aig_ManConst0(p->pFrames) )
+        {
+            Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
+            continue;
+        }
+        assert( !Aig_IsComplement(pObjFraig) );
+        assert( Aig_ObjIsPi(pObjFraig) );
+        pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+        Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
+    }
+    // set random simulation info for the second frame
+    for ( f = 1; f < p->nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pObjFraig = Ssw_ObjFrame( p, pObj, f );
+            assert( !Aig_IsComplement(pObjFraig) );
+            assert( Aig_ObjIsPi(pObjFraig) );
+            pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+            Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
+        }
+    }
+    // create random info
+    nFrames = Ssw_SmlNumFrames( p->pSml );
+    for ( ; f < nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+            Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation with counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
+{
+    int RetValue1, RetValue2, clk = clock();
+    // transfer PI simulation information from storage
+//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
+    Ssw_ManSweepTransferDyn( p );
+    // simulate internal nodes
+//    Ssw_SmlSimulateOneFrame( p->pSml );
+    Ssw_SmlSimulateOne( p->pSml );
+    // check equivalence classes
+    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+    // prepare simulation info for the next round
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+    p->nPatterns = 0;
+    p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+    return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation with counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
+{
+    Aig_Obj_t * pObj, * pRepr, ** ppClass;
+    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    p->nSimRounds++;
+    // transfer PI simulation information from storage
+//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
+    Ssw_ManSweepTransferDyn( p );
+    // determine const1 cands and classes to be simulated
+    Vec_PtrClear( p->vResimConsts );
+    Vec_PtrClear( p->vResimClasses );
+    Aig_ManIncrementTravId( p->pAig );
+    for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ )
+    {
+        if ( i >= Aig_ManObjNumMax( p->pAig ) )
+            break;
+        pObj = Aig_ManObj( p->pAig, i );
+        if ( pObj == NULL )
+            continue;
+        if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) )
+        {
+            Vec_PtrPush( p->vResimConsts, pObj );
+            continue;
+        }
+        pRepr = Aig_ObjRepr(p->pAig, pObj);
+        if ( pRepr == NULL )
+            continue;
+        if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
+            continue;
+        Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
+        Vec_PtrPush( p->vResimClasses, pRepr );
+    }
+    // simulate internal nodes
+//    Ssw_SmlSimulateOneFrame( p->pSml );
+//    Ssw_SmlSimulateOne( p->pSml );
+    // resimulate dynamically
+//    Aig_ManIncrementTravId( p->pAig );
+//    Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
+    p->nVisCounter++;
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i )
+        Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
+    // resimulate the cone of influence of the cand classes
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
+    {
+        ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
+        for ( k = 0; k < nSize; k++ )
+            Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter );
+    }
+
+    // check equivalence classes
+//    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+//    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+    // refine these nodes
+    RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
+    RetValue2 = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
+        RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );
+
+    // prepare simulation info for the next round
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+    p->nPatterns = 0;
+    p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+    return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepDyn( Ssw_Man_t * p )
+{ 
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Obj_t * pObj, * pObjNew;
+    int clk, i, f;
+
+    // perform speculative reduction
+clk = clock();
+    // create timeframes
+    p->pFrames = Ssw_FramesWithClasses( p );
+    Aig_ManFanoutStart( p->pFrames );
+    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );
+
+    // map constants and PIs of the last frame
+    f = p->pPars->nFramesK;
+    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+    Aig_ManSetPioNumbers( p->pFrames );
+    // label nodes corresponding to primary inputs
+    Ssw_ManLabelPiNodes( p );
+p->timeReduce += clock() - clk;
+
+    // prepare simulation info
+    assert( p->vSimInfo == NULL );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+
+    // sweep internal nodes
+    p->fRefined = 0;
+    Ssw_ClassesClearRefined( p->ppClasses );
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+    p->iNodeStart = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( p->iNodeStart == 0 )
+            p->iNodeStart = i;
+        if ( p->pPars->fVerbose )
+            Bar_ProgressUpdate( pProgress, i, NULL );
+        if ( Saig_ObjIsLo(p->pAig, pObj) )
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
+        else if ( Aig_ObjIsNode(pObj) )
+        { 
+            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
+        }
+        // check if it is time to recycle the solver
+        if ( p->pMSat->pSat == NULL || 
+            (p->pPars->nSatVarMax2 && 
+             p->pMSat->nSatVars > p->pPars->nSatVarMax2 && 
+             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
+        {
+            // resimulate
+            if ( p->nPatterns > 0 )
+            {
+                p->iNodeLast = i;
+                if ( p->pPars->fLocalSim )
+                    Ssw_ManSweepResimulateDynLocal( p, f );
+                else
+                    Ssw_ManSweepResimulateDyn( p, f );
+                p->iNodeStart = i+1;
+            }
+//                printf( "Recycling SAT solver with %d vars and %d calls.\n", 
+//                    p->pMSat->nSatVars, p->nRecycleCalls );
+//            Aig_ManCleanMarkAB( p->pAig );
+            Aig_ManCleanMarkAB( p->pFrames );
+            // label nodes corresponding to primary inputs
+            Ssw_ManLabelPiNodes( p );
+            // replace the solver
+            if ( p->pMSat )
+            {
+                p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
+                p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
+                Ssw_SatStop( p->pMSat );
+                p->nRecycles++;
+                p->nRecyclesTotal++;
+                p->nRecycleCalls = 0;
+            }
+            p->pMSat = Ssw_SatStart( 0 );
+            assert( p->nPatterns == 0 );
+        }
+        // resimulate
+        if ( p->nPatterns == 32 )
+        {
+            p->iNodeLast = i;
+            if ( p->pPars->fLocalSim )
+                Ssw_ManSweepResimulateDynLocal( p, f );
+            else
+                Ssw_ManSweepResimulateDyn( p, f );
+            p->iNodeStart = i+1;
+        }
+    }
+    // resimulate
+    if ( p->nPatterns > 0 )
+    {
+        p->iNodeLast = i;
+        if ( p->pPars->fLocalSim )
+            Ssw_ManSweepResimulateDynLocal( p, f );
+        else
+            Ssw_ManSweepResimulateDyn( p, f );
+    }
+    // collect stats
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
+
+    // cleanup
+//    Ssw_ClassesCheck( p->ppClasses );
+    return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+