initial commit of public abc

1 files changed, 215 insertions, 702 deletions

diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index ac1cbe5b..8aa3af80 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -19,375 +19,72 @@
 ***********************************************************************/
 
 #include "saig.h"
+#include "fra.h"
 #include "cnf.h"
 #include "satStore.h"
-#include "ssw.h"
+
+ABC_NAMESPACE_IMPL_START
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
-
-typedef struct Saig_Bmc_t_ Saig_Bmc_t;
-struct Saig_Bmc_t_
-{
-    // parameters
-    int                   nFramesMax;     // the max number of timeframes to consider
-    int                   nNodesMax;      // the max number of nodes to add
-    int                   nConfMaxOne;    // the max number of conflicts at a target
-    int                   nConfMaxAll;    // the max number of conflicts for all targets
-    int                   fVerbose;       // enables verbose output
-    // AIG managers
-    Aig_Man_t *           pAig;           // the user's AIG manager
-    Aig_Man_t *           pFrm;           // Frames manager
-    Vec_Ptr_t *           vVisited;       // nodes visited in Frames
-    // node mapping
-    int                   nObjs;          // the largest number of an AIG object
-    Vec_Ptr_t *           vAig2Frm;       // mapping of AIG nodees into Frames nodes
-//    Vec_Str_t *           vAig2Frm2;      // mapping of AIG nodees into Frames nodes
-    // SAT solver
-    sat_solver *          pSat;           // SAT solver
-    int                   nSatVars;       // the number of used SAT variables
-    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
-    // subproblems
-    Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
-    int                   iFramePrev;     // previous frame  
-    int                   iFrameLast;     // last frame  
-    int                   iOutputLast;    // last output
-    int                   iFrameFail;     // failed frame 
-    int                   iOutputFail;    // failed output
-};
-
-static inline int         Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj )                                { return Vec_IntGetEntry( p->vObj2Var, pObj->Id );  }
-static inline void        Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num )                    { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num);      }
-
-static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     }
-static inline void        Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     }
-
-static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj));  }
-static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj));  }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABS_ZER 1
-#define ABS_ONE 2
-#define ABS_UND 3
-
-static inline int Abs_ManSimInfoNot( int Value )
-{
-    if ( Value == ABS_ZER )
-        return ABS_ONE;
-    if ( Value == ABS_ONE )
-        return ABS_ZER;
-    return ABS_UND;
-}
-
-static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
-{
-    if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
-        return ABS_ZER;
-    if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
-        return ABS_ONE;
-    return ABS_UND;
-}
-
-static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame );
-    return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
-{
-    unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame );
-    assert( Value >= ABS_ZER && Value <= ABS_UND );
-    Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
-    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-}
-
 /**Function*************************************************************
 
-  Synopsis    [Performs ternary simulation for one node.]
+  Synopsis    [Create timeframes of the manager for BMC.]
 
-  Description []
+  Description [The resulting manager is combinational. POs correspond to \
+  the property outputs in each time-frame.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
 {
-    int Value0, Value1, Value;
-    Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
-    if ( Value )
-        return Value;
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        assert( Saig_ObjIsLo(p, pObj) );
-        Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
-        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
-        return Value;
-    }
-    Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
-    if ( Aig_ObjFaninC0(pObj) )
-        Value0 = Abs_ManSimInfoNot( Value0 );
-    if ( Aig_ObjIsPo(pObj) )
-    {
-        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
-        return Value0;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    if ( Value0 == ABS_ZER )
-        Value = ABS_ZER;
-    else
-    {
-        Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
-        if ( Aig_ObjFaninC1(pObj) )
-            Value1 = Abs_ManSimInfoNot( Value1 );
-        Value = Abs_ManSimInfoAnd( Value0, Value1 );
-    }
-    Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
-    assert( Value );
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation for one design.]
-
-  Description [The returned array contains the result of ternary 
-  simulation for all the frames where the output could be proved 0.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
-{
-    Vec_Ptr_t * vSimInfo;
-    Aig_Obj_t * pObj;
-    int i, f, nFramesLimit, nFrameWords;
-    int clk = clock();
-    assert( Aig_ManRegNum(p) > 0 );
-    // the maximum number of frames will be determined to use at most 200Mb of RAM
-    nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
-    nFramesLimit = ABC_MIN( nFramesLimit, nFramesMax );
-    nFrameWords  = Aig_BitWordNum( 2 * Aig_ManObjNum(p) );
-    // allocate simulation info
-    vSimInfo = Vec_PtrAlloc( nFramesLimit );
-    for ( f = 0; f < nFramesLimit; f++ )
-    {
-        Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
-        if ( f == 0 ) 
-        {
-            Saig_ManForEachLo( p, pObj, i )
-                Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
-        }
-        Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
-        Saig_ManForEachPi( p, pObj, i )
-            Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
-        Saig_ManForEachPo( p, pObj, i )
-            Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
-        // check if simulation has derived at least one fail or unknown
-        Saig_ManForEachPo( p, pObj, i )
-            if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
-            {
-                if ( fVerbose )
-                {
-                    printf( "Ternary sim found non-zero output in frame %d.  Used %5.2f Mb.  ", 
-                        f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
-                    ABC_PRT( "Time", clock() - clk );
-                }
-                return vSimInfo;
-            }
-    }
-    if ( fVerbose )
-    {
-        printf( "Ternary sim proved all outputs in the first %d frames.  Used %5.2f Mb.  ", 
-            nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
-        ABC_PRT( "Time", clock() - clk );
-    }
-    return vSimInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Free the array of simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abs_ManFreeAray( Vec_Ptr_t * p )
-{
-    void * pTemp;
-    int i;
-    Vec_PtrForEachEntry( p, pTemp, i )
-        ABC_FREE( pTemp );
-    Vec_PtrFree( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Create manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
-{
-    Saig_Bmc_t * p;
-    Aig_Obj_t * pObj;
-    int i, Lit;
-//    assert( Aig_ManRegNum(pAig) > 0 );
-    p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
-    memset( p, 0, sizeof(Saig_Bmc_t) );
-    // set parameters
-    p->nFramesMax   = nFramesMax;
-    p->nNodesMax    = nNodesMax;
-    p->nConfMaxOne  = nConfMaxOne;
-    p->nConfMaxAll  = nConfMaxAll;
-    p->fVerbose     = fVerbose;
-    p->pAig         = pAig;
-    p->nObjs        = Aig_ManObjNumMax(pAig);
-    // create node and variable mappings
-    p->vAig2Frm     = Vec_PtrAlloc( 0 );
-    Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL );
-    p->vObj2Var     = Vec_IntAlloc( 0 );
-    Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
-    // start the AIG manager and map primary inputs
-    p->pFrm         = Aig_ManStart( 5 * p->nObjs );
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
     Saig_ManForEachLo( pAig, pObj, i )
-        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
-    // create SAT solver
-    p->nSatVars     = 1;
-    p->pSat         = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 2000 );
-    Lit = toLit( p->nSatVars );
-    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
-    // other data structures
-    p->vTargets     = Vec_PtrAlloc( 0 );
-    p->vVisited     = Vec_PtrAlloc( 0 );
-    p->iOutputFail  = -1;
-    p->iFrameFail   = -1;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Delete manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcManStop( Saig_Bmc_t * p )
-{
-//    Aig_Obj_t * pObj;
-//    int i, f, Counter = 0;
-//    int i, Counter = 0;
-//    for ( i = 0; i < p->vAig2Frm2->nSize; i++ )
-//        Counter += (p->vAig2Frm2->pArray[i] != 0);
-//    for ( i = 0; i < p->vAig2Frm->nSize; i++ )
-//        Counter += (p->vAig2Frm->pArray[i] != NULL);
-//    printf( "Objs = %d.  Nodes = %d.  Frames = %d.  Used = %d.  Non-empty = %d.\n", 
-//        p->nObjs, Aig_ManNodeNum(p->pAig), p->iFrameLast, p->vAig2Frm->nSize, Counter );
-
-/*
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        int Last = -1;
-        for ( f = 0; f <= p->iFrameLast; f++ )
-            if ( Saig_BmcObjFrame( p, pObj, f ) )
-                Last = f;
-        if ( i % 50 == 0 )
-            printf( "%d ", Last );
-    }
-    printf( "\n" );
-*/
-
-    Aig_ManStop( p->pFrm  );
-    Vec_PtrFree( p->vAig2Frm );
-//    Vec_StrFree( p->vAig2Frm2 );
-    Vec_IntFree( p->vObj2Var );
-    sat_solver_delete( p->pSat );
-    Vec_PtrFree( p->vTargets );
-    Vec_PtrFree( p->vVisited );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Explores the possibility of constructing the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
-{
-    Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
-    pRes = Saig_BmcObjFrame( p, pObj, i );
-    if ( pRes != NULL )
-        return pRes;
-    if ( Saig_ObjIsPi( p->pAig, pObj ) )
-        pRes = AIG_VISITED;
-    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
-        pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
-    else if ( Aig_ObjIsPo( pObj ) )
-    {
-        pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
-        if ( pRes != AIG_VISITED )
-            pRes = Saig_BmcObjChild0( p, pObj, i );
-    }
-    else 
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
     {
-        p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
-        if ( p0 != AIG_VISITED )
-            p0 = Saig_BmcObjChild0( p, pObj, i );
-        p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
-        if ( p1 != AIG_VISITED )
-            p1 = Saig_BmcObjChild1( p, pObj, i );
-
-        if ( p0 == Aig_Not(p1) )
-            pRes = Aig_ManConst0(p->pFrm);
-        else if ( Aig_Regular(p0) == pConst1 )
-            pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
-        else if ( Aig_Regular(p1) == pConst1 )
-            pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
-        else 
-            pRes = AIG_VISITED;
-
-        if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
-            pRes = AIG_VISITED;
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
     }
-    Saig_BmcObjSetFrame( p, pObj, i, pRes );
-    return pRes;
+    Aig_ManCleanup( pFrames );
+    return pFrames;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs the actual construction of the output.]
+  Synopsis    [Returns the number of internal nodes that are not counted yet.]
 
   Description []
                
@@ -396,271 +93,88 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Ptr_t * vVisited )
+int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Aig_Obj_t * pRes;
-    pRes = Saig_BmcObjFrame( p, pObj, i );
-    if ( pRes != NULL )
-        return pRes;
-    if ( Saig_ObjIsPi( p->pAig, pObj ) )
-        pRes = Aig_ObjCreatePi(p->pFrm);
-    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
-        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
-    else if ( Aig_ObjIsPo( pObj ) )
-    {
-        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
-        pRes = Saig_BmcObjChild0( p, pObj, i );
-    }
-    else 
-    {
-        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
-        if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
-            pRes = Aig_ManConst0(p->pFrm);
-        else
-        {
-            Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
-            pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
-        }
-    }
-    assert( pRes != NULL );
-    Saig_BmcObjSetFrame( p, pObj, i, pRes );
-    Vec_PtrPush( vVisited, pObj );
-    Vec_PtrPush( vVisited, (void *)i );
-    return pRes;
+    if ( !Aig_ObjIsNode(pObj) )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + 
+        Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Adds new AIG nodes to the frames.]
+  Synopsis    [Create timeframes of the manager for BMC.]
 
-  Description []
+  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.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_BmcInterval( Saig_Bmc_t * p )
+Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
 {
-    Aig_Obj_t * pTarget;
-    Aig_Obj_t * pObj, * pRes;
-    int i, iFrame, Counter;
-    int nNodes = Aig_ManObjNum( p->pFrm );
-    Vec_PtrClear( p->vTargets );
-    p->iFramePrev = p->iFrameLast;
-    for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
+    int i, f, Counter = 0;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( nSizeMax );
+    Aig_ManIncrementTravId( pFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    Counter = 0;
+    for ( f = 0; f < nFrames; f++ )
     {
-        if ( p->iOutputLast == 0 )
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
         {
-            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
+            pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
         }
-        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
-        {
-            if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
-                return;
-//            Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
-            Vec_PtrClear( p->vVisited );
-            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
-            Vec_PtrPush( p->vTargets, pTarget );
-            Aig_ObjCreatePo( p->pFrm, pTarget );
-            Aig_ManCleanup( p->pFrm );
-            // check if the node is gone
-            Counter = 0;
-            Vec_PtrForEachEntry( p->vVisited, pObj, i )
-            {
-                iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
-                pRes = Saig_BmcObjFrame( p, pObj, iFrame );
-                if ( Aig_ObjIsNone( Aig_Regular(pRes) ) )
-                {
-                    Saig_BmcObjSetFrame( p, pObj, iFrame, NULL );
-                    Counter++;
-                }
-            }
-//            printf( "%d ", Counter );
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs the actual construction of the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
-    if ( pObj->pData )
-        return pObj->pData;
-    Vec_PtrPush( p->vVisited, pObj );
-    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) )
-        return pObj->pData = Aig_ObjCreatePi(pNew);
-    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
-    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
-    assert( pObj->pData == NULL );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AIG of the newly added nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i;
-    Aig_ManForEachObj( p->pFrm, pObj, i )
-        assert( pObj->pData == NULL );
-
-    pNew = Aig_ManStart( p->nNodesMax );
-    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
-    Vec_PtrClear( p->vVisited );
-    Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
-    Vec_PtrForEachEntry( p->vTargets, pObj, i )
-    {
-//        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
-        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
-        assert( !Aig_IsComplement(pObjNew) );
-        Aig_ObjCreatePo( pNew, pObjNew );
-    }
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for the newly added nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
-{
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, Lits[2], VarNumOld, VarNumNew;
-    Vec_PtrForEachEntry( p->vVisited, pObj, i )
-    {
-        // get the new variable of this node
-        pObjNew     = pObj->pData;
-        pObj->pData = NULL;
-        VarNumNew   = pCnf->pVarNums[ pObjNew->Id ];
-        if ( VarNumNew == -1 )
-            continue;
-        // get the old variable of this node
-        VarNumOld   = Saig_BmcSatNum( p, pObj );
-        if ( VarNumOld == 0 )
+        if ( Counter >= nSizeMax )
         {
-            Saig_BmcSetSatNum( p, pObj, VarNumNew );
-            continue;
+            Aig_ManCleanup( pFrames );
+            return pFrames;
         }
-        // add clauses connecting existing variables
-        Lits[0] = toLitCond( VarNumOld, 0 );
-        Lits[1] = toLitCond( VarNumNew, 1 );
-        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( VarNumOld, 1 );
-        Lits[1] = toLitCond( VarNumNew, 0 );
-        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // add CNF to the SAT solver
-    for ( i = 0; i < pCnf->nClauses; i++ )
-        if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+        if ( f == nFrames - 1 )
             break;
-    if ( i < pCnf->nClauses )
-        printf( "SAT solver became UNSAT after adding clauses.\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Solves targets with the given resource limit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
-{
-    int k;
-    p->iOutputFail = p->iOutputLast;
-    p->iFrameFail  = p->iFrameLast;
-    for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
-    {
-        if ( p->iOutputFail == 0 )
-        {
-            p->iOutputFail = Saig_ManPoNum(p->pAig);
-            p->iFrameFail--;
-        }
-        p->iOutputFail--;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
     }
+    Aig_ManCleanup( pFrames );
+    return pFrames;
 }
 
-/**Function*************************************************************
+ABC_NAMESPACE_IMPL_END
 
-  Synopsis    [Solves targets with the given resource limit.]
+#include "utilMem.h"
 
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
-{
-    Ssw_Cex_t * pCex;
-    Aig_Obj_t * pObj, * pObjFrm;
-    int i, f, iVarNum;
-    // start the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
-    pCex->iFrame = p->iFrameFail;
-    pCex->iPo    = p->iOutputFail;
-    // copy the bit data
-    for ( f = 0; f <= p->iFrameFail; f++ )
-    {
-        Saig_ManForEachPi( p->pAig, pObj, i )
-        {
-            pObjFrm = Saig_BmcObjFrame( p, pObj, f );
-            if ( pObjFrm == NULL )
-                continue;
-            iVarNum = Saig_BmcSatNum( p, pObjFrm );
-            if ( iVarNum == 0 )
-                continue;
-            if ( sat_solver_var_value( p->pSat, iVarNum ) )
-                Aig_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
-        }
-    }
-    // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
-    {
-        printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
-        pCex = NULL;
-    }
-    return pCex;
-}
+ABC_NAMESPACE_IMPL_START
 
+ 
 /**Function*************************************************************
 
-  Synopsis    [Solves targets with the given resource limit.]
+  Synopsis    [Performs BMC for the given AIG.]
 
   Description []
                
@@ -669,157 +183,156 @@ Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
+int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit )
 {
+    extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pFrames, * pAigTemp;
     Aig_Obj_t * pObj;
-    int i, VarNum, Lit, RetValue;
-    assert( Vec_PtrSize(p->vTargets) > 0 );
-    if ( p->pSat->qtail != p->pSat->qhead )
+    int status, clk, Lit, i, RetValue = -1;
+
+    // derive the timeframes
+    clk = clock();
+    if ( nCofFanLit )
     {
-        RetValue = sat_solver_simplify(p->pSat);
-        assert( RetValue != 0 );
+        pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
+        if ( pFrames == NULL )
+            return -1;
     }
-    Vec_PtrForEachEntry( p->vTargets, pObj, i )
+    else if ( nSizeMax > 0 )
     {
-        if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
-            continue;
-        if ( p->pSat->stats.conflicts > p->nConfMaxAll )
-            return l_Undef;
-        VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
-        Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
-        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue == l_False ) // unsat
-            continue;
-        if ( RetValue == l_Undef ) // undecided
-            return l_Undef;
-        // generate counter-example
-        Saig_BmcDeriveFailed( p, i );
-        p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
-
-        {
-//            extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
-//            Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
-        }
-        return l_True;
+        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
+        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
     }
-    return l_False;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Vec_PtrForEachEntry( p->vTargets, pObj, i )
-        Aig_ObjCreatePo( p->pFrm, pObj );
-    Aig_ManPrintStats( p->pFrm );
-    Aig_ManCleanup( p->pFrm );
-    Aig_ManPrintStats( p->pFrm );
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BMC with the given parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite )
-{
-    Saig_Bmc_t * p;
-    Aig_Man_t * pNew;
-    Cnf_Dat_t * pCnf;
-    int nOutsSolved = 0;
-    int Iter, RetValue, clk = clock(), clk2;
-/*
-    Vec_Ptr_t * vSimInfo;
-    vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
-    Abs_ManFreeAray( vSimInfo );
-*/
-    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
+    else
+        pFrames = Saig_ManFramesBmc( pAig, nFrames );
+    if ( piFrame )
+        *piFrame = nFrames;
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
             Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
-        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
-            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
-    } 
-
-    for ( Iter = 0; ; Iter++ )
+        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
+            nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
+            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
+        ABC_PRT( "Time", clock() - clk );
+        fflush( stdout );
+    }
+    // rewrite the timeframes
+    if ( fRewrite )
     {
-        clk2 = clock();
-        // add new logic interval to frames
-        Saig_BmcInterval( p );
-//        Saig_BmcAddTargetsAsPos( p );
-        if ( Vec_PtrSize(p->vTargets) == 0 )
-            break;
-        // convert logic slice into new AIG
-        pNew = Saig_BmcIntervalToAig( p );
-        // derive CNF for the new AIG
-        pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) );
-        Cnf_DataLift( pCnf, p->nSatVars );
-        p->nSatVars += pCnf->nVars;
-        // add this CNF to the solver
-        Saig_BmcLoadCnf( p, pCnf );
-        Cnf_DataFree( pCnf );
-        Aig_ManStop( pNew );
-        // solve the targets
-        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
+        clk = clock();
+//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
+        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
+        Aig_ManStop( pAigTemp );
         if ( fVerbose )
         {
-            printf( "%3d : F = %3d. O =%4d.  And = %7d. Var = %7d. Conf = %7d. ", 
-                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
-            ABC_PRT( "Time", clock() - clk2 );
+            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
+                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
+            ABC_PRT( "Time", clock() - clk );
+            fflush( stdout );
         }
-        if ( RetValue != l_False )
-            break;
     }
-    if ( RetValue == l_True )
+    // create the SAT solver
+    clk = clock();
+    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
+//if ( s_fInterrupt )
+//return -1;
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
     {
-        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
-            p->iOutputFail, p->iFrameFail );
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
     }
-    else // if ( RetValue == l_False || RetValue == l_Undef )
-        printf( "No output was asserted in %d frames.  ", p->iFramePrev-1 );
-    if ( fVerbOverwrite )
+    if ( fVerbose )
     {
-        ABC_PRTr( "Time", clock() - clk );
+        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+        ABC_PRT( "Time", clock() - clk );
+        fflush( stdout );
     }
-    else
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
     {
-        ABC_PRT( "Time", clock() - clk );
+        if ( fVerbose )
+        {
+            printf( "The BMC problem is trivially UNSAT\n" );
+            fflush( stdout );
+        }
     }
-    if ( RetValue != l_True )
+    else
     {
-        if ( p->iFrameLast >= p->nFramesMax )
-            printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-        else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
-            printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else
-            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        int clkPart = clock();
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+//if ( s_fInterrupt )
+//return -1;
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            if ( fVerbose )
+            {
+                printf( "Solving output %2d of frame %3d ... \r", 
+                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+            }
+            clk = clock();
+            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
+            {
+                printf( "Solved %2d outputs of frame %3d.  ", 
+                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+                printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
+                ABC_PRT( "T", clock() - clkPart );
+                clkPart = clock();
+                fflush( stdout );
+            }
+            if ( status == l_False )
+            {
+/*
+                Lit = lit_neg( Lit );
+                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+                assert( RetValue );
+                if ( pSat->qtail != pSat->qhead )
+                {
+                    RetValue = sat_solver_simplify(pSat);
+                    assert( RetValue );
+                }
+*/
+            }
+            else if ( status == l_True )
+            {
+//                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
+                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+                pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
+                pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
+                ABC_FREE( pModel );
+                Vec_IntFree( vCiIds );
+
+                if ( piFrame )
+                    *piFrame = i / Saig_ManPoNum(pAig);
+                RetValue = 0;
+                break;
+            }
+            else
+            {
+                if ( piFrame )
+                    *piFrame = i / Saig_ManPoNum(pAig);
+                RetValue = -1;
+                break;
+            }
+        }
     }
-    Saig_BmcManStop( p );
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pFrames );
+    return RetValue;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+