Version abc80927

17 files changed, 914 insertions, 26 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index fcaf41fa..503985b7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -480,6 +480,7 @@ extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
 /*=== aigDup.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManDupSimple( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupSimpleDfs( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
 extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index c6a4d19a..9fb19b36 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -194,6 +194,43 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates part of the AIG manager.]
+
+  Description [Orders nodes as follows: PIs, ANDs, POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
+    Vec_PtrForEachEntry( vPis, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Vec_PtrForEachEntry( vPos, pObj, i )
+    {
+        pObjNew = Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+        pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+        Aig_ObjCreatePo( pNew, pObjNew );
+    }
+    Aig_ManSetRegNum( pNew, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG manager.]
 
   Description [Assumes topological ordering of the nodes.]
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 232a789e..dce34600 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -56,6 +56,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fInterpolation    =   1;  // enables interpolation
     p->fReachability     =   1;  // enables BDD based reachability
     p->fStopOnFirstFail  =   1;  // enables stopping after first output of a miter has failed to prove
+    p->fUseNewProver     =   0;  // enables new prover
     p->fSilent           =   0;  // disables all output
     p->fVerbose          =   0;  // enables verbose reporting of statistics
     p->fVeryVerbose      =   0;  // enables very verbose reporting  
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index b09091fb..c3c0a1b6 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,10 @@
-SRC +=    src/aig/saig/saigBmc.c \
+SRC +=    src/aig/saig/saigAbs.c \
+    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigDup.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigIoa.c \
+    src/aig/saig/saigLoc.c \
     src/aig/saig/saigMiter.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 81f0fcf5..c7a40f96 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -84,6 +84,7 @@ extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigDup.c ==========================================================*/
 extern Aig_Man_t *       Said_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t *       Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigIoa.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
new file mode 100644
index 00000000..48a26a3c
--- /dev/null
+++ b/src/aig/saig/saigAbs.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+  FileName    [saigAbs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Proof-based abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+#include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                       { return ppMap[nFrames*pObj->Id + i];  }
+static inline void        Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for BMC.]
+
+  Description [The resulting manager is combinational. The only PO is
+  the output of the last frame.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t ** ppMap;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start the mapping
+    ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
+    // start the manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ManConst0( pFrames );
+        Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
+    }
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // map the constant node
+        Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+        Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // create POs for this frame
+        if ( f == nFrames - 1 )
+        {
+            Saig_ManForEachPo( pAig, pObj, i )
+            {
+                pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+                Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+            }
+            break;
+        }
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
+        }
+    }
+    Aig_ManCleanup( pFrames );
+    // remove mapping for the nodes that are no longer there
+    for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
+        if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
+            ppMap[i] = NULL;
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the set of variables involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose )
+{
+    void * pSatCnf; 
+    Intp_Man_t * pManProof;
+    sat_solver * pSat;
+    Vec_Int_t * vCore;
+    int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
+    int i, RetValue;
+    // create the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat ); 
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+        {
+            printf( "The BMC problem is trivially UNSAT.\n" );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    sat_solver_store_mark_roots( pSat ); 
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+    if ( RetValue == l_Undef )
+    {
+        printf( "Conflict limit is reached.\n" );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+    if ( RetValue == l_True )
+    {
+        printf( "The BMC problem is SAT.\n" );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+    printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    sat_solver_delete( pSat );
+    // derive the UNSAT core
+    pManProof = Intp_ManAlloc();
+    vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
+    Intp_ManFree( pManProof );
+    Sto_ManFree( pSatCnf );
+    // derive the set of variables on which the core depends
+    // collect the variable numbers
+    nVars = 0;
+    pVars = ALLOC( int, pCnf->nVars );
+    memset( pVars, 0, sizeof(int) * pCnf->nVars );
+    Vec_IntForEachEntry( vCore, iClause, i )
+    {
+        pClause1 = pCnf->pClauses[iClause];
+        pClause2 = pCnf->pClauses[iClause+1];
+        for ( pLit = pClause1; pLit < pClause2; pLit++ )
+        {
+            if ( pVars[ (*pLit) >> 1 ] == 0 )
+                nVars++;
+            pVars[ (*pLit) >> 1 ] = 1;
+            if ( fVerbose )
+            printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
+        }
+        if ( fVerbose )
+        printf( "\n" );
+    }
+    Vec_IntFree( vCore );
+    return pVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels nodes with the given CNF variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
+{
+    int iVarThis = pCnf->pVarNums[pObj->Id];
+    if ( iVarThis >= 0 && iVarThis != iVar )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
+    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
+    pCnf->pVarNums[pObj->Id] = iVar;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
+{
+    Cnf_Dat_t * pCnf;
+    Vec_Int_t * vFlops;
+    Aig_Man_t * pFrames, * pResult;
+    Aig_Obj_t ** ppAigToFrames;
+    Aig_Obj_t * pObj, * pObjFrame;
+    int f, i, * pUnsatCoreVars, clk = clock();
+    assert( Saig_ManPoNum(p) == 1 );
+    Aig_ManSetPioNumbers( p );
+    if ( fVerbose )
+        printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
+    // create the timeframes
+    pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
+    // convert them into CNF
+//    pCnf = Cnf_Derive( pFrames, 0 );
+    pCnf = Cnf_DeriveSimple( pFrames, 0 );
+    // collect CNF variables involved in UNSAT core
+    pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 );
+    if ( pUnsatCoreVars == NULL )
+    {
+        Aig_ManStop( pFrames );
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+    if ( fVerbose )
+    {
+        int Counter = 0;
+        for ( i = 0; i < pCnf->nVars; i++ )
+            Counter += pUnsatCoreVars[i];
+        printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
+    }
+    // map other nodes into existing CNF variables
+    Aig_ManForEachNode( pFrames, pObj, i )
+        if ( pCnf->pVarNums[pObj->Id] >= 0 )
+            Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
+    // collect relevant registers
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Saig_ManForEachLo( p, pObj, i )
+        {
+            pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
+            if ( pObjFrame == NULL )
+                continue;
+            pObjFrame = Aig_Regular(pObjFrame);
+            if ( Aig_ObjIsConst1( pObjFrame ) )
+                continue;
+            assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
+            if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
+                pObj->fMarkA = 1;
+        }
+    }
+    // collect the flops
+    vFlops = Vec_IntAlloc( 1000 );
+    Saig_ManForEachLo( p, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            Vec_IntPush( vFlops, i );
+        }
+    if ( fVerbose )
+    {
+        printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
+        PRT( "Time", clock() - clk );
+    }
+    // create the resulting AIG
+    pResult = Saig_ManAbstraction( p, vFlops );
+    // cleanup
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    free( ppAigToFrames );
+    free( pUnsatCoreVars );
+    Vec_IntFree( vFlops );
+    return pResult;
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index f03364a4..baf00241 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -34,8 +34,7 @@
 
   Synopsis    [Create timeframes of the manager for BMC.]
 
-  Description [The resulting manager is combinational. The primary inputs
-  corresponding to register outputs are ordered first. POs correspond to \
+  Description [The resulting manager is combinational. POs correspond to \
   the property outputs in each time-frame.]
                
   SideEffects []
@@ -106,8 +105,7 @@ int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 
   Synopsis    [Create timeframes of the manager for BMC.]
 
-  Description [The resulting manager is combinational. The primary inputs
-  corresponding to register outputs are ordered first. POs correspond to 
+  Description [The resulting manager is combinational. POs correspond to 
   the property outputs in each time-frame.
   The unrolling is stopped as soon as the number of nodes in the frames
   exceeds the given maximum size.]
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 1a050741..165a08f2 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -67,6 +67,66 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
     return pAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Numbers of flops included in the abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
+{
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, Entry;
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // label included flops
+    Vec_IntForEachEntry( vFlops, Entry, i )
+    {
+        pObjLi = Saig_ManLi( pAig, Entry );
+        assert( pObjLi->fMarkA == 0 );
+        pObjLi->fMarkA = 1;
+        pObjLo = Saig_ManLo( pAig, Entry );
+        assert( pObjLo->fMarkA == 0 );
+        pObjLo->fMarkA = 1;
+    }
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( !pObj->fMarkA )
+            pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // create variables for LOs
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            pObj->pData = Aig_ObjCreatePi( pAigNew );
+        }
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create POs
+    Aig_ManForEachPo( pAig, pObj, i )
+        if ( !pObj->fMarkA )
+            Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // create LIs
+    Aig_ManForEachPo( pAig, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+        }
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
+    return pAigNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigLoc.c b/src/aig/saig/saigLoc.c
new file mode 100644
index 00000000..60c547dd
--- /dev/null
+++ b/src/aig/saig/saigLoc.c
@@ -0,0 +1,169 @@
+/**CFile****************************************************************
+
+  FileName    [saigLoc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Localization package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigLoc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs localization by unrolling timeframes backward.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose )
+{
+    sat_solver * pSat;
+    Vec_Int_t * vTopVarNums;
+    Vec_Ptr_t * vTop, * vBot;
+    Cnf_Dat_t * pCnfTop, * pCnfBot;
+    Aig_Man_t * pPartTop, * pPartBot;
+    Aig_Obj_t * pObj, * pObjBot;
+    int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
+    assert( Saig_ManPoNum(p) == 1 );
+    Aig_ManSetPioNumbers( p );
+
+    // start the top by including the PO
+    vBot = Vec_PtrAlloc( 100 );
+    vTop = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
+    // create the manager composed of one PI/PO pair
+    pPartTop = Aig_ManStart( 10 );
+    Aig_ObjCreatePo( pPartTop, Aig_ObjCreatePi(pPartTop) );
+    pCnfTop = Cnf_Derive( pPartTop, 0 );
+    // start the array of CNF variables
+    vTopVarNums = Vec_IntAlloc( 100 );
+    Vec_IntPush( vTopVarNums, pCnfTop->pVarNums[Aig_ManPi(pPartTop,0)->Id] );
+    // start the solver
+    pSat = Cnf_DataWriteIntoSolver( pCnfTop, 1, 0 );
+
+    // iterate backward unrolling
+    RetValue = -1;
+    nSatVarNum = pCnfTop->nVars;
+    if ( fVerbose )
+        printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
+    for ( f = 0; ; f++ )
+    { 
+        clk = clock();
+        // get the bottom
+        Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
+        // derive AIG for the part between top and bottom
+        pPartBot = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
+        // convert it into CNF
+        pCnfBot = Cnf_Derive( pPartBot, Aig_ManPoNum(pPartBot) );
+        Cnf_DataLift( pCnfBot, nSatVarNum );
+        nSatVarNum += pCnfBot->nVars;
+        // stitch variables of top and bot
+        assert( Aig_ManPoNum(pPartBot) == Vec_IntSize(vTopVarNums) );
+        Aig_ManForEachPo( pPartBot, pObjBot, i )
+        {
+            Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i),   0 );
+            Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i),   1 );
+            Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+        // add CNF to the SAT solver
+        for ( i = 0; i < pCnfBot->nClauses; i++ )
+            if ( !sat_solver_addclause( pSat, pCnfBot->pClauses[i], pCnfBot->pClauses[i+1] ) )
+                break;
+        if ( i < pCnfBot->nClauses )
+        {
+//            printf( "SAT solver became UNSAT after adding clauses.\n" );
+            RetValue = 1;
+            break;
+        }
+        // run the SAT solver
+        nConfPrev = pSat->stats.conflicts;
+        status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
+        if ( fVerbose )
+        {
+            printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
+                f+1, Aig_ManPiNum(pPartBot), Aig_ManPoNum(pPartBot), Aig_ManNodeNum(pPartBot), 
+                nSatVarNum, pSat->stats.conflicts-nConfPrev );
+            PRT( "Time", clock() - clk );
+        }
+        if ( status == l_Undef )
+            break;
+        if ( status == l_False )
+        {
+            RetValue = 1;
+            break;
+        }
+        assert( status == l_True );
+        if ( f == nFramesMax - 1 )
+            break;
+        // the problem is SAT - add more clauses
+        // create new set of POs to derive new top
+        Vec_PtrClear( vTop );
+        Vec_IntClear( vTopVarNums );
+        Vec_PtrForEachEntry( vBot, pObj, i )
+        {
+            assert( Aig_ObjIsPi(pObj) );
+            if ( Saig_ObjIsLo(p, pObj) )
+            {
+                pObjBot = pObj->pData;
+                assert( pObjBot != NULL );
+                Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObj) );
+                Vec_IntPush( vTopVarNums, pCnfBot->pVarNums[pObjBot->Id] );
+            }
+        }
+        // remove old top and replace it by bottom
+        Aig_ManStop( pPartTop );
+        pPartTop = pPartBot;
+        pPartBot = NULL;
+        Cnf_DataFree( pCnfTop );
+        pCnfTop = pCnfBot;
+        pCnfBot = NULL;
+    }
+//    printf( "Completed %d interations.\n", f+1 );
+    // cleanup
+    sat_solver_delete( pSat );
+    Aig_ManStop( pPartTop );
+    Cnf_DataFree( pCnfTop );
+    Aig_ManStop( pPartBot );
+    Cnf_DataFree( pCnfBot );
+    Vec_IntFree( vTopVarNums );
+    Vec_PtrFree( vTop );
+    Vec_PtrFree( vBot );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
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                                ///
+////////////////////////////////////////////////////////////////////////
+
+