Unsuccessful attempt to improve PDR and a few minor changes.

20 files changed, 724 insertions, 354 deletions

diff --git a/.hgignore b/.hgignore
index 2c467f92..4aae48af 100644
--- a/.hgignore
+++ b/.hgignore
@@ -15,6 +15,7 @@ docs/
 src/ext/
 src/xxx/
 src/aig/au/
+src/aig/ssm/
 
 *~
 *.orig
diff --git a/abclib.dsp b/abclib.dsp
index 326bb6c1..eaef81e2 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3131,6 +3131,10 @@ SOURCE=.\src\aig\aig\aigInter.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigJust.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigMan.c
 # End Source File
 # Begin Source File
@@ -3155,6 +3159,10 @@ SOURCE=.\src\aig\aig\aigOrder.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigPack.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigPart.c
 # End Source File
 # Begin Source File
@@ -4179,10 +4187,6 @@ SOURCE=.\src\aig\au\auCec.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auCore.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\au\auCut.h
 # End Source File
 # Begin Source File
@@ -4207,10 +4211,6 @@ SOURCE=.\src\aig\au\auDec6.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auDiv.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\au\auDsdData.c
 # End Source File
 # Begin Source File
@@ -4255,6 +4255,10 @@ SOURCE=.\src\aig\au\auResCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auResCut.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auResDec.c
 # End Source File
 # Begin Source File
@@ -4298,6 +4302,10 @@ SOURCE=.\src\aig\au\auTruth.h
 SOURCE=.\src\aig\au\auUtil.c
 # End Source File
 # End Group
+# Begin Group "ssm"
+
+# PROP Default_Filter ""
+# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index f667d4e3..aa55f2fc 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -254,10 +254,17 @@ static inline int          Aig_WordFindFirstBit( unsigned uWord )
     return -1;
 }
 
-static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
-static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }
-static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
-static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int)((ABC_PTRUINT_T)(p) & 01);          }
+static inline int          Aig_Var2Lit( int Var, int fCompl )     { return Var + Var + fCompl;                       }
+static inline int          Aig_Lit2Var( int Lit )                 { return Lit >> 1;                                 }
+static inline int          Aig_LitIsCompl( int Lit )              { return Lit & 1;                                  }
+static inline int          Aig_LitNot( int Lit )                  { return Lit ^ 1;                                  }
+static inline int          Aig_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0);                       }
+static inline int          Aig_LitRegular( int Lit )              { return Lit & ~01;                                }
+
+static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
+static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int)((ABC_PTRUINT_T)(p) & 01);           }
 
 static inline int          Aig_ManPiNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PI];                     }
 static inline int          Aig_ManPoNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PO];                     }
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
new file mode 100644
index 00000000..c6b3a8c0
--- /dev/null
+++ b/src/aig/aig/aigJust.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+ 
+  FileName    [aigJust.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Justification of node values.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigJust.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define AIG_VAL0  1
+#define AIG_VAL1  2
+#define AIG_VALX  3
+
+// storing ternary values
+static inline int Aig_ObjSetTerValue( Aig_Obj_t * pNode, int Value )
+{
+    assert( Value );
+    pNode->fMarkA = (Value & 1);
+    pNode->fMarkB = ((Value >> 1) & 1);
+    return Value;
+}
+static inline int Aig_ObjGetTerValue( Aig_Obj_t * pNode )
+{
+    return (pNode->fMarkB << 1) | pNode->fMarkA;
+}
+
+// working with ternary values
+static inline int Aig_ObjNotTerValue( int Value )
+{
+    if ( Value == AIG_VAL1 )
+        return AIG_VAL0;
+    if ( Value == AIG_VAL0 )
+        return AIG_VAL1;
+    return AIG_VALX;
+}
+static inline int Aig_ObjAndTerValue( int Value0, int Value1 )
+{
+    if ( Value0 == AIG_VAL0 || Value1 == AIG_VAL0 )
+        return AIG_VAL0;
+    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
+        return AIG_VAL1;
+    return AIG_VALX;
+}
+static inline int Aig_ObjNotCondTerValue( int Value, int Cond )
+{
+    return Cond ? Aig_ObjNotTerValue( Value ) : Value;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value (0 or 1) or X if unassigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return (pNode->fMarkA ^ fCompl) ? AIG_VAL1 : AIG_VAL0;
+    return AIG_VALX;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively searched for a satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits, int Heur )
+{
+    int Value0, Value1;
+//    ++Heur;
+    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 ( Aig_ObjId(pNode) % 1000 == 0 )
+//            Value ^= 1;
+        if ( vSuppLits )
+            Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+        return 1;
+    }
+    assert( Aig_ObjIsNode(pNode) );
+    // propagation
+    if ( Value ) 
+    {
+        if ( !Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), vSuppLits, Heur) )
+            return 0;
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    }
+    // justification
+    Value0 = Aig_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
+    if ( Value0 == AIG_VAL0 )
+        return 1;
+    Value1 = Aig_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
+    if ( Value1 == AIG_VAL0 )
+        return 1;
+    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
+        return 0;
+    if ( Value0 == AIG_VAL1 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    if ( Value1 == AIG_VAL1 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
+    assert( Value0 == AIG_VALX && Value1 == AIG_VALX );
+    // decision making
+//    if ( rand() % 10 == Heur )
+//    if ( Aig_ObjId(pNode) % 8 == Heur )
+    if ( ++Heur % 8 == 0 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    else
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if SAT assignment is found; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjFindSatAssign( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits )
+{
+    int i;
+    if ( Aig_ObjIsPo(pNode) )
+        return Aig_ObjFindSatAssign( pAig, Aig_ObjFanin0(pNode), Value ^ Aig_ObjFaninC0(pNode), vSuppLits );
+    for ( i = 0; i < 8; i++ )
+    {
+        Vec_IntClear( vSuppLits );
+        Aig_ManIncrementTravId( pAig );
+        if ( Aig_NtkFindSatAssign_rec( pAig, pNode, Value, vSuppLits, i ) )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjTerSimulate_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode )
+{
+    int Value0, Value1;
+    if ( Aig_ObjIsConst1(pNode) )
+        return AIG_VAL1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return Aig_ObjGetTerValue( pNode );
+    Aig_ObjSetTravIdCurrent( pAig, pNode );
+    if ( Aig_ObjIsPi(pNode) )
+        return Aig_ObjSetTerValue( pNode, AIG_VALX );
+    Value0 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin0(pNode)), Aig_ObjFaninC0(pNode) );
+    if ( Aig_ObjIsPo(pNode) || Value0 == AIG_VAL0 )
+        return Aig_ObjSetTerValue( pNode, Value0 );
+    assert( Aig_ObjIsNode(pNode) );
+    Value1 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin1(pNode)), Aig_ObjFaninC1(pNode) );
+    return Aig_ObjSetTerValue( pNode, Aig_ObjAndTerValue(Value0, Value1) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value of the object under input assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLits )
+{
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    Aig_ManIncrementTravId( pAig );
+    Vec_IntForEachEntry( vSuppLits, Entry, i )
+    {
+        pObj = Aig_ManPi( pAig, Aig_Lit2Var(Entry) );
+        Aig_ObjSetTerValue( pObj, Aig_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
+        Aig_ObjSetTravIdCurrent( pAig, pObj );
+//printf( "%d ", Entry );
+    }
+//printf( "\n" );
+    return Aig_ObjTerSimulate_rec( pAig, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing of the framework.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManTerSimulate( Aig_Man_t * pAig )
+{
+    Vec_Int_t * vSuppLits;
+    Aig_Obj_t * pObj;
+    int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
+    int nTotalLits = 0;
+    vSuppLits = Vec_IntAlloc( 100 );
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        if ( pObj->fPhase ) // const 1
+        {
+            if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) )
+            {
+//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 );
+                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
+                    printf( "Justification error!\n" );
+                Count0++;
+                nTotalLits += Vec_IntSize(vSuppLits);
+            }
+            else
+                Count0f++;
+        }
+        else
+        {
+            if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) )
+            {
+//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 );
+                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
+                    printf( "Justification error!\n" );
+                Count1++;
+                nTotalLits += Vec_IntSize(vSuppLits);
+            }
+            else
+                Count1f++;
+        }
+    }
+    Vec_IntFree( vSuppLits );
+    printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ", 
+        Aig_ManPoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManPoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
+    Abc_PrintTime( 1, "T", clock() - clk );
+    Aig_ManCleanMarkAB( pAig );
+}
+
+
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c
new file mode 100644
index 00000000..8d7b54df
--- /dev/null
+++ b/src/aig/aig/aigPack.c
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+ 
+  FileName    [aigPack.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Bit-packing code.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigPack.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 03504138..c291433f 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -6,12 +6,14 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
     src/aig/aig/aigInter.c \
+    src/aig/aig/aigJust.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigMffc.c \
     src/aig/aig/aigObj.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigOrder.c \
+    src/aig/aig/aigPack.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigPartReg.c \
     src/aig/aig/aigPartSat.c \
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index 05db377d..1d9efca1 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -344,32 +344,6 @@ static inline int Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntSelectSort( int * pArray, int nSize )
-{
-    int temp, i, j, best_i;
-    for ( i = 0; i < nSize-1; i++ )
-    {
-        best_i = i;
-        for ( j = i+1; j < nSize; j++ )
-            if ( pArray[j] < pArray[best_i] )
-                best_i = j;
-        temp = pArray[i]; 
-        pArray[i] = pArray[best_i]; 
-        pArray[best_i] = temp;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fast mapping for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline int Vec_IntRemoveDup( int * pArray, int nSize )
 {
     int i, k;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 415e2797..b100ba19 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8418,68 +8418,49 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Abc_Ntk_t * pNtkRes = NULL;
+    int nCutMax      =  1;
+    int nLeafMax     = 10;
+    int nDivMax      = 50;
+    int nDecMax      =  3;
+    int fVerbose     =  0;
+    int fVeryVerbose =  0;
     int c;
-    int fBmc;
-    int nFrames;
-    int nLevels;
-    int fVerbose;
-    int fVeryVerbose;
-//    char * pFileName;
-
-//    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
-//    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
-//    extern int Pr_ManProofTest( char * pFileName );
-    extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
-    extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
-    extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
-//    extern void Abc_NtkDarTestBlif( char * pFileName );
-//    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
-//    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
-    extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
-    extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num );
-//    extern void Aig_ProcedureTest();
-    extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
-    extern void Amap_LibertyTest( char * pFileName );
-    extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
-    extern void Bbl_ManSimpleDemo();
-    extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
-    extern void Abc_NktMffcTest( Abc_Ntk_t * pNtk );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-
-
-
-//    Abc_Print( -1, "This command is temporarily disabled.\n" );
-//    return 0;
-
-    // set defaults
-    fVeryVerbose = 0;
-    fVerbose = 1;
-    fBmc     = 0;
-    nFrames  = 1;
-    nLevels  = 10;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
+        case 'C':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFrames = atoi(argv[globalUtilOptind]);
+            nCutMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames < 0 ) 
+            if ( nCutMax < 0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLeafMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLeafMax < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nDivMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nDivMax < 0 ) 
                 goto usage;
             break;
         case 'N':
@@ -8488,14 +8469,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nLevels = atoi(argv[globalUtilOptind]);
+            nDecMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nLevels < 0 ) 
+            if ( nDecMax < 0 ) 
                 goto usage;
             break;
-        case 'b':
-            fBmc ^= 1;
-            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8508,12 +8486,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-
+/*
     if ( pNtk == NULL )
     {
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
+*/
 /*
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
@@ -8521,79 +8500,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 */
-//    if ( fBmc )
-//        Abc_NtkBddDec( pNtk, 1 );
-//    else
-//        Abc_NktMffcTest( pNtk );
-//    Abc_NtkDarTest( pNtk, nLevels );
-
-//    Abc_NtkTestEsop( pNtk );
-//    Abc_NtkTestSop( pNtk );
-//    Abc_Print( -1, "This command is currently not used.\n" );
-    // run the command
-//    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
-//    pNtkRes = Abc_NtkNewAig( pNtk );
-
-/*
-    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-//    if ( Cut_CellIsRunning() )
-//        Cut_CellDumpToFile();
-//    else
-//        Cut_CellPrecompute();
-//        Cut_CellLoad();
-/*
-        {
-            Abc_Ntk_t * pNtkRes;
-            extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
-            pNtkRes = Abc_NtkTopmost( pNtk, nLevels );
-            Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-        }
-*/
-//    Abc_NtkSimulteBuggyMiter( pNtk );
-
-//    Rwr_Temp();
-//    Abc_MvExperiment();
-//    Ivy_TruthTest();
-
-
-//    Ivy_TruthEstimateNodesTest();
-/*
-    pNtkRes = Abc_NtkIvy( pNtk );
-//    pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
-//    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-//    Abc_NtkMaxFlowTest( pNtk );
-//    Pr_ManProofTest( "trace.cnf" );
-
-//    Abc_NtkCompareSupports( pNtk );
-//    Abc_NtkCompareCones( pNtk );
-/*
-    {
-        extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
-        Vec_Vec_t * vParts;
-        vParts = Abc_NtkPartitionSmart( pNtk, 1 );
-        Vec_VecFree( vParts );
-    }
-*/
-//    Abc_Ntk4VarTable( pNtk );
-//    Dar_NtkGenerateArrays( pNtk );
-//    Dar_ManDeriveCnfTest2();
 /*
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -8602,150 +8508,37 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 /*
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
-        return 0;
-    }
-*/
-/*
-    if ( Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Currently only works for logic circuits.\n" );
-        return 0;
-    }
-*/
-
-
-/*
-//    pNtkRes = Abc_NtkDar( pNtk );
-//    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); 
-//    pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
-    pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
-//    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-*/
-
-
-//    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
-/*
-    if ( globalUtilOptind != 1 )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    Abc_NtkDarTestBlif( argv[globalUtilOptind] );
-*/
-
-//    Abc_NtkDarPartition( pNtk );
-//Abc_NtkDarTest( pNtk );
-//Abc_NtkWriteAig( pNtk, NULL );
-
-
-/*
-//    pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
-    pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-/*
-    pNtkRes = Abc_NtkDarTestNtk( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-//Amap_LibertyTest( "bwrc.lib" );
-
-//    Abc_NtkDarTest( pNtk );
-
-//    Bbl_ManTest( pNtk );
-/*
+    if ( pNtk )
     {
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    extern void Aig_ManComputeDomsForCofactoring( Aig_Man_t * p );
-    Aig_Man_t * pAig;
-    pAig = Abc_NtkToDar( pNtk, 0, 0 );
-    Aig_ManComputeDomsForCofactoring( pAig );
-    Aig_ManStop( pAig );
+        extern Abc_Ntk_t * Au_ManPerformTest( Abc_Ntk_t * p, int nCutMax, int nLeafMax, int nDivMax, int nDecMax, int fVerbose, int fVeryVerbose );
+        Abc_Ntk_t * pNtkRes = Au_ManPerformTest( pNtk, nCutMax, nLeafMax, nDivMax, nDecMax, fVerbose, fVeryVerbose );
+        if ( pNtkRes == NULL )
+        {
+            Abc_Print( -1, "Command has failed.\n" );
+            return 1;
+        }
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
 */
-
 /*
-    if ( Abc_NtkIsStrash(pNtk) )
     {
-        extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
-        pNtkRes = Au_ManTransformTest( pNtk );
-    }
-    else
-    {
-        extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig );
-        pNtkRes = Au_ManResubTest( pNtk );
-    }
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
+        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
+        Aig_ManTerSimulate( pAig );
+        Aig_ManStop( pAig );
     }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-/*
-{
-    extern int Au_DsdVecTest( int nVars );
-    Au_DsdVecTest( 6 );
-}
 */
-
-{
-//    extern void Au_Sat3DeriveImpls();
-//    Au_Sat3DeriveImpls();
-//    extern void Au_Sat3DeriveJusts();
-//    Au_Sat3DeriveJusts();
-}
-
-{
-//    extern void Au_NtkReadFour( Abc_Ntk_t * pNtk );
-//    extern void Au_Data4VerifyFour();
-//    Au_NtkReadFour( pNtk );
-//    Au_Data4VerifyFour();
-}
-
-
-//    Abc_NtkCheckAbsorb( pNtk, 4 );
-/*
-    if ( fBmc )
-        Abc_NktMffcServerTest( pNtk );
-    else
-        Abc_ResPartitionTest( pNtk );
-*/
-//    Abc_NtkHelloWorld( pNtk );
-//    Abc_NktMffcTest( pNtk );
-//    Abc_NktMffcServerTest( pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: test [-h] <file_name>\n" );
+    Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
     Abc_Print( -2, "\t         testbench for new procedures\n" );
-//    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-//    Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax );
+    Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax );
+    Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax );
+    Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 6fcce5c6..318afd35 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1123,6 +1123,32 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSelectSort( int * pArray, int nSize )
+{
+    int temp, i, j, best_i;
+    for ( i = 0; i < nSize-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nSize; j++ )
+            if ( pArray[j] < pArray[best_i] )
+                best_i = j;
+        temp = pArray[i]; 
+        pArray[i] = pArray[best_i]; 
+        pArray[best_i] = temp;
+    }
+}
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index e888e4cf..83c334b4 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -102,26 +102,26 @@ struct Vec_Vec_t_
         Vec_PtrForEachEntry( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) 
 
 // iteratores through entries
-#define Vec_VecForEachEntryInt( Type, vGlob, Entry, i, k )                                    \
+#define Vec_VecForEachEntryInt( vGlob, Entry, i, k )                                          \
     for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
-        Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
-#define Vec_VecForEachEntryIntLevel( Type, vGlob, Entry, i, Level )                           \
-        Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, Level), Entry, i ) 
-#define Vec_VecForEachEntryIntStart( Type, vGlob, Entry, i, k, LevelStart )                   \
+        Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+#define Vec_VecForEachEntryIntLevel( vGlob, Entry, i, Level )                                 \
+        Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, Level), Entry, i ) 
+#define Vec_VecForEachEntryIntStart( vGlob, Entry, i, k, LevelStart )                         \
     for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
-        Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
-#define Vec_VecForEachEntryIntStartStop( Type, vGlob, Entry, i, k, LevelStart, LevelStop )    \
+        Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+#define Vec_VecForEachEntryIntStartStop( vGlob, Entry, i, k, LevelStart, LevelStop )          \
     for ( i = LevelStart; i < LevelStop; i++ )                                                \
-        Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
-#define Vec_VecForEachEntryIntReverse( Type, vGlob, Entry, i, k )                             \
+        Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+#define Vec_VecForEachEntryIntReverse( vGlob, Entry, i, k )                                   \
     for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
-        Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
-#define Vec_VecForEachEntryIntReverseReverse( Type, vGlob, Entry, i, k )                      \
+        Vec_IntForEachEntryReverse( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+#define Vec_VecForEachEntryIntReverseReverse( vGlob, Entry, i, k )                            \
     for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- )                                           \
-        Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
-#define Vec_VecForEachEntryIntReverseStart( Type, vGlob, Entry, i, k, LevelStart )            \
+        Vec_IntForEachEntryReverse( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+#define Vec_VecForEachEntryIntReverseStart( vGlob, Entry, i, k, LevelStart )                  \
     for ( i = LevelStart-1; i >= 0; i-- )                                                     \
-        Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
+        Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) 
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
index 27e76b6e..740eb46f 100644
--- a/src/sat/pdr/pdr.h
+++ b/src/sat/pdr/pdr.h
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [External declarations.]
 
diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c
index 31449735..3e990958 100644
--- a/src/sat/pdr/pdrClass.c
+++ b/src/sat/pdr/pdrClass.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Equivalence classes of register outputs.]
 
diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
index b40ed6d9..2c5218d8 100644
--- a/src/sat/pdr/pdrCnf.c
+++ b/src/sat/pdr/pdrCnf.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [CNF computation on demand.]
 
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 742ce381..6289889b 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Core procedures.]
 
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
index d0211278..1eadcf93 100644
--- a/src/sat/pdr/pdrInt.h
+++ b/src/sat/pdr/pdrInt.h
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Internal declarations.]
 
@@ -92,6 +92,8 @@ struct Pdr_Man_t_
     Vec_Int_t * vVisits;   // intermediate
     Vec_Int_t * vCi2Rem;   // CIs to be removed
     Vec_Int_t * vRes;      // final result
+    Vec_Int_t * vSuppLits; // support literals
+    Pdr_Set_t * pCubeJust; // justification
     // statistics
     int         nBlocks;   // the number of times blockState was called
     int         nObligs;   // the number of proof obligations derived
@@ -101,6 +103,10 @@ struct Pdr_Man_t_
     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;
@@ -133,6 +139,8 @@ 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( 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 );
@@ -156,6 +164,7 @@ extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube
 /*=== 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 );
@@ -163,6 +172,7 @@ 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 );
@@ -175,6 +185,7 @@ 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
 
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
index daf542e9..a60732cb 100644
--- a/src/sat/pdr/pdrInv.c
+++ b/src/sat/pdr/pdrInv.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Invariant computation, printing, verification.]
 
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
index 97f0992b..95a38efb 100644
--- a/src/sat/pdr/pdrMan.c
+++ b/src/sat/pdr/pdrMan.c
@@ -1,10 +1,10 @@
 /**CFile****************************************************************
 
-  FileName    [pdr.c]
+  FileName    [pdrMan.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Manager procedures.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - November 20, 2010.]
 
-  Revision    [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -65,6 +65,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
     p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
     p->vRes     = Vec_IntAlloc( 100 );  // final result
+    p->vSuppLits= Vec_IntAlloc( 100 );  // support literals
+    p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
@@ -90,6 +92,7 @@ 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", 
@@ -104,7 +107,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
         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 );
@@ -125,17 +128,19 @@ void Pdr_ManStop( Pdr_Man_t * p )
     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_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 );
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
index 45ada5c0..4ba22e84 100644
--- a/src/sat/pdr/pdrSat.c
+++ b/src/sat/pdr/pdrSat.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [SAT solver procedures.]
 
@@ -307,6 +307,24 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         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;
diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c
index 01b54e3f..ae457352 100644
--- a/src/sat/pdr/pdrTsim.c
+++ b/src/sat/pdr/pdrTsim.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Ternary simulation.]
 
diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c
index 7e83102b..a568a2d5 100644
--- a/src/sat/pdr/pdrUtil.c
+++ b/src/sat/pdr/pdrUtil.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Netlist representation.]
+  PackageName [Property driven reachability.]
 
   Synopsis    [Various utilities.]
 
@@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Performs fast mapping for one node.]
+  Synopsis    []
 
   Description []
                
@@ -43,19 +43,12 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntSelectSort( int * pArray, int nSize )
+Pdr_Set_t * Pdr_SetAlloc( int nSize )
 {
-    int temp, i, j, best_i;
-    for ( i = 0; i < nSize-1; i++ )
-    {
-        best_i = i;
-        for ( j = i+1; j < nSize; j++ )
-            if ( pArray[j] < pArray[best_i] )
-                best_i = j;
-        temp = pArray[i]; 
-        pArray[i] = pArray[best_i]; 
-        pArray[best_i] = temp;
-    }
+    Pdr_Set_t * p;
+    assert( nSize < (1<<15) );
+    p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
+    return p;
 }
 
 /**Function*************************************************************
@@ -301,6 +294,46 @@ int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
 
 /**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 []
@@ -538,6 +571,145 @@ void Pdr_QueueStop( Pdr_Man_t * p )
     p->pQueue = NULL;
 }
 
+
+#define PDR_VAL0  1
+#define PDR_VAL1  2
+#define PDR_VALX  3
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value (0 or 1) or X if unassigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0;
+    return PDR_VALX;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively searched for a satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur )
+{
+    int Value0, Value1;
+    if ( Aig_ObjIsConst1(pNode) )
+        return 1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return ((int)pNode->fMarkA == Value);
+    Aig_ObjSetTravIdCurrent(pAig, pNode);
+    pNode->fMarkA = Value;
+    if ( Aig_ObjIsPi(pNode) )
+    {
+//        if ( vSuppLits )
+//            Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+        if ( Saig_ObjIsLo(pAig, pNode) )
+        {
+//            pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value );
+            pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value );
+            pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
+        }
+        return 1;
+    }
+    assert( Aig_ObjIsNode(pNode) );
+    // propagation
+    if ( Value ) 
+    {
+        if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) )
+            return 0;
+        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur);
+    }
+    // justification
+    Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
+    if ( Value0 == PDR_VAL0 )
+        return 1;
+    Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
+    if ( Value1 == PDR_VAL0 )
+        return 1;
+    if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 )
+        return 0;
+    if ( Value0 == PDR_VAL1 )
+        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
+    if ( Value1 == PDR_VAL1 )
+        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
+    assert( Value0 == PDR_VALX && Value1 == PDR_VALX );
+    // decision making
+//    if ( rand() % 10 == Heur )
+    if ( Aig_ObjId(pNode) % 4 == Heur )
+        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
+    else
+        return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if SAT assignment is found; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+    Aig_Obj_t * pNode;
+    int i, v, fCompl;
+//    return 0;
+    for ( i = 0; i < 4; i++ )
+    {
+        // derive new assignment
+        p->pCubeJust->nLits = 0;
+        p->pCubeJust->Sign  = 0;
+        Aig_ManIncrementTravId( p->pAig );
+        for ( v = 0; v < pCube->nLits; v++ )
+        {
+            if ( pCube->Lits[v] == -1 )
+                continue;
+            pNode  = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) );
+            fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode);
+            if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) )
+                break;
+        }
+        if ( v < pCube->nLits )
+            continue;
+        // figure this out!!!
+        if ( p->pCubeJust->nLits == 0 )
+            continue;
+        // successfully derived new assignment
+        Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits );
+        // check assignment against this cube
+        if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) )
+            continue;
+//printf( "\n" );
+//Pdr_SetPrint( stdout, pCube,        Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
+//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
+        // check assignment against the clauses
+        if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) )
+            continue;
+        // find good assignment
+        return 1;
+    }
+    return 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////