Version abc70731

6 files changed, 169 insertions, 60 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 91a1f8b1..5d357290 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -70,6 +70,7 @@ struct Fra_Par_t_
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesK;          // the number of timeframes to unroll
+    int              fRewrite;          // use rewriting for constraint reduction
 };
 
 // FRAIG equivalence classes
@@ -121,11 +122,13 @@ struct Fra_Man_t_
     // statistics
     int              nSimRounds;
     int              nNodesMiter;
-    int              nClassesZero;
-    int              nClassesBeg;
-    int              nClassesEnd;
-    int              nPairsBeg;
-    int              nPairsEnd;
+    int              nLitsZero;
+    int              nLitsBeg;
+    int              nLitsEnd;
+    int              nNodesBeg;
+    int              nNodesEnd;
+    int              nRegsBeg;
+    int              nRegsEnd;
     int              nSatCalls;
     int              nSatCallsSat;
     int              nSatCallsUnsat;
@@ -138,6 +141,7 @@ struct Fra_Man_t_
     // runtime
     int              timeSim;
     int              timeTrav;
+    int              timeRwr;
     int              timeSat;
     int              timeSatUnsat;
     int              timeSatSat;
@@ -182,7 +186,7 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert(
 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
-extern void                Fra_ClassesPrint( Fra_Cla_t * p );
+extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
 extern void                Fra_ClassesPrepare( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
@@ -197,7 +201,7 @@ extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 /*=== fraDfs.c ========================================================*/
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 05c07889..31d6270a 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -215,25 +215,28 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ClassesPrint( Fra_Cla_t * p )
+void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
 {
     Aig_Obj_t ** pClass;
     Aig_Obj_t * pObj;
     int i;
+
     printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
-/*
-    printf( "Constants { " );
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-        printf( "%d ", pObj->Id );
-    printf( "}\n" );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+
+    if ( fVeryVerbose )
     {
-        printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-        Fra_PrintClass( pClass );
+        printf( "Constants { " );
+        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+            printf( "%d ", pObj->Id );
+        printf( "}\n" );
+        Vec_PtrForEachEntry( p->vClasses, pClass, i )
+        {
+            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
+            Fra_PrintClass( pClass );
+        }
+        printf( "\n" );
     }
-    printf( "\n" );
-*/
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 9f2b8ca7..71e12a75 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
+static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
 { 
     static int Counter = 0;
     char FileName[20];
@@ -47,8 +47,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr
     Aig_Obj_t * pNode;
     int i;
     // create manager with the logic for these two nodes
-    Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig };
-    pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
+    pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
     // dump the logic into a file
     sprintf( FileName, "aig\\%03d.blif", ++Counter );
     Aig_ManDumpBlif( pTemp, FileName );
@@ -70,7 +69,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
+static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
@@ -123,6 +122,8 @@ void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     // simulate the counter-example and return the Fraig node
     Fra_Resimulate( p );
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+    if ( Fra_ClassObjRepr(pObj) == pObjRepr )
+        printf( "Fra_FraigNode(): Error in class refinement!\n" );
 }
 
 /**Function*************************************************************
@@ -141,8 +142,6 @@ void Fra_FraigSweep( Fra_Man_t * p )
     ProgressBar * pProgress;
     Aig_Obj_t * pObj, * pObjNew;
     int i, k = 0;
-p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
-p->nClassesBeg  = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
     // duplicate internal nodes
     pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
     // fraig latch outputs
@@ -163,7 +162,6 @@ p->nClassesBeg  = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vC
         Fra_FraigNode( p, pObj );
     }
     Extra_ProgressBarStop( pProgress );
-p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
     // try to prove the outputs of the miter
     p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
@@ -196,15 +194,23 @@ clk = clock();
     Fra_Simulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
+    // collect initial states
+    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+    p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
+    p->nNodesBeg = Aig_ManNodeNum(pManAig);
+    p->nRegsBeg  = Aig_ManRegNum(pManAig);
+    // perform fraig sweep
     Fra_FraigSweep( p );
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     {
+        int clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig );
         Aig_ManCreateChoices( pManAigNew );
         Aig_ManStop( p->pManFraig );
         p->pManFraig = NULL;
+p->timeTrav += clock() - clk2;
     }
     else
     {
@@ -221,6 +227,10 @@ clk = clock();
 */
     }
 p->timeTotal = clock() - clk;
+    // collect final stats
+    p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
+    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
+    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
     Fra_ManStop( p );
     return pManAigNew;
 }
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 71e535f7..bb4c4287 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "cnf.h"
+#include "dar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -31,6 +32,54 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs AIG rewriting on the constaint manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigInductionRewrite( Fra_Man_t * p )
+{
+    Aig_Man_t * pTemp;
+    Aig_Obj_t * pObj, * pObjPo;
+    int nTruePis, k, i, clk = clock();
+    // perform AIG rewriting on the speculated frames
+    pTemp = Aig_ManDup( p->pManFraig, 0 );
+//    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
+    pTemp = Dar_ManRewriteDefault( pTemp );
+
+//    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
+//Aig_ManDumpBlif( p->pManFraig, "1.blif" );
+//Aig_ManDumpBlif( pTemp, "2.blif" );
+
+//    Fra_FramesWriteCone( pTemp );
+//    Aig_ManStop( pTemp );
+    // transfer PI/register pointers
+    assert( p->pManFraig->nRegs == pTemp->nRegs );
+    assert( p->pManFraig->nAsserts == pTemp->nAsserts );
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
+    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
+    Aig_ManForEachPiSeq( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) );
+    k = 0;
+    assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts );
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+    {
+        pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++);
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
+    }
+    // exchange
+    Aig_ManStop( p->pManFraig );
+    p->pManFraig = pTemp;
+p->timeRwr += clock() - clk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs speculative reduction for one node.]
 
   Description []
@@ -131,6 +180,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     Aig_ManForEachLiSeq( p->pManAig, pObj, i )
         Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
 
+    // remove dangling nodes
+    Aig_ManCleanup( pManFraig );
     // make sure the satisfying assignment is node assigned
     assert( pManFraig->pData == NULL );
     return pManFraig;
@@ -147,35 +198,39 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
-    int nIter, i;
+    int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDup(pManAig, 1);
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( nFramesK > 0 );
+//Aig_ManShow( pManAig, 0, NULL );
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
     pPars->nFramesK = nFramesK;
     pPars->fVerbose = fVerbose;
+    pPars->fRewrite = fRewrite;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
-    // derive and refine e-classes using the 1st init frame
+    // derive and refine e-classes using K initialized frames
     Fra_Simulate( p, 1 );
-//    Fra_ClassesTest( p->pCla, 2, 3 );
-//Aig_ManShow( pManAig, 0, NULL );
-
-    // refine e-classes using sequential simulation
+    // refine e-classes using sequential simulation?
  
+    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesBeg = Aig_ManNodeNum(pManAig);
+    p->nRegsBeg  = Aig_ManRegNum(pManAig);
+
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -184,6 +239,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
         p->pManFraig = Fra_FramesWithClasses( p );
+        // perform AIG rewriting
+        if ( p->pPars->fRewrite )
+            Fra_FraigInductionRewrite( p );
+        // report the intermediate results
         if ( fVerbose )
         {
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  N = %6d. NR = %6d.\n", 
@@ -191,19 +250,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
                 Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
         }
-        // perform AIG rewriting on the speculated frames
 
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
         p->nSatVars = pCnf->nVars;
+        assert( p->pSat != NULL );
+        if ( p->pSat == NULL )
+            printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
 
         // set the pointers to the manager
         Aig_ManForEachObj( p->pManFraig, pObj, i )
             pObj->pData = p;
+
         // transfer PI/LO variable numbers
         pObj = Aig_ManConst1( p->pManFraig );
         Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
@@ -216,20 +278,40 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
             Fra_ObjSetFaninVec( pObj, (void *)1 );
         }
         Cnf_DataFree( pCnf );
+/*
+        Aig_ManForEachObj( p->pManFraig, pObj, i )
+        {
+            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+            Fra_ObjSetFaninVec( pObj, (void *)1 );
+        }
+        Cnf_DataFree( pCnf );
+*/
 
         // perform sweeping
         Fra_FraigSweep( p );
         assert( p->vTimeouts == NULL );
+        if ( p->vTimeouts )
+           printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
 
         // cleanup
         Fra_ManClean( p );
     }
-
-    // move the classes into representatives
+    // move the classes into representatives and reduce AIG
+clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-    // implement the classes
     pManAigNew = Aig_ManDupRepr( pManAig );
+p->timeTrav += clock() - clk2;
+p->timeTotal = clock() - clk;
+    // get the final stats
+    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
+    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
+    // free the manager
     Fra_ManStop( p );
+    // check the output
+    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+            printf( "Proved output constant 0.\n" );
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index fdd1ccc5..95cf28d8 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -55,6 +55,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
     pPars->nFramesK         =       0;  // the number of timeframes to unroll
     pPars->fConeBias        =       1;
+    pPars->fRewrite         =       0;
 }
 
 /**Function*************************************************************
@@ -71,7 +72,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
 void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =       4;  // the number of words in the simulation info
+    pPars->nSimWords        =       1;  // the number of words in the simulation info
     pPars->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
     pPars->fPatScores       =       0;  // enables simulation pattern scoring
     pPars->MaxScore         =      25;  // max score after which resimulation is used
@@ -80,10 +81,11 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 //    pPars->dActConeBumpMax  =     5.0;  // the largest bump of activity
     pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     = 1000000;  // conflict limit at a node
+    pPars->nBTLimitNode     =10000000;  // conflict limit at a node
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
     pPars->nFramesK         =       1;  // the number of timeframes to unroll
     pPars->fConeBias        =       0;
+    pPars->fRewrite         =       0;
 }
 
 /**Function*************************************************************
@@ -165,7 +167,6 @@ void Fra_ManClean( Fra_Man_t * p )
 
     sat_solver_delete( p->pSat );  
     p->pSat = NULL; 
-    p->nSatVars = 0;
 }
 
 /**Function*************************************************************
@@ -268,23 +269,28 @@ void Fra_ManStop( Fra_Man_t * p )
 void Fra_ManPrint( Fra_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
-    printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
-    printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
-    printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
-    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
-    printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
-        p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+    printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
+        p->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
+    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
+        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
+        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->timeSim  );
-    PRT( "AIG traversal   ", p->timeTrav  );
-    PRT( "SAT solving     ", p->timeSat   );
+    PRT( "AIG traversal   ", p->timeTrav );
+    if ( p->timeRwr )
+    {
+    PRT( "AIG rewriting   ", p->timeRwr  );
+    }
+    PRT( "SAT solving     ", p->timeSat  );
     PRT( "    Unsat       ", p->timeSatUnsat );
     PRT( "    Sat         ", p->timeSatSat   );
     PRT( "    Fail        ", p->timeSatFail  );
     PRT( "Class refining  ", p->timeRef   );
     PRT( "TOTAL RUNTIME   ", p->timeTotal );
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    if ( p->nSpeculs )
     printf( "Speculations = %d.\n", p->nSpeculs );
 }
 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 4ae8a686..4a6e0251 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -142,10 +142,14 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
             Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 );
         assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) );
 
-        // flip one bit of the first frame
-        Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
-        for ( i = 0; i < Limit; i++ )
-            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
+        // flip one bit of the last frame
+        if ( p->nFramesAll == 2 )
+        {
+            Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
+            for ( i = 0; i < Limit; i++ )
+                Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, i) ), i+1 );
+//            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, nTruePis*(p->nFramesAll-2) + i) ), i+1 );
+        }
     }
 }
 
@@ -261,8 +265,8 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
     pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
-    fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj));
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+    fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
     // simulate
     if ( fCompl0 && fCompl1 )
     {
@@ -326,7 +330,7 @@ void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
     pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
     // copy information as it is
     if ( fCompl0 )
         for ( i = 0; i < nSimWords; i++ )
@@ -624,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit )
     Fra_AssignRandom( p, fInit );
     Fra_SimulateOne( p );
     Fra_ClassesPrepare( p->pCla );
-//    Fra_ClassesPrint( p->pCla );
+//    Fra_ClassesPrint( p->pCla, 0 );
 //printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
 
     // refine classes by walking 0/1 patterns
@@ -667,7 +671,7 @@ p->timeRef += clock() - clk;
 //    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
 //        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
 
-//    Fra_ClassesPrint( p->pCla );
+//    Fra_ClassesPrint( p->pCla, 0 );
 }
  
 /**Function*************************************************************
@@ -729,7 +733,7 @@ int Fra_CheckOutputSims( Fra_Man_t * p )
     int i;
     // make sure the reference simulation pattern does not detect the bug
     pObj = Aig_ManPo( p->pManAig, 0 );
-    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0
+    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachPo( p->pManAig, pObj, i )
     {
         if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )