Version abc80305

4 files changed, 16 insertions, 19 deletions

diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 2d03e65d..baae7c3f 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -207,7 +207,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
+void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
 {
     Aig_Obj_t * pTemp;
     int i;
@@ -215,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
     printf( "{ " );
     for ( i = 0; (pTemp = pClass[i]); i++ )
-        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
+        printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
     printf( "}\n" );
 }
 
@@ -248,12 +248,12 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
             assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
         printf( "Constants { " );
         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-            printf( "%d ", pObj->Id );
+            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
         printf( "}\n" );
         Vec_PtrForEachEntry( p->vClasses, pClass, i )
         {
             printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-            Fra_PrintClass( pClass );
+            Fra_PrintClass( p, pClass );
         }
         printf( "\n" );
     }
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index d95515d5..c9ea4907 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1526,11 +1526,11 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
 
 ***********************************************************************/
 void Fra_ClausWriteIndClauses( Clu_Man_t * p )
-{
+{ 
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     Aig_Man_t * pNew;
     Aig_Obj_t * pClause, * pLiteral;
-    char Buffer[500], * pName;
+    char * pName;
     int * pStart, * pVar2Id; 
     int Beg, End, i, k;
     // create mapping from SAT vars to node IDs
@@ -1560,12 +1560,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     }
     free( pVar2Id );
     Aig_ManCleanup( pNew );
-    // write the manager into a file
-    pName = Ioa_FileNameGeneric(p->pAig->pName);
-    sprintf( Buffer, "%s_care.aig", pName );
-    free( pName );
-    printf( "Care clauses are written into file \"%s\".\n", Buffer );
-    Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+    pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
+    printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
+    Ioa_WriteAiger( pNew, pName, 0, 1 );
     Aig_ManStop( pNew );
 }
 
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0a81105b..67940c4f 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -328,6 +328,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
         // quit if simulation detected a counter-example for a PO
         if ( p->pManFraig->pData )
             continue;
+//        if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
+//            continue;
         // perform fraiging
         if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
             p->pPars->nBTLimitNode = 5;
@@ -381,6 +383,8 @@ clk = clock();
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
     // perform fraig sweep
+if ( p->pPars->fVerbose )
+Fra_ClassesPrint( p->pCla, 1 );
     Fra_FraigSweep( p );
     // call back the procedure to check implications
     if ( pManAig->pImpFunc )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 7e0d080c..18c9ffcc 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -560,16 +560,12 @@ clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
         extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-        char Buffer[500], * pStart;
         Aig_Man_t * pNew;
+        char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
+        printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
         pManAigNew = Aig_ManDup( pManAig, 1 );
-//        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
-        pStart = Ioa_FileNameGeneric(p->pManAig->pName);
-        sprintf( Buffer, "%s_care.aig", pStart );
-        free( pStart );
-        printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
-        Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+        Ioa_WriteAiger( pNew, pFileName, 0, 1 );
         Aig_ManStop( pNew );
     }
     else