Version abc80927

8 files changed, 329 insertions, 21 deletions

diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 6b748598..625d72d1 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -10,4 +10,5 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswSat.c \
     src/aig/ssw/sswSim.c \
     src/aig/ssw/sswSimSat.c \
-    src/aig/ssw/sswSweep.c
+    src/aig/ssw/sswSweep.c \
+    src/aig/ssw/sswUnique.c
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 98e8c9d7..766407d4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -53,6 +53,7 @@ struct Ssw_Pars_t_
     int              fSkipCheck;    // do not run equivalence check for unaffected cones
     int              fLatchCorr;    // perform register correspondence
     int              fSemiFormal;   // enable semiformal filtering
+    int              fUniqueness;   // enable uniqueness constraints
     int              fVerbose;      // verbose stats
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
@@ -82,11 +83,15 @@ struct Ssw_Cex_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== sswAbs.c ==========================================================*/
+extern Aig_Man_t *   Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
 /*=== sswCore.c ==========================================================*/
 extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
 extern void          Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
 extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 extern Aig_Man_t *   Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+/*=== sswLoc.c ==========================================================*/
+extern int           Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
 /*=== sswPart.c ==========================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 /*=== sswPairs.c ===================================================*/
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 424e3531..8052ffcd 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,7 +45,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nPartSize      =     0;  // size of the partition
     p->nOverSize      =     0;  // size of the overlap between partitions
     p->nFramesK       =     1;  // the induction depth
-    p->nFramesAddSim  =     2;  // additional frames to simulate
+    p->nFramesAddSim  =     0;  // additional frames to simulate
     p->nConstrs       =     0;  // treat the last nConstrs POs as seq constraints
     p->nBTLimit       =  1000;  // conflict limit at a node
     p->nMinDomSize    =   100;  // min clock domain considered for optimization
@@ -53,6 +53,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fSkipCheck     =     0;  // do not run equivalence check for unaffected cones
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fSemiFormal    =     0;  // enable semiformal filtering
+    p->fUniqueness    =     0;  // enable uniqueness constraints
     p->fVerbose       =     0;  // verbose stats
     // latch correspondence
     p->fLatchCorrOpt  =     0;  // performs optimized register correspondence
@@ -153,9 +154,9 @@ clk = clock();
             RetValue = Ssw_ManSweep( p );
             if ( p->pPars->fVerbose )
             {
-                printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
+                printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", 
                     nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
                 if ( p->pPars->fSkipCheck )
                     printf( "Use = %5d. Skip = %5d. ", 
                         p->nRefUse, p->nRefSkip );
@@ -165,7 +166,7 @@ clk = clock();
         Ssw_ManCleanup( p );
         if ( !RetValue )
             break;
-
+/*
         {
             static int Flag = 0;
             if ( Flag++ == 4 && nIter == 4 )
@@ -176,6 +177,7 @@ clk = clock();
                 Aig_ManStop( pSRed );
             }
         }
+*/
 
     } 
     p->pPars->nIters = nIter + 1;
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 5daffc75..636bd139 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -78,6 +78,10 @@ struct Ssw_Man_t_
     int              nRecycleCalls;  // the number of calls since last recycling
     int              nRecycles;      // the number of time SAT solver was recycled
     int              nConeMax;       // the maximum cone size
+    // uniqueness
+    Vec_Ptr_t *      vCommon;        // the set of common variables in the logic cones
+    int              iOutputLit;     // the output literal of the uniqueness constaint
+    int              nUniques;       // the number of uniqueness constaints used 
     // sequential simulator
     Ssw_Sml_t *      pSml;
     // counter example storage
@@ -205,10 +209,13 @@ extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame
 extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
 extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
 /*=== sswSweep.c ===================================================*/
+extern int           Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
 extern int           Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
 extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
 extern int           Ssw_ManSweep( Ssw_Man_t * p );
-
+/*=== sswUnique.c ===================================================*/
+extern int           Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int           Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index ba19d46e..d4a26f64 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -59,6 +59,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     // SAT solving (latch corr only)
     p->vUsedNodes    = Vec_PtrAlloc( 1000 );
     p->vUsedPis      = Vec_PtrAlloc( 1000 );
+    p->vCommon       = Vec_PtrAlloc( 100 );
+    p->iOutputLit    = -1;
     // allocate storage for sim pattern
     p->nPatWords     = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
     p->pPatWords     = ALLOC( unsigned, p->nPatWords ); 
@@ -190,6 +192,7 @@ void Ssw_ManStop( Ssw_Man_t * p )
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vUsedPis );
     Vec_IntFree( p->vSatVars );
+    Vec_PtrFree( p->vCommon );
     FREE( p->pNodeToFrames );
     FREE( p->pPatWords );
     free( p );
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 264b39d1..af3bf80e 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -42,7 +42,7 @@
 int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int pLits[2], RetValue, RetValue1, clk;//, status;
+    int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
     p->nSatCalls++;
 
     // sanity checks
@@ -59,8 +59,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
+    nLits = 2;
     pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
     pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+    if ( p->iOutputLit > -1 )
+        pLits[nLits++] = p->iOutputLit;
     if ( p->pPars->fPolarFlip )
     {
         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
@@ -75,16 +78,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
 
 clk = clock();
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, 
         (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
 p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
+        if ( nLits == 2 )
+        {
+            pLits[0] = lit_neg( pLits[0] );
+            pLits[1] = lit_neg( pLits[1] );
+            RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+            assert( RetValue );
+        }
         p->nSatCallsUnsat++;
     }
     else if ( RetValue1 == l_True )
@@ -109,8 +115,11 @@ p->timeSatUndec += clock() - clk;
 
     // solve under assumptions
     // A = 0; B = 1     OR     A = 0; B = 0 
+    nLits = 2;
     pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
     pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+    if ( p->iOutputLit > -1 )
+        pLits[nLits++] = p->iOutputLit;
     if ( p->pPars->fPolarFlip )
     {
         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
@@ -124,16 +133,19 @@ p->timeSatUndec += clock() - clk;
     }
 
 clk = clock();
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, 
         (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
 p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
+        if ( nLits == 2 )
+        {
+            pLits[0] = lit_neg( pLits[0] );
+            pLits[1] = lit_neg( pLits[1] );
+            RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+            assert( RetValue );
+        }
         p->nSatCallsUnsat++;
     }
     else if ( RetValue1 == l_True )
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index add00a88..b971a13a 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -87,14 +87,15 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
 {
     Aig_Obj_t * pObjFraig;
     int nVarNum, Value;
-    assert( Aig_ObjIsPi(pObj) );
+//    assert( Aig_ObjIsPi(pObj) );
     pObjFraig = Ssw_ObjFrame( p, pObj, f );
     nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
     Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+//    Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
 //    Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
     if ( p->pPars->fPolarFlip )
     {
@@ -120,7 +121,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
+        if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
             Aig_InfoSetBit( p->pPatWords, i );
 }
 
@@ -179,7 +180,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
     { 
         // if the fraiged nodes are the same, return
         if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-            return 0;
+            return 0; 
         // count the number of skipped calls
         if ( !pObj->fMarkA && !pObjRepr->fMarkA )
             p->nRefSkip++;
@@ -212,6 +213,18 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
         // disproved the equivalence
         Ssw_SmlSavePatternAig( p, f );
     }
+    if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && 
+        Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
+    {
+        if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
+        {
+            int RetValue;
+            assert( p->iOutputLit > -1 );
+            RetValue = Ssw_ManSweepNode( p, pObj, f, 0 );
+            p->iOutputLit = -1;
+            return RetValue;
+        }
+    }
     if ( p->pPars->nConstrs == 0 )
         Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
     else
@@ -300,6 +313,7 @@ int Ssw_ManSweep( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
     int nConstrPairs, clk, i, f;
+    int v;
 
     // perform speculative reduction
 clk = clock();
@@ -330,6 +344,8 @@ clk = clock();
         Ssw_ManSweepMarkRefinement( p );
 p->timeMarkCones += clock() - clk;
 
+//Ssw_ManUnique( p );
+
     // map constants and PIs of the last frame
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
@@ -338,10 +354,18 @@ p->timeMarkCones += clock() - clk;
     // make sure LOs are assigned
     Saig_ManForEachLo( p->pAig, pObj, i )
         assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
+////    
+    // bring up the previous frames
+    if ( p->pPars->fUniqueness )
+        for ( v = 0; v < f; v++ )
+            Saig_ManForEachLo( p->pAig, pObj, i )
+                Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
+////
     // sweep internal nodes
     p->fRefined = 0;
     p->nSatFailsReal = 0;
     p->nRefUse = p->nRefSkip = 0;
+    p->nUniques = 0;
     Ssw_ClassesClearRefined( p->ppClasses );
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
new file mode 100644
index 00000000..888ed3da
--- /dev/null
+++ b/src/aig/ssw/sswUnique.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [sswSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [On-demand uniqueness constraints.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the result of merging the two vectors.]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+{
+    Aig_Obj_t ** pBeg  = (Aig_Obj_t **)vArr->pArray;
+    Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
+    Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
+    Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
+    Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
+    Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
+    pBeg  = (Aig_Obj_t **)vArr->pArray;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( (*pBeg1)->Id == (*pBeg2)->Id )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( (*pBeg1)->Id < (*pBeg2)->Id )
+            *pBeg++ = *pBeg1++;
+        else 
+            *pBeg++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg++ = *pBeg2++;
+    vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
+    assert( vArr->nSize <= vArr->nCap );
+    assert( vArr->nSize >= vArr1->nSize );
+    assert( vArr->nSize >= vArr2->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the result of merging the two vectors.]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+{
+    Aig_Obj_t ** pBeg  = (Aig_Obj_t **)vArr->pArray;
+    Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
+    Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
+    Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
+    Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
+    Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
+    pBeg  = (Aig_Obj_t **)vArr->pArray;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( (*pBeg1)->Id == (*pBeg2)->Id )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( (*pBeg1)->Id < (*pBeg2)->Id )
+//            *pBeg++ = *pBeg1++;
+            pBeg1++;
+        else 
+//            *pBeg++ = *pBeg2++;
+            pBeg2++;
+    }
+//    while ( pBeg1 < pEnd1 )
+//        *pBeg++ = *pBeg1++;
+//    while ( pBeg2 < pEnd2 )
+//        *pBeg++ = *pBeg2++;
+    vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
+    assert( vArr->nSize <= vArr->nCap );
+    assert( vArr->nSize <= vArr1->nSize );
+    assert( vArr->nSize <= vArr2->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if uniqueness constraints can be added.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+{
+    int fVerbose = 0;
+    Aig_Obj_t * ppObjs[2], * pTemp;
+    Vec_Ptr_t * vSupp, * vSupp2;
+    int i, k, Value0, Value1, RetValue;
+    assert( p->pPars->nFramesK > 1 );
+
+    vSupp  = Vec_PtrAlloc( 100 );
+    vSupp2 = Vec_PtrAlloc( 100 );
+    Vec_PtrClear( p->vCommon );
+
+    // compute the first support in terms of LOs
+    ppObjs[0] = pRepr; 
+    ppObjs[1] = pObj;
+    Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
+    // modify support to be in terms of LIs
+    k = 0;
+    Vec_PtrForEachEntry( vSupp, pTemp, i )
+        if ( Saig_ObjIsLo(p->pAig, pTemp) )
+            Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
+    Vec_PtrShrink( vSupp, k );
+    // compute the support of support
+    Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
+    // return support to LO
+    Vec_PtrForEachEntry( vSupp, pTemp, i )
+        Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
+    // find the number of common vars
+    Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
+    Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
+    Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
+/*
+    {
+        Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
+        Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+        if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
+            printf( "Not unique!\n" );
+    }
+    {
+        Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
+        Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+        if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
+            printf( "Not unique!\n" );
+    }
+    {
+        Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
+        Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+        if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
+            printf( "Not unique!\n" );
+    }
+*/
+    if ( fVerbose )
+        printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d.  ",
+            Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
+
+    // check the current values
+    RetValue = 1;
+    Vec_PtrForEachEntry( p->vCommon, pTemp, i )
+    {
+        Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
+        Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
+        if ( Value0 != Value1 )
+            RetValue = 0;
+        if ( fVerbose )
+            printf( "%d", Value0 ^ Value1 );
+    }
+    if ( Vec_PtrSize(p->vCommon) == 0 )
+        RetValue = 0;
+    if ( fVerbose )
+        printf( "\n" );
+
+    Vec_PtrFree( vSupp );
+    Vec_PtrFree( vSupp2 );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the output of the uniqueness constraint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 )
+{
+    Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
+    int i, pLits[2];
+//    int RetValue;
+    assert( Vec_PtrSize(vCommon) > 0 );
+    // generate the constraint
+    pTotal = Aig_ManConst0(p->pFrames);
+    Vec_PtrForEachEntry( vCommon, pObj, i )
+    {
+        assert( Saig_ObjIsLo(p->pAig, pObj) );
+        pObj1New = Ssw_ObjFrame( p, pObj, f1 );
+        pObj2New = Ssw_ObjFrame( p, pObj, f2 );
+        pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
+        pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
+    }
+    if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
+    {
+//        printf( "Skipped\n" );
+        return 0;
+    }
+    p->nUniques++;
+    // create CNF
+    Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
+    // add output constraint
+    pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
+/*
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+    assert( RetValue );
+    // simplify the solver
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pSat);
+        assert( RetValue != 0 );
+    }
+*/
+    assert( p->iOutputLit == -1 );
+    p->iOutputLit = pLits[0];
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+