Version abc80912

4 files changed, 32 insertions, 12 deletions

diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index e6096c54..b03a248e 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -139,8 +139,9 @@ clk = clock();
             printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
                 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
                 p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
-            printf( "Use = %5d. Skip = %5d. ", 
-                p->nRefUse, p->nRefSkip );
+            if ( p->pPars->fSkipCheck )
+                printf( "Use = %5d. Skip = %5d. ", 
+                    p->nRefUse, p->nRefSkip );
             PRT( "T", clock() - clk );
         } 
         Ssw_ManCleanup( p );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index f25cee45..559f7b6c 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -47,14 +47,14 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     Aig_ManFanoutStart( pAig );
     Aig_ManSetPioNumbers( pAig );
     // create interpolation manager
-    p = ALLOC( Ssw_Man_t, 1 );
+    p = ALLOC( Ssw_Man_t, 1 ); 
     memset( p, 0, sizeof(Ssw_Man_t) );
     p->pPars         = pPars;
     p->pAig          = pAig;
     p->nFrames       = pPars->nFramesK + 1;
     p->pNodeToFraig  = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // SAT solving
-    p->pSatVars      = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    p->pSatVars      = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
     p->vFanins       = Vec_PtrAlloc( 100 );
     p->vSimRoots     = Vec_PtrAlloc( 1000 );
     p->vSimClasses   = Vec_PtrAlloc( 1000 );
@@ -99,8 +99,8 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
 
-    printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
-        p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
+    printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
+        p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
     printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  Ave SAT vars = %d.\n", 
         Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 
         p->nSatVarsTotal/p->pPars->nIters );
@@ -149,7 +149,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
         p->nSatVarsTotal += p->pSat->size;
         sat_solver_delete( p->pSat );
         p->pSat = NULL;
-        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
+        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
     }
     p->nConstrTotal = 0;
     p->nConstrReduced = 0;
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 6ef5ec20..3fa39612 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -234,7 +234,6 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachPi( p->pAig, pObj, i )
-//        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
         pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
     // simulate internal nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
@@ -244,10 +243,18 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
     RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
     RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
     // make sure refinement happened
-    if ( Aig_ObjIsConst1(pRepr) )
+    if ( Aig_ObjIsConst1(pRepr) ) 
+    {
         assert( RetValue1 );
+        if ( RetValue1 == 0 )
+            printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" );
+    }
     else
+    {
         assert( RetValue2 );
+        if ( RetValue2 == 0 )
+            printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" );
+    }
 p->timeSimSat += clock() - clk;
 }
 
@@ -266,8 +273,6 @@ p->timeSimSat += clock() - clk;
 void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
 {
     int RetValue1, RetValue2, clk = clock();
-    // save the counter-example
-//    Ssw_SmlSavePatternAig( p, f );
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
@@ -277,9 +282,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
     RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
     // make sure refinement happened
     if ( Aig_ObjIsConst1(pRepr) )
+    {
         assert( RetValue1 );
+        if ( RetValue1 == 0 )
+            printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" );
+    }
     else
+    {
         assert( RetValue2 );
+        if ( RetValue2 == 0 )
+            printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" );
+    }
 p->timeSimSat += clock() - clk;
 }
 
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 5ad6d78e..3dccc08d 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -222,6 +222,7 @@ clk = clock();
     p->fRefined = 0;
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+    Ssw_ManStartSolver( p );
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs
@@ -241,8 +242,13 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
+        // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
-            Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
+        {
+            pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
+            Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew );
+            Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
+        }
     }
     if ( p->pPars->fVerbose )
         Bar_ProgressStop( pProgress );