Major restructuring of the code.

12 files changed, 0 insertions, 3752 deletions

diff --git a/src/sat/pdr/module.make b/src/sat/pdr/module.make
deleted file mode 100644
index 5cf4491c..00000000
--- a/src/sat/pdr/module.make
+++ /dev/null
@@ -1,8 +0,0 @@
-SRC +=    src/sat/pdr/pdr.c \
-    src/sat/pdr/pdrCnf.c \
-    src/sat/pdr/pdrCore.c \
-    src/sat/pdr/pdrInv.c \
-    src/sat/pdr/pdrMan.c \
-    src/sat/pdr/pdrSat.c \
-    src/sat/pdr/pdrTsim.c \
-    src/sat/pdr/pdrUtil.c 
diff --git a/src/sat/pdr/pdr.c b/src/sat/pdr/pdr.c
deleted file mode 100644
index 6bdf75b5..00000000
--- a/src/sat/pdr/pdr.c
+++ /dev/null
@@ -1,53 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdr.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Netlist representation.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
deleted file mode 100644
index 03854509..00000000
--- a/src/sat/pdr/pdr.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdr.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __PDR_H__
-#define __PDR_H__
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Pdr_Par_t_ Pdr_Par_t;
-struct Pdr_Par_t_
-{
-    int iOutput;      // zero-based number of primary output to solve
-    int nRecycle;     // limit on vars for recycling
-    int nFrameMax;    // limit on frame count
-    int nConfLimit;   // limit on SAT solver conflicts
-    int nTimeOut;     // timeout in seconds
-    int fTwoRounds;   // use two rounds for generalization
-    int fMonoCnf;     // monolythic CNF
-    int fDumpInv;     // dump inductive invariant
-    int fShortest;    // forces bug traces to be shortest
-    int fSkipGeneral; // skips expensive generalization step
-    int fVerbose;     // verbose output
-    int fVeryVerbose; // very verbose output
-    int iFrame;       // explored up to this frame
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== pdrCore.c ==========================================================*/
-extern void            Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int             Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c
deleted file mode 100644
index 3e990958..00000000
--- a/src/sat/pdr/pdrClass.c
+++ /dev/null
@@ -1,223 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrClass.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Equivalence classes of register outputs.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs duplication with the variable map.]
-
-  Description [Var map contains -1 if const0 and <reg_num> otherwise.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj;
-    int i, iReg;
-    assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) );
-    // start the fraig package
-    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) );
-    pFrames->pName = Aig_UtilStrsav( pAig->pName );
-    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
-    // create CI mapping
-    Aig_ManCleanData( pAig );
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pFrames);
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-        iReg = Vec_IntEntry(vMap, i);
-        if ( iReg == -1 )
-            pObj->pData = Aig_ManConst0(pFrames);
-        else
-            pObj->pData = Saig_ManLo(pAig, iReg)->pData;
-    }
-    // add internal nodes of this frame
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // add output nodes
-    Aig_ManForEachPo( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-    // finish off
-    Aig_ManCleanup( pFrames );
-    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates mapping of registers.]
-
-  Description [Var map contains -1 if const0 and <reg_num> otherwise.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    Vec_Int_t * vMap;
-    int * pLit2Id, Lit, i;
-    pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 );
-    for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ )
-        pLit2Id[i] = -1;
-    vMap = Vec_IntAlloc( Aig_ManRegNum(p) );
-    Saig_ManForEachLi( p, pObj, i )
-    {
-        if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) )
-        {
-            Vec_IntPush( vMap, -1 );
-            continue;
-        }
-        Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj);
-        if ( pLit2Id[Lit] < 0 ) // the first time
-            pLit2Id[Lit] = i;
-        Vec_IntPush( vMap, pLit2Id[Lit] );
-    }
-    ABC_FREE( pLit2Id );
-    return vMap;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts reduced registers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCountMap( Vec_Int_t * vMap )
-{
-    int i, Entry, Counter = 0;
-    Vec_IntForEachEntry( vMap, Entry, i )
-        if ( Entry != i )
-            Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts reduced registers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManPrintMap( Vec_Int_t * vMap )
-{
-    Vec_Int_t * vMarks;
-    int f, i, iClass, Entry, Counter = 0;
-    printf( "    Consts: " );
-    Vec_IntForEachEntry( vMap, Entry, i )
-        if ( Entry == -1 )
-            printf( "%d ", i );
-    printf( "\n" );
-    vMarks = Vec_IntAlloc( 100 );
-    Vec_IntForEachEntry( vMap, iClass, f )
-    {
-        if ( iClass == -1 )
-            continue;
-        if ( iClass == f )
-            continue;
-        // check previous classes
-        if ( Vec_IntFind( vMarks, iClass ) >= 0 )
-            continue;
-        Vec_IntPush( vMarks, iClass );
-        // print class
-        printf( "    Class %d : ", iClass );
-        Vec_IntForEachEntry( vMap, Entry, i )
-            if ( Entry == iClass )
-                printf( "%d ", i );
-        printf( "\n" );
-    }
-    Vec_IntFree( vMarks );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManEquivClasses( Aig_Man_t * pAig )
-{
-    Vec_Int_t * vMap;
-    Aig_Man_t * pTemp;
-    int f, nFrames = 100;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    // start the map
-    vMap = Vec_IntAlloc( 0 );
-    Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 );
-    // iterate and print changes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // implement variable map
-        pTemp = Pdr_ManRehashWithMap( pAig, vMap );
-        // report the result
-        printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n", 
-            f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap), 
-            Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
-        // recreate the map
-        Pdr_ManPrintMap( vMap );
-        Vec_IntFree( vMap );
-        vMap = Pdr_ManCreateMap( pTemp );
-        Aig_ManStop( pTemp );
-        if ( Pdr_ManCountMap(vMap) == 0 )
-            break;
-    }
-    Vec_IntFree( vMap );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
deleted file mode 100644
index fddd292b..00000000
--- a/src/sat/pdr/pdrCnf.c
+++ /dev/null
@@ -1,357 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrCnf.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [CNF computation on demand.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrCnf.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-/*
-    The CNF (p->pCnf2) is expressed in terms of object IDs.
-    Each node in the CNF is marked if it has clauses (p->pCnf2->pObj2Count[Id] > 0).
-    Each node in the CNF has the first clause (p->pCnf2->pObj2Clause) 
-    and the number of clauses (p->pCnf2->pObj2Count).
-    Each node used in a CNF of any timeframe has its SAT var recorded.
-    Each frame has a reserve mapping of SAT variables into ObjIds.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns SAT variable of the given object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
-    return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns SAT variable of the given object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{ 
-    assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
-    if ( p->pvId2Vars[Aig_ObjId(pObj)] == NULL )
-        p->pvId2Vars[Aig_ObjId(pObj)] = Vec_IntStart( 16 );
-    if ( Vec_IntGetEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ) == 0 )
-    {
-        sat_solver * pSat = Pdr_ManSolver(p, k);
-        Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
-        int iVarNew = Vec_IntSize( vVar2Ids );
-        assert( iVarNew > 0 );
-        Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
-        Vec_IntWriteEntry( p->pvId2Vars[Aig_ObjId(pObj)], k, iVarNew );
-        sat_solver_setnvars( pSat, iVarNew + 1 );
-        if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
-        {
-            int Lit = toLitCond( iVarNew, 1 );
-            int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-            assert( RetValue == 1 );
-            sat_solver_compress( pSat );
-        }
-    }
-    return Vec_IntEntry( p->pvId2Vars[Aig_ObjId(pObj)], k );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively adds CNF for the given object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
-    sat_solver * pSat;
-    Vec_Int_t * vLits;
-    Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
-    int nVarCount = Vec_IntSize(vVar2Ids);
-    int iVarThis  = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
-    int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
-    if ( nVarCount == Vec_IntSize(vVar2Ids) )
-        return iVarThis;
-    assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
-    if ( Aig_ObjIsPi(pObj) )
-        return iVarThis;
-    nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
-    iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
-    assert( nClauses > 0 );
-    pSat = Pdr_ManSolver(p, k);
-    vLits = Vec_IntAlloc( 16 );
-    for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
-    {
-        Vec_IntClear( vLits );
-        for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
-        {
-            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)) );
-            Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
-        }
-        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
-        assert( RetValue );
-    }
-    Vec_IntFree( vLits );
-    return iVarThis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns SAT variable of the given object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
-    if ( p->pPars->fMonoCnf )
-        return Pdr_ObjSatVar1( p, k, pObj );
-    else
-        return Pdr_ObjSatVar2( p, k, pObj );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns register number for the given SAT variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Pdr_ObjRegNum1( Pdr_Man_t * p, int k, int iSatVar )
-{
-    int RegId;
-    assert( iSatVar >= 0 );
-    // consider the case of auxiliary variable
-    if ( iSatVar >= p->pCnf1->nVars )
-        return -1;
-    // consider the case of register output
-    RegId = Vec_IntEntry( p->vVar2Reg, iSatVar );
-    assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
-    return RegId;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns register number for the given SAT variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
-{
-    Aig_Obj_t * pObj;
-    int ObjId;
-    Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
-    assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) );
-    ObjId = Vec_IntEntry( vVar2Ids, iSatVar );
-    if ( ObjId == -1 ) // activation variable
-        return -1;
-    pObj = Aig_ManObj( p->pAig, ObjId );
-    if ( Saig_ObjIsLi( p->pAig, pObj ) )
-        return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig);
-    assert( 0 ); // should be called for register inputs only
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns register number for the given SAT variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar )
-{
-    if ( p->pPars->fMonoCnf )
-        return Pdr_ObjRegNum1( p, k, iSatVar );
-    else
-        return Pdr_ObjRegNum2( p, k, iSatVar );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the index of unused SAT variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManFreeVar( Pdr_Man_t * p, int k )
-{
-    if ( p->pPars->fMonoCnf )
-        return sat_solver_nvars( Pdr_ManSolver(p, k) );
-    else
-    {
-        Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( p->vVar2Ids, k );
-        Vec_IntPush( vVar2Ids, -1 );
-        return Vec_IntSize( vVar2Ids ) - 1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    assert( pSat );
-    if ( p->pCnf1 == NULL )
-    {
-        int nRegs = p->pAig->nRegs;
-        p->pAig->nRegs = Aig_ManPoNum(p->pAig);
-        p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
-        p->pAig->nRegs = nRegs;
-        assert( p->vVar2Reg == NULL );
-        p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
-        Saig_ManForEachLi( p->pAig, pObj, i )
-            Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
-    }
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
-    sat_solver_set_runtime_limit( pSat, p->timeToStop );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
-    Vec_Int_t * vVar2Ids;
-    int i, Entry;
-    assert( pSat );
-    if ( p->pCnf2 == NULL )
-    {
-        p->pCnf2     = Cnf_DeriveOther( p->pAig );
-        p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
-        p->vVar2Ids  = Vec_PtrAlloc( 256 );
-    }
-    // update the variable mapping
-    vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( p->vVar2Ids, k );
-    if ( vVar2Ids == NULL )
-    {
-        vVar2Ids = Vec_IntAlloc( 500 );
-        Vec_PtrWriteEntry( p->vVar2Ids, k, vVar2Ids );
-    }
-    Vec_IntForEachEntry( vVar2Ids, Entry, i )
-    {
-        if ( Entry == -1 )
-            continue;
-        assert( Vec_IntEntry( p->pvId2Vars[Entry], k ) > 0 );
-        Vec_IntWriteEntry( p->pvId2Vars[Entry], k, 0 );
-    }
-    Vec_IntClear( vVar2Ids );
-    Vec_IntPush( vVar2Ids, -1 );
-    // start the SAT solver
-//    pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, 500 );
-    sat_solver_set_runtime_limit( pSat, p->timeToStop );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
-    assert( pSat != NULL );
-    if ( p->pPars->fMonoCnf )
-        return Pdr_ManNewSolver1( pSat, p, k, fInit );
-    else
-        return Pdr_ManNewSolver2( pSat, p, k, fInit );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
deleted file mode 100644
index 025ada06..00000000
--- a/src/sat/pdr/pdrCore.c
+++ /dev/null
@@ -1,722 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Core procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the state could be blocked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(Pdr_Par_t) );
-    pPars->iOutput       =      -1;  // zero-based output number
-    pPars->nRecycle      =     300;  // limit on vars for recycling
-    pPars->nFrameMax     =    5000;  // limit on number of timeframes
-    pPars->nTimeOut      =       0;  // timeout in seconds
-    pPars->nConfLimit    =  100000;  // limit on SAT solver conflicts
-    pPars->fTwoRounds    =       0;  // use two rounds for generalization
-    pPars->fMonoCnf      =       0;  // monolythic CNF
-    pPars->fDumpInv      =       0;  // dump inductive invariant
-    pPars->fShortest     =       0;  // forces bug traces to be shortest
-    pPars->fVerbose      =       0;  // verbose output
-    pPars->fVeryVerbose  =       0;  // very verbose output
-    pPars->iFrame        =      -1;  // explored up to this frame
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reduces clause using analyzeFinal.]
-
-  Description [Assumes that the SAT solver just terminated an UNSAT call.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
-    Pdr_Set_t * pCubeMin;
-    Vec_Int_t * vLits;
-    int i, Entry, nCoreLits, * pCoreLits;
-    // get relevant SAT literals
-    nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
-    // translate them into register literals and remove auxiliary
-    vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
-    // skip if there is no improvement
-    if ( Vec_IntSize(vLits) == pCube->nLits )
-        return NULL;
-    assert( Vec_IntSize(vLits) < pCube->nLits );
-    // if the cube overlaps with init, add any literal
-    Vec_IntForEachEntry( vLits, Entry, i )
-        if ( lit_sign(Entry) == 0 ) // positive literal
-            break;
-    if ( i == Vec_IntSize(vLits) ) // only negative literals
-    {
-        // add the first positive literal
-        for ( i = 0; i < pCube->nLits; i++ )
-            if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
-            {
-                Vec_IntPush( vLits, pCube->Lits[i] );
-                break;
-            }
-        assert( i < pCube->nLits );
-    }
-    // generate a starting cube
-    pCubeMin  = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
-    assert( !Pdr_SetIsInit(pCubeMin, -1) );
-/*
-    // make sure the cube works
-    {
-    int RetValue;
-    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
-    assert( RetValue );
-    }
-*/
-    return pCubeMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the state could be blocked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManPushClauses( Pdr_Man_t * p )
-{
-    Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
-    Vec_Ptr_t * vArrayK, * vArrayK1;
-    int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
-    int Counter = 0;
-    int clk = clock();
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
-    {
-        Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
-        vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
-        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
-        {
-            Counter++;
-
-            // remove cubes in the same frame that are contained by pCubeK
-            Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
-            {
-                if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
-                    continue;
-                Pdr_SetDeref( pTemp );
-                Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
-                Vec_PtrPop(vArrayK);
-                m--;
-            }
-
-            // check if the clause can be moved to the next frame
-            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
-            if ( RetValue2 == -1 )
-                return -1;
-            if ( !RetValue2 )
-                continue;
-
-            {
-                Pdr_Set_t * pCubeMin;
-                pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
-                if ( pCubeMin != NULL )
-                {
-//                printf( "%d ", pCubeK->nLits - pCubeMin->nLits );
-                    Pdr_SetDeref( pCubeK );
-                    pCubeK = pCubeMin;
-                }
-            }
-
-            // if it can be moved, add it to the next frame
-            Pdr_ManSolverAddClause( p, k+1, pCubeK );
-            // check if the clause subsumes others
-            Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
-            {
-                if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
-                    continue;
-                Pdr_SetDeref( pCubeK1 );
-                Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
-                Vec_PtrPop(vArrayK1);
-                i--;
-            }
-            // add the last clause
-            Vec_PtrPush( vArrayK1, pCubeK );
-            Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
-            Vec_PtrPop(vArrayK);
-            j--;
-        }
-        if ( Vec_PtrSize(vArrayK) == 0 )
-            RetValue = 1;
-    }
-
-    // clean up the last one
-    vArrayK = Vec_VecEntry( p->vClauses, kMax );
-    Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
-    Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
-    {
-        // remove cubes in the same frame that are contained by pCubeK
-        Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
-        {
-            if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
-                continue;
-/*
-            printf( "===\n" );
-            Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
-            printf( "\n" );
-            Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
-            printf( "\n" );
-*/
-            Pdr_SetDeref( pTemp );
-            Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
-            Vec_PtrPop(vArrayK);
-            m--;
-        }
-    }
-    p->tPush += clock() - clk;
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the clause is contained in higher clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
-{
-    Pdr_Set_t * pThis;
-    Vec_Ptr_t * vArrayK;
-    int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
-        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
-            if ( Pdr_SetContains( pSet, pThis ) )
-                return 1;
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Sorts literals by priority.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
-{
-    int * pPrios = Vec_IntArray(p->vPrio);
-    int * pArray = p->pOrder;
-    int temp, i, j, best_i, nSize = pCube->nLits;
-    // initialize variable order
-    for ( i = 0; i < nSize; i++ )
-        pArray[i] = i;
-    for ( i = 0; i < nSize-1; i++ )
-    {
-        best_i = i;
-        for ( j = i+1; j < nSize; j++ )
-//            if ( pArray[j] < pArray[best_i] )
-            if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
-                best_i = j;
-        temp = pArray[i]; 
-        pArray[i] = pArray[best_i]; 
-        pArray[best_i] = temp;
-    }
-/*
-    for ( i = 0; i < pCube->nLits; i++ )
-        printf( "%2d : %5d    %5d  %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
-    printf( "\n" );
-*/
-    return pArray;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the state could be blocked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
-{
-    Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
-    int i, j, n, Lit, RetValue,  clk = clock();
-    int * pOrder;
-    // if there is no induction, return
-    *ppCubeMin = NULL;
-    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
-    if ( RetValue == -1 )
-        return -1;
-    if ( RetValue == 0 )
-    {
-        p->tGeneral += clock() - clk;
-        return 0;
-    }
-
-    // reduce clause using assumptions
-//    pCubeMin = Pdr_SetDup( pCube );
-    pCubeMin = Pdr_ManReduceClause( p, k, pCube );
-    if ( pCubeMin == NULL )
-        pCubeMin = Pdr_SetDup( pCube );
-
-    // perform generalization
-    if ( !p->pPars->fSkipGeneral )
-    {
-        // sort literals by their occurences
-        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-        // try removing literals
-        for ( j = 0; j < pCubeMin->nLits; j++ )
-        {
-            // use ordering
-    //        i = j;
-            i = pOrder[j];
-
-            // check init state
-            assert( pCubeMin->Lits[i] != -1 );
-            if ( Pdr_SetIsInit(pCubeMin, i) )
-                continue;
-            // try removing this literal
-            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-            if ( RetValue == -1 )
-            {
-                Pdr_SetDeref( pCubeMin );
-                return -1;
-            }
-            pCubeMin->Lits[i] = Lit;
-            if ( RetValue == 0 )
-                continue;
-
-            // remove j-th entry
-            for ( n = j; n < pCubeMin->nLits-1; n++ )
-                pOrder[n] = pOrder[n+1];
-            j--;
-
-            // success - update the cube
-            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-            Pdr_SetDeref( pCubeTmp );
-            assert( pCubeMin->nLits > 0 );
-            i--;
-
-            // get the ordering by decreasing priorit
-            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-        }
-
-        if ( p->pPars->fTwoRounds )
-        for ( j = 0; j < pCubeMin->nLits; j++ )
-        {
-            // use ordering
-    //        i = j;
-            i = pOrder[j];
-
-            // check init state
-            assert( pCubeMin->Lits[i] != -1 );
-            if ( Pdr_SetIsInit(pCubeMin, i) )
-                continue;
-            // try removing this literal
-            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-            if ( RetValue == -1 )
-            {
-                Pdr_SetDeref( pCubeMin );
-                return -1;
-            }
-            pCubeMin->Lits[i] = Lit;
-            if ( RetValue == 0 )
-                continue;
-
-            // remove j-th entry
-            for ( n = j; n < pCubeMin->nLits-1; n++ )
-                pOrder[n] = pOrder[n+1];
-            j--;
-
-            // success - update the cube
-            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-            Pdr_SetDeref( pCubeTmp );
-            assert( pCubeMin->nLits > 0 );
-            i--;
-
-            // get the ordering by decreasing priorit
-            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-        }
-    }
-
-    assert( ppCubeMin != NULL );
-    *ppCubeMin = pCubeMin;
-    p->tGeneral += clock() - clk;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the state could be blocked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
-{
-    Pdr_Obl_t * pThis;
-    Pdr_Set_t * pPred, * pCubeMin;
-    int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
-    int kMax = Vec_PtrSize(p->vSolvers)-1, clk;
-    p->nBlocks++;
-    // create first proof obligation
-    assert( p->pQueue == NULL );
-    pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
-    Pdr_QueuePush( p, pThis );
-    // try to solve it recursively
-    while ( !Pdr_QueueIsEmpty(p) )
-    {
-        Counter++;
-        pThis = Pdr_QueueHead( p );
-        if ( pThis->iFrame == 0 )
-            return 0; // SAT
-        pThis = Pdr_QueuePop( p );
-        assert( pThis->iFrame > 0 );
-        assert( !Pdr_SetIsInit(pThis->pState, -1) );
-
-        clk = clock();
-        if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
-        {
-            p->tContain += clock() - clk;
-            Pdr_OblDeref( pThis );
-            continue;
-        }
-        p->tContain += clock() - clk;
-
-        // check if the cube is already contained
-        RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
-        if ( RetValue == -1 ) // cube is blocked by clauses in this frame
-        {
-            Pdr_OblDeref( pThis );
-            return -1;
-        }
-        if ( RetValue ) // cube is blocked by clauses in this frame
-        {
-            Pdr_OblDeref( pThis );
-            continue;
-        }
-
-        // check if the cube holds with relative induction
-        pCubeMin = NULL;
-        RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
-        if ( RetValue == -1 )
-        {
-            Pdr_OblDeref( pThis );
-            return -1;
-        }
-        if ( RetValue ) // cube is blocked inductively in this frame
-        {
-            assert( pCubeMin != NULL );
-
-            // k is the last frame where pCubeMin holds
-            k = pThis->iFrame;
-
-            // check other frames
-            assert( pPred == NULL );
-            for ( k = pThis->iFrame; k < kMax; k++ )
-                if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) )
-                    break;
-
-            // add new clause
-            if ( p->pPars->fVeryVerbose )
-            {
-            printf( "Adding cube " );
-            Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
-            printf( " to frame %d.\n", k );
-            }
-            // set priority flops
-            for ( i = 0; i < pCubeMin->nLits; i++ )
-            {
-                assert( pCubeMin->Lits[i] >= 0 );
-                assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
-                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
-            }
-
-            Vec_VecPush( p->vClauses, k, pCubeMin );   // consume ref
-            p->nCubes++;
-            // add clause
-            for ( i = 1; i <= k; i++ )
-                Pdr_ManSolverAddClause( p, i, pCubeMin );
-            // schedule proof obligation
-            if ( k < kMax && !p->pPars->fShortest )
-            {
-                pThis->iFrame = k+1;
-                pThis->prio   = Prio--;
-                Pdr_QueuePush( p, pThis );
-            }
-            else
-            {
-                Pdr_OblDeref( pThis );
-            }
-        }
-        else
-        {
-            assert( pCubeMin == NULL );
-            assert( pPred != NULL );
-            pThis->prio = Prio--;
-            Pdr_QueuePush( p, pThis );
-
-            pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
-            Pdr_QueuePush( p, pThis );
-        }
-
-        // check the timeout
-        if ( p->timeToStop && time(NULL) > p->timeToStop )
-            return -1;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManSolveInt( Pdr_Man_t * p )
-{
-    int fPrintClauses = 0;
-    Pdr_Set_t * pCube;
-    int k, RetValue = -1;
-    int clkTotal = clock();
-    int clkStart = clock();
-    p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
-    assert( Vec_PtrSize(p->vSolvers) == 0 );
-    // create the first timeframe
-    Pdr_ManCreateSolver( p, (k = 0) );
-    while ( 1 )
-    {
-        p->nFrames = k;
-        assert( k == Vec_PtrSize(p->vSolvers)-1 );
-        RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
-        {
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            printf( "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-            p->pPars->iFrame = k;
-            return -1;
-        }
-        if ( RetValue == 0 )
-        {
-            RetValue = Pdr_ManBlockCube( p, pCube );
-            if ( RetValue == -1 )
-            {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                printf( "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                p->pPars->iFrame = k;
-                return -1;
-            }
-            if ( RetValue == 0 )
-            {
-                if ( fPrintClauses )
-                {
-                    printf( "*** Clauses after frame %d:\n", k );
-                    Pdr_ManPrintClauses( p, 0 );
-                }
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                p->pPars->iFrame = k;
-                return 0; // SAT
-            }
-        }
-        else
-        {
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            // open a new timeframe
-            assert( pCube == NULL );
-            Pdr_ManSetPropertyOutput( p, k );
-            Pdr_ManCreateSolver( p, ++k );
-            if ( fPrintClauses )
-            {
-                printf( "*** Clauses after frame %d:\n", k );
-                Pdr_ManPrintClauses( p, 0 );
-            }
-            // push clauses into this timeframe
-            RetValue = Pdr_ManPushClauses( p );
-            if ( RetValue == -1 )
-            {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                printf( "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                p->pPars->iFrame = k;
-                return -1;
-            }
-            if ( RetValue )
-            {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Pdr_ManReportInvariant( p );
-                Pdr_ManVerifyInvariant( p );
-                p->pPars->iFrame = k;
-                return 1; // UNSAT
-            }
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 0, clock() - clkStart );
-            clkStart = clock();
-        }
-
-        // check the timeout
-        if ( p->timeToStop && time(NULL) > p->timeToStop )
-        {
-            if ( fPrintClauses )
-            {
-                printf( "*** Clauses after frame %d:\n", k );
-                Pdr_ManPrintClauses( p, 0 );
-            }
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            printf( "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
-            p->pPars->iFrame = k;
-            return -1;
-        }
-        if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
-        {
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
-            p->pPars->iFrame = k;
-            return -1;
-        } 
-    }
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex )
-{
-    Pdr_Man_t * p;
-    int RetValue;
-    int clk = clock();
-    p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
-    RetValue = Pdr_ManSolveInt( p );
-    *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
-    if ( p->pPars->fDumpInv )
-        Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-
-//    if ( *ppCex && pPars->fVerbose )
-//        printf( "Found counter-example in frame %d after exploring %d frames.\n", 
-//            (*ppCex)->iFrame, p->nFrames );
-    p->tTotal += clock() - clk;
-    if ( pvPrioInit )
-    {
-        *pvPrioInit = p->vPrio;
-        p->vPrio = NULL;
-    }
-    Pdr_ManStop( p );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
-{
-/*
-    Vec_Int_t * vPrioInit = NULL;
-    int RetValue, nTimeOut;
-    if ( pPars->nTimeOut > 0 )
-        return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
-    nTimeOut = pPars->nTimeOut;
-    pPars->nTimeOut = 10;
-    RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
-    pPars->nTimeOut = nTimeOut;
-    if ( RetValue == -1 )
-        RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
-    Vec_IntFree( vPrioInit );
-    return RetValue;
-*/
-    return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
deleted file mode 100644
index f49ee7d0..00000000
--- a/src/sat/pdr/pdrInt.h
+++ /dev/null
@@ -1,198 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrInt.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Internal declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __PDR_INT_H__
-#define __PDR_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "saig.h"
-#include "cnf.h"
-#include "satSolver.h"
-#include "pdr.h" 
-
-ABC_NAMESPACE_HEADER_START
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-             
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Pdr_Set_t_ Pdr_Set_t;
-struct Pdr_Set_t_
-{
-    word        Sign;      // signature
-    int         nRefs;     // ref counter
-    int         nTotal;    // total literals
-    int         nLits;     // num flop literals
-    int         Lits[0];
-};
-
-typedef struct Pdr_Obl_t_ Pdr_Obl_t;
-struct Pdr_Obl_t_
-{
-    int         iFrame;    // time frame
-    int         prio;      // priority
-    int         nRefs;     // reference counter
-    Pdr_Set_t * pState;    // state cube
-    Pdr_Obl_t * pNext;     // next one
-    Pdr_Obl_t * pLink;     // queue link
-};
-
-typedef struct Pdr_Man_t_ Pdr_Man_t;
-struct Pdr_Man_t_
-{
-    // input problem
-    Pdr_Par_t * pPars;     // parameters
-    Aig_Man_t * pAig;      // user's AIG
-    // static CNF representation
-    Cnf_Dat_t * pCnf1;     // CNF for this AIG
-    Vec_Int_t * vVar2Reg;  // mapping of SAT var into registers
-    // dynamic CNF representation
-    Cnf_Dat_t * pCnf2;     // CNF for this AIG
-    Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var
-    Vec_Ptr_t * vVar2Ids;  // for each used frame, maps SAT var into ObjId
-    // data representation
-    Vec_Ptr_t * vSolvers;  // SAT solvers
-    Vec_Vec_t * vClauses;  // clauses by timeframe
-    Pdr_Obl_t * pQueue;    // proof obligations
-    int *       pOrder;    // ordering of the lits
-    Vec_Int_t * vActVars;  // the counter of activation variables
-    // internal use
-    Vec_Int_t * vPrio;     // priority flops
-    Vec_Int_t * vLits;     // array of literals
-    Vec_Int_t * vCiObjs;   // cone leaves
-    Vec_Int_t * vCoObjs;   // cone roots
-    Vec_Int_t * vCiVals;   // cone leaf values
-    Vec_Int_t * vCoVals;   // cone root values
-    Vec_Int_t * vNodes;    // cone nodes
-    Vec_Int_t * vUndo;     // cone undos
-    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
-    // statistics
-    int         nBlocks;   // the number of times blockState was called
-    int         nObligs;   // the number of proof obligations derived
-    int         nCubes;    // the number of cubes derived
-    int         nCalls;    // the number of SAT calls
-    int         nCallsS;   // the number of SAT calls (sat)
-    int         nCallsU;   // the number of SAT calls (unsat)
-    int         nStarts;   // the number of SAT solver restarts
-    int         nFrames;   // frames explored
-    int         nCasesSS;
-    int         nCasesSU;
-    int         nCasesUS;
-    int         nCasesUU;
-    // runtime
-    int         timeStart;
-    int         timeToStop;
-    // time stats
-    int         tSat;
-    int         tSatSat;
-    int         tSatUnsat;
-    int         tGeneral;
-    int         tPush;
-    int         tTsim;
-    int         tContain;
-    int         tCnf;
-    int         tTotal;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k )  { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== pdrCex.c ==========================================================*/
-extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
-/*=== pdrCnf.c ==========================================================*/
-extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
-extern int             Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
-extern int             Pdr_ManFreeVar( Pdr_Man_t * p, int k );
-extern sat_solver *    Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
-/*=== pdrCore.c ==========================================================*/
-extern int             Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
-/*=== pdrInv.c ==========================================================*/
-extern void            Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
-extern void            Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
-extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
-extern void            Pdr_ManReportInvariant( Pdr_Man_t * p );
-extern void            Pdr_ManVerifyInvariant( Pdr_Man_t * p );
-/*=== pdrMan.c ==========================================================*/
-extern Pdr_Man_t *     Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
-extern void            Pdr_ManStop( Pdr_Man_t * p );
-extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
-/*=== pdrSat.c ==========================================================*/
-extern sat_solver *    Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
-extern sat_solver *    Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
-extern void            Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
-extern Vec_Int_t *     Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
-extern Vec_Int_t *     Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
-extern void            Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern void            Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
-extern int             Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
-/*=== pdrTsim.c ==========================================================*/
-extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-/*=== pdrUtil.c ==========================================================*/
-extern Pdr_Set_t *     Pdr_SetAlloc( int nSize );
-extern Pdr_Set_t *     Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
-extern Pdr_Set_t *     Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
-extern Pdr_Set_t *     Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
-extern Pdr_Set_t *     Pdr_SetDup( Pdr_Set_t * pSet );
-extern Pdr_Set_t *     Pdr_SetRef( Pdr_Set_t * p );
-extern void            Pdr_SetDeref( Pdr_Set_t * p );
-extern int             Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
-extern int             Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
-extern int             Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
-extern void            Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
-extern int             Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
-extern Pdr_Obl_t *     Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
-extern Pdr_Obl_t *     Pdr_OblRef( Pdr_Obl_t * p );
-extern void            Pdr_OblDeref( Pdr_Obl_t * p );
-extern int             Pdr_QueueIsEmpty( Pdr_Man_t * p );
-extern Pdr_Obl_t *     Pdr_QueueHead( Pdr_Man_t * p );
-extern Pdr_Obl_t *     Pdr_QueuePop( 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
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
deleted file mode 100644
index 2f630e28..00000000
--- a/src/sat/pdr/pdrInv.c
+++ /dev/null
@@ -1,376 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrInv.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Invariant computation, printing, verification.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"  // for Abc_NtkCollectCioNames()
-#include "main.h" // for Abc_FrameReadGlobalFrame()
-
-#include "pdrInt.h"
-#include "extra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
-{
-    static int PastSize;
-    Vec_Ptr_t * vVec;
-    int i, ThisSize, Length, LengthStart;
-    if ( Vec_PtrSize(p->vSolvers) < 2 )
-        return;
-    // count the total length of the printout
-    Length = 0;
-    Vec_VecForEachLevel( p->vClauses, vVec, i )
-        Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
-    // determine the starting point
-    LengthStart = ABC_MAX( 0, Length - 70 );
-    printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
-    ThisSize = 6;
-    if ( LengthStart > 0 )
-    {
-        printf( " ..." );
-        ThisSize += 4;
-    }
-    Length = 0;
-    Vec_VecForEachLevel( p->vClauses, vVec, i )
-    {
-        if ( Length < LengthStart )
-        {
-            Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
-            continue;
-        }
-        printf( " %d", Vec_PtrSize(vVec) );
-        Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
-        ThisSize += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
-    }
-    if ( fClose )
-    {
-        for ( i = 0; i < PastSize - ThisSize; i++ )
-            printf( " " );
-        printf( "\n" );
-    }
-    else
-    {
-        printf( "\r" );
-        PastSize = ThisSize;
-    }
-//    printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts how many times each flop appears in the set of cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
-{
-    Vec_Int_t * vFlopCount;
-    Pdr_Set_t * pCube;
-    int i, n;
-    vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
-    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
-        for ( n = 0; n < pCube->nLits; n++ )
-        {
-            assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
-            Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
-        }
-    return vFlopCount;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
-{
-    Vec_Ptr_t * vArrayK;
-    int k, kMax = Vec_PtrSize(p->vSolvers)-1;
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
-        if ( Vec_PtrSize(vArrayK) == 0 )
-            return k;
-//    return -1;
-    // if there is no starting point (as in case of SAT or undecided), return the last frame
-//    printf( "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
-    return kMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of variables used in the clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
-{
-    Vec_Ptr_t * vResult;
-    Vec_Ptr_t * vArrayK;
-    Pdr_Set_t * pSet;
-    int i, j;
-    vResult = Vec_PtrAlloc( 100 );
-    Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
-        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
-            Vec_PtrPush( vResult, pSet );
-    return vResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of variables used in the clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
-{
-    Vec_Int_t * vFlopCounts;
-    Vec_Ptr_t * vCubes;
-    int i, Entry, Counter = 0;
-    vCubes = Pdr_ManCollectCubes( p, kStart );
-    vFlopCounts = Pdr_ManCountFlops( p, vCubes );
-    Vec_IntForEachEntry( vFlopCounts, Entry, i )
-        Counter += (Entry > 0);
-    Vec_IntFreeP( &vFlopCounts );
-    Vec_PtrFree( vCubes );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
-{
-    Vec_Ptr_t * vArrayK;
-    Pdr_Set_t * pCube;
-    int i, k, Counter = 0;
-    Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
-    {
-        Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
-        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
-        {
-            printf( "C=%4d. F=%4d ", Counter++, k );
-            Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );  
-            printf( "\n" ); 
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     [] 
-
-***********************************************************************/
-void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
-{
-    int fUseSupp = 1;
-    FILE * pFile;
-    Vec_Int_t * vFlopCounts;
-    Vec_Ptr_t * vCubes;
-    Pdr_Set_t * pCube;
-    char ** pNamesCi;
-    int i, kStart;
-    // create file
-    pFile = fopen( pFileName, "w" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\" for writing invariant.\n", pFileName );
-        return;
-    } 
-    // collect cubes
-    kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
-    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
-    // collect variable appearances
-    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
-    // output the header
-    if ( fProved )
-        fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
-    else
-        fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
-    fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
-    fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
-    fprintf( pFile, ".o 1\n" );
-    fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
-    // output flop names
-    pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
-    if ( pNamesCi )
-    {
-        fprintf( pFile, ".ilb" );
-        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-            if ( !fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
-                fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
-        fprintf( pFile, "\n" );
-        ABC_FREE( pNamesCi );
-        fprintf( pFile, ".ob inv\n" );
-    }
-    // output cubes
-    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
-    {
-        Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
-        fprintf( pFile, " 1\n" ); 
-    }
-    fprintf( pFile, ".e\n\n" );
-    fclose( pFile );
-    Vec_IntFreeP( &vFlopCounts );
-    Vec_PtrFree( vCubes );
-    if ( fProved )
-        printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
-    else
-        printf( "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManReportInvariant( Pdr_Man_t * p )
-{
-    Vec_Ptr_t * vCubes;
-    int kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
-    printf( "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", 
-        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
-    Vec_PtrFree( vCubes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
-{
-    sat_solver * pSat;
-    Vec_Int_t * vLits;
-    Vec_Ptr_t * vCubes;
-    Pdr_Set_t * pCube;
-    int i, kStart, kThis, RetValue, Counter = 0, clk = clock();
-    // collect cubes used in the inductive invariant
-    kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
-    // create solver with the cubes
-    kThis = Vec_PtrSize(p->vSolvers);
-    pSat  = Pdr_ManCreateSolver( p, kThis );
-    // add the property output
-    Pdr_ManSetPropertyOutput( p, kThis );
-    // add the clauses
-    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
-    {
-        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
-        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
-        assert( RetValue );
-        sat_solver_compress( pSat );
-    }
-    // check each clause
-    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
-    {
-        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
-        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
-        if ( RetValue != l_False )
-        {
-            printf( "Verification of clause %d failed.\n", i );
-            Counter++;
-        }
-    }
-    if ( Counter )
-        printf( "Verification of %d clauses has failed.\n", Counter );
-    else
-    {
-        printf( "Verification of invariant with %d clauses was successful.  ", Vec_PtrSize(vCubes) );
-        Abc_PrintTime( 1, "Time", clock() - clk );
-    }
-//    sat_solver_delete( pSat );
-    Vec_PtrFree( vCubes );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
deleted file mode 100644
index 95a38efb..00000000
--- a/src/sat/pdr/pdrMan.c
+++ /dev/null
@@ -1,194 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Manager procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
-{
-    Pdr_Man_t * p;
-    p = ABC_CALLOC( Pdr_Man_t, 1 );
-    p->pPars    = pPars;
-    p->pAig     = pAig;
-    p->vSolvers = Vec_PtrAlloc( 0 );
-    p->vClauses = Vec_VecAlloc( 0 );
-    p->pQueue   = NULL;
-    p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
-    p->vActVars = Vec_IntAlloc( 256 );
-    // internal use
-    p->vPrio    = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) );  // priority flops
-    p->vLits    = Vec_IntAlloc( 100 );  // array of literals
-    p->vCiObjs  = Vec_IntAlloc( 100 );  // cone leaves
-    p->vCoObjs  = Vec_IntAlloc( 100 );  // cone roots
-    p->vCiVals  = Vec_IntAlloc( 100 );  // cone leaf values
-    p->vCoVals  = Vec_IntAlloc( 100 );  // cone root values
-    p->vNodes   = Vec_IntAlloc( 100 );  // cone nodes
-    p->vUndo    = Vec_IntAlloc( 100 );  // cone undos
-    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) );
-    // additional AIG data-members
-    if ( pAig->pFanData == NULL )
-        Aig_ManFanoutStart( pAig );
-    if ( pAig->pTerSimData == NULL )
-        pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
-    p->timeStart = clock();
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManStop( Pdr_Man_t * p )
-{
-    Pdr_Set_t * pCla;
-    sat_solver * pSat;
-    int i, k;
-    Aig_ManCleanMarkAB( p->pAig );
-    if ( p->pPars->fVerbose ) 
-    {
-        printf( "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Start =%4d\n", 
-            p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
-        ABC_PRTP( "SAT solving", p->tSat,       p->tTotal );
-        ABC_PRTP( "  unsat    ", p->tSatUnsat,  p->tTotal );
-        ABC_PRTP( "  sat      ", p->tSatSat,    p->tTotal );
-        ABC_PRTP( "Generalize ", p->tGeneral,   p->tTotal );
-        ABC_PRTP( "Push clause", p->tPush,      p->tTotal );
-        ABC_PRTP( "Ternary sim", p->tTsim,      p->tTotal );
-        ABC_PRTP( "Containment", p->tContain,   p->tTotal );
-        ABC_PRTP( "CNF compute", p->tCnf,       p->tTotal );
-        ABC_PRTP( "TOTAL      ", p->tTotal,     p->tTotal );
-    }
-//    printf( "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
-    Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
-        sat_solver_delete( pSat );
-    Vec_PtrFree( p->vSolvers );
-    Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
-        Pdr_SetDeref( pCla );
-    Vec_VecFree( p->vClauses );
-    Pdr_QueueStop( p );
-    ABC_FREE( p->pOrder );
-    Vec_IntFree( p->vActVars );
-    // static CNF
-    Cnf_DataFree( p->pCnf1 );
-    Vec_IntFreeP( &p->vVar2Reg );
-    // dynamic CNF
-    Cnf_DataFree( p->pCnf2 );
-    if ( p->pvId2Vars )
-    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
-        Vec_IntFreeP( &p->pvId2Vars[i] );
-    ABC_FREE( p->pvId2Vars );
-    Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
-    // internal use
-    Vec_IntFreeP( &p->vPrio   );  // priority flops
-    Vec_IntFree( p->vLits     );  // array of literals
-    Vec_IntFree( p->vCiObjs   );  // cone leaves
-    Vec_IntFree( p->vCoObjs   );  // cone roots
-    Vec_IntFree( p->vCiVals   );  // cone leaf values
-    Vec_IntFree( p->vCoVals   );  // cone root values
-    Vec_IntFree( p->vNodes    );  // cone nodes
-    Vec_IntFree( p->vUndo     );  // cone undos
-    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
-    ABC_FREE( p->pCubeJust );
-    // additional AIG data-members
-    if ( p->pAig->pFanData != NULL )
-        Aig_ManFanoutStop( p->pAig );
-    if ( p->pAig->pTerSimData != NULL )
-        ABC_FREE( p->pAig->pTerSimData );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
-{
-    Abc_Cex_t * pCex;
-    Pdr_Obl_t * pObl;
-    int i, f, Lit, nFrames = 0;
-    // count the number of frames
-    for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
-        nFrames++;
-    // create the counter-example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
-    pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
-    pCex->iFrame = nFrames-1;
-    for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
-        for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
-        {
-            Lit = pObl->pState->Lits[i];
-            if ( lit_sign(Lit) )
-                continue;
-            assert( lit_var(Lit) < pCex->nPis );
-            Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
-        }
-    assert( f == nFrames );
-    return pCex;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
deleted file mode 100644
index cc4c2b1b..00000000
--- a/src/sat/pdr/pdrSat.c
+++ /dev/null
@@ -1,373 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [SAT solver procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates new SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
-{
-    sat_solver * pSat;
-    assert( Vec_PtrSize(p->vSolvers) == k );
-    assert( Vec_VecSize(p->vClauses) == k );
-    assert( Vec_IntSize(p->vActVars) == k );
-    // create new solver
-    pSat = sat_solver_new();
-    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
-    Vec_PtrPush( p->vSolvers, pSat );
-    Vec_VecExpand( p->vClauses, k );
-    Vec_IntPush( p->vActVars, 0 );
-    // add property cone
-    Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns old or restarted solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
-{
-    sat_solver * pSat;
-    Vec_Ptr_t * vArrayK;
-    Pdr_Set_t * pCube;
-    int i, j;
-    pSat = Pdr_ManSolver(p, k);
-    if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
-        return pSat;
-    assert( k < Vec_PtrSize(p->vSolvers) - 1 );
-    p->nStarts++;
-//    sat_solver_delete( pSat );
-//    pSat = sat_solver_new();
-    sat_solver_rollback( pSat );
-    // create new SAT solver
-    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
-    // write new SAT solver
-    Vec_PtrWriteEntry( p->vSolvers, k, pSat );
-    Vec_IntWriteEntry( p->vActVars, k, 0 );
-    // set the property output
-    Pdr_ManSetPropertyOutput( p, k );
-    // add the clauses
-    Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
-        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
-            Pdr_ManSolverAddClause( p, k, pCube );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts SAT variables into register IDs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
-{
-    int i, RegId;
-    Vec_IntClear( p->vLits );
-    for ( i = 0; i < nArray; i++ )
-    {
-        RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
-        if ( RegId == -1 )
-            continue;
-        assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
-        Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
-    }
-    assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
-    return p->vLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the cube in terms of RO numbers into array of CNF literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
-{
-    Aig_Obj_t * pObj;
-    int i, iVar, iVarMax = 0;
-    int clk = clock();
-    Vec_IntClear( p->vLits );
-    for ( i = 0; i < pCube->nLits; i++ )
-    {
-        if ( pCube->Lits[i] == -1 )
-            continue;
-        if ( fNext )
-            pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
-        else
-            pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
-        iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
-        iVarMax = ABC_MAX( iVarMax, iVar );
-        Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
-    }
-//    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
-    p->tCnf += clock() - clk;
-    return p->vLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the property output to 0 (sat) forever.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
-{
-    sat_solver * pSat;
-    int Lit, RetValue;
-    pSat = Pdr_ManSolver(p, k);
-    Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
-    RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-    assert( RetValue == 1 );
-    sat_solver_compress( pSat );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one clause in terms of ROs to the k-th SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
-    sat_solver * pSat;
-    Vec_Int_t * vLits;
-    int RetValue;
-    pSat  = Pdr_ManSolver(p, k);
-    vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
-    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
-    assert( RetValue == 1 );
-    sat_solver_compress( pSat );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects values of the RO/RI variables in k-th SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
-{
-    sat_solver * pSat;
-    Aig_Obj_t * pObj;
-    int iVar, i;
-    Vec_IntClear( vValues );
-    pSat = Pdr_ManSolver(p, k);
-    Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
-    {
-        iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
-        Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
- 
-  Description [Return 1/0 if cube or property are proved to hold/fail
-  in k-th timeframe.  Returns the predecessor bad state in ppPred.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{ 
-    sat_solver * pSat;
-    Vec_Int_t * vLits;
-    int RetValue;
-    pSat = Pdr_ManFetchSolver( p, k );
-    vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
-    RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
-    if ( RetValue == l_Undef )
-        return -1;
-    return (RetValue == l_False);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
- 
-  Description [Return 1/0 if cube or property are proved to hold/fail
-  in k-th timeframe.  Returns the predecessor bad state in ppPred.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
-{ 
-    int fUseLit = 1;
-    int fLitUsed = 0;
-    sat_solver * pSat;
-    Vec_Int_t * vLits;
-    int Lit, RetValue, clk;
-    p->nCalls++;
-    pSat = Pdr_ManFetchSolver( p, k );
-    if ( pCube == NULL ) // solve the property
-    {
-        clk = clock();
-        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
-        RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
-        if ( RetValue == l_Undef )
-            return -1;
-    }
-    else // check relative containment in terms of next states
-    {
-        if ( fUseLit )
-        {
-            fLitUsed = 1;
-            Vec_IntAddToEntry( p->vActVars, k, 1 );
-            // add the cube in terms of current state variables
-            vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
-            // add activation literal
-            Lit = toLit( Pdr_ManFreeVar(p, k) );
-            // add activation literal
-            Vec_IntPush( vLits, Lit );
-            RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
-            assert( RetValue == 1 );
-            sat_solver_compress( pSat );
-            // create assumptions
-            vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
-            // add activation literal
-            Vec_IntPush( vLits, lit_neg(Lit) );
-        }
-        else
-            vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
-
-        // solve 
-        clk = clock();
-        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
-        if ( RetValue == l_Undef )
-            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 = clock() - clk;
-    p->tSat += clk;
-    assert( RetValue != l_Undef );
-    if ( RetValue == l_False )
-    {
-        p->tSatUnsat += clk;
-        p->nCallsU++;
-        if ( ppPred )
-            *ppPred = NULL;
-        RetValue = 1;
-    }
-    else // if ( RetValue == l_True )
-    {
-        p->tSatSat += clk;
-        p->nCallsS++;
-        if ( ppPred )
-            *ppPred = Pdr_ManTernarySim( p, k, pCube );
-        RetValue = 0;
-    }
-
-/* // for some reason, it does not work...
-    if ( fLitUsed )
-    {
-        int RetValue;
-        Lit = lit_neg(Lit);
-        RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-        assert( RetValue == 1 );
-        sat_solver_compress( pSat );
-    }
-*/
-    return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c
deleted file mode 100644
index 6fec1605..00000000
--- a/src/sat/pdr/pdrTsim.c
+++ /dev/null
@@ -1,450 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrTsim.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Ternary simulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define PDR_ZER 1
-#define PDR_ONE 2
-#define PDR_UND 3
-
-static inline int Pdr_ManSimInfoNot( int Value )
-{
-    if ( Value == PDR_ZER )
-        return PDR_ONE;
-    if ( Value == PDR_ONE )
-        return PDR_ZER;
-    return PDR_UND;
-}
-
-static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
-{
-    if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
-        return PDR_ZER;
-    if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
-        return PDR_ONE;
-    return PDR_UND;
-}
-
-static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
-{
-    assert( Value >= PDR_ZER && Value <= PDR_UND );
-    Value ^= Pdr_ManSimInfoGet( p, pObj );
-    p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the TFI cone and collects CIs and nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(pAig, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
-        return;
-    }
-    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
-    if ( Aig_ObjIsPo(pObj) )
-        return;
-    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
-    Vec_IntPush( vNodes, Aig_ObjId(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the TFI cone and collects CIs and nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Vec_IntClear( vCiObjs );
-    Vec_IntClear( vNodes );
-    Aig_ManIncrementTravId( pAig );
-    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
-    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
-        Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
-    int Value0, Value1, Value;
-    Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
-    if ( Aig_ObjFaninC0(pObj) )
-        Value0 = Pdr_ManSimInfoNot( Value0 );
-    if ( Aig_ObjIsPo(pObj) )
-    {
-        Pdr_ManSimInfoSet( pAig, pObj, Value0 );
-        return Value0;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
-    if ( Aig_ObjFaninC1(pObj) )
-        Value1 = Pdr_ManSimInfoNot( Value1 );
-    Value = Pdr_ManSimInfoAnd( Value0, Value1 );
-    Pdr_ManSimInfoSet( pAig, pObj, Value );
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation for one design.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManSimDataInit( Aig_Man_t * pAig, 
-    Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes, 
-    Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // set the CI values
-    Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
-    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
-        Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
-    // set the FOs to remove
-    if ( vCi2Rem != NULL )
-    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
-        Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
-    // perform ternary simulation
-    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
-        Pdr_ManExtendOneEval( pAig, pObj );
-    // transfer results to the output
-    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
-        Pdr_ManExtendOneEval( pAig, pObj );
-    // check the results
-    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
-        if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Tries to assign ternary value to one of the CIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
-{
-    Aig_Obj_t * pFanout;
-    int i, k, iFanout, Value, Value2;
-    assert( Saig_ObjIsLo(pAig, pObj) );
-    assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
-    // save original value
-    Value = Pdr_ManSimInfoGet( pAig, pObj );
-    assert( Value == PDR_ZER || Value == PDR_ONE );
-    Vec_IntPush( vUndo, Aig_ObjId(pObj) );
-    Vec_IntPush( vUndo, Value );
-    // update original value
-    Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
-    // traverse
-    Vec_IntClear( vVis );
-    Vec_IntPush( vVis, Aig_ObjId(pObj) );
-    Aig_ManForEachObjVec( vVis, pAig, pObj, i )
-    {
-        Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
-        {
-            if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
-                continue;
-            assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
-            Value = Pdr_ManSimInfoGet( pAig, pFanout );
-            if ( Value == PDR_UND )
-                continue;
-            Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
-            if ( Value2 == Value )
-                continue;
-            assert( Value2 == PDR_UND );
-            Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
-            Vec_IntPush( vUndo, Value );
-            if ( Aig_ObjIsPo(pFanout) )
-                return 0;
-            assert( Aig_ObjIsNode(pFanout) );
-            Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Undoes the partial results of ternary simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
-{
-    Aig_Obj_t * pObj;
-    int i, Value;
-    Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
-    {
-        Value  = Vec_IntEntry(vUndo, ++i);
-        assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
-        Pdr_ManSimInfoSet( pAig, pObj, Value );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the resulting cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
-{
-    Aig_Obj_t * pObj;
-    int i, Lit;
-    // mark removed flop outputs
-    Aig_ManIncrementTravId( pAig );
-    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
-    {
-        assert( Saig_ObjIsLo( pAig, pObj ) );
-        Aig_ObjSetTravIdCurrent(pAig, pObj);
-    }
-    // collect flop outputs that are not marked
-    Vec_IntClear( vRes );
-    Vec_IntClear( vPiLits );
-    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
-    {
-        if ( Saig_ObjIsPi(pAig, pObj) )
-        {
-            Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
-            Vec_IntPush( vPiLits, Lit );
-            continue;
-        }
-        assert( Saig_ObjIsLo(pAig, pObj) );
-        if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
-            continue;
-        Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
-        Vec_IntPush( vRes, Lit );
-    }
-    if ( Vec_IntSize(vRes) == 0 )
-        Vec_IntPush(vRes, 0);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the resulting cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
-    for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
-        pBuff[i] = '-';
-    pBuff[i] = 0;
-    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
-        pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
-    if ( vCi2Rem )
-    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
-        pBuff[Aig_ObjPioNum(pObj)] = 'x';
-    printf( "%s\n", pBuff );
-    ABC_FREE( pBuff );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Shrinks values using ternary simulation.]
-
-  Description [The cube contains the set of flop index literals which,
-  when converted into a clause and applied to the combinational outputs, 
-  led to a satisfiable SAT run in frame k (values stored in the SAT solver).
-  If the cube is NULL, it is assumed that the first property output was
-  asserted and failed.
-  The resulting array is a set of flop index literals that asserts the COs.
-  Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
-    Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
-    Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
-    Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
-    Vec_Int_t * vCoObjs = p->vCoObjs;  // cone roots (CO obj IDs)
-    Vec_Int_t * vCiVals = p->vCiVals;  // cone leaf values (0/1 CI values)
-    Vec_Int_t * vCoVals = p->vCoVals;  // cone root values (0/1 CO values)
-    Vec_Int_t * vNodes  = p->vNodes;   // cone nodes (node obj IDs)
-    Vec_Int_t * vUndo   = p->vUndo;    // cone undos (node obj IDs)
-    Vec_Int_t * vVisits = p->vVisits;  // intermediate (obj IDs)
-    Vec_Int_t * vCi2Rem = p->vCi2Rem;  // CIs to be removed (CI obj IDs)
-    Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
-    Aig_Obj_t * pObj;
-    int i, Entry, RetValue;
-    int clk = clock();
-
-    // collect CO objects
-    Vec_IntClear( vCoObjs );
-    if ( pCube == NULL ) // the target is the property output
-        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); 
-    else // the target is the cube
-    {
-        for ( i = 0; i < pCube->nLits; i++ )
-        {
-            if ( pCube->Lits[i] == -1 )
-                continue;
-            pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
-            Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
-        }
-    }
-if ( p->pPars->fVeryVerbose )
-{
-printf( "Trying to justify cube " );
-if ( pCube )
-    Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
-else
-    printf( "<prop=fail>" );
-printf( " in frame %d.\n", k );
-}
-
-    // collect CI objects
-    Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
-    // collect values
-    Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
-    Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
-    // simulate for the first time
-if ( p->pPars->fVeryVerbose )
-Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
-    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
-    assert( RetValue );
-
-    // try removing high-priority flops
-    Vec_IntClear( vCi2Rem );
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
-    {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
-    }
-    // try removing low-priority flops
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
-    {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
-    }
-if ( p->pPars->fVeryVerbose )
-Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
-    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
-    assert( RetValue ); 
-
-    // derive the set of resulting registers
-    Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
-    assert( Vec_IntSize(vRes) > 0 );
-    p->tTsim += clock() - clk;
-    return Pdr_SetCreate( vRes, vPiLits );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c
deleted file mode 100644
index 1107aec7..00000000
--- a/src/sat/pdr/pdrUtil.c
+++ /dev/null
@@ -1,719 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [pdrUtil.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Property driven reachability.]
-
-  Synopsis    [Various utilities.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 20, 2010.]
-
-  Revision    [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetAlloc( int nSize )
-{
-    Pdr_Set_t * p;
-    assert( nSize >= 0 && nSize < (1<<30) );
-    p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
-{
-    Pdr_Set_t * p;
-    int i;
-    assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) );
-    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
-    p->nLits  = Vec_IntSize(vLits);
-    p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
-    p->nRefs  = 1;
-    p->Sign   = 0;
-    for ( i = 0; i < p->nLits; i++ )
-    {
-        p->Lits[i] = Vec_IntEntry(vLits, i);
-        p->Sign   |= ((word)1 << (p->Lits[i] % 63));
-    }
-    Vec_IntSelectSort( p->Lits, p->nLits );
-/*
-    for ( i = 0; i < p->nLits; i++ )
-        printf( "%d ", p->Lits[i] );
-    printf( "\n" );
-*/
-    // remember PI literals 
-    for ( i = p->nLits; i < p->nTotal; i++ )
-        p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
-{
-    Pdr_Set_t * p;
-    int i, k = 0;
-    assert( iRemove >= 0 && iRemove < pSet->nLits );
-    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
-    p->nLits  = pSet->nLits - 1;
-    p->nTotal = pSet->nTotal - 1;
-    p->nRefs  = 1;
-    p->Sign   = 0;
-    for ( i = 0; i < pSet->nTotal; i++ )
-    {
-        if ( i == iRemove )
-            continue;
-        p->Lits[k++] = pSet->Lits[i];
-        if ( i >= pSet->nLits )
-            continue;
-        p->Sign   |= ((word)1 << (pSet->Lits[i] % 63));
-    }
-    assert( k == p->nTotal );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
-{
-    Pdr_Set_t * p;
-    int i, k = 0;
-    assert( nLits >= 0 && nLits <= pSet->nLits );
-    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
-    p->nLits  = nLits;
-    p->nTotal = nLits + pSet->nTotal - pSet->nLits;
-    p->nRefs  = 1;
-    p->Sign   = 0;
-    for ( i = 0; i < nLits; i++ )
-    {
-        assert( pLits[i] >= 0 );
-        p->Lits[k++] = pLits[i];
-        p->Sign   |= ((word)1 << (pLits[i] % 63));
-    }
-    Vec_IntSelectSort( p->Lits, p->nLits );
-    for ( i = pSet->nLits; i < pSet->nTotal; i++ )
-        p->Lits[k++] = pSet->Lits[i];
-    assert( k == p->nTotal );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
-{
-    Pdr_Set_t * p;
-    int i;
-    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
-    p->nLits  = pSet->nLits;
-    p->nTotal = pSet->nTotal;
-    p->nRefs  = 1;
-    p->Sign   = pSet->Sign;
-    for ( i = 0; i < pSet->nTotal; i++ )
-        p->Lits[i] = pSet->Lits[i];
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p )
-{
-    p->nRefs++;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_SetDeref( Pdr_Set_t * p )
-{
-    if ( --p->nRefs == 0 )
-        ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
-{
-    char * pBuff;
-    int i, k, Entry;
-    pBuff = ABC_ALLOC( char, nRegs + 1 );
-    for ( i = 0; i < nRegs; i++ )
-        pBuff[i] = '-';
-    pBuff[i] = 0;
-    for ( i = 0; i < p->nLits; i++ )
-    {
-        if ( p->Lits[i] == -1 )
-            continue;
-        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
-    }
-    if ( vFlopCounts )
-    {
-        // skip some literals
-        k = 0;
-        Vec_IntForEachEntry( vFlopCounts, Entry, i )
-            if ( Entry ) 
-                pBuff[k++] = pBuff[i];
-        pBuff[k] = 0;
-    }
-    fprintf( pFile, "%s", pBuff );
-    ABC_FREE( pBuff );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Return 1 if pOld set-theoretically contains pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
-{
-    int * pOldInt, * pNewInt;
-    assert( pOld->nLits > 0 );
-    assert( pNew->nLits > 0 );
-    if ( pOld->nLits < pNew->nLits )
-        return 0;
-    if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
-        return 0;
-    pOldInt = pOld->Lits + pOld->nLits - 1;
-    pNewInt = pNew->Lits + pNew->nLits - 1;
-    while ( pNew->Lits <= pNewInt )
-    {
-        if ( pOld->Lits > pOldInt )
-            return 0;
-        assert( *pNewInt != -1 );
-        assert( *pOldInt != -1 );
-        if ( *pNewInt == *pOldInt )
-            pNewInt--, pOldInt--;
-        else if ( *pNewInt < *pOldInt )
-            pOldInt--;
-        else
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Return 1 if pOld set-theoretically contains pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
-{
-    int * pOldInt, * pNewInt;
-    assert( pOld->nLits > 0 );
-    assert( pNew->nLits > 0 );
-    pOldInt = pOld->Lits + pOld->nLits - 1;
-    pNewInt = pNew->Lits + pNew->nLits - 1;
-    while ( pNew->Lits <= pNewInt )
-    {
-        assert( *pOldInt != -1 );
-        if ( *pNewInt == -1 )
-        {
-            pNewInt--;
-            continue;
-        }
-        if ( pOld->Lits > pOldInt )
-            return 0;
-        assert( *pNewInt != -1 );
-        assert( *pOldInt != -1 );
-        if ( *pNewInt == *pOldInt )
-            pNewInt--, pOldInt--;
-        else if ( *pNewInt < *pOldInt )
-            pOldInt--;
-        else
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Return 1 if the state cube contains init state (000...0).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
-{
-    int i;
-    for ( i = 0; i < pCube->nLits; i++ )
-    {
-        assert( pCube->Lits[i] != -1 );
-        if ( i == iRemove )
-            continue;
-        if ( lit_sign( pCube->Lits[i] ) == 0 )
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
-{
-    Pdr_Set_t * p1 = *pp1;
-    Pdr_Set_t * p2 = *pp2;
-    int i;
-    for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
-    {
-        if ( p1->Lits[i] > p2->Lits[i] )
-            return -1;
-        if ( p1->Lits[i] < p2->Lits[i] )
-            return 1;
-    }
-    if ( i == p1->nLits && i < p2->nLits )
-        return -1;
-    if ( i < p1->nLits && i == p2->nLits )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
-{
-    Pdr_Obl_t * p;
-    p = ABC_ALLOC( Pdr_Obl_t, 1 );
-    p->iFrame = k;
-    p->prio   = prio;
-    p->nRefs  = 1;
-    p->pState = pState;
-    p->pNext  = pNext;
-    p->pLink  = NULL;
-    return p;    
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
-{
-    p->nRefs++;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_OblDeref( Pdr_Obl_t * p )
-{
-    if ( --p->nRefs == 0 )
-    {
-        if ( p->pNext )
-            Pdr_OblDeref( p->pNext );
-        Pdr_SetDeref( p->pState );
-        ABC_FREE( p );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_QueueIsEmpty( Pdr_Man_t * p )
-{
-    return p->pQueue == NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
-{
-    return p->pQueue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
-{
-    Pdr_Obl_t * pRes = p->pQueue;
-    if ( p->pQueue == NULL )
-        return NULL;
-    p->pQueue = p->pQueue->pLink;
-    Pdr_OblDeref( pRes );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
-{
-    Pdr_Obl_t * pTemp, ** ppPrev;
-    p->nObligs++;
-    Pdr_OblRef( pObl );
-    if ( p->pQueue == NULL )
-    {
-        p->pQueue = pObl;
-        return;
-    }
-    for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
-        if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
-            break;
-    *ppPrev = pObl;
-    pObl->pLink = pTemp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_QueuePrint( Pdr_Man_t * p )
-{
-    Pdr_Obl_t * pObl;
-    for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
-        printf( "Frame = %2d.  Prio = %8d.\n", pObl->iFrame, pObl->prio );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Pdr_QueueStop( Pdr_Man_t * p )
-{
-    Pdr_Obl_t * pObl;
-    while ( !Pdr_QueueIsEmpty(p) )
-    {
-        pObl = Pdr_QueuePop(p);
-        Pdr_OblDeref( pObl );
-    }
-    p->pQueue = NULL;
-}
-
-
-#define PDR_VAL0  1
-#define PDR_VAL1  2
-#define PDR_VALX  3
-
-/**Function*************************************************************
-
-  Synopsis    [Returns value (0 or 1) or X if unassigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
-{
-    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
-        return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0;
-    return PDR_VALX;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively searched for a satisfying assignment.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur )
-{
-    int Value0, Value1;
-    if ( Aig_ObjIsConst1(pNode) )
-        return 1;
-    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
-        return ((int)pNode->fMarkA == Value);
-    Aig_ObjSetTravIdCurrent(pAig, pNode);
-    pNode->fMarkA = Value;
-    if ( Aig_ObjIsPi(pNode) )
-    {
-//        if ( vSuppLits )
-//            Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
-        if ( Saig_ObjIsLo(pAig, pNode) )
-        {
-//            pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value );
-            pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value );
-            pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
-        }
-        return 1;
-    }
-    assert( Aig_ObjIsNode(pNode) );
-    // propagation
-    if ( Value ) 
-    {
-        if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) )
-            return 0;
-        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur);
-    }
-    // justification
-    Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
-    if ( Value0 == PDR_VAL0 )
-        return 1;
-    Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
-    if ( Value1 == PDR_VAL0 )
-        return 1;
-    if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 )
-        return 0;
-    if ( Value0 == PDR_VAL1 )
-        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
-    if ( Value1 == PDR_VAL1 )
-        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
-    assert( Value0 == PDR_VALX && Value1 == PDR_VALX );
-    // decision making
-//    if ( rand() % 10 == Heur )
-    if ( Aig_ObjId(pNode) % 4 == Heur )
-        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
-    else
-        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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-