#include "msatInt.h"

Include dependency graph for msatSolverApi.c:

Functions
int	Msat_SolverReadVarNum (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///.

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_Type_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, int 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_SolverAlloc()

Msat_Solver_t * Msat_SolverAlloc	(	int	nVarsAlloc,
		double	dClaInc,
		double	dClaDecay,
		double	dVarInc,
		double	dVarDecay,
		int	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 154 of file msatSolverApi.c.

{
    Msat_Solver_t * p;
    int i;
 
    assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
    assert(sizeof(float)     == sizeof(unsigned));
 
    p = ABC_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 = 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  = 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 = 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  = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
    p->pLevel = ABC_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     = ABC_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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverClausesDecrement()

void Msat_SolverClausesDecrement ( Msat_Solver_t * p )

Definition at line 65 of file msatSolverApi.c.

65{ p->nClausesAlloc--; }

◆ Msat_SolverClausesDecrementL()

void Msat_SolverClausesDecrementL ( Msat_Solver_t * p )

Definition at line 67 of file msatSolverApi.c.

67{ p->nClausesAllocL--; }

◆ Msat_SolverClausesIncrement()

void Msat_SolverClausesIncrement ( Msat_Solver_t * p )

Definition at line 64 of file msatSolverApi.c.

64{ p->nClausesAlloc++; }

◆ Msat_SolverClausesIncrementL()

void Msat_SolverClausesIncrementL ( Msat_Solver_t * p )

Definition at line 66 of file msatSolverApi.c.

66{ p->nClausesAllocL++; }

◆ Msat_SolverClean()

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 307 of file msatSolverApi.c.

{
    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 );
 
//    ABC_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] );
//    ABC_FREE( p->pvWatched );
//    Msat_QueueFree( p->pQueue );
    Msat_QueueClear( p->pQueue );
 
//    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 );
//    ABC_FREE( p->pReasons );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
//    ABC_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;
 
//    ABC_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 );
//    ABC_FREE( p );
}

Here is the call graph for this function:

◆ Msat_SolverFree()

void Msat_SolverFree ( Msat_Solver_t * p )

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

Synopsis [Frees the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file msatSolverApi.c.

{
    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 );
 
    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] );
    ABC_FREE( p->pvWatched );
    Msat_QueueFree( p->pQueue );
 
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pModel );
    Msat_IntVecFree( p->vTrail );
    Msat_IntVecFree( p->vTrailLim );
    ABC_FREE( p->pReasons );
    ABC_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 );
 
    ABC_FREE( p->pSeen );
    Msat_IntVecFree( p->vReason );
    Msat_IntVecFree( p->vTemp );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverIncrementSeenId()

int Msat_SolverIncrementSeenId ( Msat_Solver_t * p )

Definition at line 62 of file msatSolverApi.c.

62{ return ++p->nSeenId; }

Here is the caller graph for this function:

◆ Msat_SolverMarkClausesStart()

void Msat_SolverMarkClausesStart ( Msat_Solver_t * p )

Definition at line 69 of file msatSolverApi.c.

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

Here is the call graph for this function:

◆ Msat_SolverMarkLastClauseTypeA()

void Msat_SolverMarkLastClauseTypeA ( Msat_Solver_t * p )

Definition at line 68 of file msatSolverApi.c.

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

Msat_ClauseVecReadEntry

Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)

Definition msatClauseVec.c:225

Msat_ClauseSetTypeA

void Msat_ClauseSetTypeA(Msat_Clause_t *pC, int fTypeA)

Definition msatClause.c:264

Here is the call graph for this function:

◆ Msat_SolverPrepare()

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 451 of file msatSolverApi.c.

{
 
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverReadAdjacents()

Msat_ClauseVec_t * Msat_SolverReadAdjacents ( Msat_Solver_t * p )

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file msatSolverApi.c.

{
    return p->vAdjacents;
}

Here is the caller graph for this function:

◆ Msat_SolverReadAssignsArray()

int * Msat_SolverReadAssignsArray ( Msat_Solver_t * p )

Definition at line 56 of file msatSolverApi.c.

56{ return p->pAssigns; }

Here is the caller graph for this function:

◆ Msat_SolverReadBackTracks()

int Msat_SolverReadBackTracks ( Msat_Solver_t * p )

Definition at line 58 of file msatSolverApi.c.

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

Here is the caller graph for this function:

◆ Msat_SolverReadClause()

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 83 of file msatSolverApi.c.

{
    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 );
}

Here is the call graph for this function:

◆ Msat_SolverReadClauseNum()

int Msat_SolverReadClauseNum ( Msat_Solver_t * p )

Definition at line 48 of file msatSolverApi.c.

48{ return p->nClauses; }

◆ Msat_SolverReadConeVars()

Msat_IntVec_t * Msat_SolverReadConeVars ( Msat_Solver_t * p )

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file msatSolverApi.c.

{
    return p->vConeVars;
}

Here is the caller graph for this function:

◆ Msat_SolverReadDecisionLevel()

int Msat_SolverReadDecisionLevel ( Msat_Solver_t * p )

Definition at line 50 of file msatSolverApi.c.

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

Msat_IntVecReadSize

int Msat_IntVecReadSize(Msat_IntVec_t *p)

Definition msatVec.c:233

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverReadDecisionLevelArray()

int * Msat_SolverReadDecisionLevelArray ( Msat_Solver_t * p )

Definition at line 51 of file msatSolverApi.c.

51{ return p->pLevel; }

Here is the caller graph for this function:

◆ Msat_SolverReadFactors()

float * Msat_SolverReadFactors ( Msat_Solver_t * p )

Definition at line 70 of file msatSolverApi.c.

70{ return p->pFactors; }

◆ Msat_SolverReadInspects()

int Msat_SolverReadInspects ( Msat_Solver_t * p )

Definition at line 59 of file msatSolverApi.c.

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

Here is the caller graph for this function:

◆ Msat_SolverReadLearned()

Msat_ClauseVec_t * Msat_SolverReadLearned ( Msat_Solver_t * p )

Definition at line 54 of file msatSolverApi.c.

54{ return p->vLearned; }

Here is the caller graph for this function:

◆ Msat_SolverReadMem()

Msat_MmStep_t * Msat_SolverReadMem ( Msat_Solver_t * p )

Definition at line 60 of file msatSolverApi.c.

60{ return p->pMem; }

Here is the caller graph for this function:

◆ Msat_SolverReadModelArray()

int * Msat_SolverReadModelArray ( Msat_Solver_t * p )

Definition at line 57 of file msatSolverApi.c.

57{ return p->pModel; }

Here is the caller graph for this function:

◆ Msat_SolverReadReasonArray()

Msat_Clause_t ** Msat_SolverReadReasonArray ( Msat_Solver_t * p )

Definition at line 52 of file msatSolverApi.c.

52{ return p->pReasons; }

Here is the caller graph for this function:

◆ Msat_SolverReadSeenArray()

int * Msat_SolverReadSeenArray ( Msat_Solver_t * p )

Definition at line 61 of file msatSolverApi.c.

61{ return p->pSeen; }

Here is the caller graph for this function:

◆ Msat_SolverReadVarAllocNum()

int Msat_SolverReadVarAllocNum ( Msat_Solver_t * p )

Definition at line 49 of file msatSolverApi.c.

49{ return p->nVarsAlloc; }

◆ Msat_SolverReadVarNum()

int Msat_SolverReadVarNum ( Msat_Solver_t * p )

FUNCTION DEFINITIONS ///.

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

Synopsis [Simple SAT solver APIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatSolverApi.c.

47{ return p->nVars; }

Here is the caller graph for this function:

◆ Msat_SolverReadVarsUsed()

Msat_IntVec_t * Msat_SolverReadVarsUsed ( Msat_Solver_t * p )

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatSolverApi.c.

{
    return p->vVarsUsed;
}

Here is the caller graph for this function:

◆ Msat_SolverReadVarValue()

Msat_Type_t Msat_SolverReadVarValue	(	Msat_Solver_t *	p,
		Msat_Var_t	Var )

Definition at line 53 of file msatSolverApi.c.

53{ return (Msat_Type_t)p->pAssigns[Var]; }

Var

int Var

Definition exorList.c:228

Msat_Type_t

Definition msat.h:50

◆ Msat_SolverReadWatchedArray()

Msat_ClauseVec_t ** Msat_SolverReadWatchedArray ( Msat_Solver_t * p )

Definition at line 55 of file msatSolverApi.c.

55{ return p->pvWatched; }

Here is the caller graph for this function:

◆ Msat_SolverResize()

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 242 of file msatSolverApi.c.

{
    int nVarsAllocOld, i;
 
    nVarsAllocOld = p->nVarsAlloc;
    p->nVarsAlloc = 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  = 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 = 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  = 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     = ABC_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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverSetVerbosity()

void Msat_SolverSetVerbosity	(	Msat_Solver_t *	p,
		int	fVerbose )

Definition at line 63 of file msatSolverApi.c.

63{ p->fVerbose = fVerbose; }

Functions

Function Documentation

◆ Msat_SolverAlloc()

◆ Msat_SolverClausesDecrement()

◆ Msat_SolverClausesDecrementL()

◆ Msat_SolverClausesIncrement()

◆ Msat_SolverClausesIncrementL()

◆ Msat_SolverClean()

◆ Msat_SolverFree()

◆ Msat_SolverIncrementSeenId()

◆ Msat_SolverMarkClausesStart()

◆ Msat_SolverMarkLastClauseTypeA()

◆ Msat_SolverPrepare()

◆ Msat_SolverReadAdjacents()

◆ Msat_SolverReadAssignsArray()

◆ Msat_SolverReadBackTracks()

◆ Msat_SolverReadClause()

◆ Msat_SolverReadClauseNum()

◆ Msat_SolverReadConeVars()

◆ Msat_SolverReadDecisionLevel()

◆ Msat_SolverReadDecisionLevelArray()

◆ Msat_SolverReadFactors()

◆ Msat_SolverReadInspects()

◆ Msat_SolverReadLearned()

◆ Msat_SolverReadMem()

◆ Msat_SolverReadModelArray()

◆ Msat_SolverReadReasonArray()

◆ Msat_SolverReadSeenArray()

◆ Msat_SolverReadVarAllocNum()

◆ Msat_SolverReadVarNum()

◆ Msat_SolverReadVarsUsed()

◆ Msat_SolverReadVarValue()

◆ Msat_SolverReadWatchedArray()

◆ Msat_SolverResize()

◆ Msat_SolverSetVerbosity()