Version abc71130

14 files changed, 1485 insertions, 18 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 313406c7..b2e0293c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -71,6 +71,7 @@ struct Aig_Obj_t_  // 8 words
     Aig_Obj_t *      pNext;          // strashing table
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
+    Aig_Obj_t *      pHaig;          // pointer to the HAIG node
     unsigned int     Type    :  3;   // object type
     unsigned int     fPhase  :  1;   // value under 000...0 pattern
     unsigned int     fMarkA  :  1;   // multipurpose mask
@@ -140,6 +141,7 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     void *           pSeqModel;
+    Aig_Man_t *      pManHaig;
     // timing statistics
     int              time1;
     int              time2;
@@ -251,11 +253,14 @@ static inline Aig_Obj_t *  Aig_ObjChild0( Aig_Obj_t * pObj )      { return pObj-
 static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj->pFanin1;                          }
 static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
+static inline void         Aig_ObjChild0Flip( Aig_Obj_t * pObj )  { pObj->pFanin0 = Aig_Not(pObj->pFanin0);        }
+static inline void         Aig_ObjChild1Flip( Aig_Obj_t * pObj )  { pObj->pFanin1 = Aig_Not(pObj->pFanin1);        }
 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->Level;                            }
 static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
-static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } 
+static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;             } 
+static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } 
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
@@ -398,6 +403,10 @@ extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Ob
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ManFanoutStart( Aig_Man_t * p );
 extern void            Aig_ManFanoutStop( Aig_Man_t * p );
+/*=== aigFrames.c ==========================================================*/
+extern Aig_Man_t *     Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap );
+/*=== aigHaig.c ==========================================================*/
+extern void            Aig_ManHaigRecord( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
@@ -463,6 +472,8 @@ extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManMarkValidChoices( Aig_Man_t * p );
 /*=== aigRet.c ========================================================*/
 extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
+/*=== aigRetF.c ========================================================*/
+extern Aig_Man_t *     Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax );
 /*=== aigScl.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
 extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
@@ -479,6 +490,7 @@ extern void            Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_TableCountEntries( Aig_Man_t * p );
 extern void            Aig_TableProfile( Aig_Man_t * p );
+extern void            Aig_TableClear( Aig_Man_t * p );
 /*=== aigTiming.c ========================================================*/
 extern void            Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
new file mode 100644
index 00000000..dc3efe28
--- /dev/null
+++ b/src/aig/aig/aigFrames.c
@@ -0,0 +1,133 @@
+/**CFile****************************************************************
+
+  FileName    [aigFrames.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Performs timeframe expansion of the AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigFrames.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i )                       { return pObjMap[nFs*pObj->Id + i];  }
+static inline void        Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs timeframe expansion of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** pObjMap;
+    int i, f;
+
+    // create mapping for the frames nodes
+    pObjMap  = ALLOC( Aig_Obj_t *, nFs * Aig_ManObjNumMax(pAig) );
+    memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFs * Aig_ManObjNumMax(pAig) );
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    // map constant nodes
+    for ( f = 0; f < nFs; f++ )
+        Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+    // create PI nodes for the frames
+    for ( f = 0; f < nFs; f++ )
+        Aig_ManForEachPiSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFs, pObj, f, Aig_ObjCreatePi(pFrames) );
+    // set initial state for the latches
+    if ( fInit )
+    {
+        Aig_ManForEachLoSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ManConst0(pFrames) );
+    }
+    else 
+    {
+        Aig_ManForEachLoSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ObjCreatePi(pFrames) );
+    }
+
+    // add timeframes
+    for ( f = 0; f < nFs; f++ )
+    {
+//        printf( "Frame = %d.\n", f );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+//            Aig_Obj_t * pFanin0 = Aig_ObjChild0Frames(pObjMap,nFs,pObj,f);
+//            Aig_Obj_t * pFanin1 = Aig_ObjChild1Frames(pObjMap,nFs,pObj,f);
+//            printf( "Node = %3d.  Fanin0 = %3d. Fanin1 = %3d.\n", pObj->Id, Aig_Regular(pFanin0)->Id, Aig_Regular(pFanin1)->Id );
+            pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f), Aig_ObjChild1Frames(pObjMap,nFs,pObj,f) );
+            Aig_ObjSetFrames( pObjMap, nFs, pObj, f, pObjNew );
+        }
+        // set the latch inputs and copy them into the latch outputs of the next frame
+        Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Aig_ObjChild0Frames(pObjMap,nFs,pObjLi,f);
+            if ( f < nFs - 1 )
+                Aig_ObjSetFrames( pObjMap, nFs, pObjLo, f+1, pObjNew );
+        }
+    }
+    if ( fOuts )
+    {
+        for ( f = 0; f < nFs; f++ )
+            Aig_ManForEachPoSeq( pAig, pObj, i )
+            {
+                pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) );
+                Aig_ObjSetFrames( pObjMap, nFs, pObj, f, pObjNew );
+            }
+    }
+    if ( fRegs )
+    {
+        pFrames->nRegs = pAig->nRegs;
+        Aig_ManForEachLiSeq( pAig, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,nFs-1) );
+            Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
+        }
+    }
+    Aig_ManCleanup( pFrames );
+    // return the new manager
+    if ( ppObjMap )
+        *ppObjMap = pObjMap;
+    else
+        free( pObjMap );
+    return pFrames;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
new file mode 100644
index 00000000..273dc723
--- /dev/null
+++ b/src/aig/aig/aigHaig.c
@@ -0,0 +1,270 @@
+/**CFile****************************************************************
+
+  FileName    [aigHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t *  Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f )                       { return ppMap[nFrames*pObj->Id + f];  }
+static inline void         Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; }
+static inline Aig_Obj_t *  Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs speculative reduction for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame )
+{
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+    // skip nodes without representative
+    pObjRepr = pObj->pHaig;
+    if ( pObjRepr == NULL )
+        return;
+    assert( !Aig_IsComplement(pObjRepr) );
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame );
+    // get the new node of the representative
+    pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame );
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+    Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 );
+    // add the constraint
+    pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+    pMiter = Aig_Not( pMiter );
+    Aig_ObjCreatePo( pFrames, pMiter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** ppMap;
+    int i, k, f;
+    assert( nFrames >= 2 );
+    assert( Aig_ManRegNum(pHaig) > 0 );
+    assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) );
+
+    // create node mapping
+    ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames );
+    memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames );
+
+    // start the frames
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+    pFrames->nRegs = pHaig->nRegs;
+
+    // create PI nodes for the frames
+    for ( f = 0; f < nFrames; f++ )
+        Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) );
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ManForEachPiSeq( pHaig, pObj, i )
+            Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
+    // create latches for the first frame
+    Aig_ManForEachLoSeq( pHaig, pObj, i )
+        Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
+
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // mark the asserts
+        if ( f == nFrames - 1 )
+            pFrames->nAsserts = Aig_ManPoNum(pFrames);
+        // constrain latch outputs and internal nodes
+        Aig_ManForEachObj( pHaig, pObj, i )
+        {
+            if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL )
+            {
+                Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
+            }
+            else if ( Aig_ObjIsNode(pObj) )
+            {
+                pObjNew = Aig_And( pFrames, 
+                    Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), 
+                    Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
+                Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
+                Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
+            }
+        }
+
+/*
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( pHaig, pObj, i )
+            Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pHaig, pObj, i )
+        {
+            pObjNew = Aig_And( pFrames, 
+                Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), 
+                Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
+            Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
+            Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
+        }
+*/
+        // transfer latch inputs to the latch outputs 
+        Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k )
+        {
+            pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f);
+            Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew );
+        }
+    }
+
+    // remove dangling nodes
+    Aig_ManCleanup( pFrames );
+    free( ppMap );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pHaig )
+{
+    int nBTLimit = 0;
+    Aig_Man_t * pFrames;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i, Lit, RetValue, Counter;
+    int clk = clock();
+
+    // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+    pFrames = Aig_ManHaigFrames( pHaig, 2 );
+    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf );
+
+    printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n", 
+        Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );
+    printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n", 
+        Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames), 
+        pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+
+PRT( "Preparation", clock() - clk );
+    if ( pSat == NULL )
+    {
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return -1;
+    }
+    
+    // solve each output
+clk = clock();
+    Counter = 0;
+    Aig_ManForEachPo( pFrames, pObj, i )
+    {
+        if ( i < pFrames->nAsserts )
+            continue;
+        Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase );
+        RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue != l_False )
+            Counter++;
+    }
+PRT( "Solving    ", clock() - clk );
+    if ( Counter )
+        printf( "Verification failed for %d classes.\n", Counter );
+    else
+        printf( "Verification is successful.\n" );
+
+    // clean up
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManHaigRecord( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // start the HAIG
+    p->pManHaig = Aig_ManDup( p, 1 );
+    // set the pointers to the HAIG nodes
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->pHaig = pObj->pData;
+    // remove structural hashing table
+    Aig_TableClear( p->pManHaig );
+    // perform a sequence of synthesis steps
+    pNew = Aig_ManRetimeFrontier( p, 10000 );
+    // use the haig for verification
+    Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif" );
+    Aig_ManHaigVerify( pNew->pManHaig );
+    Aig_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 71ec389e..b915df99 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -115,7 +115,14 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    if ( pNew->pManHaig == NULL )
+        return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    else
+    {
+        Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
+        return pObj->pData = pObjNew;
+    }
 }
 
 /**Function*************************************************************
@@ -132,28 +139,52 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjNew;
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
+    pNew->pManHaig = p->pManHaig;  
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
     // duplicate internal nodes
     if ( fOrdered )
     {
         Aig_ManForEachObj( p, pObj, i )
             if ( Aig_ObjIsBuf(pObj) )
-                pObj->pData = Aig_ObjChild0Copy(pObj);
+            {
+                if ( pNew->pManHaig == NULL )
+                    pObj->pData = Aig_ObjChild0Copy(pObj);
+                else
+                {
+                    Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj);
+                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
+                    pObj->pData = pObjNew;
+                }
+            }
             else if ( Aig_ObjIsNode(pObj) )
-                pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            {
+                if ( pNew->pManHaig == NULL )
+                    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+                else
+                {
+                    Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
+                    pObj->pData = pObjNew;
+                }
+            }
     }
     else
     {
@@ -166,8 +197,16 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     }
     // add the POs
     Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    // pass the HAIG to the new AIG
+    p->pManHaig = NULL;
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->pHaig = NULL;
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDup(): The check has failed.\n" );
@@ -228,6 +267,8 @@ void Aig_ManStop( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
+    if ( p->pManHaig )
+        Aig_ManStop( p->pManHaig );
     if ( p->vMapped )
         Vec_PtrFree( p->vMapped );
     // print time
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 8323249e..80838e19 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     Aig_Obj_t * pObj;
     assert( !Aig_IsComplement(pGhost) );
     assert( Aig_ObjIsHash(pGhost) );
-    assert( pGhost == &p->Ghost );
+//    assert( pGhost == &p->Ghost );
     // get memory for the new object
     pObj = Aig_ManFetchMemory( p );
     pObj->Type = pGhost->Type;
@@ -97,6 +97,12 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
+    if ( p->pManHaig )
+    {
+        pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
+        pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
+        pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
+    }
     return pObj;
 }
 
@@ -365,6 +371,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     // make sure object is not pointing to itself
     assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
     assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
+    // map the HAIG nodes
+    if ( p->pManHaig != NULL )
+    {
+        assert( pObjNewR->pHaig != NULL );
+        assert( pObjNewR->pHaig->pHaig == NULL );
+        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+    }
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
     Aig_ObjDelete_rec( p, pObjOld, 0 );
@@ -385,6 +398,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         pObjOld->Type = pObjNew->Type;
         Aig_ObjDisconnect( p, pObjNew );
         Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
+        // update the haig node
+        pObjOld->pHaig = pObjNew->pHaig;
         // delete the new object
         Aig_ObjDelete( p, pObjNew );
         // update levels
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index 66a6dce1..c19f551e 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -139,6 +139,15 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 {
     Aig_Obj_t * pGhost, * pResult;
 //    Aig_Obj_t * pFan0, * pFan1;
+    if ( p->pTable == NULL )
+    {
+//        pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
+        pGhost = Aig_ManGhost(p);
+        pGhost->Type = AIG_OBJ_AND;
+        pGhost->pFanin0 = p0;
+        pGhost->pFanin1 = p1;
+        return Aig_ObjCreate( p, pGhost );
+    }
     // check trivial cases
     if ( p0 == p1 )
         return p0;
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
new file mode 100644
index 00000000..8ca4fba1
--- /dev/null
+++ b/src/aig/aig/aigRetF.c
@@ -0,0 +1,219 @@
+/**CFile****************************************************************
+
+  FileName    [aigRetF.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Retiming frontier.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigRetF.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Mark the nodes reachable from the PIs in the reverse order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManRetimeMark_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj->fMarkB )
+        return 1;
+    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->fMarkB;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ManRetimeMark_rec( p, Aig_ObjFanin0(pObj) ) )
+        return pObj->fMarkB = 1;
+    if ( Aig_ObjIsNode(pObj) && Aig_ManRetimeMark_rec( p, Aig_ObjFanin1(pObj) ) )
+        return pObj->fMarkB = 1;
+    assert( pObj->fMarkB == 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark the nodes reachable from the true PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManRetimeMark( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int fChange, i;
+    // mark the PIs
+    Aig_ManForEachObj( p, pObj, i )
+        assert( pObj->fMarkB == 0 );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        pObj->fMarkB = 1;
+    // map registers into each other
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        assert( pObjLo->pNext == NULL );
+        assert( pObjLi->pNext == NULL );
+        pObjLo->pNext = pObjLi;
+        pObjLi->pNext = pObjLo;
+    }
+    // iterativively mark the logic reachable from PIs
+    fChange = 1;
+    while ( fChange )
+    {
+        fChange = 0;
+        Aig_ManIncrementTravId( p );
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            if ( pObj->fMarkB )
+                continue;
+            if ( Aig_ManRetimeMark_rec( p, pObj ) )
+            {
+                if ( pObj->pNext )
+                    pObj->pNext->fMarkB = 1;
+                fChange = 1;
+            }
+        }
+    }
+    // clean register mapping
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = pObjLi->pNext = NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
+{
+    Aig_Obj_t * pObj, * pObjNew, * pObjLo, * pObjLo0, * pObjLo1, * pObjLi, * pObjLi0, * pObjLi1;//, * pObjLi0_, * pObjLi1_, * pObjLi0__, * pObjLi1__;
+    int i, Counter, fCompl, fChange;
+    assert( Aig_ManRegNum(p) > 0 );
+    // remove structural hashing table
+    Aig_TableClear( p );
+    // mark the retimable nodes
+    Aig_ManRetimeMark( p );
+    // mark the register outputs
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        pObjLo->fMarkA = 1;
+        pObjLo->pNext = pObjLi;
+        pObjLi->pNext = pObjLo;
+    }
+    // go through the nodes and find retimable ones
+    Counter = 0;
+    fChange = 1;
+    while ( fChange )
+    {
+        fChange = 0;
+        Aig_ManForEachNode( p, pObj, i )
+        {
+            if ( !pObj->fMarkB )
+                continue;
+            if ( Aig_ObjIsBuf(pObj) )
+                continue;
+            // get the real inputs of the node (skipping the buffers)
+            pObjLo0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+            pObjLo1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
+            if ( !Aig_Regular(pObjLo0)->fMarkA || !Aig_Regular(pObjLo1)->fMarkA )
+                continue;
+            // remember complemented attribute
+            fCompl = Aig_IsComplement(pObjLo0) & Aig_IsComplement(pObjLo1);
+            // get the register inputs
+//            pObjLi0_ = Aig_Regular(pObjLo0)->pNext;
+//            pObjLi1_ = Aig_Regular(pObjLo1)->pNext;
+//            pObjLi0__ = Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext);
+//            pObjLi1__ = Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext);
+            pObjLi0 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext), Aig_IsComplement(pObjLo0) );
+            pObjLi1 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext), Aig_IsComplement(pObjLo1) );
+            // create new node
+            pObjNew = Aig_And( p, pObjLi0, pObjLi1 );
+            pObjNew->fMarkB = 1;
+            // create new register
+            pObjLo = Aig_ObjCreatePi(p);
+            pObjLo->fMarkA = 1;
+            pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
+            p->nRegs++;
+            pObjLo->pNext = pObjLi;
+            pObjLi->pNext = pObjLo;
+            // add the buffer
+            Aig_ObjDisconnect( p, pObj );
+            pObj->Type = AIG_OBJ_BUF;
+            p->nObjs[AIG_OBJ_AND]--;
+            p->nObjs[AIG_OBJ_BUF]++;
+            Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
+            // create HAIG if defined
+            if ( p->pManHaig )
+            {
+                // create HAIG latch
+                pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig );
+                pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) );
+                // create equivalence class
+                assert( pObjLo->pHaig != NULL );
+                assert( pObjLo->pHaig->pHaig == NULL );
+                pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
+            }
+            // mark the change
+            fChange = 1;
+            // check the limit
+            if ( ++Counter >= nStepsMax )
+            {
+                fChange = 0;
+                break;
+            }
+        }
+    }
+    // clean the markings
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        pObjLo->fMarkA = 0;
+        pObjLo->pNext = pObjLi->pNext = NULL;
+    }
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkB = 0;
+    // remove useless registers
+    Aig_ManSeqCleanup( p );
+    // rehash the nodes
+    return Aig_ManDup( p, 1 ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index aae088a3..9721dd17 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -32,7 +32,7 @@
 
   Synopsis    [Remaps the manager.]
 
-  Description [Map in the array specifies for each CI nodes the node that
+  Description [Map in the array specifies for each CI node the node that
   should be used after remapping.]
                
   SideEffects []
@@ -101,7 +101,7 @@ void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes
         Vec_PtrPush( vNodes, pObj->pNext );
         return;
     }
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsPo(pObj) || Aig_ObjIsBuf(pObj) )
     {
         Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
         return;
@@ -127,7 +127,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
     Vec_Ptr_t * vNodes, * vCis, * vCos;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i, nTruePis, nTruePos;
-    assert( Aig_ManBufNum(p) == 0 );
+//    assert( Aig_ManBufNum(p) == 0 );
 
     // mark the PIs
     Aig_ManIncrementTravId( p );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 94593d70..357b63c3 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -184,6 +184,8 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t *
 void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t ** ppPlace;
+    if ( p->pTable == NULL )
+        return;
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_TableLookup(p, pObj) == NULL );
     if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
@@ -207,6 +209,8 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
 void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t ** ppPlace;
+    if ( p->pTable == NULL )
+        return;
     assert( !Aig_IsComplement(pObj) );
     ppPlace = Aig_TableFind( p, pObj );
     assert( *ppPlace == pObj ); // node should be in the table
@@ -261,6 +265,23 @@ void Aig_TableProfile( Aig_Man_t * p )
     }
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Aig_TableClear( Aig_Man_t * p )
+{
+    FREE( p->pTable );
+    p->nTableSize = 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index b70d11c7..354d94db 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -649,7 +649,7 @@ void Aig_ManDump( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the AIG into the BLIF file.]
+  Synopsis    [Writes the AIG into a BLIF file.]
 
   Description []
                
@@ -680,7 +680,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->iData = Counter++;
     nDigits = Aig_Base10Log( Counter );
-    // write the file
+    // write the file 
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
 //    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
@@ -702,7 +702,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
         fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
     fprintf( pFile, "\n" );
-    }
+    } 
     // write nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
@@ -731,7 +731,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the AIG into the BLIF file.]
+  Synopsis    [Writes the AIG into a Verilog file.]
 
   Description []
                
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
new file mode 100644
index 00000000..ea71c83b
--- /dev/null
+++ b/src/aig/fra/fraClau.c
@@ -0,0 +1,737 @@
+/**CFile****************************************************************
+
+  FileName    [fraClau.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Induction with clause strengthening.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+/*
+    This code is inspired by the paper: Aaron Bradley and Zohar Manna, 
+    "Checking safety by inductive generalization of counterexamples to 
+    induction", FMCAD '07.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cla_Man_t_    Cla_Man_t;
+struct Cla_Man_t_
+{
+    // SAT solvers
+    sat_solver *     pSatMain;
+    sat_solver *     pSatTest;
+    sat_solver *     pSatBmc;
+    // CNF for the test solver
+//    Cnf_Dat_t *      pCnfTest;
+    // SAT variables
+    Vec_Int_t *      vSatVarsMainCs;
+    Vec_Int_t *      vSatVarsTestCs;
+    Vec_Int_t *      vSatVarsTestNs;
+    Vec_Int_t *      vSatVarsBmcNs;
+    // helper variables
+    int              nSatVarsTestBeg;
+    int              nSatVarsTestCur;
+    // counter-examples
+    Vec_Int_t *      vCexMain0;
+    Vec_Int_t *      vCexMain;
+    Vec_Int_t *      vCexTest;
+    Vec_Int_t *      vCexBase;
+    Vec_Int_t *      vCexAssm;
+    Vec_Int_t *      vCexBmc;
+    // mapping of CS into NS var numbers
+    int *            pMapCsMainToCsTest; 
+    int *            pMapCsTestToCsMain; 
+    int *            pMapCsTestToNsTest; 
+    int *            pMapCsTestToNsBmc;  
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Saves variables corresponding to latch outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars )
+{
+    Vec_Int_t * vVars;
+    Aig_Obj_t * pObjLo, * pObjLi;
+    int i;
+    vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
+        Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] );
+    return vVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves variables corresponding to latch outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
+{
+    Vec_Int_t * vVars;
+    Aig_Obj_t * pObj;
+    int i;
+    vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
+    Aig_ManForEachPo( pMan, pObj, i )
+        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
+    return vVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves variables corresponding to latch outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting )
+{
+    Vec_Int_t * vVars;
+    Aig_Obj_t * pObj;
+    int i;
+    vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
+    Aig_ManForEachPi( pMan, pObj, i )
+    {
+        if ( i < nStarting )
+            continue;
+        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
+    }
+    return vVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves variables corresponding to latch outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax )
+{
+    int * pMapping, Var, i;
+    assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
+    pMapping = ALLOC( int, nVarsMax );
+    for ( i = 0; i < nVarsMax; i++ )
+        pMapping[i] = -1;
+    Vec_IntForEachEntry( vSatVarsFrom, Var, i )
+        pMapping[Var] = Vec_IntEntry(vSatVarsTo,i);
+    return pMapping;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauStop( Cla_Man_t * p )
+{
+    free( p->pMapCsMainToCsTest );
+    free( p->pMapCsTestToCsMain );
+    free( p->pMapCsTestToNsTest );
+    free( p->pMapCsTestToNsBmc  );
+    Vec_IntFree( p->vSatVarsMainCs );
+    Vec_IntFree( p->vSatVarsTestCs );
+    Vec_IntFree( p->vSatVarsTestNs );
+    Vec_IntFree( p->vSatVarsBmcNs );
+    Vec_IntFree( p->vCexMain0 );
+    Vec_IntFree( p->vCexMain );
+    Vec_IntFree( p->vCexTest );
+    Vec_IntFree( p->vCexBase );
+    Vec_IntFree( p->vCexAssm );
+    Vec_IntFree( p->vCexBmc  );
+    if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
+    if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
+    if ( p->pSatBmc )  sat_solver_delete( p->pSatBmc );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Takes the AIG with the single output to be checked.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
+{
+    Cla_Man_t * p;
+    Cnf_Dat_t * pCnfMain;
+    Cnf_Dat_t * pCnfTest;
+    Cnf_Dat_t * pCnfBmc;
+    Aig_Man_t * pFramesMain;
+    Aig_Man_t * pFramesTest;
+    Aig_Man_t * pFramesBmc;
+    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+
+    // start the manager
+    p = ALLOC( Cla_Man_t, 1 );
+    memset( p, 0, sizeof(Cla_Man_t) );
+    p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    p->vCexMain  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    p->vCexTest  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    p->vCexBase  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    p->vCexAssm  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+    p->vCexBmc   = Vec_IntAlloc( Aig_ManRegNum(pMan) );
+
+    // derive two timeframes to be checked
+    pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs
+//Aig_ManShow( pFramesMain, 0, NULL );
+    assert( Aig_ManPoNum(pFramesMain) == 2 );
+    Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
+    pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
+//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
+    p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain );
+/*
+    {
+        int i;
+        Aig_Obj_t * pObj;
+        Aig_ManForEachObj( pFramesMain, pObj, i )
+            printf( "%d -> %d  \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] );
+        printf( "\n" );
+    }
+*/
+
+    // derive one timeframe to be checked
+    pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL );
+    assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
+    pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
+    p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest );
+    p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
+
+    // derive one timeframe to be checked for BMC
+    pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL );
+//Aig_ManShow( pFramesBmc, 0, NULL );
+    assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
+    pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
+    p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc );
+
+    // create variable sets
+    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
+    p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
+    p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
+    p->vSatVarsBmcNs  = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
+    assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) );
+    assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) );
+
+    // create mapping of CS into NS vars
+    p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) );
+    p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) );
+    p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) );
+    p->pMapCsTestToNsBmc  = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs,  Aig_ManObjNumMax(pFramesTest) );
+
+    // cleanup
+    Cnf_DataFree( pCnfMain );
+    Cnf_DataFree( pCnfTest );
+    Cnf_DataFree( pCnfBmc );
+    Aig_ManStop( pFramesMain );
+    Aig_ManStop( pFramesTest );
+    Aig_ManStop( pFramesBmc );
+    if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL )
+    {
+        Fra_ClauStop( p );
+        return NULL;
+    }
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits off second half and returns it as a new vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
+{
+    Vec_Int_t * vPart;
+    int Entry, i;
+    assert( Vec_IntSize(vVec) > 1 );
+    vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 );
+    Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 )
+        Vec_IntPush( vPart, Entry );
+    Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 );
+    return vPart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends the contents of the second vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int Entry, i;
+    Vec_IntForEachEntry( vVec2, Entry, i )
+        Vec_IntPush( vVec1, Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complements all literals in the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Vec_IntComplement( Vec_Int_t * vVec )
+{
+    int i;
+    for ( i = 0; i < Vec_IntSize(vVec); i++ )
+        vVec->pArray[i] = lit_neg( vVec->pArray[i] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the property holds. Returns counter-example if not.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
+{
+    int nBTLimit = 0;
+    int RetValue, iVar, i;
+    sat_solver_act_var_clear( p->pSatMain );
+    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    Vec_IntClear( vCex );
+    if ( RetValue == l_False )
+        return 1;
+    assert( RetValue == l_True );
+    Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i )
+        Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) );
+/*
+    {
+        int i;
+        for (i = 0; i < p->pSatMain->size; i++)
+            printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True );
+        printf( "\n" );
+    }
+*/
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the clause holds using BMC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
+{
+    int nBTLimit = 0;
+    int RetValue;
+    RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), 
+        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( RetValue == l_False )
+        return 1;
+    assert( RetValue == l_True );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Lifts the clause to depend on NS variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv )
+{
+    int iLit, i;
+    Vec_IntClear( vRemapped );
+    Vec_IntForEachEntry( vClause, iLit, i )
+    {
+        assert( pMap[lit_var(iLit)] >= 0 );
+        iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv );
+        Vec_IntPush( vRemapped, iLit );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the clause holds. Returns counter example if not.]
+
+  Description [Uses test SAT solver.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
+{
+    int nBTLimit = 0;
+    int RetValue, iVar, i;
+    int nClauseSize = Vec_IntSize( vClause );
+    // complement literals
+    Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive
+    Vec_IntComplement( vClause ); // helper negative (the clause is C v h')
+    // add the clause
+    RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+    assert( RetValue == 1 );
+    // complement all literals
+    Vec_IntPop( vClause );  // helper removed
+    Vec_IntComplement( vClause ); 
+    // create the assumption in terms of NS variables
+    Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 );
+    // add helper literals
+    for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ )
+        Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative
+    Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
+    // try to solve
+    RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm), 
+        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( vCex )
+        Vec_IntClear( vCex );
+    if ( RetValue == l_False )
+        return 1;
+    assert( RetValue == l_True );
+    if ( vCex )
+    {
+        Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i )
+            Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the counter-example by removing complemented literals.]
+
+  Description [Removes literals from vMain that differ from those in the  
+  counter-example (vNew). Relies on the fact that the PI variables are
+  assigned in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
+{
+    int LitM, LitN, VarM, VarN, i, j, k;
+    assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
+    for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
+    {
+        LitM = Vec_IntEntry( vMain, i );
+        LitN = Vec_IntEntry( vNew, j );
+        VarM = lit_var( LitM );
+        VarN = lit_var( LitN );
+        if ( VarM > VarN )
+        {
+            assert( 0 );
+        }
+        else if ( VarM < VarN )
+        {
+            j++;
+        }
+        else // if ( VarM == VarN )
+        {
+            i++;
+            j++;
+            if ( LitM == LitN )
+                Vec_IntWriteEntry( vMain, k++, LitM );
+        }
+    }
+    assert( i == Vec_IntSize(vMain) );
+    Vec_IntShrink( vMain, k );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the minimal invariant that holds.]
+
+  Description [On entrace, vBasis does not hold, vBasis+vExtra holds but
+  is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
+{
+    Vec_Int_t * vExtra2;
+    int nSizeOld;
+    if ( Vec_IntSize(vExtra) == 1 )
+        return;
+    nSizeOld = Vec_IntSize( vBasis );
+    vExtra2 = Vec_IntSplitHalf( vExtra );
+
+    // try the first half
+    Vec_IntAppend( vBasis, vExtra );
+    if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
+    {
+        Vec_IntShrink( vBasis, nSizeOld );
+        Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
+        return;
+    }
+    Vec_IntShrink( vBasis, nSizeOld );
+
+    // try the second half
+    Vec_IntAppend( vBasis, vExtra2 );
+    if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
+    {
+        Vec_IntShrink( vBasis, nSizeOld );
+        Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
+        return;
+    }
+//    Vec_IntShrink( vBasis, nSizeOld );
+
+    // find the smallest with the second half added
+    Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
+    Vec_IntShrink( vBasis, nSizeOld );
+    Vec_IntAppend( vBasis, vExtra );
+    // find the smallest with the second half added
+    Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
+    Vec_IntShrink( vBasis, nSizeOld );
+    Vec_IntAppend( vExtra, vExtra2 );
+    Vec_IntFree( vExtra2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the clauses using a simple method.]
+
+  Description [The input and output clause are in vExtra.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
+{
+    int iLit, iLit2, i, k;
+    Vec_IntForEachEntryReverse( vExtra, iLit, i )
+    {
+        // copy literals without the given one
+        Vec_IntClear( vBasis );
+        Vec_IntForEachEntry( vExtra, iLit2, k )
+            if ( iLit2 != iLit )
+                Vec_IntPush( vBasis, iLit2 );
+        // try whether it is inductive
+        if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
+            continue;
+        // the clause is inductive
+        // remove the literal
+        for ( k = iLit; k < Vec_IntSize(vExtra)-1; k++ )
+            Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
+        Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
+{
+    int LitM, VarM, VarN, i, j, k;
+    assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) );
+    for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); )
+    {
+        LitM = Vec_IntEntry( vCex, i );
+        VarM = lit_var( LitM );
+        VarN = Vec_IntEntry( vSatCsVars, j );
+        if ( VarM > VarN )
+        {
+            assert( 0 );
+        }
+        else if ( VarM < VarN )
+        {
+            j++;
+            printf( "-" );
+        }
+        else // if ( VarM == VarN )
+        {
+            i++;
+            j++;
+            printf( "%d", !lit_sign(LitM) );
+        }
+    }
+    assert( i == Vec_IntSize(vCex) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Takes the AIG with the single output to be checked.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
+{
+    Cla_Man_t * p;
+    int Iter, RetValue, fFailed, i;
+    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+    // create the manager
+    p = Fra_ClauStart( pMan );
+    if ( p == NULL )
+    {
+        printf( "The property is trivially inductive.\n" );
+        return 1;
+    }
+    // generate counter-examples and expand them
+    for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ )
+    {
+        if ( fVerbose )
+            printf( "%4d : ", Iter );
+        // remap clause into the test manager
+        Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
+        if ( fVerbose )
+            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
+        // the main counter-example is in p->vCexMain
+        // intermediate counter-examples are in p->vCexTest
+        // generate the reduced counter-example to the inductive property
+        fFailed = 0;
+        for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ )
+        {
+            Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
+            Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
+            if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
+            {
+                fFailed = 1;
+                break;
+            }
+        }
+        if ( fFailed )
+        {
+            if ( fVerbose )
+                printf( " Reducing failed after %d iterations (BMC failed).\n", i );
+            continue;
+        }
+        if ( Vec_IntSize(p->vCexMain) == 0 )
+        {
+            if ( fVerbose )
+                printf( " Reducing failed after %d iterations (nothing left).\n", i );
+            continue;
+        }
+        if ( fVerbose )
+            printf( " LitsAfterRed = %3d.  ", Vec_IntSize(p->vCexMain) );
+        // minimize the inductive property
+        Vec_IntClear( p->vCexBase );
+//        Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
+//        Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
+        assert( Vec_IntSize(p->vCexMain) > 0 );
+        if ( fVerbose )
+            printf( " LitsAfterMin = %3d.  ", Vec_IntSize(p->vCexMain) );
+        if ( fVerbose )
+            printf( "\n" );
+        // add the clause to the solver
+        Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 );
+        RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) );
+        if ( RetValue == 0 )
+        {
+            Iter++;
+            break;
+        }
+    }
+
+    // report the results
+    if ( Iter == nIters )
+    {
+        printf( "Property is not proved after %d iterations.\n", nIters );
+        return 0;
+    }
+    printf( "Property is proved after %d iterations.\n", Iter );
+    Fra_ClauStop( p );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 7400b3f9..95d65e25 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -280,6 +280,8 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
 //        Fra_FraigVerifyCounterEx( p, p->vCex );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
+    if ( p->pManFraig->pData )
+        return;
     if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
     assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index b41b7a29..6cfdc3ff 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -402,16 +402,21 @@ p->timeTrav += clock() - clk2;
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
             if ( p->pCla->vImps )
                 printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
-            printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) );
+            printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
+            printf( "\n" );
         } 
 
         // perform sweeping
         p->nSatCallsRecent = 0;
         p->nSatCallsSkipped = 0;
+clk2 = clock();
         Fra_FraigSweep( p );
+        if ( fVerbose )
+        {
+//            PRT( "t", clock() - clk2 ); 
+        } 
 
 //        Sat_SolverPrintStats( stdout, p->pSat );
-
         // remove FRAIG and SAT solver
         Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
         sat_solver_delete( p->pSat );  p->pSat = NULL; 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 573d3570..17a7335c 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -228,9 +228,11 @@ PRT( "Time", clock() - clk );
         }
 
         if ( pNew->nRegs )
-        pNew = Aig_ManConstReduce( pNew, 0 );
+            pNew = Aig_ManConstReduce( pNew, 0 );
 
         // perform sequential simulation
+        if ( pNew->nRegs )
+        {
 clk = clock();
         pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 
         if ( fVerbose )
@@ -250,6 +252,7 @@ PRT( "Time", clock() - clkTotal );
             return RetValue;
         }
         Fra_SmlStop( pSml );
+        }
     }
 
     // get the miter status