Major restructuring of the code.

12 files changed, 3750 insertions, 0 deletions

diff --git a/src/proof/pdr/module.make b/src/proof/pdr/module.make
new file mode 100644
index 00000000..93fd8071
--- /dev/null
+++ b/src/proof/pdr/module.make
@@ -0,0 +1,8 @@
+SRC +=    src/proof/pdr/pdr.c \
+    src/proof/pdr/pdrCnf.c \
+    src/proof/pdr/pdrCore.c \
+    src/proof/pdr/pdrInv.c \
+    src/proof/pdr/pdrMan.c \
+    src/proof/pdr/pdrSat.c \
+    src/proof/pdr/pdrTsim.c \
+    src/proof/pdr/pdrUtil.c 
diff --git a/src/proof/pdr/pdr.c b/src/proof/pdr/pdr.c
new file mode 100644
index 00000000..6bdf75b5
--- /dev/null
+++ b/src/proof/pdr/pdr.c
@@ -0,0 +1,53 @@
+/**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/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
new file mode 100644
index 00000000..4f0f769e
--- /dev/null
+++ b/src/proof/pdr/pdr.h
@@ -0,0 +1,79 @@
+/**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 ABC__sat__pdr__pdr_h
+#define ABC__sat__pdr__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/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c
new file mode 100644
index 00000000..519384c5
--- /dev/null
+++ b/src/proof/pdr/pdrClass.c
@@ -0,0 +1,223 @@
+/**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 = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_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/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
new file mode 100644
index 00000000..fddd292b
--- /dev/null
+++ b/src/proof/pdr/pdrCnf.c
@@ -0,0 +1,357 @@
+/**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/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
new file mode 100644
index 00000000..025ada06
--- /dev/null
+++ b/src/proof/pdr/pdrCore.c
@@ -0,0 +1,722 @@
+/**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/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
new file mode 100644
index 00000000..baf4ca02
--- /dev/null
+++ b/src/proof/pdr/pdrInt.h
@@ -0,0 +1,198 @@
+/**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 ABC__sat__pdr__pdrInt_h
+#define ABC__sat__pdr__pdrInt_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "src/aig/saig/saig.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/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/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
new file mode 100644
index 00000000..30d1145d
--- /dev/null
+++ b/src/proof/pdr/pdrInv.c
@@ -0,0 +1,374 @@
+/**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 "pdrInt.h"
+#include "src/base/abc/abc.h"      // for Abc_NtkCollectCioNames()
+#include "src/base/main/main.h"    // for Abc_FrameReadGlobalFrame()
+
+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 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
+    // determine the starting point
+    LengthStart = Abc_MaxInt( 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 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
+            continue;
+        }
+        printf( " %d", Vec_PtrSize(vVec) );
+        Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
+        ThisSize += 1 + Abc_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/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
new file mode 100644
index 00000000..33c94d40
--- /dev/null
+++ b/src/proof/pdr/pdrMan.c
@@ -0,0 +1,194 @@
+/**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 );
+            Abc_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/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
new file mode 100644
index 00000000..c191654a
--- /dev/null
+++ b/src/proof/pdr/pdrSat.c
@@ -0,0 +1,373 @@
+/**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_MaxInt( 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/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
new file mode 100644
index 00000000..6fec1605
--- /dev/null
+++ b/src/proof/pdr/pdrTsim.c
@@ -0,0 +1,450 @@
+/**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/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
new file mode 100644
index 00000000..17383425
--- /dev/null
+++ b/src/proof/pdr/pdrUtil.c
@@ -0,0 +1,719 @@
+/**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, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+        if ( Saig_ObjIsLo(pAig, pNode) )
+        {
+//            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value );
+            pCube->Lits[pCube->nLits++] = Abc_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
+