Version abc90215

1 files changed, 34 insertions, 34 deletions

diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 025652fe..3cee19ca 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -44,7 +44,7 @@ static int nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects )
 {
     sat_solver * pSat;
     lbool   status;
@@ -70,13 +70,13 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
 //return 1;
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
     status = sat_solver_simplify(pSat);
 //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
     if ( status == 0 )
     {
         sat_solver_delete( pSat );
@@ -88,7 +88,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
@@ -106,7 +106,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     }
     else
         assert( 0 );
-//    PRT( "SAT sat_solver time", clock() - clk );
+//    ABC_PRT( "SAT sat_solver time", clock() - clk );
 //    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
 
     // if the problem is SAT, get the counterexample
@@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
         pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         Vec_IntFree( vCiIds );
     }
-    // free the sat_solver
+    // ABC_FREE the sat_solver
     if ( fVerbose )
         Sat_SolverPrintStats( stdout, pSat );
 
@@ -151,7 +151,7 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
     int i;
     vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
     Abc_NtkForEachCi( pNtk, pObj, i )
-        Vec_IntPush( vCiIds, (int)(PORT_PTRINT_T)pObj->pCopy );
+        Vec_IntPush( vCiIds, (int)(ABC_PTRINT_T)pObj->pCopy );
     return vCiIds;
 }
 
@@ -172,7 +172,7 @@ int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+    Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -195,7 +195,7 @@ int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
     Vec_PtrForEachEntry( vNodes, pNode, i )
-        Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+        Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -220,7 +220,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
     assert( Abc_ObjIsNode( pNode ) );
 
 //    nVars = sat_solver_nvars(pSat);
-    Var = (int)(PORT_PTRINT_T)pNode->pCopy;
+    Var = (int)(ABC_PTRINT_T)pNode->pCopy;
 //    Var = pNode->Id;
 
 //    assert( Var  < nVars ); 
@@ -230,7 +230,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
 
         // check that the variables are in the SAT manager
@@ -255,7 +255,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
         // add this variable to the array
         Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
@@ -283,10 +283,10 @@ int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC,
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_NodeIsMuxType( pNode ) );
     // get the variable numbers
-    VarF = (int)(PORT_PTRINT_T)pNode->pCopy;
-    VarI = (int)(PORT_PTRINT_T)pNodeC->pCopy;
-    VarT = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
-    VarE = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
+    VarF = (int)(ABC_PTRINT_T)pNode->pCopy;
+    VarI = (int)(ABC_PTRINT_T)pNodeC->pCopy;
+    VarT = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
+    VarE = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
 //    VarF = (int)pNode->Id;
 //    VarI = (int)pNodeC->Id;
 //    VarT = (int)Abc_ObjRegular(pNodeT)->Id;
@@ -479,7 +479,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     // add the clause for the constant node
     pNode = Abc_AigConst1(pNtk);
     pNode->fMarkA = 1;
-    pNode->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+    pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
     Vec_PtrPush( vNodes, pNode );
     Abc_NtkClauseTriv( pSat, pNode, vVars );
 /*
@@ -501,7 +501,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
         if ( pFanin->fMarkA == 0 )
         {
             pFanin->fMarkA = 1;
-            pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+            pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
             Vec_PtrPush( vNodes, pFanin );
         }
         // add the trivial clause
@@ -536,7 +536,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -555,7 +555,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -577,7 +577,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     // set preferred variables
     if ( fOrderCiVarsFirst )
     {
-        int * pPrefVars = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        int * pPrefVars = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
         int nVars = 0;
         Abc_NtkForEachCi( pNtk, pNode, i )
         {
@@ -644,7 +644,7 @@ sat_solver_store_mark_roots( pSat );
         return NULL;
     }
 //    printf( "Ands = %6d.  Muxes = %6d (%5.2f %%).  ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
-//    PRT( "Creating sat_solver", clock() - clk );
+//    ABC_PRT( "Creating sat_solver", clock() - clk );
     return pSat;
 }
 
@@ -840,7 +840,7 @@ sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
 
     // transfer the IDs to the copy field
     Abc_NtkForEachPi( pNtk, pNode, i )
-        pNode->pCopy = (void *)(PORT_PTRINT_T)pNode->Id;
+        pNode->pCopy = (void *)(ABC_PTRINT_T)pNode->Id;
 
     // start the data structures
     pSat    = sat_solver_new();
@@ -945,9 +945,9 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pCopy = (void *)~0;
     Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
+        pObj->pCopy = (void *)(ABC_PTRINT_T)Counter++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
+        pObj->pCopy = (void *)(ABC_PTRINT_T)Counter++;
 
 /*
         OutVar   = pCnf->pVarNums[ pObj->Id ];
@@ -975,14 +975,14 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // positive phase
-        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
-            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
+            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
         // negative phase
-        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
-        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
     }
     Vec_PtrFree( vNodes );
 
@@ -992,10 +992,10 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
 */
     // assert the first literal to zero
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
+        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
     // assert the second literal to one
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
+        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
     fclose( pFile );
 }