abc/src/proof/dch/dchSimSat.c

/**CFile****************************************************************

  FileName    [dchSimSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

  Synopsis    [Performs resimulation using counter-examples.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

***********************************************************************/

#include "dchInt.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Collects internal nodes in the reverse DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pFanout, * pRepr;
    int iFanout = -1, i;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    // traverse the fanouts
    Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
        Dch_ManCollectTfoCands_rec( p, pFanout );
    // check if the given node has a representative
    pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
    if ( pRepr == NULL )
        return;
    // pRepr is the constant 1 node
    if ( pRepr == Aig_ManConst1(p->pAigTotal) )
    {
        Vec_PtrPush( p->vSimRoots, pObj );
        return;
    }
    // pRepr is the representative of an equivalence class
    if ( pRepr->fMarkA )
        return;
    pRepr->fMarkA = 1;
    Vec_PtrPush( p->vSimClasses, pRepr );
}

/**Function*************************************************************

  Synopsis    [Collect equivalence classes and const1 cands in the TFO.]

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrClear( p->vSimRoots );
    Vec_PtrClear( p->vSimClasses );
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );    
    Dch_ManCollectTfoCands_rec( p, pObj1 );
    Dch_ManCollectTfoCands_rec( p, pObj2 );
    Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
    Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
        pObj->fMarkA = 0;
}

/**Function*************************************************************

  Synopsis    [Resimulates the cone of influence of the solved nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        Aig_Obj_t * pObjFraig;
        int nVarNum;
        pObjFraig = Dch_ObjFraig( pObj );
        assert( !Aig_IsComplement(pObjFraig) );
        nVarNum = Dch_ObjSatNum( p, pObjFraig );
        // get the value from the SAT solver
        // (account for the fact that some vars may be minimized away)
        pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
//        pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
        return;
    }
    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
    // count the cone size
    if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
        p->nConeThis++;
}

/**Function*************************************************************

  Synopsis    [Resimulates the cone of influence of the other nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        // set random value
        pObj->fMarkB = Aig_ManRandom(0) & 1;
        return;
    }
    Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
    Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
}

/**Function*************************************************************

  Synopsis    [Handle the counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
    Aig_Obj_t * pRoot, ** ppClass;
    int i, k, nSize, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // get the equivalence classes
    Dch_ManCollectTfoCands( p, pObj, pRepr );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine these nodes
    RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    // resimulate the cone of influence of the cand classes
    RetValue2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
    {
        ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
        for ( k = 0; k < nSize; k++ )
            Dch_ManResimulateOther_rec( p, ppClass[k] );
        // refine this class
        RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
    }
    // make sure refinement happened
    if ( Aig_ObjIsConst1(pRepr) )
        assert( RetValue1 );
    else
        assert( RetValue2 );
p->timeSimSat += Abc_Clock() - clk;
}

/**Function*************************************************************

  Synopsis    [Handle the counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
    Aig_Obj_t * pRoot;
    int i, RetValue;
    abctime clk = Abc_Clock();
    // get the equivalence class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
    else
        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine this class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    else
        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
    assert( RetValue );
p->timeSimSat += Abc_Clock() - clk;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END