Reducing memory usage in bmc2 and bmc3.

2 files changed, 149 insertions, 172 deletions

diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index ca6049ef..d28320fc 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -25,12 +25,11 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
+//#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
 
 typedef struct Saig_Bmc_t_ Saig_Bmc_t;
 struct Saig_Bmc_t_
@@ -44,11 +43,10 @@ struct Saig_Bmc_t_
     // 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
+    Vec_Int_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
@@ -63,15 +61,43 @@ struct Saig_Bmc_t_
     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 (Aig_Obj_t *)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_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       
+{ 
+//    return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     
+    Aig_Obj_t * pRes;
+    Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
+    int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
+    if ( iObjLit == -1 )
+        return NULL;
+    pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
+    if ( pRes == NULL )
+        Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
+    else
+        pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
+    return pRes;
+}
+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 );     
+    Vec_Int_t * vFrame;
+    int iObjLit;
+    if ( i == Vec_PtrSize(p->vAig2Frm) )
+        Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
+    assert( i < Vec_PtrSize(p->vAig2Frm) );
+    vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
+    if ( pNode == NULL )
+        iObjLit = -1;
+    else
+        iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
+    Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
+}
 
 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));  }
 
+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);      }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -268,12 +294,11 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
     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->vAig2Frm     = Vec_PtrAlloc( 100 );
     p->vObj2Var     = Vec_IntAlloc( 0 );
-    Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
+    Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
     // start the AIG manager and map primary inputs
-    p->pFrm         = Aig_ManStart( 5 * p->nObjs );
+    p->pFrm         = Aig_ManStart( p->nObjs );
     Saig_ManForEachLo( pAig, pObj, i )
         Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
     // create SAT solver
@@ -284,8 +309,8 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
     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->vTargets     = Vec_PtrAlloc( 1000 );
+    p->vVisited     = Vec_IntAlloc( 1000 );
     p->iOutputFail  = -1;
     p->iFrameFail   = -1;
     return p;
@@ -304,36 +329,12 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
 ***********************************************************************/
 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_VecFree( (Vec_Vec_t *)p->vAig2Frm );
     Vec_IntFree( p->vObj2Var );
     sat_solver_delete( p->pSat );
     Vec_PtrFree( p->vTargets );
-    Vec_PtrFree( p->vVisited );
+    Vec_IntFree( p->vVisited );
     ABC_FREE( p );
 }
 
@@ -348,6 +349,7 @@ void Saig_BmcManStop( Saig_Bmc_t * p )
   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);
@@ -388,6 +390,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
     Saig_BmcObjSetFrame( p, pObj, i, pRes );
     return pRes;
 }
+*/
 
 /**Function*************************************************************
 
@@ -400,7 +403,7 @@ 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 )
+Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
 {
     Aig_Obj_t * pRes;
     pRes = Saig_BmcObjFrame( p, pObj, i );
@@ -428,8 +431,8 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
     }
     assert( pRes != NULL );
     Saig_BmcObjSetFrame( p, pObj, i, pRes );
-    Vec_PtrPush( vVisited, pObj );
-    Vec_PtrPush( vVisited, (void *)(ABC_PTRINT_T)i );
+    Vec_IntPush( vVisited, Aig_ObjId(pObj) );
+    Vec_IntPush( vVisited, i );
     return pRes;
 }
 
@@ -447,13 +450,12 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
 void Saig_BmcInterval( Saig_Bmc_t * p )
 {
     Aig_Obj_t * pTarget;
-    Aig_Obj_t * pObj, * pRes;
-    int i, iFrame, Counter;
+    int i, iObj, iFrame;
     int nNodes = Aig_ManObjNum( p->pFrm );
     Vec_PtrClear( p->vTargets );
     p->iFramePrev = p->iFrameLast;
     for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
-    {
+    { 
         if ( p->iOutputLast == 0 )
         {
             Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
@@ -463,24 +465,14 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
             if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
                 return;
 //            Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
-            Vec_PtrClear( p->vVisited );
+            Vec_IntClear( p->vVisited );
             pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
             Vec_PtrPush( p->vTargets, pTarget );
             Aig_ObjCreateCo( p->pFrm, pTarget );
             Aig_ManCleanup( p->pFrm );
             // check if the node is gone
-            Counter = 0;
-            Vec_PtrForEachEntry( Aig_Obj_t *, 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 );
+            Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
+                Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
         }
     }
 }
@@ -500,7 +492,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj
 {
     if ( pObj->pData )
         return (Aig_Obj_t *)pObj->pData;
-    Vec_PtrPush( p->vVisited, pObj );
+    Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
     if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
     {
         p->nStitchVars += !Aig_ObjIsCi(pObj);
@@ -533,15 +525,15 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
 
     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_IntClear( p->vVisited );
+    Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
     {
 //        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
         pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
         assert( !Aig_IsComplement(pObjNew) );
         Aig_ObjCreateCo( pNew, pObjNew );
-    }
+    } 
     return pNew;
 }
 
@@ -560,7 +552,7 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
 {
     Aig_Obj_t * pObj, * pObjNew;
     int i, Lits[2], VarNumOld, VarNumNew;
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vVisited, pObj, i )
+    Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
     {
         // get the new variable of this node
         pObjNew     = (Aig_Obj_t *)pObj->pData;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 17a85bad..0a283bb5 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -40,14 +40,13 @@ struct Gia_ManBmc_t_
     Vec_Int_t *       vMapping;    // mapping
     Vec_Vec_t *       vSects;      // sections
     Vec_Int_t *       vId2Num;     // number of each node 
-    Vec_Int_t *       vVisited;    // visited nodes
-    // SAT variables
-    Vec_Int_t *       vPiVars;     // SAT vars for the PIs 
+    Vec_Ptr_t *       vTerInfo;    // ternary information
     Vec_Ptr_t *       vId2Var;     // SAT vars for each object
     // SAT solver
     sat_solver *      pSat;        // SAT solver
     int               nSatVars;    // SAT variables
     int               nObjNums;    // SAT objects
+    int               nWordNum;    // unsigned words for ternary simulation
     int               nBufNum;     // the number of simple nodes
     int               nDupNum;     // the number of simple nodes
     char * pSopSizes, ** pSops;    // CNF representation
@@ -684,14 +683,15 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
             Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
     Aig_ManForEachCo( pAig, pObj, i )
         Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
-    p->vPiVars  = Vec_IntAlloc( 1000 );
     p->vId2Var  = Vec_PtrAlloc( 100 );
-    p->vVisited = Vec_IntAlloc( 1000 );
+    p->vTerInfo = Vec_PtrAlloc( 100 );
     // create solver
     p->nSatVars = 1;
     p->pSat     = sat_solver_new();
     sat_solver_setnvars( p->pSat, 1000 );
     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
+    // terminary simulation 
+    p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
     return p;
 }
 
@@ -708,7 +708,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
 ***********************************************************************/
 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
-    Aig_ManCleanMarkA( p->pAig );
+//    Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
         assert( p->pAig->vSeqModelVec == NULL );
@@ -719,9 +719,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Vec_IntFree( p->vMapping );
     Vec_VecFree( p->vSects );
     Vec_IntFree( p->vId2Num );
-    Vec_IntFree( p->vPiVars );
-    Vec_IntFree( p->vVisited );
     Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
+    Vec_PtrFreeFree( p->vTerInfo );
     sat_solver_delete( p->pSat );
     free( p->pSopSizes );
     free( p->pSops[1] );
@@ -790,13 +789,6 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int
     ObjNum  = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
     vFrame  = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
     Vec_IntWriteEntry( vFrame, ObjNum, iLit );
-    if ( iLit == ABC_INFINITY || iLit == ABC_INFINITY+1 )
-    {
-        Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
-        Vec_IntPush( p->vVisited, iFrame );
-    }
-    else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num
-        Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjCioId(pObj), lit_var(iLit) );
     return iLit;
 }
 
@@ -1058,12 +1050,14 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
     {
         iLit = ABC_INFINITY;
     }
+    assert( iLit != ABC_INFINITY );
     return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Derives CNF for one node.]
+  Synopsis    [Recursively performs terminary simulation.]
 
   Description []
                
@@ -1072,25 +1066,59 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
+int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
 {
-    int i, iLit, Entry, iFrameOld, Value;
-    Vec_IntClear( p->vVisited );
-    iLit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 0 );
-    Vec_IntForEachEntry( p->vVisited, Entry, i )
+    unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
+    int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
+    if ( Value != SAIG_TER_NON )
+        return Value;
+    if ( Aig_ObjIsCo(pObj) )
     {
-        iFrameOld = Vec_IntEntry( p->vVisited, ++i );
-        Value = Saig_ManBmcLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld );
-//        assert( Value == 0 || Value == 1 || Value == ABC_INFINITY || Value == ABC_INFINITY+1 );
-        assert( Value == ABC_INFINITY || Value == ABC_INFINITY+1 );
-        if ( !(Value == ABC_INFINITY || Value == ABC_INFINITY+1) )
-            printf( "Internal error!\n" );
-//        if ( Value == 0 || Value == 1 )
-//            continue;
-        Saig_ManBmcSetLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld, ~0 );
+        Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
+        if ( Aig_ObjFaninC0(pObj) )
+            Value = Saig_ManBmcSimInfoNot( Value );
     }
-    if ( iLit < 2 )
-        return iLit;
+    else if ( Saig_ObjIsLo(p->pAig, pObj) )
+    {
+        assert( iFrame > 0 );
+        Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
+    }
+    else if ( Aig_ObjIsNode(pObj) )
+    {
+        Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame  );
+        Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame  );
+        if ( Aig_ObjFaninC0(pObj) )
+            Val0 = Saig_ManBmcSimInfoNot( Val0 );
+        if ( Aig_ObjFaninC1(pObj) )
+            Val1 = Saig_ManBmcSimInfoNot( Val1 );
+        Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
+    }
+    else assert( 0 );
+    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
+    // transfer to the unrolling
+    if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
+        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
+    return Value;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives CNF for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+    // perform terminary simulation
+    int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
+    if ( Value != SAIG_TER_UND )
+        return (int)(Value == SAIG_TER_ONE);
+    // construct CNF if value is ternary
     return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 1 );
 }
 
@@ -1124,44 +1152,6 @@ int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
 
 /**Function*************************************************************
 
-  Synopsis    [Mark PIs to be skipped based on nPisAbstract.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract )
-{
-    Vec_Ptr_t * vPis;
-    Aig_Obj_t * pObj;
-    int i;
-    if ( nPisAbstract < 1 )
-        return;
-    // sort PIs by the number of their fanouts
-    vPis = Vec_PtrAlloc( 100 );
-    Saig_ManForEachPi( pAig, pObj, i )
-        Vec_PtrPush( vPis, pObj );
-    Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsIncrease );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i )
-    {
-        if ( i < nPisAbstract )
-        {
-            pObj->fMarkA = 1;
-//            printf( "%d=%d ", Aig_ObjCioId(pObj), Aig_ObjRefs(pObj) );
-        }
-    }
-//    printf( "\n" );
-    // print primary inputs
-//    Saig_ManForEachPi( pAig, pObj, i )
-//        printf( "%d=%d ", i, Aig_ObjRefs(pObj) );
-//    printf( "\n" );
-}
-
-/**Function*************************************************************
-
   Synopsis    [This procedure sets default parameters.]
 
   Description []
@@ -1203,19 +1193,18 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
 {
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
+    unsigned * pInfo;
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
-    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
+    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
     int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
     int nTimeToStop = time(NULL) + pPars->nTimeOut;
-    if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
-        printf( "Performing BMC with constraints...\n" );
     p = Saig_Bmc3ManStart( pAig );
     p->pPars = pPars;
     if ( pPars->fVerbose )
     {
-        printf( "Running \"bmc3\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.  Map = %6d. Sect =%3d.\n", 
+        printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n", 
             Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
-            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), (Vec_IntSize(p->vMapping)-Aig_ManObjNumMax(pAig))/5, Vec_VecSize(p->vSects) );
+            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) );
         printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
             pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
     } 
@@ -1225,7 +1214,6 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     // perform frames
     Aig_ManRandom( 1 );
-    Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
         // stop BMC after exploring all reachable states
@@ -1235,7 +1223,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             return pPars->nFailOuts ? 0 : 1;
         }
         // stop BMC if all targets are solved
-        if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
+        if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) )
         {
             Saig_Bmc3ManStop( p );
             return 0;
@@ -1243,11 +1231,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         // consider the next timeframe
         if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
             pPars->iFrame = f-1;
-        // resize the array
-        Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
         // map nodes of this section
         Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
+        Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
 /*
+        // cannot remove mapping of frame values for any timeframes
+        // because with constant propagation they may be needed arbitrarily far
         if ( f > 2*Vec_VecSize(p->vSects) )
         {
             int iFrameOld = f - 2*Vec_VecSize( p->vSects );
@@ -1257,28 +1246,15 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
 */
         // prepare some nodes
         Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
+        Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
+        Saig_ManForEachPi( pAig, pObj, i )
+            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
         if ( f == 0 )
-            Saig_ManForEachLo( p->pAig, pObj, i )
-                Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
-        // set PIs to zero if they are marked
-        Saig_ManForEachPi( p->pAig, pObj, i )
-            if ( pObj->fMarkA )
-                Saig_ManBmcSetLiteral( p, pObj, f, Aig_ManRandom(0) & 1 );
-        // add the constraints for this frame
-        Saig_ManForEachPo( pAig, pObj, i )
         {
-            if ( i < Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
-                continue;            
-clk2 = clock();
-            Lit = Saig_ManBmcCreateCnf( p, pObj, f );
-            Lit = lit_neg( Lit );
-clkOther += clock() - clk2;
-            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-            if ( status == 0 )
+            Saig_ManForEachLo( p->pAig, pObj, i )
             {
-                printf( "SAT problem became UNSAT after adding constraints in frame %d.\n", f );
-                Saig_Bmc3ManStop( p );
-                return 1;
+                Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
+                Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
             }
         }
         if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
@@ -1287,7 +1263,7 @@ clkOther += clock() - clk2;
         clk = clock(); 
         Saig_ManForEachPo( pAig, pObj, i )
         {
-            if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
+            if ( i >= Saig_ManPoNum(pAig) )
                 break;
             // skip solved outputs
             if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
@@ -1311,7 +1287,7 @@ clkOther += clock() - clk2;
                 }
                 pPars->nFailOuts++;
                 printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
+                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
@@ -1332,13 +1308,19 @@ clkOther += clock() - clk2;
             }
             else if ( status == l_True )
             {
-                int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) );
-                Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 );
-                ABC_FREE( pModel );
+                Aig_Obj_t * pObjPi;
+                Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
+                int j, k, iBit = Saig_ManRegNum(pAig);
+                for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
+                    Saig_ManForEachPi( p->pAig, pObjPi, k )
+                    {
+                        int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
+                        if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
+                            Abc_InfoSetBit( pCex->pData, iBit + k );
+                    }
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
                 {
-//ABC_PRT( "CNF generation runtime", clkOther );
                     if ( pPars->fVerbose )
                     {
                         printf( "%3d %s : ", f,  fUnfinished ? "-" : "+" );
@@ -1347,8 +1329,9 @@ clkOther += clock() - clk2;
                         printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
                         printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
 //                        ABC_PRT( "Time", clock() - clk );
+                        printf( "%4.0f Mb",     4.0*(f+1)*p->nObjNums /(1<<20) );
+                        printf( "%4.0f Mb",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
                         printf( "%9.2f sec ",   (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
-                        printf( "%5.0f Mb",      1.0+sat_solver_memory(p->pSat)/(1<<20) );
                         printf( "\n" );
 //                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@@ -1364,7 +1347,7 @@ clkOther += clock() - clk2;
                 }
                 pPars->nFailOuts++;
                 printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
+                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
@@ -1409,8 +1392,10 @@ clkOther += clock() - clk2;
             printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
             printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
 //            ABC_PRT( "Time", clock() - clk );
+//            printf( "%4.0f Mb",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
+            printf( "%4.0f Mb",     4.0*(f+1)*p->nObjNums /(1<<20) );
+            printf( "%4.0f Mb",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
             printf( "%9.2f sec ",  (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
-            printf( "%5.0f Mb",     1.0+sat_solver_memory(p->pSat)/(1<<20) );
             printf( "\n" );
 //            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );