diff options
Diffstat (limited to 'abc70930/src/sat/msat/msatSolverApi.c')
-rw-r--r-- | abc70930/src/sat/msat/msatSolverApi.c | 500 |
1 files changed, 0 insertions, 500 deletions
diff --git a/abc70930/src/sat/msat/msatSolverApi.c b/abc70930/src/sat/msat/msatSolverApi.c deleted file mode 100644 index ee3507a6..00000000 --- a/abc70930/src/sat/msat/msatSolverApi.c +++ /dev/null @@ -1,500 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverApi.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [APIs of the SAT solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Simple SAT solver APIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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; } -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 (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_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************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num ) -{ - int nClausesP; - assert( Num < p->nClauses ); - nClausesP = Msat_ClauseVecReadSize( p->vClauses ); - if ( Num < nClausesP ) - return Msat_ClauseVecReadEntry( p->vClauses, Num ); - return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP ); -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p ) -{ - return p->vAdjacents; -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p ) -{ - return p->vConeVars; -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p ) -{ - return p->vVarsUsed; -} - - -/**Function************************************************************* - - Synopsis [Allocates the solver.] - - Description [After the solver is allocated, the procedure - Msat_SolverClean() should be called to set the number of variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, - double dClaInc, double dClaDecay, - double dVarInc, double dVarDecay, - bool fVerbose ) -{ - Msat_Solver_t * p; - int i; - - assert(sizeof(Msat_Lit_t) == sizeof(unsigned)); - assert(sizeof(float) == sizeof(unsigned)); - - p = ALLOC( Msat_Solver_t, 1 ); - memset( p, 0, sizeof(Msat_Solver_t) ); - - p->nVarsAlloc = nVarsAlloc; - p->nVars = 0; - - p->nClauses = 0; - p->vClauses = Msat_ClauseVecAlloc( 512 ); - p->vLearned = Msat_ClauseVecAlloc( 512 ); - - p->dClaInc = dClaInc; - p->dClaDecay = dClaDecay; - p->dVarInc = dVarInc; - 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.0; - p->pFactors[i] = 1.0; - } - - p->pAssigns = ALLOC( int, p->nVarsAlloc ); - p->pModel = 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 ); - 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 ); - memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc ); - p->pLevel = ALLOC( int, p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pLevel[i] = -1; - p->dRandSeed = 91648253; - p->fVerbose = fVerbose; - p->dProgress = 0.0; -// p->pModel = Msat_IntVecAlloc( p->nVarsAlloc ); - p->pMem = Msat_MmStepStart( 10 ); - - p->vConeVars = Msat_IntVecAlloc( p->nVarsAlloc ); - p->vAdjacents = Msat_ClauseVecAlloc( p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) ); - p->vVarsUsed = Msat_IntVecAlloc( p->nVarsAlloc ); - Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); - - - p->pSeen = ALLOC( int, p->nVarsAlloc ); - memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc ); - p->nSeenId = 1; - p->vReason = Msat_IntVecAlloc( p->nVarsAlloc ); - p->vTemp = Msat_IntVecAlloc( p->nVarsAlloc ); - return p; -} - -/**Function************************************************************* - - Synopsis [Resizes the solver.] - - Description [Assumes that the solver contains some clauses, and that - it is currently between the calls. Resizes the solver to accomodate - more variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) -{ - int nVarsAllocOld, i; - - nVarsAllocOld = p->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.0; - p->pFactors[i] = 1.0; - } - - p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc ); - p->pModel = 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 ); - 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 ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - { - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - } - - p->pSeen = REALLOC( int, p->pSeen, p->nVarsAlloc ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - p->pSeen[i] = 0; - - Msat_IntVecGrow( p->vTrail, p->nVarsAlloc ); - Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc ); - - // make sure the array of adjucents has room to store the variable numbers - for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ ) - Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) ); - Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); -} - -/**Function************************************************************* - - Synopsis [Prepares the solver.] - - Description [Cleans the solver assuming that the problem will involve - the given number of variables (nVars). This procedure is useful - for many small (incremental) SAT problems, to prevent the solver - from being reallocated each time.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverClean( Msat_Solver_t * p, int nVars ) -{ - int i; - // free the clauses - int nClauses; - Msat_Clause_t ** pClauses; - - assert( p->nVarsAlloc >= nVars ); - p->nVars = nVars; - p->nClauses = 0; - - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); -// Msat_ClauseVecFree( p->vClauses ); - Msat_ClauseVecClear( p->vClauses ); - - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); -// Msat_ClauseVecFree( p->vLearned ); - Msat_ClauseVecClear( p->vLearned ); - -// FREE( p->pdActivity ); - for ( i = 0; i < p->nVars; i++ ) - p->pdActivity[i] = 0; - -// Msat_OrderFree( p->pOrder ); -// Msat_OrderClean( p->pOrder, p->nVars, NULL ); - Msat_OrderSetBounds( p->pOrder, p->nVars ); - - for ( i = 0; i < 2 * p->nVars; i++ ) -// Msat_ClauseVecFree( p->pvWatched[i] ); - Msat_ClauseVecClear( p->pvWatched[i] ); -// FREE( p->pvWatched ); -// Msat_QueueFree( p->pQueue ); - Msat_QueueClear( p->pQueue ); - -// 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 ); - memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars ); -// FREE( p->pLevel ); - for ( i = 0; i < p->nVars; i++ ) - p->pLevel[i] = -1; -// Msat_IntVecFree( p->pModel ); -// Msat_MmStepStop( p->pMem, 0 ); - p->dRandSeed = 91648253; - p->dProgress = 0.0; - -// FREE( p->pSeen ); - memset( p->pSeen, 0, sizeof(int) * p->nVars ); - p->nSeenId = 1; -// Msat_IntVecFree( p->vReason ); - Msat_IntVecClear( p->vReason ); -// Msat_IntVecFree( p->vTemp ); - Msat_IntVecClear( p->vTemp ); -// printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL ); -// FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Frees the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverFree( Msat_Solver_t * p ) -{ - int i; - - // free the clauses - int nClauses; - Msat_Clause_t ** pClauses; -//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), -// Msat_ClauseVecReadSize( p->vLearned ) ); - - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); - Msat_ClauseVecFree( p->vClauses ); - - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); - Msat_ClauseVecFree( p->vLearned ); - - FREE( p->pdActivity ); - FREE( p->pFactors ); - Msat_OrderFree( p->pOrder ); - - for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) - Msat_ClauseVecFree( p->pvWatched[i] ); - FREE( p->pvWatched ); - Msat_QueueFree( p->pQueue ); - - FREE( p->pAssigns ); - FREE( p->pModel ); - Msat_IntVecFree( p->vTrail ); - Msat_IntVecFree( p->vTrailLim ); - FREE( p->pReasons ); - FREE( p->pLevel ); - - Msat_MmStepStop( p->pMem, 0 ); - - nClauses = Msat_ClauseVecReadSize( p->vAdjacents ); - pClauses = Msat_ClauseVecReadArray( p->vAdjacents ); - for ( i = 0; i < nClauses; i++ ) - Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] ); - Msat_ClauseVecFree( p->vAdjacents ); - Msat_IntVecFree( p->vConeVars ); - Msat_IntVecFree( p->vVarsUsed ); - - FREE( p->pSeen ); - Msat_IntVecFree( p->vReason ); - Msat_IntVecFree( p->vTemp ); - FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Prepares the solver to run on a subset of variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars ) -{ - - int i; - // undo the previous data - for ( i = 0; i < p->nVarsAlloc; i++ ) - { - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - p->pdActivity[i] = 0.0; - } - - // set the new variable order - Msat_OrderClean( p->pOrder, vVars ); - - Msat_QueueClear( p->pQueue ); - Msat_IntVecClear( p->vTrail ); - Msat_IntVecClear( p->vTrailLim ); - p->dProgress = 0.0; -} - -/**Function************************************************************* - - Synopsis [Sets up the truth tables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ) -{ - int m, v; - // set up the truth tables - for ( m = 0; m < 32; m++ ) - for ( v = 0; v < 5; v++ ) - if ( m & (1 << v) ) - uTruths[v][0] |= (1 << m); - // make adjustments for the case of 6 variables - for ( v = 0; v < 5; v++ ) - uTruths[v][1] = uTruths[v][0]; - uTruths[5][0] = 0; - uTruths[5][1] = ~((unsigned)0); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |