Changes to be able to compile ABC without CUDD.

1 files changed, 0 insertions, 222 deletions

diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c
deleted file mode 100644
index 1471f377..00000000
--- a/src/proof/llb/llb2Driver.c
+++ /dev/null
@@ -1,222 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [llb2Driver.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD based reachability.]
-
-  Synopsis    [Procedures working with flop drivers.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: llb2Driver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "llbInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// driver issue:arises when creating
-// - driver ref-counter array
-// - Ns2Glo maps
-// - final partition
-// - change-phase cube
-
-// LI variable is used when
-// - driver drives more than one LI
-// - driver is a PI
-// - driver is a constant
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of times each flop driver is referenced.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p )
-{
-    Vec_Int_t * vCounts;
-    Aig_Obj_t * pObj;
-    int i;
-    vCounts = Vec_IntStart( Aig_ManObjNumMax(p) );
-    Saig_ManForEachLi( p, pObj, i )
-        Vec_IntAddToEntry( vCounts, Aig_ObjFaninId0(pObj), 1 );
-    return vCounts;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns array of NS variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs )
-{
-    Vec_Int_t * vVars;
-    Aig_Obj_t * pObj, * pDri;
-    int i;
-    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
-    Saig_ManForEachLi( pAig, pObj, i )
-    {
-        pDri = Aig_ObjFanin0(pObj);
-        if ( Vec_IntEntry( vDriRefs, Aig_ObjId(pDri) ) != 1 || Saig_ObjIsPi(pAig, pDri) || Aig_ObjIsConst1(pDri) )
-            Vec_IntPush( vVars, Aig_ObjId(pObj) );
-        else
-            Vec_IntPush( vVars, Aig_ObjId(pDri) );
-    }
-    return vVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns array of CS variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig )
-{
-    Vec_Int_t * vVars;
-    Aig_Obj_t * pObj;
-    int i;
-    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
-    Saig_ManForEachLo( pAig, pObj, i )
-        Vec_IntPush( vVars, Aig_ObjId(pObj) );
-    return vVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create cube for phase swapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd )
-{
-    DdNode * bCube, * bVar, * bTemp;
-    Aig_Obj_t * pObj;
-    int i;
-    abctime TimeStop;
-    TimeStop = dd->TimeStop; dd->TimeStop = 0;
-    bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
-    Saig_ManForEachLi( pAig, pObj, i )
-    {
-        assert( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) >= 1 );
-        if ( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) != 1 )
-            continue;
-        if ( !Aig_ObjFaninC0(pObj) )
-            continue;
-        bVar  = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
-        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
-        Cudd_RecursiveDeref( dd, bTemp );
-    }
-    Cudd_Deref( bCube );
-    dd->TimeStop = TimeStop;
-    return bCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute the last partition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, abctime TimeTarget )
-{
-//    int fVerbose = 1;
-    DdManager * dd;
-    DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp;
-    Aig_Obj_t * pObj;
-    int i;
-    dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
-    dd->TimeStop = TimeTarget;
-    bRes = Cudd_ReadOne(dd);                                   Cudd_Ref( bRes );
-
-    // mark the duplicated flop inputs
-    Aig_ManForEachObjVec( vVarsNs, p, pObj, i )
-    {
-        if ( !Saig_ObjIsLi(p, pObj) )
-            continue;
-        bVar1 = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
-        bVar2 = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
-        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
-            bVar2 = Cudd_ReadOne(dd);
-        bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
-        bProd = Cudd_bddXnor( dd, bVar1, bVar2 );              Cudd_Ref( bProd );
-//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
-//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
-        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
-        if ( bRes == NULL )
-        {
-            Cudd_RecursiveDeref( dd, bTemp );
-            Cudd_RecursiveDeref( dd, bProd );
-            return NULL;
-        }        
-        Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bProd );
-    }
-
-/*
-    Saig_ManForEachLi( p, pObj, i )
-        printf( "%d ", Aig_ObjId(pObj) );
-    printf( "\n" );
-    Saig_ManForEachLi( p, pObj, i )
-        printf( "%c%d ", Aig_ObjFaninC0(pObj)? '-':'+', Aig_ObjFaninId0(pObj) );
-    printf( "\n" );
-*/
-    Cudd_AutodynDisable( dd );
-//    Cudd_RecursiveDeref( dd, bRes );
-//    Extra_StopManager( dd );
-    dd->bFunc = bRes;
-    dd->TimeStop = 0;
-    return dd;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-