diff options
Diffstat (limited to 'src/sat')
39 files changed, 481 insertions, 548 deletions
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index fe2ed113..849ceb71 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -55,7 +55,7 @@ struct Int_Man_t_ Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) // interpolation data int nVarsAB; // the number of global variables - char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] unsigned * pInters; // storage for interpolants as truth tables (size nClauses) int nIntersAlloc; // the allocated size of truth table array int nWords; // the number of words in the truth table @@ -105,11 +105,11 @@ Int_Man_t * Int_ManAlloc() { Int_Man_t * p; // allocate the manager - p = (Int_Man_t *)malloc( sizeof(Int_Man_t) ); + p = (Int_Man_t *)ABC_ALLOC( char, sizeof(Int_Man_t) ); memset( p, 0, sizeof(Int_Man_t) ); // verification p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // parameters p->fProofWrite = 0; p->fProofVerif = 1; @@ -214,18 +214,18 @@ void Int_ManResize( Int_Man_t * p ) while ( p->nVarsAlloc < p->pCnf->nVars ) p->nVarsAlloc *= 2; // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the free space + // clean the ABC_FREE space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); - memset( p->pVarTypes, 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); @@ -243,7 +243,7 @@ void Int_ManResize( Int_Man_t * p ) while ( p->nClosAlloc < p->pCnf->nClauses ) p->nClosAlloc *= 2; // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + p->pProofNums = ABC_REALLOC(int, p->pProofNums, p->nClosAlloc ); } memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); @@ -251,7 +251,7 @@ void Int_ManResize( Int_Man_t * p ) if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses ) { p->nIntersAlloc = p->nWords * p->pCnf->nClauses; - p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc ); + p->pInters = ABC_REALLOC(unsigned, p->pInters, p->nIntersAlloc ); } // memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses ); } @@ -271,20 +271,20 @@ void Int_ManFree( Int_Man_t * p ) { /* printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); */ - free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); } diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 5edc5b67..5dcc7f0b 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -106,11 +106,11 @@ Inta_Man_t * Inta_ManAlloc() { Inta_Man_t * p; // allocate the manager - p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) ); + p = (Inta_Man_t *)ABC_ALLOC( char, sizeof(Inta_Man_t) ); memset( p, 0, sizeof(Inta_Man_t) ); // verification p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // parameters p->fProofWrite = 0; p->fProofVerif = 1; @@ -195,15 +195,15 @@ void Inta_ManResize( Inta_Man_t * p ) while ( p->nVarsAlloc < p->pCnf->nVars ) p->nVarsAlloc *= 2; // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the free space + // clean the ABC_FREE space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -222,7 +222,7 @@ void Inta_ManResize( Inta_Man_t * p ) while ( p->nClosAlloc < p->pCnf->nClauses ) p->nClosAlloc *= 2; // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); } memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); @@ -230,7 +230,7 @@ void Inta_ManResize( Inta_Man_t * p ) if ( p->nIntersAlloc < p->pCnf->nClauses ) { p->nIntersAlloc = p->pCnf->nClauses; - p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc ); + p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc ); } memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); } @@ -250,20 +250,20 @@ void Inta_ManFree( Inta_Man_t * p ) { /* printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); */ - free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); } @@ -1004,7 +1004,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { -// PRT( "Interpo", clock() - clkTotal ); +// ABC_PRT( "Interpo", clock() - clkTotal ); printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c index e0f4328d..cb7f7828 100644 --- a/src/sat/bsat/satInterB.c +++ b/src/sat/bsat/satInterB.c @@ -108,11 +108,11 @@ Intb_Man_t * Intb_ManAlloc() { Intb_Man_t * p; // allocate the manager - p = (Intb_Man_t *)malloc( sizeof(Intb_Man_t) ); + p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) ); memset( p, 0, sizeof(Intb_Man_t) ); // verification p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // parameters p->fProofWrite = 0; p->fProofVerif = 1; @@ -197,15 +197,15 @@ void Intb_ManResize( Intb_Man_t * p ) while ( p->nVarsAlloc < p->pCnf->nVars ) p->nVarsAlloc *= 2; // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the free space + // clean the ABC_FREE space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -224,7 +224,7 @@ void Intb_ManResize( Intb_Man_t * p ) while ( p->nClosAlloc < p->pCnf->nClauses ) p->nClosAlloc *= 2; // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); } memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); @@ -232,7 +232,7 @@ void Intb_ManResize( Intb_Man_t * p ) if ( p->nIntersAlloc < p->pCnf->nClauses ) { p->nIntersAlloc = p->pCnf->nClauses; - p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc ); + p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc ); } memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); } @@ -252,20 +252,20 @@ void Intb_ManFree( Intb_Man_t * p ) { /* printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); */ - free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); } @@ -987,7 +987,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { -// PRT( "Interpo", clock() - clkTotal ); +// ABC_PRT( "Interpo", clock() - clkTotal ); printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c index c944c36d..57fb79d2 100644 --- a/src/sat/bsat/satInterP.c +++ b/src/sat/bsat/satInterP.c @@ -23,6 +23,7 @@ #include <string.h> #include <assert.h> #include <time.h> + #include "satStore.h" #include "vec.h" @@ -92,11 +93,11 @@ Intp_Man_t * Intp_ManAlloc() { Intp_Man_t * p; // allocate the manager - p = (Intp_Man_t *)malloc( sizeof(Intp_Man_t) ); + p = (Intp_Man_t *)ABC_ALLOC( char, sizeof(Intp_Man_t) ); memset( p, 0, sizeof(Intp_Man_t) ); // verification p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // proof recording p->vAnties = Vec_IntAlloc( 1000 ); p->vBreaks = Vec_IntAlloc( 1000 ); @@ -128,15 +129,15 @@ void Intp_ManResize( Intp_Man_t * p ) while ( p->nVarsAlloc < p->pCnf->nVars ) p->nVarsAlloc *= 2; // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); -// p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); +// p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the free space + // clean the ABC_FREE space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); // memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -152,7 +153,7 @@ void Intp_ManResize( Intp_Man_t * p ) while ( p->nClosAlloc < p->pCnf->nClauses ) p->nClosAlloc *= 2; // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); } memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); } @@ -172,22 +173,22 @@ void Intp_ManFree( Intp_Man_t * p ) { /* printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); */ Vec_IntFree( p->vAnties ); Vec_IntFree( p->vBreaks ); -// free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); -// free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); +// ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); +// ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); } @@ -864,7 +865,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore ) } Vec_PtrFree( vClauses ); // solve the problem - RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); sat_solver_delete( pSat ); if ( fVerbose ) { @@ -874,7 +875,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore ) printf( "UNSAT core verification FAILED. " ); else printf( "UNSAT core verification succeeded. " ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } else { @@ -989,7 +990,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ) if ( fVerbose ) { - PRT( "Core", clock() - clkTotal ); + ABC_PRT( "Core", clock() - clkTotal ); printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c index 1dacb854..f789f927 100644 --- a/src/sat/bsat/satMem.c +++ b/src/sat/bsat/satMem.c @@ -16,8 +16,13 @@ ***********************************************************************/ +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + +#include "abc_global.h" #include "satMem.h" -#include "vec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -30,7 +35,7 @@ struct Sat_MmFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries + char * pEntriesFree; // the linked list of ABC_FREE entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -47,8 +52,8 @@ struct Sat_MmFlex_t_ { // information about individual entries int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to free memory - char * pEnd; // the first entry outside the free memory + char * pCurrent; // the current pointer to ABC_FREE memory + char * pEnd; // the first entry outside the ABC_FREE memory // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -93,7 +98,7 @@ Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize ) { Sat_MmFixed_t * p; - p = ALLOC( Sat_MmFixed_t, 1 ); + p = ABC_ALLOC( Sat_MmFixed_t, 1 ); memset( p, 0, sizeof(Sat_MmFixed_t) ); p->nEntrySize = nEntrySize; @@ -110,7 +115,7 @@ Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize ) p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -141,9 +146,9 @@ void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose ) p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -162,16 +167,16 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ) char * pTemp; int i; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize ); p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; // transform these entries into a linked list pTemp = p->pEntriesFree; @@ -191,7 +196,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list + // return the first entry in the ABC_FREE entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -212,7 +217,7 @@ void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of free entries + // add the entry to the linked list of ABC_FREE entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -235,7 +240,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p ) // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); + ABC_FREE( p->pChunks[i] ); p->nChunks = 1; // transform these entries into a linked list pTemp = p->pChunks[0]; @@ -246,7 +251,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the free entry list + // set the ABC_FREE entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -288,7 +293,7 @@ Sat_MmFlex_t * Sat_MmFlexStart() { Sat_MmFlex_t * p; - p = ALLOC( Sat_MmFlex_t, 1 ); + p = ABC_ALLOC( Sat_MmFlex_t, 1 ); memset( p, 0, sizeof(Sat_MmFlex_t) ); p->nEntriesUsed = 0; @@ -298,7 +303,7 @@ Sat_MmFlex_t * Sat_MmFlexStart() p->nChunkSize = (1 << 16); p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -329,9 +334,9 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose ) p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -348,13 +353,13 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose ) char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes ) { char * pTemp; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) { // need to allocate more entries if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } if ( nBytes > p->nChunkSize ) { @@ -362,7 +367,7 @@ char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes ) // (ideally, this should never happen) p->nChunkSize = 2 * nBytes; } - p->pCurrent = ALLOC( char, p->nChunkSize ); + p->pCurrent = ABC_ALLOC( char, p->nChunkSize ); p->pEnd = p->pCurrent + p->nChunkSize; p->nMemoryAlloc += p->nChunkSize; // add the chunk to the chunk storage @@ -412,7 +417,7 @@ int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p ) are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger - entries are handed over to malloc() and then free()ed.] + entries are handed over to malloc() and then ABC_FREE()ed.] SideEffects [] @@ -423,15 +428,15 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps ) { Sat_MmStep_t * p; int i, k; - p = ALLOC( Sat_MmStep_t, 1 ); + p = ABC_ALLOC( Sat_MmStep_t, 1 ); p->nMems = nSteps; // start the fixed memory managers - p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems ); + p->pMems = ABC_ALLOC( Sat_MmFixed_t *, p->nMems ); for ( i = 0; i < p->nMems; i++ ) p->pMems[i] = Sat_MmFixedStart( (8<<i) ); // set up the mapping of the required memory size into the corresponding manager p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 ); + p->pMap = ABC_ALLOC( Sat_MmFixed_t *, p->nMapSize+1 ); p->pMap[0] = NULL; for ( k = 1; k <= 4; k++ ) p->pMap[k] = p->pMems[0]; @@ -442,7 +447,7 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps ) //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); return p; } @@ -463,14 +468,14 @@ void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose ) if ( p->nChunksAlloc ) { for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); } for ( i = 0; i < p->nMems; i++ ) Sat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); + ABC_FREE( p->pMems ); + ABC_FREE( p->pMap ); + ABC_FREE( p ); } /**Function************************************************************* @@ -493,9 +498,9 @@ char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes ) if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes ); + p->pChunks[ p->nChunks++ ] = ABC_ALLOC( char, nBytes ); return p->pChunks[p->nChunks-1]; } return Sat_MmFixedEntryFetch( p->pMap[nBytes] ); @@ -519,7 +524,7 @@ void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { -// free( pEntry ); +// ABC_FREE( pEntry ); return; } Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h index f60d7fdd..b6d93807 100644 --- a/src/sat/bsat/satMem.h +++ b/src/sat/bsat/satMem.h @@ -23,11 +23,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> - //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 833ea394..d2ebf552 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <math.h> #include "satSolver.h" -#include "port_type.h" //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT @@ -91,9 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ //================================================================================================= // Encode literals in clause pointers: -static inline clause* clause_from_lit (lit l) { return (clause*)((PORT_PTRUINT_T)l + (PORT_PTRUINT_T)l + 1); } -static inline bool clause_is_lit (clause* c) { return ((PORT_PTRUINT_T)c & 1); } -static inline lit clause_read_lit (clause* c) { return (lit)((PORT_PTRUINT_T)c >> 1); } +static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); } +static inline bool clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } +static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); } //================================================================================================= // Simple helpers: @@ -288,15 +287,15 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); size = end - begin; -// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); +// c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); + c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); #else c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); #endif c->size_learnt = (size << 1) | learnt; - assert(((PORT_PTRUINT_T)c & 1) == 0); + assert(((ABC_PTRUINT_T)c & 1) == 0); for (i = 0; i < size; i++) c->lits[i] = begin[i]; @@ -344,7 +343,7 @@ static void clause_remove(sat_solver* s, clause* c) } #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - free(c); + ABC_FREE(c); #else Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); #endif @@ -378,15 +377,15 @@ void sat_solver_setnvars(sat_solver* s,int n) while (s->cap < n) s->cap = s->cap*2+1; - s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); - s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); - s->factors = (double*) realloc(s->factors, sizeof(double)*s->cap); - s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); - s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); - s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); - s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); - s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); - s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); + s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); + s->activity = ABC_REALLOC(double, s->activity, s->cap); + s->factors = ABC_REALLOC(double, s->factors, s->cap); + s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap); + s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); + s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap); + s->levels = ABC_REALLOC(int, s->levels, s->cap); + s->tags = ABC_REALLOC(lbool, s->tags, s->cap); + s->trail = ABC_REALLOC(lit, s->trail, s->cap); } for (var = s->size; var < n; var++){ @@ -830,14 +829,14 @@ void sat_solver_reducedb(sat_solver* s) vecp_resize(&s->learnts,j); } -static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts) +static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts) { int* levels = s->levels; double var_decay = 0.95; double clause_decay = 0.999; double random_var_freq = 0.02; - sint64 conflictC = 0; + ABC_INT64_T conflictC = 0; veci learnt_clause; int i; @@ -950,7 +949,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l sat_solver* sat_solver_new(void) { - sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver)); + sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver)); memset( s, 0, sizeof(sat_solver) ); // initialize vectors @@ -990,7 +989,7 @@ sat_solver* sat_solver_new(void) s->simpdb_props = 0; s->random_seed = 91648253; s->progress_estimate = 0; - s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); + s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); s->binary->size_learnt = (2 << 1); s->verbosity = 0; @@ -1021,9 +1020,9 @@ void sat_solver_delete(sat_solver* s) #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT int i; for (i = 0; i < vecp_size(&s->clauses); i++) - free(vecp_begin(&s->clauses)[i]); + ABC_FREE(vecp_begin(&s->clauses)[i]); for (i = 0; i < vecp_size(&s->learnts); i++) - free(vecp_begin(&s->learnts)[i]); + ABC_FREE(vecp_begin(&s->learnts)[i]); #else Sat_MmStepStop( s->pMem, 0 ); #endif @@ -1038,7 +1037,7 @@ void sat_solver_delete(sat_solver* s) veci_delete(&s->model); veci_delete(&s->act_vars); veci_delete(&s->temp_clause); - free(s->binary); + ABC_FREE(s->binary); // delete arrays if (s->wlists != 0){ @@ -1047,19 +1046,19 @@ void sat_solver_delete(sat_solver* s) vecp_delete(&s->wlists[i]); // if one is different from null, all are - free(s->wlists ); - free(s->activity ); - free(s->factors ); - free(s->assigns ); - free(s->orderpos ); - free(s->reasons ); - free(s->levels ); - free(s->trail ); - free(s->tags ); + ABC_FREE(s->wlists ); + ABC_FREE(s->activity ); + ABC_FREE(s->factors ); + ABC_FREE(s->assigns ); + ABC_FREE(s->orderpos ); + ABC_FREE(s->reasons ); + ABC_FREE(s->levels ); + ABC_FREE(s->trail ); + ABC_FREE(s->tags ); } sat_solver_store_free(s); - free(s); + ABC_FREE(s); } @@ -1172,10 +1171,10 @@ bool sat_solver_simplify(sat_solver* s) } -int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal) +int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { - sint64 nof_conflicts = 100; - sint64 nof_learnts = sat_solver_nclauses(s) / 3; + ABC_INT64_T nof_conflicts = 100; + ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; lit* i; @@ -1398,6 +1397,9 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) { +// int i; double seed = 91648253; sortrnd(array,size,comp,&seed); +// for ( i = 1; i < size; i++ ) +// assert(comp(array[i-1], array[i])<0); } diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 7bb4bd6c..f37c1738 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -22,10 +22,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef satSolver_h #define satSolver_h -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 -#endif +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include "abc_global.h" #include "satVec.h" #include "satMem.h" @@ -46,17 +48,6 @@ static const bool false = 0; typedef int lit; typedef char lbool; -#ifndef SINT64 -#define SINT64 - -#ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 -#else -typedef long long sint64; -#endif - -#endif - static const int var_Undef = -1; static const lit lit_Undef = -2; @@ -85,7 +76,7 @@ extern void sat_solver_delete(sat_solver* s); extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end); extern bool sat_solver_simplify(sat_solver* s); -extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal); +extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_nvars(sat_solver* s); extern int sat_solver_nclauses(sat_solver* s); @@ -95,8 +86,8 @@ extern void sat_solver_setnvars(sat_solver* s,int n); struct stats_t { - sint64 starts, decisions, propagations, inspects, conflicts; - sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; + ABC_INT64_T starts, decisions, propagations, inspects, conflicts; + ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; }; typedef struct stats_t stats; @@ -167,8 +158,8 @@ struct sat_solver_t stats stats; - sint64 nConfLimit; // external limit on the number of conflicts - sint64 nInsLimit; // external limit on the number of implications + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications veci act_vars; // variables whose activity has changed double* factors; // the activity factors diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c index 31fe92ca..fff8a836 100644 --- a/src/sat/bsat/satStore.c +++ b/src/sat/bsat/satStore.c @@ -23,6 +23,7 @@ #include <string.h> #include <assert.h> #include <time.h> + #include "satStore.h" //////////////////////////////////////////////////////////////////////// @@ -49,7 +50,7 @@ char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes ) char * pMem; if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) { - pMem = (char *)malloc( p->nChunkSize ); + pMem = (char *)ABC_ALLOC( char, p->nChunkSize ); *(char **)pMem = p->pChunkLast; p->pChunkLast = pMem; p->nChunkUsed = sizeof(char *); @@ -76,8 +77,8 @@ void Sto_ManMemoryStop( Sto_Man_t * p ) if ( p->pChunkLast == NULL ) return; for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext ) - free( pMem ); - free( pMem ); + ABC_FREE( pMem ); + ABC_FREE( pMem ); } /**Function************************************************************* @@ -119,7 +120,7 @@ Sto_Man_t * Sto_ManAlloc() { Sto_Man_t * p; // allocate the manager - p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) ); + p = (Sto_Man_t *)ABC_ALLOC( char, sizeof(Sto_Man_t) ); memset( p, 0, sizeof(Sto_Man_t) ); // memory management p->nChunkSize = (1<<16); // use 64K chunks @@ -140,7 +141,7 @@ Sto_Man_t * Sto_ManAlloc() void Sto_ManFree( Sto_Man_t * p ) { Sto_ManMemoryStop( p ); - free( p ); + ABC_FREE( p ); } /**Function************************************************************* @@ -398,7 +399,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) // alloc the array of literals nLitsAlloc = 1024; - pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc ); + pLits = (lit *)ABC_ALLOC( char, sizeof(lit) * nLitsAlloc ); // read file header p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0; @@ -429,7 +430,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) if ( nLits == nLitsAlloc ) { nLitsAlloc *= 2; - pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc ); + pLits = ABC_REALLOC( lit, pLits, nLitsAlloc ); } pLits[ nLits++ ] = lit_read(Number); } @@ -449,7 +450,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) return NULL; } - free( pLits ); + ABC_FREE( pLits ); fclose( pFile ); return p; } diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h index f63703d3..ea11f46a 100644 --- a/src/sat/bsat/satStore.h +++ b/src/sat/bsat/satStore.h @@ -21,8 +21,6 @@ #ifndef __SAT_STORE_H__ #define __SAT_STORE_H__ -#include "satSolver.h" - /* The trace of SAT solving contains the original clauses of the problem along with the learned clauses derived during SAT solving. @@ -30,6 +28,16 @@ c <num_vars> <num_all_clauses> <num_root_clauses> */ +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + #ifdef __cplusplus extern "C" { #endif @@ -38,21 +46,9 @@ extern "C" { #define inline __inline // compatible with MS VS 6.0 #endif -#ifndef PRT -#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) -#endif - #define STO_MAX(a,b) ((a) > (b) ? (a) : (b)) //////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c index 111e8dfb..08cfadf6 100644 --- a/src/sat/bsat/satTrace.c +++ b/src/sat/bsat/satTrace.c @@ -18,8 +18,6 @@ ***********************************************************************/ -#include <stdio.h> -#include <assert.h> #include "satSolver.h" /* diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index ff8f9fd6..5f8008bb 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -21,7 +21,6 @@ #include <stdio.h> #include <assert.h> #include "satSolver.h" -#include "vec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -170,7 +169,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) { int * pModel; int i; - pModel = ALLOC( int, nVars+1 ); + pModel = ABC_ALLOC( int, nVars+1 ); for ( i = 0; i < nVars; i++ ) { assert( pVars[i] >= 0 && pVars[i] < p->size ); diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index d7fce5c0..f017c90b 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -22,8 +22,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef satVec_h #define satVec_h -#include <stdlib.h> - // vector of 32-bit intergers (added for 64-bit portability) struct veci_t { int size; @@ -35,10 +33,10 @@ typedef struct veci_t veci; static inline void veci_new (veci* v) { v->size = 0; v->cap = 4; - v->ptr = (int*)malloc(sizeof(int)*v->cap); + v->ptr = (int*)ABC_ALLOC( char, sizeof(int)*v->cap); } -static inline void veci_delete (veci* v) { free(v->ptr); } +static inline void veci_delete (veci* v) { ABC_FREE(v->ptr); } static inline int* veci_begin (veci* v) { return v->ptr; } static inline int veci_size (veci* v) { return v->size; } static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! @@ -46,7 +44,7 @@ static inline void veci_push (veci* v, int e) { if (v->size == v->cap) { int newsize = v->cap * 2;//+1; - v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); + v->ptr = ABC_REALLOC( int, v->ptr, newsize ); v->cap = newsize; } v->ptr[v->size++] = e; } @@ -63,10 +61,10 @@ typedef struct vecp_t vecp; static inline void vecp_new (vecp* v) { v->size = 0; v->cap = 4; - v->ptr = (void**)malloc(sizeof(void*)*v->cap); + v->ptr = (void**)ABC_ALLOC( char, sizeof(void*)*v->cap); } -static inline void vecp_delete (vecp* v) { free(v->ptr); } +static inline void vecp_delete (vecp* v) { ABC_FREE(v->ptr); } static inline void** vecp_begin (vecp* v) { return v->ptr; } static inline int vecp_size (vecp* v) { return v->size; } static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !! @@ -74,7 +72,7 @@ static inline void vecp_push (vecp* v, void* e) { if (v->size == v->cap) { int newsize = v->cap * 2;//+1; - v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize); + v->ptr = ABC_REALLOC( void*, v->ptr, newsize ); v->cap = newsize; } v->ptr[v->size++] = e; } diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index e755d8d4..79c0655b 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -77,7 +77,7 @@ ABC_Manager ABC_InitManager() { ABC_Manager_t * mng; Abc_Start(); - mng = ALLOC( ABC_Manager_t, 1 ); + mng = ABC_ALLOC( ABC_Manager_t, 1 ); memset( mng, 0, sizeof(ABC_Manager_t) ); mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); mng->pNtk->pName = Extra_UtilStrsav("csat_network"); @@ -116,8 +116,8 @@ void ABC_ReleaseManager( ABC_Manager mng ) if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); if ( mng->vNodes ) Vec_PtrFree( mng->vNodes ); if ( mng->vValues ) Vec_IntFree( mng->vValues ); - FREE( mng->pDumpFileName ); - free( mng ); + ABC_FREE( mng->pDumpFileName ); + ABC_FREE( mng ); Abc_Stop(); } @@ -442,7 +442,7 @@ void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num ) +void ABC_SetTotalBacktrackLimit( ABC_Manager mng, ABC_UINT64_T num ) { mng->Params.nTotalBacktrackLimit = num; } @@ -458,7 +458,7 @@ void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num ) SeeAlso [] ***********************************************************************/ -void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num ) +void ABC_SetTotalInspectLimit( ABC_Manager mng, ABC_UINT64_T num ) { mng->Params.nTotalInspectLimit = num; } @@ -473,7 +473,7 @@ void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num ) SeeAlso [] ***********************************************************************/ -uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng ) +ABC_UINT64_T ABC_GetTotalBacktracksMade( ABC_Manager mng ) { return mng->Params.nTotalBacktracksMade; } @@ -489,7 +489,7 @@ uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng ) SeeAlso [] ***********************************************************************/ -uint64 ABC_GetTotalInspectsMade( ABC_Manager mng ) +ABC_UINT64_T ABC_GetTotalInspectsMade( ABC_Manager mng ) { return mng->Params.nTotalInspectsMade; } @@ -507,7 +507,7 @@ uint64 ABC_GetTotalInspectsMade( ABC_Manager mng ) ***********************************************************************/ void ABC_EnableDump( ABC_Manager mng, char * dump_file ) { - FREE( mng->pDumpFileName ); + ABC_FREE( mng->pDumpFileName ); mng->pDumpFileName = Extra_UtilStrsav( dump_file ); } @@ -569,7 +569,7 @@ void ABC_SolveInit( ABC_Manager mng ) if ( mng->nog == 0 ) { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; } - // free the previous target network if present + // ABC_FREE the previous target network if present if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); // set the new target network @@ -614,7 +614,7 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) // try to prove the miter using a number of techniques if ( mng->mode ) - RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( mng->pTarget, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL ); else // RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine @@ -634,7 +634,7 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) mng->pResult->names[i] = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) ); mng->pResult->values[i] = mng->pTarget->pModel[i]; } - FREE( mng->pTarget->pModel ); + ABC_FREE( mng->pTarget->pModel ); } else assert( 0 ); @@ -704,11 +704,11 @@ void ABC_Dump_Bench_File( ABC_Manager mng ) CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars ) { CSAT_Target_ResultT * p; - p = ALLOC( CSAT_Target_ResultT, 1 ); + p = ABC_ALLOC( CSAT_Target_ResultT, 1 ); memset( p, 0, sizeof(CSAT_Target_ResultT) ); p->no_sig = nVars; - p->names = ALLOC( char *, nVars ); - p->values = ALLOC( int, nVars ); + p->names = ABC_ALLOC( char *, nVars ); + p->values = ABC_ALLOC( int, nVars ); memset( p->names, 0, sizeof(char *) * nVars ); memset( p->values, 0, sizeof(int) * nVars ); return p; @@ -734,12 +734,12 @@ void ABC_TargetResFree( CSAT_Target_ResultT * p ) int i = 0; for ( i = 0; i < p->no_sig; i++ ) { - FREE(p->names[i]); + ABC_FREE(p->names[i]); } } - FREE( p->names ); - FREE( p->values ); - free( p ); + ABC_FREE( p->names ); + ABC_FREE( p->values ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index b80eddbf..337056a3 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -19,10 +19,6 @@ #ifndef __ABC_APIS_H__ #define __ABC_APIS_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -31,6 +27,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -182,10 +182,10 @@ extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num); extern void ABC_EnableDump(ABC_Manager mng, char* dump_file); -extern void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num ); -extern void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num ); -extern uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng ); -extern uint64 ABC_GetTotalInspectsMade( ABC_Manager mng ); +extern void ABC_SetTotalBacktrackLimit( ABC_Manager mng, ABC_UINT64_T num ); +extern void ABC_SetTotalInspectLimit( ABC_Manager mng, ABC_UINT64_T num ); +extern ABC_UINT64_T ABC_GetTotalBacktracksMade( ABC_Manager mng ); +extern ABC_UINT64_T ABC_GetTotalInspectsMade( ABC_Manager mng ); // the meaning of the parameters are: // nog: number of gates that are in the targets diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index c08e7e3a..ce686cef 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -19,29 +19,18 @@ #ifndef __FRAIG_H__ #define __FRAIG_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#ifndef SINT64 -#define SINT64 - -#ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 -#else -typedef long long sint64; -#endif - -#endif - //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -70,7 +59,7 @@ struct Fraig_ParamsStruct_t_ int fVerboseP; // the verbosiness flag (for proof reporting) int fInternal; // is set to 1 for internal fraig calls int nConfLimit; // the limit on the number of conflicts - sint64 nInspLimit; // the limit on the number of inspections + ABC_INT64_T nInspLimit; // the limit on the number of inspections }; struct Prove_ParamsStruct_t_ @@ -97,11 +86,11 @@ struct Prove_ParamsStruct_t_ // last-gasp mitering int nMiteringLimitLast; // final mitering limit // global SAT solver limits - sint64 nTotalBacktrackLimit; // global limit on the number of backtracks - sint64 nTotalInspectLimit; // global limit on the number of clause inspects + ABC_INT64_T nTotalBacktrackLimit; // global limit on the number of backtracks + ABC_INT64_T nTotalInspectLimit; // global limit on the number of clause inspects // global resources applied - sint64 nTotalBacktracksMade; // the total number of backtracks made - sint64 nTotalInspectsMade; // the total number of inspects made + ABC_INT64_T nTotalBacktracksMade; // the total number of backtracks made + ABC_INT64_T nTotalInspectsMade; // the total number of inspects made }; //////////////////////////////////////////////////////////////////////// @@ -113,10 +102,10 @@ struct Prove_ParamsStruct_t_ //////////////////////////////////////////////////////////////////////// // macros working with complemented attributes of the nodes -#define Fraig_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01))) -#define Fraig_Regular(p) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) & ~01)) -#define Fraig_Not(p) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ 01)) -#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ (c))) +#define Fraig_IsComplement(p) (((int)((ABC_PTRUINT_T) (p) & 01))) +#define Fraig_Regular(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) +#define Fraig_Not(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) +#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c))) // these are currently not used #define Fraig_Ref(p) diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c index e1e8d12c..7d99d146 100644 --- a/src/sat/fraig/fraigFeed.c +++ b/src/sat/fraig/fraigFeed.c @@ -391,7 +391,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ) vColumns = Fraig_FeedBackCoveringStart( p ); // collect the number of 1s in each simulation vector nOnesTotal = 0; - pHits = ALLOC( int, vColumns->nSize ); + pHits = ABC_ALLOC( int, vColumns->nSize ); for ( i = 0; i < vColumns->nSize; i++ ) { pSims = (unsigned *)vColumns->pArray[i]; @@ -412,7 +412,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ) Msat_IntVecPush( vPats, iPat ); } - // free the set of columns + // ABC_FREE the set of columns for ( i = 0; i < vColumns->nSize; i++ ) Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] ); @@ -427,7 +427,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ) printf( "\n" ); } Fraig_NodeVecFree( vColumns ); - free( pHits ); + ABC_FREE( pHits ); } @@ -736,7 +736,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) // signatures remain without changes } - // replace the manager to free up some memory + // replace the manager to ABC_FREE up some memory Fraig_MemFixedStop( p->mmSims, 0 ); p->mmSims = mmSimsNew; @@ -783,7 +783,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ) { int * pModel; - pModel = ALLOC( int, p->vInputs->nSize ); + pModel = ABC_ALLOC( int, p->vInputs->nSize ); memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); return pModel; } @@ -896,7 +896,7 @@ printf( "\n" ); assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); return pModel; } - FREE( pModel ); + ABC_FREE( pModel ); return NULL; } diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 0e8b1e31..3bea5e42 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -29,9 +29,9 @@ #include <assert.h> #include <time.h> +#include "abc_global.h" #include "fraig.h" #include "msat.h" -#include "port_type.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -57,9 +57,9 @@ #define FRAIG_MAX_PRIMES 1024 // the maximum number of primes used for hashing // this parameter determines when simulation info is extended -// it will be extended when the free storage in the dynamic simulation +// it will be extended when the ABC_FREE storage in the dynamic simulation // info is less or equal to this number of words (FRAIG_WORDS_STORE) -// this is done because if the free storage for dynamic simulation info +// this is done because if the ABC_FREE storage for dynamic simulation info // is not sufficient, computation becomes inefficient #define FRAIG_WORDS_STORE 5 @@ -86,35 +86,14 @@ #define Fraig_NodeSetVarStr(p,i) Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i) #define Fraig_NodeHasVarStr(p,i) Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i) -// copied from "util.h" for standaloneness -#ifndef ALLOC -# define ALLOC(type, num) \ - ((type *) malloc(sizeof(type) * (num))) -#endif - -#ifndef REALLOC -# define REALLOC(type, obj, num) \ - (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \ - ((type *) malloc(sizeof(type) * (num))) -#endif - -#ifndef FREE -# define FREE(obj) \ - ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) -#endif - // copied from "extra.h" for stand-aloneness #define Fraig_PrintTime(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) -#define Fraig_HashKey2(a,b,TSIZE) (((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * 12582917) % TSIZE) +#define Fraig_HashKey2(a,b,TSIZE) (((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * 12582917) % TSIZE) //#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE) //#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE) // the other two hash functions give bad distribution of hash chain lengths (not clear why) -#ifndef PRT -#define PRT(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) -#endif - //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -152,7 +131,7 @@ struct Fraig_ManStruct_t_ int fTryProve; // tries to solve the final miter int fVerbose; // the verbosiness flag int fVerboseP; // the verbosiness flag - sint64 nInspLimit; // the inspection limit + ABC_INT64_T nInspLimit; // the inspection limit int nTravIds; // the traversal counter int nTravIds2; // the traversal counter diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index cbeef4c6..b71262d8 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -204,7 +204,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) pParams->nPatsRand = pParams->nPatsDyna = 128; // start the manager - p = ALLOC( Fraig_Man_t, 1 ); + p = ABC_ALLOC( Fraig_Man_t, 1 ); memset( p, 0, sizeof(Fraig_Man_t) ); // set the default parameters @@ -286,25 +286,25 @@ void Fraig_ManFree( Fraig_Man_t * p ) if ( p->vProj ) Msat_IntVecFree( p->vProj ); if ( p->vCones ) Fraig_NodeVecFree( p->vCones ); if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal ); - if ( p->pModel ) free( p->pModel ); + if ( p->pModel ) ABC_FREE( p->pModel ); Fraig_MemFixedStop( p->mmNodes, 0 ); Fraig_MemFixedStop( p->mmSims, 0 ); if ( p->pSuppS ) { - FREE( p->pSuppS[0] ); - FREE( p->pSuppS ); + ABC_FREE( p->pSuppS[0] ); + ABC_FREE( p->pSuppS ); } if ( p->pSuppF ) { - FREE( p->pSuppF[0] ); - FREE( p->pSuppF ); + ABC_FREE( p->pSuppF[0] ); + ABC_FREE( p->pSuppF ); } - FREE( p->ppOutputNames ); - FREE( p->ppInputNames ); - FREE( p ); + ABC_FREE( p->ppOutputNames ); + ABC_FREE( p->ppInputNames ); + ABC_FREE( p ); } /**Function************************************************************* @@ -366,8 +366,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); } if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); } if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); } -// PRT( "Selection ", timeSelect ); -// PRT( "Assignment", timeAssign ); +// ABC_PRT( "Selection ", timeSelect ); +// ABC_PRT( "Assignment", timeAssign ); fflush( stdout ); } @@ -389,7 +389,7 @@ Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean ) int i; assert( nSize > 0 && nWords > 0 ); vInfo = Fraig_NodeVecAlloc( nSize ); - pUnsigned = ALLOC( unsigned, nSize * nWords ); + pUnsigned = ABC_ALLOC( unsigned, nSize * nWords ); vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned; if ( fClean ) memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords ); diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c index 500431c6..1cc99790 100644 --- a/src/sat/fraig/fraigMem.c +++ b/src/sat/fraig/fraigMem.c @@ -29,7 +29,7 @@ struct Fraig_MemFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries + char * pEntriesFree; // the linked list of ABC_FREE entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -61,7 +61,7 @@ Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ) { Fraig_MemFixed_t * p; - p = ALLOC( Fraig_MemFixed_t, 1 ); + p = ABC_ALLOC( Fraig_MemFixed_t, 1 ); memset( p, 0, sizeof(Fraig_MemFixed_t) ); p->nEntrySize = nEntrySize; @@ -78,7 +78,7 @@ Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ) p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -109,9 +109,9 @@ void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose ) p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -130,16 +130,16 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ) char * pTemp; int i; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize ); p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; // transform these entries into a linked list pTemp = p->pEntriesFree; @@ -159,7 +159,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list + // return the first entry in the ABC_FREE entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -180,7 +180,7 @@ void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of free entries + // add the entry to the linked list of ABC_FREE entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -203,7 +203,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); + ABC_FREE( p->pChunks[i] ); p->nChunks = 1; // transform these entries into a linked list pTemp = p->pChunks[0]; @@ -214,7 +214,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the free entry list + // set the ABC_FREE entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 53057fc3..66698600 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -109,7 +109,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) } if ( p->fVerboseP ) { -// PRT( "Final miter proof time", clock() - clk ); +// ABC_PRT( "Final miter proof time", clock() - clk ); } } @@ -128,7 +128,7 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p ) { Fraig_Node_t * pNode; int i; - FREE( p->pModel ); + ABC_FREE( p->pModel ); for ( i = 0; i < p->vOutputs->nSize; i++ ) { // get the output node (it can be complemented!) @@ -352,7 +352,7 @@ clk = clock(); p->timeTrav += clock() - clk; // printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); -// PRT( "Time", clock() - clk ); +// ABC_PRT( "Time", clock() - clk ); if ( fVerbose ) printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); @@ -391,8 +391,8 @@ p->timeSat += clock() - clk; if ( fVerbose ) { - printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // add the clause @@ -409,8 +409,8 @@ PRT( "time", clock() - clk ); if ( fVerbose ) { - printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // record the counter example @@ -468,8 +468,8 @@ p->timeSat += clock() - clk; if ( fVerbose ) { - printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // add the clause @@ -486,8 +486,8 @@ PRT( "time", clock() - clk ); if ( fVerbose ) { - printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // record the counter example @@ -599,8 +599,8 @@ p->timeSat += clock() - clk; if ( fVerbose ) { - printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // add the clause @@ -618,8 +618,8 @@ PRT( "time", clock() - clk ); if ( fVerbose ) { - printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // record the counter example Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); @@ -690,8 +690,8 @@ p->timeSat += clock() - clk; if ( fVerbose ) { - printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // add the clause @@ -709,8 +709,8 @@ PRT( "time", clock() - clk ); if ( fVerbose ) { - printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); -PRT( "time", clock() - clk ); +// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) ); +//ABC_PRT( "time", clock() - clk ); } // record the counter example // Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R ); @@ -907,7 +907,7 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t { // create the fanins of the supergate assert( pNode->fClauses == 0 ); - // detecting a fanout-free cone (experiment only) + // detecting a fanout-ABC_FREE cone (experiment only) // Fraig_DetectFanoutFreeCone( pMan, pNode ); if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c index b68bbe0e..55d92b4a 100644 --- a/src/sat/fraig/fraigTable.c +++ b/src/sat/fraig/fraigTable.c @@ -44,11 +44,11 @@ Fraig_HashTable_t * Fraig_HashTableCreate( int nSize ) { Fraig_HashTable_t * p; // allocate the table - p = ALLOC( Fraig_HashTable_t, 1 ); + p = ABC_ALLOC( Fraig_HashTable_t, 1 ); memset( p, 0, sizeof(Fraig_HashTable_t) ); // allocate and clean the bins p->nBins = Cudd_PrimeFraig(nSize); - p->pBins = ALLOC( Fraig_Node_t *, p->nBins ); + p->pBins = ABC_ALLOC( Fraig_Node_t *, p->nBins ); memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins ); return p; } @@ -66,8 +66,8 @@ Fraig_HashTable_t * Fraig_HashTableCreate( int nSize ) ***********************************************************************/ void Fraig_HashTableFree( Fraig_HashTable_t * p ) { - FREE( p->pBins ); - FREE( p ); + ABC_FREE( p->pBins ); + ABC_FREE( p ); } /**Function************************************************************* @@ -264,7 +264,7 @@ clk = clock(); // get the new table size nBinsNew = Cudd_PrimeFraig(2 * p->nBins); // allocate a new array - pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew ); + pBinsNew = ABC_ALLOC( Fraig_Node_t *, nBinsNew ); memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew ); // rehash the entries from the old table Counter = 0; @@ -278,9 +278,9 @@ clk = clock(); } assert( Counter == p->nEntries ); // printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew ); -// PRT( "Time", clock() - clk ); +// ABC_PRT( "Time", clock() - clk ); // replace the table and the parameters - free( p->pBins ); + ABC_FREE( p->pBins ); p->pBins = pBinsNew; p->nBins = nBinsNew; } @@ -307,7 +307,7 @@ clk = clock(); // get the new table size nBinsNew = Cudd_PrimeFraig(2 * p->nBins); // allocate a new array - pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew ); + pBinsNew = ABC_ALLOC( Fraig_Node_t *, nBinsNew ); memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew ); // rehash the entries from the old table Counter = 0; @@ -324,9 +324,9 @@ clk = clock(); } assert( Counter == p->nEntries ); // printf( "Increasing the functional table size from %6d to %6d. ", p->nBins, nBinsNew ); -// PRT( "Time", clock() - clk ); +// ABC_PRT( "Time", clock() - clk ); // replace the table and the parameters - free( p->pBins ); + ABC_FREE( p->pBins ); p->pBins = pBinsNew; p->nBins = nBinsNew; } @@ -605,7 +605,7 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv ) unsigned Key; // allocate a new array of bins - pBinsNew = ALLOC( Fraig_Node_t *, pT->nBins ); + pBinsNew = ABC_ALLOC( Fraig_Node_t *, pT->nBins ); memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins ); // rehash the entries in the table @@ -645,7 +645,7 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv ) } assert( Counter == pT->nEntries ); // replace the table and the parameters - free( pT->pBins ); + ABC_FREE( pT->pBins ); pT->pBins = pBinsNew; return ReturnValue; } diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c index 342a7111..ea52d363 100644 --- a/src/sat/fraig/fraigUtil.c +++ b/src/sat/fraig/fraigUtil.c @@ -237,7 +237,7 @@ int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNe Description [This procedure collects the nodes reachable from the POs of the AIG and sets the type of fanout counter (none, one, or many) for each node. This procedure is useful to determine - fanout-free cones of AND-nodes, which is helpful for rebalancing + fanout-ABC_FREE cones of AND-nodes, which is helpful for rebalancing the AIG (see procedure Fraig_ManRebalance, or something like that).] SideEffects [] @@ -881,7 +881,7 @@ clk = clock(); } } printf( "Number of candidate pairs = %d. Proved = %d.\n", Counter, nProved ); -PRT( "Time", clock() - clk ); +//ABC_PRT( "Time", clock() - clk ); return 0; } diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c index ba3feecd..b47c6a2f 100644 --- a/src/sat/fraig/fraigVec.c +++ b/src/sat/fraig/fraigVec.c @@ -40,12 +40,12 @@ Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap ) { Fraig_NodeVec_t * p; - p = ALLOC( Fraig_NodeVec_t, 1 ); + p = ABC_ALLOC( Fraig_NodeVec_t, 1 ); if ( nCap > 0 && nCap < 8 ) nCap = 8; p->nSize = 0; p->nCap = nCap; - p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL; return p; } @@ -62,8 +62,8 @@ Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap ) ***********************************************************************/ void Fraig_NodeVecFree( Fraig_NodeVec_t * p ) { - FREE( p->pArray ); - FREE( p ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); } /**Function************************************************************* @@ -80,10 +80,10 @@ void Fraig_NodeVecFree( Fraig_NodeVec_t * p ) Fraig_NodeVec_t * Fraig_NodeVecDup( Fraig_NodeVec_t * pVec ) { Fraig_NodeVec_t * p; - p = ALLOC( Fraig_NodeVec_t, 1 ); + p = ABC_ALLOC( Fraig_NodeVec_t, 1 ); p->nSize = pVec->nSize; p->nCap = pVec->nCap; - p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL; memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize ); return p; } @@ -135,7 +135,7 @@ void Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; - p->pArray = REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); + p->pArray = ABC_REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); p->nCap = nCapMin; } diff --git a/src/sat/lsat/solver.h b/src/sat/lsat/solver.h index a15e42d6..8d198cb2 100644 --- a/src/sat/lsat/solver.h +++ b/src/sat/lsat/solver.h @@ -2,7 +2,7 @@ Copyright (c) 2008, Niklas Sorensson 2008, Koen Claessen -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make index 0dadfbe1..33133963 100644 --- a/src/sat/msat/module.make +++ b/src/sat/msat/module.make @@ -2,7 +2,7 @@ SRC += src/sat/msat/msatActivity.c \ src/sat/msat/msatClause.c \ src/sat/msat/msatClauseVec.c \ src/sat/msat/msatMem.c \ - src/sat/msat/msatOrderJ.c \ + src/sat/msat/msatOrderH.c \ src/sat/msat/msatQueue.c \ src/sat/msat/msatRead.c \ src/sat/msat/msatSolverApi.c \ diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 53353ba6..2b28700c 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -21,10 +21,6 @@ #ifndef __MSAT_H__ #define __MSAT_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +29,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index 2ba8cd32..ca698866 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -152,7 +152,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, // nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned); nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned); #ifdef USE_SYSTEM_MEMORY_MANAGEMENT - pC = (Msat_Clause_t *)ALLOC( char, nBytes ); + pC = (Msat_Clause_t *)ABC_ALLOC( char, nBytes ); #else pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes ); #endif @@ -231,7 +231,7 @@ void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched } #ifdef USE_SYSTEM_MEMORY_MANAGEMENT - free( pC ); + ABC_FREE( pC ); #else Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc ); #endif diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c index 04691cf2..f29de389 100644 --- a/src/sat/msat/msatClauseVec.c +++ b/src/sat/msat/msatClauseVec.c @@ -42,12 +42,12 @@ Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) { Msat_ClauseVec_t * p; - p = ALLOC( Msat_ClauseVec_t, 1 ); + p = ABC_ALLOC( Msat_ClauseVec_t, 1 ); if ( nCap > 0 && nCap < 16 ) nCap = 16; p->nSize = 0; p->nCap = nCap; - p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL; return p; } @@ -64,8 +64,8 @@ Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) ***********************************************************************/ void Msat_ClauseVecFree( Msat_ClauseVec_t * p ) { - FREE( p->pArray ); - FREE( p ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); } /**Function************************************************************* @@ -115,7 +115,7 @@ void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; - p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); + p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); p->nCap = nCapMin; } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 2ff0e695..b6759a0f 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -31,6 +31,7 @@ #include <assert.h> #include <time.h> #include <math.h> +#include "abc_global.h" #include "msat.h" //////////////////////////////////////////////////////////////////////// @@ -41,25 +42,6 @@ /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#ifdef _MSC_VER -typedef __int64 int64; -#else -typedef long long int64; -#endif - -// outputs the runtime in seconds -#define PRT(a,t) \ - printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) - -// memory management macros -#define ALLOC(type, num) \ - ((type *) malloc(sizeof(type) * (num))) -#define REALLOC(type, obj, num) \ - ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ - ((type *) malloc(sizeof(type) * (num)))) -#define FREE(obj) \ - ((obj) ? (free((char *)(obj)), (obj) = 0) : 0) - // By default, custom memory management is used // which guarantees constant time allocation/deallocation // for SAT clauses and other frequently modified objects. @@ -92,12 +74,12 @@ typedef int Msat_Var_t; typedef struct Msat_SolverStats_t_ Msat_SolverStats_t; struct Msat_SolverStats_t_ { - int64 nStarts; // the number of restarts - int64 nDecisions; // the number of decisions - int64 nPropagations; // the number of implications - int64 nInspects; // the number of times clauses are vising while watching them - int64 nConflicts; // the number of conflicts - int64 nSuccesses; // the number of sat assignments found + ABC_INT64_T nStarts; // the number of restarts + ABC_INT64_T nDecisions; // the number of decisions + ABC_INT64_T nPropagations; // the number of implications + ABC_INT64_T nInspects; // the number of times clauses are vising while watching them + ABC_INT64_T nConflicts; // the number of conflicts + ABC_INT64_T nSuccesses; // the number of sat assignments found }; typedef struct Msat_SearchParams_t_ Msat_SearchParams_t; diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c index 30bf4a96..439661f4 100644 --- a/src/sat/msat/msatMem.c +++ b/src/sat/msat/msatMem.c @@ -31,7 +31,7 @@ struct Msat_MmFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries + char * pEntriesFree; // the linked list of ABC_FREE entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -48,8 +48,8 @@ struct Msat_MmFlex_t_ { // information about individual entries int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to free memory - char * pEnd; // the first entry outside the free memory + char * pCurrent; // the current pointer to ABC_FREE memory + char * pEnd; // the first entry outside the ABC_FREE memory // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -91,7 +91,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ) { Msat_MmFixed_t * p; - p = ALLOC( Msat_MmFixed_t, 1 ); + p = ABC_ALLOC( Msat_MmFixed_t, 1 ); memset( p, 0, sizeof(Msat_MmFixed_t) ); p->nEntrySize = nEntrySize; @@ -108,7 +108,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ) p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -139,9 +139,9 @@ void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose ) p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -160,16 +160,16 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) char * pTemp; int i; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize ); p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; // transform these entries into a linked list pTemp = p->pEntriesFree; @@ -189,7 +189,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list + // return the first entry in the ABC_FREE entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -210,7 +210,7 @@ void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of free entries + // add the entry to the linked list of ABC_FREE entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -233,7 +233,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); + ABC_FREE( p->pChunks[i] ); p->nChunks = 1; // transform these entries into a linked list pTemp = p->pChunks[0]; @@ -244,7 +244,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the free entry list + // set the ABC_FREE entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -286,7 +286,7 @@ Msat_MmFlex_t * Msat_MmFlexStart() { Msat_MmFlex_t * p; - p = ALLOC( Msat_MmFlex_t, 1 ); + p = ABC_ALLOC( Msat_MmFlex_t, 1 ); memset( p, 0, sizeof(Msat_MmFlex_t) ); p->nEntriesUsed = 0; @@ -296,7 +296,7 @@ Msat_MmFlex_t * Msat_MmFlexStart() p->nChunkSize = (1 << 12); p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -327,9 +327,9 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ) p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -346,13 +346,13 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ) char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ) { char * pTemp; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) { // need to allocate more entries if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } if ( nBytes > p->nChunkSize ) { @@ -360,7 +360,7 @@ char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ) // (ideally, this should never happen) p->nChunkSize = 2 * nBytes; } - p->pCurrent = ALLOC( char, p->nChunkSize ); + p->pCurrent = ABC_ALLOC( char, p->nChunkSize ); p->pEnd = p->pCurrent + p->nChunkSize; p->nMemoryAlloc += p->nChunkSize; // add the chunk to the chunk storage @@ -410,7 +410,7 @@ int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p ) are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger - entries are handed over to malloc() and then free()ed.] + entries are handed over to malloc() and then ABC_FREE()ed.] SideEffects [] @@ -421,15 +421,15 @@ Msat_MmStep_t * Msat_MmStepStart( int nSteps ) { Msat_MmStep_t * p; int i, k; - p = ALLOC( Msat_MmStep_t, 1 ); + p = ABC_ALLOC( Msat_MmStep_t, 1 ); p->nMems = nSteps; // start the fixed memory managers - p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems ); + p->pMems = ABC_ALLOC( Msat_MmFixed_t *, p->nMems ); for ( i = 0; i < p->nMems; i++ ) p->pMems[i] = Msat_MmFixedStart( (8<<i) ); // set up the mapping of the required memory size into the corresponding manager p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 ); + p->pMap = ABC_ALLOC( Msat_MmFixed_t *, p->nMapSize+1 ); p->pMap[0] = NULL; for ( k = 1; k <= 4; k++ ) p->pMap[k] = p->pMems[0]; @@ -457,9 +457,9 @@ void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ) int i; for ( i = 0; i < p->nMems; i++ ) Msat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); + ABC_FREE( p->pMems ); + ABC_FREE( p->pMap ); + ABC_FREE( p ); } /**Function************************************************************* @@ -480,7 +480,7 @@ char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes ) if ( nBytes > p->nMapSize ) { // printf( "Allocating %d bytes.\n", nBytes ); - return ALLOC( char, nBytes ); + return ABC_ALLOC( char, nBytes ); } return Msat_MmFixedEntryFetch( p->pMap[nBytes] ); } @@ -503,7 +503,7 @@ void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); + ABC_FREE( pEntry ); return; } Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c index 956e7fc6..7d8484d5 100644 --- a/src/sat/msat/msatOrderH.c +++ b/src/sat/msat/msatOrderH.c @@ -75,7 +75,7 @@ extern int timeSelect; Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) { Msat_Order_t * p; - p = ALLOC( Msat_Order_t, 1 ); + p = ABC_ALLOC( Msat_Order_t, 1 ); memset( p, 0, sizeof(Msat_Order_t) ); p->pSat = pSat; p->vIndex = Msat_IntVecAlloc( 0 ); @@ -161,7 +161,7 @@ void Msat_OrderFree( Msat_Order_t * p ) { Msat_IntVecFree( p->vHeap ); Msat_IntVecFree( p->vIndex ); - free( p ); + ABC_FREE( p ); } diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c index 5938e042..0bcaf6b2 100644 --- a/src/sat/msat/msatQueue.c +++ b/src/sat/msat/msatQueue.c @@ -50,10 +50,10 @@ struct Msat_Queue_t_ Msat_Queue_t * Msat_QueueAlloc( int nVars ) { Msat_Queue_t * p; - p = ALLOC( Msat_Queue_t, 1 ); + p = ABC_ALLOC( Msat_Queue_t, 1 ); memset( p, 0, sizeof(Msat_Queue_t) ); p->nVars = nVars; - p->pVars = ALLOC( int, nVars ); + p->pVars = ABC_ALLOC( int, nVars ); return p; } @@ -70,8 +70,8 @@ Msat_Queue_t * Msat_QueueAlloc( int nVars ) ***********************************************************************/ void Msat_QueueFree( Msat_Queue_t * p ) { - free( p->pVars ); - free( p ); + ABC_FREE( p->pVars ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c index 20453fed..ba33278c 100644 --- a/src/sat/msat/msatRead.c +++ b/src/sat/msat/msatRead.c @@ -51,7 +51,7 @@ char * Msat_FileRead( FILE * pFile ) // move the file current reading position to the beginning rewind( pFile ); // load the contents of the file into memory - pBuffer = ALLOC( char, nFileSize + 3 ); + pBuffer = ABC_ALLOC( char, nFileSize + 3 ); fread( pBuffer, nFileSize, 1, pFile ); // terminate the string with '\0' pBuffer[ nFileSize + 0] = '\n'; @@ -257,7 +257,7 @@ bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) bool Value; pText = Msat_FileRead( pFile ); Value = Msat_ReadDimacs( pText, p, fVerbose ); - free( pText ); + ABC_FREE( pText ); return Value; } diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index ee3507a6..dece390c 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -159,7 +159,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, assert(sizeof(Msat_Lit_t) == sizeof(unsigned)); assert(sizeof(float) == sizeof(unsigned)); - p = ALLOC( Msat_Solver_t, 1 ); + p = ABC_ALLOC( Msat_Solver_t, 1 ); memset( p, 0, sizeof(Msat_Solver_t) ); p->nVarsAlloc = nVarsAlloc; @@ -174,31 +174,31 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarInc = dVarInc; p->dVarDecay = dVarDecay; - p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pFactors = ALLOC( float, p->nVarsAlloc ); + p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc ); + p->pFactors = ABC_ALLOC( float, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0.0; p->pFactors[i] = 1.0; } - p->pAssigns = ALLOC( int, p->nVarsAlloc ); - p->pModel = ALLOC( int, p->nVarsAlloc ); + p->pAssigns = ABC_ALLOC( int, p->nVarsAlloc ); + p->pModel = ABC_ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc ); p->pOrder = Msat_OrderAlloc( p ); - p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); + p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc ); p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc ); - p->pReasons = ALLOC( Msat_Clause_t *, p->nVarsAlloc ); + p->pReasons = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc ); memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc ); - p->pLevel = ALLOC( int, p->nVarsAlloc ); + p->pLevel = ABC_ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) p->pLevel[i] = -1; p->dRandSeed = 91648253; @@ -215,7 +215,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); - p->pSeen = ALLOC( int, p->nVarsAlloc ); + p->pSeen = ABC_ALLOC( int, p->nVarsAlloc ); memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc ); p->nSeenId = 1; p->vReason = Msat_IntVecAlloc( p->nVarsAlloc ); @@ -243,38 +243,38 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) nVarsAllocOld = p->nVarsAlloc; p->nVarsAlloc = nVarsAlloc; - p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc ); + p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc ); + p->pFactors = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0.0; p->pFactors[i] = 1.0; } - p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc ); - p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc ); + p->pModel = ABC_REALLOC( int, p->pModel, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc ); Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc ); - p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); + p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ ) p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); Msat_QueueFree( p->pQueue ); p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); - p->pReasons = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc ); - p->pLevel = REALLOC( int, p->pLevel, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc ); + p->pLevel = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) { p->pReasons[i] = NULL; p->pLevel[i] = -1; } - p->pSeen = REALLOC( int, p->pSeen, p->nVarsAlloc ); + p->pSeen = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pSeen[i] = 0; @@ -304,7 +304,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) void Msat_SolverClean( Msat_Solver_t * p, int nVars ) { int i; - // free the clauses + // ABC_FREE the clauses int nClauses; Msat_Clause_t ** pClauses; @@ -326,7 +326,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) // Msat_ClauseVecFree( p->vLearned ); Msat_ClauseVecClear( p->vLearned ); -// FREE( p->pdActivity ); +// ABC_FREE( p->pdActivity ); for ( i = 0; i < p->nVars; i++ ) p->pdActivity[i] = 0; @@ -337,20 +337,20 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) for ( i = 0; i < 2 * p->nVars; i++ ) // Msat_ClauseVecFree( p->pvWatched[i] ); Msat_ClauseVecClear( p->pvWatched[i] ); -// FREE( p->pvWatched ); +// ABC_FREE( p->pvWatched ); // Msat_QueueFree( p->pQueue ); Msat_QueueClear( p->pQueue ); -// FREE( p->pAssigns ); +// ABC_FREE( p->pAssigns ); for ( i = 0; i < p->nVars; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // Msat_IntVecFree( p->vTrail ); Msat_IntVecClear( p->vTrail ); // Msat_IntVecFree( p->vTrailLim ); Msat_IntVecClear( p->vTrailLim ); -// FREE( p->pReasons ); +// ABC_FREE( p->pReasons ); memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars ); -// FREE( p->pLevel ); +// ABC_FREE( p->pLevel ); for ( i = 0; i < p->nVars; i++ ) p->pLevel[i] = -1; // Msat_IntVecFree( p->pModel ); @@ -358,7 +358,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) p->dRandSeed = 91648253; p->dProgress = 0.0; -// FREE( p->pSeen ); +// ABC_FREE( p->pSeen ); memset( p->pSeen, 0, sizeof(int) * p->nVars ); p->nSeenId = 1; // Msat_IntVecFree( p->vReason ); @@ -366,7 +366,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) // Msat_IntVecFree( p->vTemp ); Msat_IntVecClear( p->vTemp ); // printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL ); -// FREE( p ); +// ABC_FREE( p ); } /**Function************************************************************* @@ -384,7 +384,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) { int i; - // free the clauses + // ABC_FREE the clauses int nClauses; Msat_Clause_t ** pClauses; //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), @@ -402,21 +402,21 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseFree( p, pClauses[i], 0 ); Msat_ClauseVecFree( p->vLearned ); - FREE( p->pdActivity ); - FREE( p->pFactors ); + ABC_FREE( p->pdActivity ); + ABC_FREE( p->pFactors ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) Msat_ClauseVecFree( p->pvWatched[i] ); - FREE( p->pvWatched ); + ABC_FREE( p->pvWatched ); Msat_QueueFree( p->pQueue ); - FREE( p->pAssigns ); - FREE( p->pModel ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pModel ); Msat_IntVecFree( p->vTrail ); Msat_IntVecFree( p->vTrailLim ); - FREE( p->pReasons ); - FREE( p->pLevel ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pLevel ); Msat_MmStepStop( p->pMem, 0 ); @@ -428,10 +428,10 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_IntVecFree( p->vConeVars ); Msat_IntVecFree( p->vVarsUsed ); - FREE( p->pSeen ); + ABC_FREE( p->pSeen ); Msat_IntVecFree( p->vReason ); Msat_IntVecFree( p->vTemp ); - FREE( p ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index e86ab511..0462f11b 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -139,7 +139,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra Msat_Type_t Status; int timeStart = clock(); -// p->pFreq = ALLOC( int, p->nVarsAlloc ); +// p->pFreq = ABC_ALLOC( int, p->nVarsAlloc ); // memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); if ( vAssumps ) @@ -184,7 +184,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; /* - PRT( "True solver runtime", clock() - timeStart ); + ABC_PRT( "True solver runtime", clock() - timeStart ); // print the statistics { int i, Counter = 0; @@ -197,7 +197,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra if ( Counter ) printf( "\n" ); printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); - PRT( "Time", clock() - timeStart ); + ABC_PRT( "Time", clock() - timeStart ); } */ return Status; diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c index 36ad55ba..3716dbf7 100644 --- a/src/sat/msat/msatVec.c +++ b/src/sat/msat/msatVec.c @@ -45,12 +45,12 @@ static int Msat_IntVecSortCompare2( int * pp1, int * pp2 ); Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); if ( nCap > 0 && nCap < 16 ) nCap = 16; p->nSize = 0; p->nCap = nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; return p; } @@ -68,7 +68,7 @@ Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = nSize; p->nCap = nSize; p->pArray = pArray; @@ -89,10 +89,10 @@ Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = nSize; p->nCap = nSize; - p->pArray = ALLOC( int, nSize ); + p->pArray = ABC_ALLOC( int, nSize ); memcpy( p->pArray, pArray, sizeof(int) * nSize ); return p; } @@ -111,10 +111,10 @@ Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = pVec->nSize; p->nCap = pVec->nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize ); return p; } @@ -133,7 +133,7 @@ Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = pVec->nSize; p->nCap = pVec->nCap; p->pArray = pVec->pArray; @@ -156,8 +156,8 @@ Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) ***********************************************************************/ void Msat_IntVecFree( Msat_IntVec_t * p ) { - FREE( p->pArray ); - FREE( p ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); } /**Function************************************************************* @@ -297,7 +297,7 @@ void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; - p->pArray = REALLOC( int, p->pArray, nCapMin ); + p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); p->nCap = nCapMin; } diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c index 2d1ab2d1..a951071a 100644 --- a/src/sat/proof/pr.c +++ b/src/sat/proof/pr.c @@ -24,6 +24,7 @@ #include <assert.h> #include <time.h> //#include "vec.h" +#include "abc_global.h" #include "pr.h" //////////////////////////////////////////////////////////////////////// @@ -91,10 +92,6 @@ struct Pr_Man_t_ int timeTotal; }; -#ifndef PRT -#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) -#endif - // variable assignments static const lit LIT_UNDEF = 0xffffffff; @@ -143,7 +140,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) { Pr_Man_t * p; // allocate the manager - p = (Pr_Man_t *)malloc( sizeof(Pr_Man_t) ); + p = (Pr_Man_t *)ABC_ALLOC( char, sizeof(Pr_Man_t) ); memset( p, 0, sizeof(Pr_Man_t) ); // allocate internal arrays Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 ); @@ -153,7 +150,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) p->nChunkSize = (1<<16); // use 64K chunks // verification p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // parameters p->fProofWrite = 0; p->fProofVerif = 0; @@ -183,13 +180,13 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew ) while ( p->nVarsAlloc < nVarsNew ) p->nVarsAlloc *= 2; // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc ); - p->pReasons = (Pr_Cls_t **)realloc( p->pReasons, sizeof(Pr_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Pr_Cls_t **)realloc( p->pWatches, sizeof(Pr_Cls_t *) * p->nVarsAlloc*2 ); - // clean the free space + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + 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 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) ); @@ -215,20 +212,20 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew ) void Pr_ManFree( Pr_Man_t * p ) { printf( "Runtime stats:\n" ); -PRT( "Reading ", p->timeRead ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); +ABC_PRT( "Reading ", p->timeRead ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); Pr_ManMemoryStop( p ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); } /**Function************************************************************* @@ -348,7 +345,7 @@ char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes ) char * pMem; if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) { - pMem = (char *)malloc( p->nChunkSize ); + pMem = (char *)ABC_ALLOC( char, p->nChunkSize ); *(char **)pMem = p->pChunkLast; p->pChunkLast = pMem; p->nChunkUsed = sizeof(char *); @@ -375,8 +372,8 @@ void Pr_ManMemoryStop( Pr_Man_t * p ) if ( p->pChunkLast == NULL ) return; for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) - free( pMem ); - free( pMem ); + ABC_FREE( pMem ); + ABC_FREE( pMem ); } /**Function************************************************************* @@ -1124,7 +1121,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName ) } // read the file - pBuffer = (char *)malloc( (1<<16) ); + pBuffer = (char *)ABC_ALLOC( char, (1<<16) ); for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); ) { if ( pBuffer[0] == 'c' ) @@ -1139,7 +1136,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName ) printf( "Wrong input file format.\n" ); } p = Pr_ManAlloc( nVars ); - pArray = (int *)malloc( sizeof(int) * (nVars + 10) ); + pArray = (int *)ABC_ALLOC( char, sizeof(int) * (nVars + 10) ); continue; } // skip empty lines @@ -1178,8 +1175,8 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName ) printf( "Expected %d clauses but read %d.\n", nClauses, Counter ); // finish - if ( pArray ) free( pArray ); - if ( pBuffer ) free( pBuffer ); + if ( pArray ) ABC_FREE( pArray ); + if ( pBuffer ) ABC_FREE( pBuffer ); fclose( pFile ); return p; } diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h index 1e71a2d3..bc55e016 100644 --- a/src/sat/proof/pr.h +++ b/src/sat/proof/pr.h @@ -21,10 +21,6 @@ #ifndef __PR_H__ #define __PR_H__ -#ifdef __cplusplus -extern "C" { -#endif - #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -37,6 +33,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// |