From 6b44b18e69f4e26249140e10c459615a77b32fc5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 4 Aug 2006 08:01:00 -0700 Subject: Version abc60804 --- src/sat/msat/msatActivity.c | 2 +- src/sat/msat/msatInt.h | 2 +- src/sat/msat/msatSolverApi.c | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'src/sat') diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index f808d9bc..23925669 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -46,7 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) return; Var = MSAT_LIT2VAR(Lit); if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 ) -// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 ) +// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 ) Msat_SolverVarRescaleActivity( p ); Msat_OrderUpdate( p->pOrder, Var ); } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 15932c67..7845ec0b 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -119,7 +119,7 @@ struct Msat_Solver_t_ double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. double * pdActivity; // A heuristic measurement of the activity of a variable. - int * pLevels; // the levels of the variables + int * pActLevels; // the levels of the variables double dVarInc; // Amount to bump next variable with. double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. Msat_Order_t * pOrder; // Keeps track of the decision variable order. diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index 8c1542df..9317dcac 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -174,11 +174,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarDecay = dVarDecay; p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pLevels = ALLOC( int, p->nVarsAlloc ); + p->pActLevels = ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0; - p->pLevels = 0; + p->pActLevels[i] = 0; } p->pAssigns = ALLOC( int, p->nVarsAlloc ); @@ -243,7 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) p->nVarsAlloc = nVarsAlloc; p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pLevels = REALLOC( int, p->pLevels, p->nVarsAlloc ); + p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pdActivity[i] = 0; @@ -399,7 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseVecFree( p->vLearned ); FREE( p->pdActivity ); - FREE( p->pLevels ); + FREE( p->pActLevels ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) -- cgit v1.2.3