Removing dead code in 'pdr'.

src/proof/pdr/pdrInt.h

@@ -103,8 +103,6 @@ struct Pdr_Man_t_
     Vec_Int_t * vVisits;   // intermediate
     Vec_Int_t * vCi2Rem;   // CIs to be removed
     Vec_Int_t * vRes;      // final result
-    Vec_Int_t * vSuppLits; // support literals
-    Pdr_Set_t * pCubeJust; // justification
     abctime *   pTime4Outs;// timeout per output
     Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
     // statistics
@@ -224,7 +222,6 @@ extern void            Pdr_QueueClean( Pdr_Man_t * p );
 extern void            Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
 extern void            Pdr_QueuePrint( Pdr_Man_t * p );
 extern void            Pdr_QueueStop( Pdr_Man_t * p );
-extern int             Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
 
 ABC_NAMESPACE_HEADER_END
 

src/proof/pdr/pdrMan.c

@@ -67,8 +67,6 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
     p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
     p->vRes     = Vec_IntAlloc( 100 );  // final result
-    p->vSuppLits= Vec_IntAlloc( 100 );  // support literals
-    p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
     p->pCnfMan  = Cnf_ManStart();
     // ternary simulation
     p->pTxs     = Txs_ManStart( p, pAig, p->vPrio );
@@ -166,9 +164,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFree( p->vVisits   );  // intermediate
     Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
     Vec_IntFree( p->vRes      );  // final result
-    Vec_IntFree( p->vSuppLits );  // support literals
     Vec_PtrFreeP( &p->vInfCubes );
-    ABC_FREE( p->pCubeJust );
     ABC_FREE( p->pTime4Outs );
     if ( p->vCexes )
         Vec_PtrFreeFree( p->vCexes );

src/proof/pdr/pdrSat.c

@@ -342,24 +342,6 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
             else
                 return -1;
         }
-/*
-        if ( RetValue == l_True )
-        {
-            int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
-            if ( RetValue2 )
-                p->nCasesSS++;
-            else
-                p->nCasesSU++;
-        }
-        else
-        {
-            int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
-            if ( RetValue2 )
-                p->nCasesUS++;
-            else
-                p->nCasesUU++;
-        }
-*/
     }
     clk = Abc_Clock() - clk;
     p->tSat += clk;

src/proof/pdr/pdrUtil.c

@@ -753,8 +753,6 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
     pNode->fMarkA = Value;
     if ( Aig_ObjIsCi(pNode) )
     {
-//        if ( vSuppLits )
-//            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
         if ( Saig_ObjIsLo(pAig, pNode) )
         {
 //            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
@@ -793,60 +791,6 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
         return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if SAT assignment is found; 0 otherwise.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
-    Aig_Obj_t * pNode;
-    int i, v, fCompl;
-//    return 0;
-    for ( i = 0; i < 4; i++ )
-    {
-        // derive new assignment
-        p->pCubeJust->nLits = 0;
-        p->pCubeJust->Sign  = 0;
-        Aig_ManIncrementTravId( p->pAig );
-        for ( v = 0; v < pCube->nLits; v++ )
-        {
-            if ( pCube->Lits[v] == -1 )
-                continue;
-            pNode  = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) );
-            fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode);
-            if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) )
-                break;
-        }
-        if ( v < pCube->nLits )
-            continue;
-        // figure this out!!!
-        if ( p->pCubeJust->nLits == 0 )
-            continue;
-        // successfully derived new assignment
-        Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits );
-        // check assignment against this cube
-        if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) )
-            continue;
-//printf( "\n" );
-//Pdr_SetPrint( stdout, pCube,        Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
-//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
-        // check assignment against the clauses
-        if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) )
-            continue;
-        // find good assignment
-        return 1;
-    }
-    return 0;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////