From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 1 Nov 2010 01:35:04 -0700
Subject: initial commit of public abc

---
 src/sat/proof/pr.c | 22 ++++++++++++++--------
 src/sat/proof/pr.h | 16 ++++++++++------
 2 files changed, 24 insertions(+), 14 deletions(-)

(limited to 'src/sat/proof')

diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
index a951071a..0da16eaf 100644
--- a/src/sat/proof/pr.c
+++ b/src/sat/proof/pr.c
@@ -23,10 +23,14 @@
 #include <string.h>
 #include <assert.h>
 #include <time.h>
+
 //#include "vec.h"
 #include "abc_global.h"
 #include "pr.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -186,7 +190,7 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
         p->pVarTypes = ABC_REALLOC(char,       p->pVarTypes, p->nVarsAlloc );
         p->pReasons  = ABC_REALLOC(Pr_Cls_t *, p->pReasons,  p->nVarsAlloc );
         p->pWatches  = ABC_REALLOC(Pr_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
-        // clean the ABC_FREE space
+        // clean the free space
         memset( p->pAssigns  + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) );
         memset( p->pSeens    + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
         memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
@@ -649,10 +653,10 @@ void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause )
     if ( p->fProofWrite )
     {
         int v;
-        fprintf( p->pManProof, "%d", (int)pClause->pProof );
+        fprintf( (FILE *)p->pManProof, "%d", (int)pClause->pProof );
         for ( v = 0; v < (int)pClause->nLits; v++ )
-            fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) );
-        fprintf( p->pManProof, " 0 0\n" );
+            fprintf( (FILE *)p->pManProof, " %d", lit_print(pClause->pLits[v]) );
+        fprintf( (FILE *)p->pManProof, " 0 0\n" );
     }
 }
 
@@ -718,7 +722,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
         assert( pReason->pProof > 0 );
         p->Counter++;
         if ( p->fProofWrite )
-            fprintf( p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof );
+            fprintf( (FILE *)p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof );
         PrevId = p->Counter;
 
         if ( p->nClausesA )
@@ -1086,7 +1090,7 @@ int Pr_ManProofWrite( Pr_Man_t * p )
     // stop the proof
     if ( p->fProofWrite )
     {
-        fclose( p->pManProof );
+        fclose( (FILE *)p->pManProof );
         p->pManProof = NULL;    
     }
     return RetValue;
@@ -1162,7 +1166,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName )
             for ( ; *pCur && *pCur != ' '; pCur++ );
         }
         // add the clause
-        if ( !Pr_ManAddClause( p, pArray, pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) )
+        if ( !Pr_ManAddClause( p, (unsigned *)pArray, (unsigned *)pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) )
         {
             printf( "Bad clause number %d.\n", Counter );
             return NULL;
@@ -1204,7 +1208,7 @@ int Pr_ManProofCount_rec( Pr_Cls_t * pClause )
     pClause->fVisit = 1;
     // count the number of visited clauses
     Counter = 1;
-    Vec_PtrForEachEntry( pClause->pAntis, pNext, i )
+    Vec_PtrForEachEntry( Pr_Cls_t *, pClause->pAntis, pNext, i )
         Counter += Pr_ManProofCount_rec( pNext );
     return Counter;
 }
@@ -1258,3 +1262,5 @@ p->timeTotal = clock() - clkTotal;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h
index bc55e016..9088c89b 100644
--- a/src/sat/proof/pr.h
+++ b/src/sat/proof/pr.h
@@ -21,6 +21,7 @@
 #ifndef __PR_H__
 #define __PR_H__
 
+
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -33,9 +34,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -53,9 +55,11 @@ typedef struct Pr_Man_t_ Pr_Man_t;
 
 /*=== pr.c ==========================================================*/
  
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
-- 
cgit v1.2.3