diff options
Diffstat (limited to 'src/sat/msat/msatSolverApi.c')
| -rw-r--r-- | src/sat/msat/msatSolverApi.c | 50 |
1 files changed, 31 insertions, 19 deletions
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index ba506993..ee3507a6 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -27,7 +27,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -41,27 +41,30 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); SeeAlso [] ***********************************************************************/ -int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } -int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;} +int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } +int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; } +int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc; } int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } -int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } -Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; } +int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } +Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; } Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; } -Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; } -Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; } -int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; } -int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; } -int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return p->nBackTracks; } -Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; } -int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; } -int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; } +Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; } +Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; } +int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; } +int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; } +int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; } +int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; } +Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; } +int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; } +int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; } void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; } -void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; } -void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; } -void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; } -void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; } +void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; } +void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; } +void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; } +void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; } void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); } void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); } +float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; } /**Function************************************************************* @@ -172,8 +175,12 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarDecay = dVarDecay; p->pdActivity = ALLOC( double, p->nVarsAlloc ); + p->pFactors = ALLOC( float, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pdActivity[i] = 0; + { + p->pdActivity[i] = 0.0; + p->pFactors[i] = 1.0; + } p->pAssigns = ALLOC( int, p->nVarsAlloc ); p->pModel = ALLOC( int, p->nVarsAlloc ); @@ -237,8 +244,12 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) p->nVarsAlloc = nVarsAlloc; p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); + p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - p->pdActivity[i] = 0; + { + 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 ); @@ -392,6 +403,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseVecFree( p->vLearned ); FREE( p->pdActivity ); + FREE( p->pFactors ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) |