Unsuccessful attempt to improve PDR and a few minor changes.

.hgignore

@@ -15,6 +15,7 @@ docs/
 src/ext/
 src/xxx/
 src/aig/au/
+src/aig/ssm/
 
 *~
 *.orig

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"

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];                     }

src/aig/aig/aigJust.c

+/**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
+

src/aig/aig/aigPack.c

+/**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
+

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 \

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;

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
 

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                         ///

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.]
 

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.]
 

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.]
 

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.]
 

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
 

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.]
 

src/sat/pdr/pdrMan.c

 /**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 );

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;

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.]
 

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                                ///
 ////////////////////////////////////////////////////////////////////////