Extracting CSAT interface and several cleanups.

src/aig/gia/gia.h

@@ -113,6 +113,7 @@ struct Gia_Man_t_
     int            fAddStrash;    // performs additional structural hashing
     int            fSweeper;      // sweeper is running
     int            fGiaSimple;    // simple mode (no const-propagation and strashing)
+    Vec_Int_t      vRefs;         // the reference count
     int *          pRefs;         // the reference count
     int *          pLutRefs;      // the reference count
     Vec_Int_t *    vLevels;       // levels of the nodes
@@ -1203,6 +1204,10 @@ extern Abc_Cex_t *         Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, A
 /*=== giaCsatOld.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
+typedef struct Cbs_Man_t_  Cbs_Man_t;
+extern Cbs_Man_t *         Cbs_ManAlloc( Gia_Man_t * pGia );
+extern void                Cbs_ManStop( Cbs_Man_t * p );
+extern int                 Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCTas.c ============================================================*/
 extern Vec_Int_t *         Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );

src/aig/gia/giaCSat.c

@@ -59,7 +59,7 @@ struct Cbs_Que_t_
     Gia_Obj_t **  pData;        // nodes stored in the queue
 };
  
-typedef struct Cbs_Man_t_ Cbs_Man_t;
+//typedef struct Cbs_Man_t_ Cbs_Man_t;
 struct Cbs_Man_t_
 {
     Cbs_Par_t     Pars;         // parameters
@@ -146,7 +146,7 @@ void Cbs_SetDefaultParams( Cbs_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Cbs_Man_t * Cbs_ManAlloc()
+Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia )
 {
     Cbs_Man_t * p;
     p = ABC_CALLOC( Cbs_Man_t, 1 );
@@ -158,6 +158,7 @@ Cbs_Man_t * Cbs_ManAlloc()
     p->vModel   = Vec_IntAlloc( 1000 );
     p->vLevReas = Vec_IntAlloc( 1000 );
     p->vTemp    = Vec_PtrAlloc( 1000 );
+    p->pAig     = pGia;
     Cbs_SetDefaultParams( &p->Pars );
     return p;
 }
@@ -619,7 +620,7 @@ static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
         pReason = Cbs_VarReason0( p, pObj );
         if ( pReason == pObj ) // no reason
         {
-            assert( pQue->pData[pQue->iHead] == NULL );
+            //assert( pQue->pData[pQue->iHead] == NULL );
             pQue->pData[pQue->iHead] = pObj;
             continue;
         }
@@ -929,7 +930,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
   SeeAlso     []
 
 ***********************************************************************/
-int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
+int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
 {
     int RetValue = 0;
     s_Counter = 0;
@@ -938,6 +939,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
     assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
     p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
     Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+    if ( pObj2 ) 
+    Cbs_ManAssign( p, pObj2, 0, NULL, NULL );
     if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
         Cbs_ManSaveModel( p, p->vModel );
     else
@@ -1014,9 +1017,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Gia_ManFillValue( pAig ); // maps nodes into trail ids
     Gia_ManSetPhase( pAig ); // maps nodes into trail ids
     // create logic network
-    p = Cbs_ManAlloc();
+    p = Cbs_ManAlloc( pAig );
     p->Pars.nBTLimit = nConfs;
-    p->pAig   = pAig;
     // create resulting data-structures
     vStatus   = Vec_StrAlloc( Gia_ManPoNum(pAig) );
     vCexStore = Vec_IntAlloc( 10000 );
@@ -1046,14 +1048,14 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
         clk = Abc_Clock();
         p->Pars.fUseHighest = 1;
         p->Pars.fUseLowest  = 0;
-        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
 //        printf( "\n" );
 /*
         if ( status == -1 )
         {
             p->Pars.fUseHighest = 0;
             p->Pars.fUseLowest  = 1;
-            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
         }
 */
         Vec_StrPush( vStatus, (char)status );

src/aig/gia/giaDup.c

@@ -1988,10 +1988,11 @@ void Gia_ManQuantExist_rec( Gia_Man_t * p, int iObj, int pRes[2] )
 }
 int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int), void * pData )
 {
+//    abctime clk = Abc_Clock();
     Gia_Man_t * pNew;
     Vec_Int_t * vOuts, * vOuts2, * vCis; 
     Gia_Obj_t * pObj = Gia_ManObj( p0, Abc_Lit2Var(iLit) );
-    int i, n, Entry, Lit, OutLit = -1, pLits[2]; 
+    int i, n, Entry, Lit, OutLit = -1, pLits[2], nVarsQua, nAndsOld, nAndsNew; 
     if ( iLit < 2 ) return iLit;
     if ( Gia_ObjIsCi(pObj) ) return pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ? iLit : 1;
     assert( Gia_ObjIsAnd(pObj) );
@@ -2007,6 +2008,8 @@ int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int
     vOuts2 = Vec_IntAlloc( 100 );
     assert( OutLit > 1 );
     Vec_IntPush( vOuts, OutLit );
+    nVarsQua = pNew->iSuppPi;
+    nAndsOld = Gia_ManAndNum(pNew);
     while ( --pNew->iSuppPi >= 0 )
     {
         //printf( "Quantifying input %d:\n", p->iSuppPi );
@@ -2047,8 +2050,14 @@ int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int
     Vec_IntFree( vOuts2 );
     // transfer back
     Gia_ManAppendCo( pNew, OutLit );
+    nAndsNew = Gia_ManAndNum(p0);
     Lit = Gia_ManDupConeBack( p0, pNew, vCis );
+    nAndsNew = Gia_ManAndNum(p0) - nAndsNew;
     Gia_ManStop( pNew );
+    // report the result
+//    printf( "Performed quantification with %6d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d new nodes. ", 
+//        nAndsOld, Vec_IntSize(vCis) - nVarsQua, nVarsQua, nAndsNew );
+//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Vec_IntFree( vCis );
     return Lit;
 }

src/aig/gia/giaMan.c

@@ -142,6 +142,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFree( p->vCos );
     Vec_IntErase( &p->vHash );
     Vec_IntErase( &p->vHTable );
+    Vec_IntErase( &p->vRefs );
     ABC_FREE( p->pData2 );
     ABC_FREE( p->pTravIds );
     ABC_FREE( p->pPlacement );
@@ -157,7 +158,6 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pSibls );
     ABC_FREE( p->pRefs );
     ABC_FREE( p->pLutRefs );
-//    ABC_FREE( p->pHTable );
     ABC_FREE( p->pMuxes );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pSpec );

src/sat/glucose/AbcGlucose.cpp

@@ -919,15 +919,9 @@ void bmcg_sat_generate_dvars( Vec_Int_t * vCiVars, Vec_Str_t * vSop, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-
-abctime clkQuaSetup = 0;
-abctime clkQuaSolve = 0;
-abctime clkQuaSynth = 0;
-
 int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
 {
     int fSynthesize = 0;
-    abctime clk = Abc_Clock();//, clkAll = Abc_Clock();
     extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
     Gia_Man_t * pMan, * pNew, * pTemp;  Vec_Str_t * vSop;
     int i, CiId, ObjId, Res, nCubes = 0, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit);
@@ -946,7 +940,6 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
     nNodes = Gia_ManAndNum(pNew);
 
     // perform quantification one CI at a time
-    clk = Abc_Clock();
     assert( pFuncCiToKeep );
     Vec_IntForEachEntry( vCisUsed, CiId, i )
         if ( !pFuncCiToKeep( pData, CiId ) )
@@ -956,7 +949,6 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
             Gia_ManStop( pTemp );
             Count++;
         }
-    clkQuaSetup += Abc_Clock() - clk;
     if ( Gia_ManPoIsConst(pNew, 0) )
     {
         int RetValue = Gia_ManPoIsConst1(pNew, 0);
@@ -967,16 +959,10 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
 
     if ( fSynthesize )
     {
-        clk = Abc_Clock();
         vSop = bmcg_sat_solver_sop( pNew, 0 );
         Gia_ManStop( pNew );
-        clkQuaSolve += Abc_Clock() - clk;
-
-        clk = Abc_Clock();
         pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 );
         nCubes = Vec_StrCountEntry(vSop, '\n');
-        clkQuaSynth += Abc_Clock() - clk;
-
         if ( vDLits )
         {
             // convert into object IDs
@@ -1095,7 +1081,6 @@ int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, in
 }
 int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
 {
-    abctime clk;//, clkAll = Abc_Clock();
     Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); // GIA objs
     Vec_Int_t * vCiVars = Vec_IntAlloc( 100 );   // CI SAT vars
     Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL; 
@@ -1112,13 +1097,10 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
     assert( iVar == 0 );    
 
     // collect other variables
-    clk = Abc_Clock();
     iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCiVars );
     Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
-    clkQuaSetup += Abc_Clock() - clk;
 
     // check constants
-    clk = Abc_Clock();
     Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) ); 
     RetValue = bmcg_sat_solver_addclause( pSats[0], &Lit, 1 ); // offset
     if ( !RetValue || bmcg_sat_solver_solve(pSats[0], NULL, 0) == GLUCOSE_UNSAT )
@@ -1169,7 +1151,6 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
     }
     // generate cubes
     vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap, 0 );
-    clkQuaSolve += Abc_Clock() - clk;
     //printf( "%s", Vec_StrArray(vSop) );
     // convert into object IDs
     Vec_IntForEachEntry( vCiVars, iVar, i )
@@ -1178,10 +1159,8 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
     if ( vDLits )
         bmcg_sat_generate_dvars( vCiVars, vSop, vDLits );
     // convert into an AIG
-    clk = Abc_Clock();
     RetValue = Gia_ManAndNum(p);
     Result = Gia_ManFactorSop( p, vCiVars, vSop, fHash );
-    clkQuaSynth += Abc_Clock() - clk;
 
     // report the result
 //    printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", 
@@ -1200,7 +1179,6 @@ cleanup:
 int Gia_ManCiIsToKeep( void * pData, int i )
 {
     return i % 5 != 0;
-//    return 1;
 }
 void Glucose_QuantifyAigTest( Gia_Man_t * p )
 {
@@ -1259,12 +1237,8 @@ int bmcg_sat_solver_quantify_test( bmcg_sat_solver * pSats[], Gia_Man_t * p, int
   SeeAlso     []
 
 ***********************************************************************/
-abctime clkTrav = 0;
-abctime clkSatRun = 0;
-
 int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv )
 {
-    abctime clk;
     bmcg_sat_solver * pSats[2] = { pSat, NULL };
     Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); 
     int i, iVar, iSatVar[2], iSatLit[2], Lits[2], status;
@@ -1277,16 +1251,8 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
     Gia_ObjSetCopyArray( p, 0, iVar );
     assert( iVar == 0 );
 
-//printf( "%d ", iLit0 );
-//printf( "%d ", iLit1 );
-//printf( " -> " );
-    clk = Abc_Clock();
     iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL );
-//printf( "%d ", Vec_IntSize(vObjsUsed) );
     iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL );
-    clkTrav += Abc_Clock() - clk;
-//printf( "%d ", Vec_IntSize(vObjsUsed) );
-//printf( "\n" );
 
     iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) );
     iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) );
@@ -1295,7 +1261,6 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
         Gia_ObjSetCopyArray( p, iVar, -1 );
     Vec_IntFree( vObjsUsed );
 
-    clk = Abc_Clock();
     if ( fEquiv )
     {
         Lits[0] = iSatLit[0];
@@ -1307,7 +1272,6 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
             Lits[1] = iSatLit[1];
             status  = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
         }
-        clkSatRun += Abc_Clock() - clk;
         return status == GLUCOSE_UNSAT;
     }
     else
@@ -1315,7 +1279,6 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
         Lits[0] = iSatLit[0];
         Lits[1] = iSatLit[1];
         status  = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
-        clkSatRun += Abc_Clock() - clk;
         return status == GLUCOSE_SAT;
     }
 }