Version abc90315

abclib.dsp

@@ -3651,6 +3651,14 @@ SOURCE=.\src\aig\gia\giaCof.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaCSat0.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\gia\giaCSat2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File

src/aig/cec/cecCore.c

@@ -282,6 +282,9 @@ p->timeSim += clock() - clk;
 //            Gia_ManEquivTransform( p->pAig, 1 );
         }
         pSrm = Cec_ManFraSpecReduction( p ); 
+
+//        Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
+
         if ( pPars->fVeryVerbose )
             Gia_ManPrintStats( pSrm );
         if ( Gia_ManCoNum(pSrm) == 0 )

src/aig/gia/gia.h

@@ -435,14 +435,15 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== giaAig.c ============================================================*/
+/*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
-/*=== giaAiger.c ==========================================================*/
+/*=== giaAiger.c ===========================================================*/
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
-/*=== giaCof.c ============================================================*/
+/*=== giaCsat.c ============================================================*/
+/*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose );

src/aig/gia/giaCSat0.c

@@ -122,8 +122,10 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
     }
     Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) );
     if ( Value != GIA_ONE )
-        printf( "Gia_SatVerifyPattern(): Verification failed.\n" );
-    assert( Value == GIA_ONE );
+        printf( "Gia_SatVerifyPattern(): Verification FAILED.\n" );
+//    else
+//        printf( "Gia_SatVerifyPattern(): Verification succeeded.\n" );
+//    assert( Value == GIA_ONE );
     // clean the nodes
     Gia_ManForEachObjVec( vVisit, p, pObj, i )
         Sat_ObjSetXValue( pObj, 0 );

src/base/abci/abc.c

@@ -3729,8 +3729,8 @@ int Abc_CommandLutmin( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutSize = 6;
-    fVerbose = 1;
+    nLutSize = 4;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Kvh" ) ) != EOF )
     {
@@ -3744,8 +3744,6 @@ int Abc_CommandLutmin( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             nLutSize = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nLutSize > 1 ) 
-                goto usage;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -23956,6 +23954,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     extern void Gia_SatSolveTest( Gia_Man_t * p );
+    extern void Cbs_ManSolveTest( Gia_Man_t * pGia );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -23983,8 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_SatSolveTest( pAbc->pAig );
 //    For_ManExperiment( pAbc->pAig, 20, 1, 1 );
 //    Gia_ManUnrollSpecial( pAbc->pAig, 5, 100, 1 );
-    pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
-    Gia_ManStop( pTemp );
+//    pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
+//    Gia_ManStop( pTemp );
+//    Cbs_ManSolveTest( pAbc->pAig );
     return 0;
 
 usage:

src/misc/extra/extra.h

@@ -169,7 +169,7 @@ extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
 extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
 extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
 extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
-extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int fShiftUp );
+extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
 extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
 extern void         Extra_StopManager( DdManager * dd );
 extern void         Extra_bddPrint( DdManager * dd, DdNode * F );

src/misc/extra/extraBddMisc.c

@@ -221,6 +221,7 @@ void Extra_StopManager( DdManager * dd )
     // check for remaining references in the package
     RetValue = Cudd_CheckZeroRef( dd );
     if ( RetValue > 10 )
+//    if ( RetValue )
         printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
 //  Cudd_PrintInfo( dd, stdout );
     Cudd_Quit( dd );

src/opt/mfs/mfsSat.c

@@ -43,11 +43,16 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
 {
     int Lits[MFS_FANIN_MAX];
     int RetValue, nBTLimit, iVar, b, Mint;
+//    int nConfs = p->pSat->stats.conflicts;
     if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
         return -1;
     nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
     RetValue = sat_solver_solve( p->pSat, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
+//printf( "%c", RetValue==l_Undef ? '?' : (RetValue==l_False ? '-' : '+') );
+//printf( "%d ", p->pSat->stats.conflicts-nConfs );
+//if ( RetValue==l_False )
+//printf( "\n" );
     if ( RetValue == l_Undef )
         return -1;
     if ( RetValue == l_False )