src/sat/msat/msatSolverApi.c File Reference

#include "msatInt.h"
Include dependency graph for msatSolverApi.c:

Go to the source code of this file.

Functions

static void Msat_SolverSetupTruthTables (unsigned uTruths[][2])
int Msat_SolverReadVarNum (Msat_Solver_t *p)
int Msat_SolverReadClauseNum (Msat_Solver_t *p)
int Msat_SolverReadVarAllocNum (Msat_Solver_t *p)
int Msat_SolverReadDecisionLevel (Msat_Solver_t *p)
int * Msat_SolverReadDecisionLevelArray (Msat_Solver_t *p)
Msat_Clause_t ** Msat_SolverReadReasonArray (Msat_Solver_t *p)
Msat_Lit_t Msat_SolverReadVarValue (Msat_Solver_t *p, Msat_Var_t Var)
Msat_ClauseVec_t * Msat_SolverReadLearned (Msat_Solver_t *p)
Msat_ClauseVec_t ** Msat_SolverReadWatchedArray (Msat_Solver_t *p)
int * Msat_SolverReadAssignsArray (Msat_Solver_t *p)
int * Msat_SolverReadModelArray (Msat_Solver_t *p)
int Msat_SolverReadBackTracks (Msat_Solver_t *p)
int Msat_SolverReadInspects (Msat_Solver_t *p)
Msat_MmStep_t * Msat_SolverReadMem (Msat_Solver_t *p)
int * Msat_SolverReadSeenArray (Msat_Solver_t *p)
int Msat_SolverIncrementSeenId (Msat_Solver_t *p)
void Msat_SolverSetVerbosity (Msat_Solver_t *p, int fVerbose)
void Msat_SolverClausesIncrement (Msat_Solver_t *p)
void Msat_SolverClausesDecrement (Msat_Solver_t *p)
void Msat_SolverClausesIncrementL (Msat_Solver_t *p)
void Msat_SolverClausesDecrementL (Msat_Solver_t *p)
void Msat_SolverMarkLastClauseTypeA (Msat_Solver_t *p)
void Msat_SolverMarkClausesStart (Msat_Solver_t *p)
float * Msat_SolverReadFactors (Msat_Solver_t *p)
Msat_Clause_t * Msat_SolverReadClause (Msat_Solver_t *p, int Num)
Msat_ClauseVec_t * Msat_SolverReadAdjacents (Msat_Solver_t *p)
Msat_IntVec_t * Msat_SolverReadConeVars (Msat_Solver_t *p)
Msat_IntVec_t * Msat_SolverReadVarsUsed (Msat_Solver_t *p)
Msat_Solver_t * Msat_SolverAlloc (int nVarsAlloc, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose)
void Msat_SolverResize (Msat_Solver_t *p, int nVarsAlloc)
void Msat_SolverClean (Msat_Solver_t *p, int nVars)
void Msat_SolverFree (Msat_Solver_t *p)
void Msat_SolverPrepare (Msat_Solver_t *p, Msat_IntVec_t *vVars)

Function Documentation

Msat_Solver_t* Msat_SolverAlloc ( int  nVarsAlloc,
double  dClaInc,
double  dClaDecay,
double  dVarInc,
double  dVarDecay,
bool  fVerbose 
)

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 []

Definition at line 151 of file msatSolverApi.c.

00155 {
00156     Msat_Solver_t * p;
00157     int i;
00158 
00159     assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
00160     assert(sizeof(float)     == sizeof(unsigned));
00161 
00162     p = ALLOC( Msat_Solver_t, 1 );
00163     memset( p, 0, sizeof(Msat_Solver_t) );
00164 
00165     p->nVarsAlloc = nVarsAlloc;
00166     p->nVars     = 0;
00167 
00168     p->nClauses  = 0;
00169     p->vClauses  = Msat_ClauseVecAlloc( 512 );
00170     p->vLearned  = Msat_ClauseVecAlloc( 512 );
00171 
00172     p->dClaInc   = dClaInc;
00173     p->dClaDecay = dClaDecay;
00174     p->dVarInc   = dVarInc;
00175     p->dVarDecay = dVarDecay;
00176 
00177     p->pdActivity = ALLOC( double, p->nVarsAlloc );
00178     p->pFactors   = ALLOC( float, p->nVarsAlloc );
00179     for ( i = 0; i < p->nVarsAlloc; i++ )
00180     {
00181         p->pdActivity[i] = 0.0;
00182         p->pFactors[i]   = 1.0;
00183     }
00184 
00185     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
00186     p->pModel    = ALLOC( int, p->nVarsAlloc ); 
00187     for ( i = 0; i < p->nVarsAlloc; i++ )
00188         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00189 //    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
00190     p->pOrder    = Msat_OrderAlloc( p );
00191 
00192     p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
00193     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
00194         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
00195     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
00196 
00197     p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
00198     p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
00199     p->pReasons  = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
00200     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
00201     p->pLevel = ALLOC( int, p->nVarsAlloc );
00202     for ( i = 0; i < p->nVarsAlloc; i++ )
00203         p->pLevel[i] = -1;
00204     p->dRandSeed = 91648253;
00205     p->fVerbose  = fVerbose;
00206     p->dProgress = 0.0;
00207 //    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
00208     p->pMem = Msat_MmStepStart( 10 );
00209 
00210     p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
00211     p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
00212     for ( i = 0; i < p->nVarsAlloc; i++ )
00213         Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
00214     p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
00215     Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
00216 
00217 
00218     p->pSeen     = ALLOC( int, p->nVarsAlloc );
00219     memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
00220     p->nSeenId   = 1;
00221     p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
00222     p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
00223     return p;
00224 }

void Msat_SolverClausesDecrement ( Msat_Solver_t *  p  ) 

Definition at line 62 of file msatSolverApi.c.

00062 { p->nClausesAlloc--;   }

void Msat_SolverClausesDecrementL ( Msat_Solver_t *  p  ) 

Definition at line 64 of file msatSolverApi.c.

00064 { p->nClausesAllocL--;  }

void Msat_SolverClausesIncrement ( Msat_Solver_t *  p  ) 

Definition at line 61 of file msatSolverApi.c.

00061 { p->nClausesAlloc++;   }

void Msat_SolverClausesIncrementL ( Msat_Solver_t *  p  ) 

Definition at line 63 of file msatSolverApi.c.

00063 { p->nClausesAllocL++;  }

void Msat_SolverClean ( Msat_Solver_t *  p,
int  nVars 
)

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 []

Definition at line 304 of file msatSolverApi.c.

00305 {
00306     int i;
00307     // free the clauses
00308     int nClauses;
00309     Msat_Clause_t ** pClauses;
00310 
00311     assert( p->nVarsAlloc >= nVars );
00312     p->nVars    = nVars;
00313     p->nClauses = 0;
00314 
00315     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00316     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00317     for ( i = 0; i < nClauses; i++ )
00318         Msat_ClauseFree( p, pClauses[i], 0 );
00319 //    Msat_ClauseVecFree( p->vClauses );
00320     Msat_ClauseVecClear( p->vClauses );
00321 
00322     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00323     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00324     for ( i = 0; i < nClauses; i++ )
00325         Msat_ClauseFree( p, pClauses[i], 0 );
00326 //    Msat_ClauseVecFree( p->vLearned );
00327     Msat_ClauseVecClear( p->vLearned );
00328 
00329 //    FREE( p->pdActivity );
00330     for ( i = 0; i < p->nVars; i++ )
00331         p->pdActivity[i] = 0;
00332 
00333 //    Msat_OrderFree( p->pOrder );
00334 //    Msat_OrderClean( p->pOrder, p->nVars, NULL );
00335     Msat_OrderSetBounds( p->pOrder, p->nVars );
00336 
00337     for ( i = 0; i < 2 * p->nVars; i++ )
00338 //        Msat_ClauseVecFree( p->pvWatched[i] );
00339         Msat_ClauseVecClear( p->pvWatched[i] );
00340 //    FREE( p->pvWatched );
00341 //    Msat_QueueFree( p->pQueue );
00342     Msat_QueueClear( p->pQueue );
00343 
00344 //    FREE( p->pAssigns );
00345     for ( i = 0; i < p->nVars; i++ )
00346         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00347 //    Msat_IntVecFree( p->vTrail );
00348     Msat_IntVecClear( p->vTrail );
00349 //    Msat_IntVecFree( p->vTrailLim );
00350     Msat_IntVecClear( p->vTrailLim );
00351 //    FREE( p->pReasons );
00352     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
00353 //    FREE( p->pLevel );
00354     for ( i = 0; i < p->nVars; i++ )
00355         p->pLevel[i] = -1;
00356 //    Msat_IntVecFree( p->pModel );
00357 //    Msat_MmStepStop( p->pMem, 0 );
00358     p->dRandSeed = 91648253;
00359     p->dProgress = 0.0;
00360 
00361 //    FREE( p->pSeen );
00362     memset( p->pSeen, 0, sizeof(int) * p->nVars );
00363     p->nSeenId = 1;
00364 //    Msat_IntVecFree( p->vReason );
00365     Msat_IntVecClear( p->vReason );
00366 //    Msat_IntVecFree( p->vTemp );
00367     Msat_IntVecClear( p->vTemp );
00368 //    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
00369 //    FREE( p );
00370 }

void Msat_SolverFree ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Frees the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file msatSolverApi.c.

00384 {
00385     int i;
00386 
00387     // free the clauses
00388     int nClauses;
00389     Msat_Clause_t ** pClauses;
00390 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
00391 //                                         Msat_ClauseVecReadSize( p->vLearned ) );
00392 
00393     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00394     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00395     for ( i = 0; i < nClauses; i++ )
00396         Msat_ClauseFree( p, pClauses[i], 0 );
00397     Msat_ClauseVecFree( p->vClauses );
00398 
00399     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00400     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00401     for ( i = 0; i < nClauses; i++ )
00402         Msat_ClauseFree( p, pClauses[i], 0 );
00403     Msat_ClauseVecFree( p->vLearned );
00404 
00405     FREE( p->pdActivity );
00406     FREE( p->pFactors );
00407     Msat_OrderFree( p->pOrder );
00408 
00409     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
00410         Msat_ClauseVecFree( p->pvWatched[i] );
00411     FREE( p->pvWatched );
00412     Msat_QueueFree( p->pQueue );
00413 
00414     FREE( p->pAssigns );
00415     FREE( p->pModel );
00416     Msat_IntVecFree( p->vTrail );
00417     Msat_IntVecFree( p->vTrailLim );
00418     FREE( p->pReasons );
00419     FREE( p->pLevel );
00420 
00421     Msat_MmStepStop( p->pMem, 0 );
00422 
00423     nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
00424     pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
00425     for ( i = 0; i < nClauses; i++ )
00426         Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
00427     Msat_ClauseVecFree( p->vAdjacents );
00428     Msat_IntVecFree( p->vConeVars );
00429     Msat_IntVecFree( p->vVarsUsed );
00430 
00431     FREE( p->pSeen );
00432     Msat_IntVecFree( p->vReason );
00433     Msat_IntVecFree( p->vTemp );
00434     FREE( p );
00435 }

int Msat_SolverIncrementSeenId ( Msat_Solver_t *  p  ) 

Definition at line 59 of file msatSolverApi.c.

00059 { return ++p->nSeenId;  }

void Msat_SolverMarkClausesStart ( Msat_Solver_t *  p  ) 

Definition at line 66 of file msatSolverApi.c.

00066 { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }

void Msat_SolverMarkLastClauseTypeA ( Msat_Solver_t *  p  ) 

Definition at line 65 of file msatSolverApi.c.

00065 { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }

void Msat_SolverPrepare ( Msat_Solver_t *  p,
Msat_IntVec_t *  vVars 
)

Function*************************************************************

Synopsis [Prepares the solver to run on a subset of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file msatSolverApi.c.

00449 {
00450 
00451     int i;
00452     // undo the previous data
00453     for ( i = 0; i < p->nVarsAlloc; i++ )
00454     {
00455         p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
00456         p->pReasons[i]   = NULL;
00457         p->pLevel[i]     = -1;
00458         p->pdActivity[i] = 0.0;
00459     }
00460 
00461     // set the new variable order
00462     Msat_OrderClean( p->pOrder, vVars );
00463 
00464     Msat_QueueClear( p->pQueue );
00465     Msat_IntVecClear( p->vTrail );
00466     Msat_IntVecClear( p->vTrailLim );
00467     p->dProgress = 0.0;
00468 }

Msat_ClauseVec_t* Msat_SolverReadAdjacents ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file msatSolverApi.c.

00102 {
00103     return p->vAdjacents;
00104 }

int* Msat_SolverReadAssignsArray ( Msat_Solver_t *  p  ) 

Definition at line 53 of file msatSolverApi.c.

00053 { return p->pAssigns;   }

int Msat_SolverReadBackTracks ( Msat_Solver_t *  p  ) 

Definition at line 55 of file msatSolverApi.c.

00055 { return (int)p->Stats.nConflicts; }

Msat_Clause_t* Msat_SolverReadClause ( Msat_Solver_t *  p,
int  Num 
)

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file msatSolverApi.c.

00081 {
00082     int nClausesP;
00083     assert( Num < p->nClauses );
00084     nClausesP = Msat_ClauseVecReadSize( p->vClauses );
00085     if ( Num < nClausesP )
00086         return Msat_ClauseVecReadEntry( p->vClauses, Num );
00087     return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
00088 }

int Msat_SolverReadClauseNum ( Msat_Solver_t *  p  ) 

Definition at line 45 of file msatSolverApi.c.

00045 { return p->nClauses;   }

Msat_IntVec_t* Msat_SolverReadConeVars ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatSolverApi.c.

00118 {
00119     return p->vConeVars;
00120 }

int Msat_SolverReadDecisionLevel ( Msat_Solver_t *  p  ) 

Definition at line 47 of file msatSolverApi.c.

00047 { return Msat_IntVecReadSize(p->vTrailLim); }

int* Msat_SolverReadDecisionLevelArray ( Msat_Solver_t *  p  ) 

Definition at line 48 of file msatSolverApi.c.

00048 { return p->pLevel;     }

float* Msat_SolverReadFactors ( Msat_Solver_t *  p  ) 

Definition at line 67 of file msatSolverApi.c.

00067 { return p->pFactors;   }

int Msat_SolverReadInspects ( Msat_Solver_t *  p  ) 

Definition at line 56 of file msatSolverApi.c.

00056 { return (int)p->Stats.nInspects;  }

Msat_ClauseVec_t* Msat_SolverReadLearned ( Msat_Solver_t *  p  ) 

Definition at line 51 of file msatSolverApi.c.

00051 { return p->vLearned;   }

Msat_MmStep_t* Msat_SolverReadMem ( Msat_Solver_t *  p  ) 

Definition at line 57 of file msatSolverApi.c.

00057 { return p->pMem;       }

int* Msat_SolverReadModelArray ( Msat_Solver_t *  p  ) 

Definition at line 54 of file msatSolverApi.c.

00054 { return p->pModel;     }

Msat_Clause_t** Msat_SolverReadReasonArray ( Msat_Solver_t *  p  ) 

Definition at line 49 of file msatSolverApi.c.

00049 { return p->pReasons;   }

int* Msat_SolverReadSeenArray ( Msat_Solver_t *  p  ) 

Definition at line 58 of file msatSolverApi.c.

00058 { return p->pSeen;      }

int Msat_SolverReadVarAllocNum ( Msat_Solver_t *  p  ) 

Definition at line 46 of file msatSolverApi.c.

00046 { return p->nVarsAlloc; }

int Msat_SolverReadVarNum ( Msat_Solver_t *  p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Simple SAT solver APIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file msatSolverApi.c.

00044 { return p->nVars;      }

Msat_IntVec_t* Msat_SolverReadVarsUsed ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatSolverApi.c.

00134 {
00135     return p->vVarsUsed;
00136 }

Msat_Lit_t Msat_SolverReadVarValue ( Msat_Solver_t *  p,
Msat_Var_t  Var 
)

Definition at line 50 of file msatSolverApi.c.

00050 { return p->pAssigns[Var]; }

Msat_ClauseVec_t** Msat_SolverReadWatchedArray ( Msat_Solver_t *  p  ) 

Definition at line 52 of file msatSolverApi.c.

00052 { return p->pvWatched;  }

void Msat_SolverResize ( Msat_Solver_t *  p,
int  nVarsAlloc 
)

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 []

Definition at line 239 of file msatSolverApi.c.

00240 {
00241     int nVarsAllocOld, i;
00242 
00243     nVarsAllocOld = p->nVarsAlloc;
00244     p->nVarsAlloc = nVarsAlloc;
00245 
00246     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
00247     p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
00248     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00249     {
00250         p->pdActivity[i] = 0.0;
00251         p->pFactors[i]   = 1.0;
00252     }
00253 
00254     p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
00255     p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
00256     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00257         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00258 
00259 //    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
00260     Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
00261 
00262     p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
00263     for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
00264         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
00265 
00266     Msat_QueueFree( p->pQueue );
00267     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
00268 
00269     p->pReasons  = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
00270     p->pLevel    = REALLOC( int, p->pLevel, p->nVarsAlloc );
00271     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00272     {
00273         p->pReasons[i] = NULL;
00274         p->pLevel[i] = -1;
00275     }
00276 
00277     p->pSeen     = REALLOC( int, p->pSeen, p->nVarsAlloc );
00278     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00279         p->pSeen[i] = 0;
00280 
00281     Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
00282     Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
00283 
00284     // make sure the array of adjucents has room to store the variable numbers
00285     for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
00286         Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
00287     Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
00288 }

void Msat_SolverSetupTruthTables ( unsigned  uTruths[][2]  )  [static]

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

] DECLARATIONS ///

Function*************************************************************

Synopsis [Sets up the truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file msatSolverApi.c.

00482 {
00483     int m, v;
00484     // set up the truth tables
00485     for ( m = 0; m < 32; m++ )
00486         for ( v = 0; v < 5; v++ )
00487             if ( m & (1 << v) )
00488                 uTruths[v][0] |= (1 << m);
00489     // make adjustments for the case of 6 variables
00490     for ( v = 0; v < 5; v++ )
00491         uTruths[v][1] = uTruths[v][0];
00492     uTruths[5][0] = 0;
00493     uTruths[5][1] = ~((unsigned)0);
00494 }

void Msat_SolverSetVerbosity ( Msat_Solver_t *  p,
int  fVerbose 
)

Definition at line 60 of file msatSolverApi.c.

00060 { p->fVerbose = fVerbose; }

Generated on Tue Jan 5 12:19:40 2010 for abc70930 by  doxygen 1.6.1