#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <math.h>
#include "misc/util/abc_global.h"
#include "msat.h"

Include dependency graph for msatInt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Msat_SolverStats_t_

struct	Msat_SearchParams_t_

struct	Msat_Solver_t_

struct	Msat_ClauseVec_t_

struct	Msat_IntVec_t_

Macros
#define	MSAT_VAR_UNASSIGNED (-1)

#define	MSAT_LIT_UNASSIGNED (-2)

#define	MSAT_ORDER_UNKNOWN (-3)

#define	L_IND "%-*d"

#define	L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)

#define	L_LIT "%s%d"

#define	L_lit(Lit)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_	Msat_Clause_t
	INCLUDES ///.

typedef struct Msat_Queue_t_	Msat_Queue_t

typedef struct Msat_Order_t_	Msat_Order_t

typedef struct Msat_MmFixed_t_	Msat_MmFixed_t

typedef struct Msat_MmFlex_t_	Msat_MmFlex_t

typedef struct Msat_MmStep_t_	Msat_MmStep_t

typedef int	Msat_Lit_t

typedef int	Msat_Var_t

typedef struct Msat_SolverStats_t_	Msat_SolverStats_t

typedef struct Msat_SearchParams_t_	Msat_SearchParams_t

Functions
void	Msat_SolverVarDecayActivity (Msat_Solver_t *p)
	GLOBAL VARIABLES ///.

void	Msat_SolverVarRescaleActivity (Msat_Solver_t *p)

void	Msat_SolverClaDecayActivity (Msat_Solver_t *p)

void	Msat_SolverClaRescaleActivity (Msat_Solver_t *p)

Msat_Clause_t *	Msat_SolverReadClause (Msat_Solver_t *p, int Num)

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_SolverReadSeenArray (Msat_Solver_t *p)

int	Msat_SolverIncrementSeenId (Msat_Solver_t *p)

Msat_MmStep_t *	Msat_SolverReadMem (Msat_Solver_t *p)

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_SolverVarBumpActivity (Msat_Solver_t *p, Msat_Lit_t Lit)
	DECLARATIONS ///.

void	Msat_SolverClaBumpActivity (Msat_Solver_t p, Msat_Clause_t pC)

int	Msat_SolverEnqueue (Msat_Solver_t p, Msat_Lit_t Lit, Msat_Clause_t pC)

double	Msat_SolverProgressEstimate (Msat_Solver_t *p)

int	Msat_SolverAssume (Msat_Solver_t *p, Msat_Lit_t Lit)
	FUNCTION DEFINITIONS ///.

Msat_Clause_t *	Msat_SolverPropagate (Msat_Solver_t *p)

void	Msat_SolverCancelUntil (Msat_Solver_t *p, int Level)

Msat_Type_t	Msat_SolverSearch (Msat_Solver_t p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t pPars)

Msat_Queue_t *	Msat_QueueAlloc (int nVars)
	FUNCTION DEFINITIONS ///.

void	Msat_QueueFree (Msat_Queue_t *p)

int	Msat_QueueReadSize (Msat_Queue_t *p)

void	Msat_QueueInsert (Msat_Queue_t *p, int Lit)

int	Msat_QueueExtract (Msat_Queue_t *p)

void	Msat_QueueClear (Msat_Queue_t *p)

Msat_Order_t *	Msat_OrderAlloc (Msat_Solver_t *pSat)
	FUNCTION DEFINITIONS ///.

void	Msat_OrderSetBounds (Msat_Order_t *p, int nVarsMax)

void	Msat_OrderClean (Msat_Order_t p, Msat_IntVec_t vCone)

int	Msat_OrderCheck (Msat_Order_t *p)

void	Msat_OrderFree (Msat_Order_t *p)

int	Msat_OrderVarSelect (Msat_Order_t *p)

void	Msat_OrderVarAssigned (Msat_Order_t *p, int Var)

void	Msat_OrderVarUnassigned (Msat_Order_t *p, int Var)

void	Msat_OrderUpdate (Msat_Order_t *p, int Var)

int	Msat_ClauseCreate (Msat_Solver_t p, Msat_IntVec_t vLits, int fLearnt, Msat_Clause_t **pClause_out)
	FUNCTION DEFINITIONS ///.

Msat_Clause_t *	Msat_ClauseCreateFake (Msat_Solver_t p, Msat_IntVec_t vLits)

Msat_Clause_t *	Msat_ClauseCreateFakeLit (Msat_Solver_t *p, Msat_Lit_t Lit)

int	Msat_ClauseReadLearned (Msat_Clause_t *pC)

int	Msat_ClauseReadSize (Msat_Clause_t *pC)

int *	Msat_ClauseReadLits (Msat_Clause_t *pC)

int	Msat_ClauseReadMark (Msat_Clause_t *pC)

void	Msat_ClauseSetMark (Msat_Clause_t *pC, int fMark)

int	Msat_ClauseReadNum (Msat_Clause_t *pC)

void	Msat_ClauseSetNum (Msat_Clause_t *pC, int Num)

int	Msat_ClauseReadTypeA (Msat_Clause_t *pC)

void	Msat_ClauseSetTypeA (Msat_Clause_t *pC, int fTypeA)

int	Msat_ClauseIsLocked (Msat_Solver_t p, Msat_Clause_t pC)

float	Msat_ClauseReadActivity (Msat_Clause_t *pC)

void	Msat_ClauseWriteActivity (Msat_Clause_t *pC, float Num)

void	Msat_ClauseFree (Msat_Solver_t p, Msat_Clause_t pC, int fRemoveWatched)

int	Msat_ClausePropagate (Msat_Clause_t pC, Msat_Lit_t Lit, int pAssigns, Msat_Lit_t *pLit_out)

int	Msat_ClauseSimplify (Msat_Clause_t pC, int pAssigns)

void	Msat_ClauseCalcReason (Msat_Solver_t p, Msat_Clause_t pC, Msat_Lit_t Lit, Msat_IntVec_t *vLits_out)

void	Msat_ClauseRemoveWatch (Msat_ClauseVec_t vClauses, Msat_Clause_t pC)

void	Msat_ClausePrint (Msat_Clause_t *pC)

void	Msat_ClausePrintSymbols (Msat_Clause_t *pC)

void	Msat_ClauseWriteDimacs (FILE pFile, Msat_Clause_t pC, int fIncrement)

unsigned	Msat_ClauseComputeTruth (Msat_Solver_t p, Msat_Clause_t pC)

void	Msat_SolverSortDB (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///.

Msat_ClauseVec_t *	Msat_ClauseVecAlloc (int nCap)
	DECLARATIONS ///.

void	Msat_ClauseVecFree (Msat_ClauseVec_t *p)

Msat_Clause_t **	Msat_ClauseVecReadArray (Msat_ClauseVec_t *p)

int	Msat_ClauseVecReadSize (Msat_ClauseVec_t *p)

void	Msat_ClauseVecGrow (Msat_ClauseVec_t *p, int nCapMin)

void	Msat_ClauseVecShrink (Msat_ClauseVec_t *p, int nSizeNew)

void	Msat_ClauseVecClear (Msat_ClauseVec_t *p)

void	Msat_ClauseVecPush (Msat_ClauseVec_t p, Msat_Clause_t Entry)

Msat_Clause_t *	Msat_ClauseVecPop (Msat_ClauseVec_t *p)

void	Msat_ClauseVecWriteEntry (Msat_ClauseVec_t p, int i, Msat_Clause_t Entry)

Msat_Clause_t *	Msat_ClauseVecReadEntry (Msat_ClauseVec_t *p, int i)

Msat_MmFixed_t *	Msat_MmFixedStart (int nEntrySize)
	FUNCTION DEFINITIONS ///.

void	Msat_MmFixedStop (Msat_MmFixed_t *p, int fVerbose)

char *	Msat_MmFixedEntryFetch (Msat_MmFixed_t *p)

void	Msat_MmFixedEntryRecycle (Msat_MmFixed_t p, char pEntry)

void	Msat_MmFixedRestart (Msat_MmFixed_t *p)

int	Msat_MmFixedReadMemUsage (Msat_MmFixed_t *p)

Msat_MmFlex_t *	Msat_MmFlexStart ()

void	Msat_MmFlexStop (Msat_MmFlex_t *p, int fVerbose)

char *	Msat_MmFlexEntryFetch (Msat_MmFlex_t *p, int nBytes)

int	Msat_MmFlexReadMemUsage (Msat_MmFlex_t *p)

Msat_MmStep_t *	Msat_MmStepStart (int nSteps)

void	Msat_MmStepStop (Msat_MmStep_t *p, int fVerbose)

char *	Msat_MmStepEntryFetch (Msat_MmStep_t *p, int nBytes)

void	Msat_MmStepEntryRecycle (Msat_MmStep_t p, char pEntry, int nBytes)

int	Msat_MmStepReadMemUsage (Msat_MmStep_t *p)

Macro Definition Documentation

◆ L_IND

#define L_IND "%-*d"

Definition at line 73 of file msatInt.h.

◆ L_ind

#define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)

Definition at line 74 of file msatInt.h.

◆ L_LIT

#define L_LIT "%s%d"

Definition at line 75 of file msatInt.h.

◆ L_lit

#define L_lit ( Lit )

Value:

MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1

MSAT_LIT2VAR

#define MSAT_LIT2VAR(l)

Definition msat.h:59

MSAT_LITSIGN

#define MSAT_LITSIGN(l)

Definition msat.h:58

Definition at line 76 of file msatInt.h.

◆ MSAT_LIT_UNASSIGNED

#define MSAT_LIT_UNASSIGNED (-2)

Definition at line 69 of file msatInt.h.

◆ MSAT_ORDER_UNKNOWN

#define MSAT_ORDER_UNKNOWN (-3)

Definition at line 70 of file msatInt.h.

◆ MSAT_VAR_UNASSIGNED

#define MSAT_VAR_UNASSIGNED (-1)

Definition at line 68 of file msatInt.h.

Typedef Documentation

◆ Msat_Clause_t

typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t

INCLUDES ///.

CFile****************************************************************

FileName [msatInt.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 [Internal definitions of the solver.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

] PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 57 of file msatInt.h.

◆ Msat_Lit_t

typedef int Msat_Lit_t

Definition at line 65 of file msatInt.h.

◆ Msat_MmFixed_t

typedef struct Msat_MmFixed_t_ Msat_MmFixed_t

Definition at line 61 of file msatInt.h.

◆ Msat_MmFlex_t

typedef struct Msat_MmFlex_t_ Msat_MmFlex_t

Definition at line 62 of file msatInt.h.

◆ Msat_MmStep_t

typedef struct Msat_MmStep_t_ Msat_MmStep_t

Definition at line 63 of file msatInt.h.

◆ Msat_Order_t

typedef struct Msat_Order_t_ Msat_Order_t

Definition at line 59 of file msatInt.h.

◆ Msat_Queue_t

typedef struct Msat_Queue_t_ Msat_Queue_t

Definition at line 58 of file msatInt.h.

◆ Msat_SearchParams_t

typedef struct Msat_SearchParams_t_ Msat_SearchParams_t

Definition at line 89 of file msatInt.h.

◆ Msat_SolverStats_t

typedef struct Msat_SolverStats_t_ Msat_SolverStats_t

Definition at line 78 of file msatInt.h.

◆ Msat_Var_t

typedef int Msat_Var_t

Definition at line 66 of file msatInt.h.

Function Documentation

◆ Msat_ClauseCalcReason()

void Msat_ClauseCalcReason	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC,
		Msat_Lit_t	Lit,
		Msat_IntVec_t *	vLits_out )

extern

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

Synopsis [Computes reason of conflict in the given clause.]

Description [If the literal is unassigned, finds the reason by complementing literals in the given cluase (pC). If the literal is assigned, makes sure that this literal is the first one in the clause and computes the complement of all other literals in the clause. Returns the reason in the given array (vLits_out). If the clause is learned, bumps its activity.]

SideEffects []

SeeAlso []

Definition at line 418 of file msatClause.c.

{
    int i;
    // clear the reason
    Msat_IntVecClear( vLits_out );
    assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
    for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
    {
        assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
        Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
    }
    if ( pC->fLearned ) 
        Msat_SolverClaBumpActivity( p, pC );
}

Here is the call graph for this function:

◆ Msat_ClauseComputeTruth()

unsigned Msat_ClauseComputeTruth	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC )

extern

◆ Msat_ClauseCreate()

int Msat_ClauseCreate	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vLits,
		int	fLearned,
		Msat_Clause_t **	pClause_out )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates a new clause.]

Description [Returns FALSE if top-level conflict detected (must be handled); TRUE otherwise. 'pClause_out' may be set to NULL if clause is already satisfied by the top-level assignment.]

SideEffects []

SeeAlso []

Definition at line 58 of file msatClause.c.

{
    int * pAssigns = Msat_SolverReadAssignsArray(p);
    Msat_ClauseVec_t ** pvWatched;
    Msat_Clause_t * pC;
    int * pLits;
    int nLits, i, j;
    int nBytes;
    Msat_Var_t Var;
    int  Sign;
 
    *pClause_out = NULL;
 
    nLits = Msat_IntVecReadSize(vLits);
    pLits = Msat_IntVecReadArray(vLits);
 
    if ( !fLearned ) 
    {
        int * pSeen = Msat_SolverReadSeenArray( p );
        int nSeenId;
        assert( Msat_SolverReadDecisionLevel(p) == 0 );
        // sorting literals makes the code trace-equivalent 
        // with to the original C++ solver
        Msat_IntVecSort( vLits, 0 );
        // increment the counter of seen twice
        nSeenId = Msat_SolverIncrementSeenId( p );
        nSeenId = Msat_SolverIncrementSeenId( p );
        // nSeenId - 1 stands for negative
        // nSeenId     stands for positive
        // Remove false literals
 
        // there is a bug here!!!!
        // when the same var in opposite polarities is given, it drops one polarity!!!
 
        for ( i = j = 0; i < nLits; i++ ) {
            // get the corresponding variable
            Var  = MSAT_LIT2VAR(pLits[i]);
            Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
            // check if we already saw this variable in the this clause
            if ( pSeen[Var] >= nSeenId - 1 )
            {
                if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
                    continue;
                return 1; // two opposite polarity lits -- don't add the clause
            }
            // mark the variable as seen
            pSeen[Var] = nSeenId - !Sign;
 
            // analize the value of this literal
            if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
            {
                if ( pAssigns[Var] == pLits[i] )
                    return 1;  // the clause is always true -- don't add anything
                // the literal has no impact - skip it
                continue;
            }
            // otherwise, add this literal to the clause
            pLits[j++] = pLits[i];
        }
        Msat_IntVecShrink( vLits, j );
        nLits = j;
/*
        // the problem with this code is that performance is very
        // sensitive to the ordering of adjacency lits
        // the best ordering requires fanins first, next fanouts
        // this ordering is more convenient to make from FRAIG
 
        // create the adjacency information
        if ( nLits > 2 )
        {
            Msat_Var_t VarI, VarJ;
            Msat_IntVec_t * pAdjI, * pAdjJ;
 
            for ( i = 0; i < nLits; i++ )
            {
                VarI = MSAT_LIT2VAR(pLits[i]);
                pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];
 
                for ( j = i+1; j < nLits; j++ )
                {
                    VarJ = MSAT_LIT2VAR(pLits[j]);
                    pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];
 
                    Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
                    Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
                }
            }
        }
*/
    }
    // 'vLits' is now the (possibly) reduced vector of literals.
    if ( nLits == 0 )
        return 0;
    if ( nLits == 1 )
        return Msat_SolverEnqueue( p, pLits[0], NULL );
 
    // Allocate clause:
//    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
    nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
    pC = (Msat_Clause_t *)ABC_ALLOC( char, nBytes );
#else
    pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
#endif
    pC->Num        = p->nClauses++;
    pC->fTypeA     = 0;
    pC->fMark      = 0;
    pC->fLearned   = fLearned;
    pC->nSize      = nLits;
    pC->nSizeAlloc = nBytes;
    memcpy( pC->pData, pLits, sizeof(int)*nLits );
 
    // For learnt clauses only:
    if ( fLearned )
    {
        int * pLevel = Msat_SolverReadDecisionLevelArray( p );
        int iLevelMax, iLevelCur, iLitMax;
 
        // Put the second watch on the literal with highest decision level:
        iLitMax = 1;
        iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
        for ( i = 2; i < nLits; i++ )
        {
            iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
            assert( iLevelCur != -1 );
            if ( iLevelMax < iLevelCur )
            // this is very strange - shouldn't it be???
            // if ( iLevelMax > iLevelCur )
                iLevelMax = iLevelCur, iLitMax = i;
        }
        pC->pData[1]       = pLits[iLitMax];
        pC->pData[iLitMax] = pLits[1];
 
        // Bumping:
        // (newly learnt clauses should be considered active)
        Msat_ClauseWriteActivity( pC, 0.0 );
        Msat_SolverClaBumpActivity( p, pC ); 
//        if ( nLits < 20 )
        for ( i = 0; i < nLits; i++ )
        {
            Msat_SolverVarBumpActivity( p, pLits[i] );
//            Msat_SolverVarBumpActivity( p, pLits[i] );
//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
        }
    }
 
    // Store clause:
    pvWatched = Msat_SolverReadWatchedArray( p );
    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
    *pClause_out = pC;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseCreateFake()

Msat_Clause_t * Msat_ClauseCreateFake	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vLits )

extern

◆ Msat_ClauseCreateFakeLit()

Msat_Clause_t * Msat_ClauseCreateFakeLit	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit )

extern

◆ Msat_ClauseFree()

void Msat_ClauseFree	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC,
		int	fRemoveWatched )

extern

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

Synopsis [Deallocates the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file msatClause.c.

{
    if ( fRemoveWatched )
    {
        Msat_Lit_t Lit;
        Msat_ClauseVec_t ** pvWatched;
        pvWatched = Msat_SolverReadWatchedArray( p );
        Lit = MSAT_LITNOT( pC->pData[0] );
        Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
        Lit = MSAT_LITNOT( pC->pData[1] );
        Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
    }
 
#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
    ABC_FREE( pC );
#else
    Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
#endif
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseIsLocked()

int Msat_ClauseIsLocked	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC )

extern

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

Synopsis [Checks whether the learned clause is locked.]

Description [The clause may be locked if it is the reason of a recent conflict. Such clause cannot be removed from the database.]

SideEffects []

SeeAlso []

Definition at line 278 of file msatClause.c.

{
    Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
    return (int )(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClausePrint()

void Msat_ClausePrint ( Msat_Clause_t * pC )

extern

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

Synopsis [Prints the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file msatClause.c.

{
    int i;
    if ( pC == NULL )
        printf( "NULL pointer" );
    else 
    {
        if ( pC->fLearned )
            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
        for ( i = 0; i < (int)pC->nSize; i++ )
            printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
    }
    printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClausePrintSymbols()

void Msat_ClausePrintSymbols ( Msat_Clause_t * pC )

extern

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

Synopsis [Prints the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 515 of file msatClause.c.

{
    int i;
    if ( pC == NULL )
        printf( "NULL pointer" );
    else 
    {
//        if ( pC->fLearned )
//            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
        for ( i = 0; i < (int)pC->nSize; i++ )
            printf(" " L_LIT, L_lit(pC->pData[i]));
    }
    printf( "\n" );
}

Here is the caller graph for this function:

◆ Msat_ClausePropagate()

int Msat_ClausePropagate	(	Msat_Clause_t *	pC,
		Msat_Lit_t	Lit,
		int *	pAssigns,
		Msat_Lit_t *	pLit_out )

extern

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

Synopsis [Propages the assignment.]

Description [The literal that has become true (Lit) is given to this procedure. The array of current variable assignments is given for efficiency. The output literal (pLit_out) can be the second watched literal (if TRUE is returned) or the conflict literal (if FALSE is returned). This messy interface is used to improve performance. This procedure accounts for ~50% of the runtime of the solver.]

SideEffects []

SeeAlso []

Definition at line 335 of file msatClause.c.

{
    // make sure the false literal is pC->pData[1]
    Msat_Lit_t LitF = MSAT_LITNOT(Lit);
    if ( pC->pData[0] == LitF )
         pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
    assert( pC->pData[1] == LitF );
    // if the 0-th watch is true, clause is already satisfied
    if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
        return 1; 
    // look for a new watch
    if ( pC->nSize > 2 )
    {
        int i;
        for ( i = 2; i < (int)pC->nSize; i++ )
            if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
            {
                pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
                *pLit_out = MSAT_LITNOT(pC->pData[1]);
                return 1; 
            }
    }
    // clause is unit under assignment
    *pLit_out = pC->pData[0];
    return 0;
}

Here is the caller graph for this function:

◆ Msat_ClauseReadActivity()

float Msat_ClauseReadActivity ( Msat_Clause_t * pC )

extern

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

Synopsis [Reads the activity of the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file msatClause.c.

{
    float f;
 
    memcpy( &f, pC->pData + pC->nSize, sizeof (f));
    return f;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseReadLearned()

int Msat_ClauseReadLearned ( Msat_Clause_t * pC )

extern

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

Synopsis [Access the data field of the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file msatClause.c.

255{ return pC->fLearned; }

◆ Msat_ClauseReadLits()

int * Msat_ClauseReadLits ( Msat_Clause_t * pC )

extern

Definition at line 257 of file msatClause.c.

257{ return pC->pData; }

◆ Msat_ClauseReadMark()

int Msat_ClauseReadMark ( Msat_Clause_t * pC )

extern

Definition at line 258 of file msatClause.c.

258{ return pC->fMark; }

◆ Msat_ClauseReadNum()

int Msat_ClauseReadNum ( Msat_Clause_t * pC )

extern

Definition at line 259 of file msatClause.c.

259{ return pC->Num; }

◆ Msat_ClauseReadSize()

int Msat_ClauseReadSize ( Msat_Clause_t * pC )

extern

Definition at line 256 of file msatClause.c.

256{ return pC->nSize; }

◆ Msat_ClauseReadTypeA()

int Msat_ClauseReadTypeA ( Msat_Clause_t * pC )

extern

Definition at line 260 of file msatClause.c.

260{ return pC->fTypeA; }

◆ Msat_ClauseRemoveWatch()

void Msat_ClauseRemoveWatch	(	Msat_ClauseVec_t *	vClauses,
		Msat_Clause_t *	pC )

extern

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

Synopsis [Removes the given clause from the watched list.]

Description []

SideEffects []

SeeAlso []

Definition at line 444 of file msatClause.c.

{
    Msat_Clause_t ** pClauses;
    int nClauses, i;
    nClauses = Msat_ClauseVecReadSize( vClauses );
    pClauses = Msat_ClauseVecReadArray( vClauses );
    for ( i = 0; pClauses[i] != pC; i++ )
        assert( i < nClauses );
    for (      ; i < nClauses - 1; i++ )
        pClauses[i] = pClauses[i+1];
    Msat_ClauseVecPop( vClauses );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseSetMark()

void Msat_ClauseSetMark	(	Msat_Clause_t *	pC,
		int	fMark )

extern

Definition at line 262 of file msatClause.c.

262{ pC->fMark = fMark; }

◆ Msat_ClauseSetNum()

void Msat_ClauseSetNum	(	Msat_Clause_t *	pC,
		int	Num )

extern

Definition at line 263 of file msatClause.c.

263{ pC->Num = Num; }

Here is the caller graph for this function:

◆ Msat_ClauseSetTypeA()

void Msat_ClauseSetTypeA	(	Msat_Clause_t *	pC,
		int	fTypeA )

extern

Definition at line 264 of file msatClause.c.

264{ pC->fTypeA = fTypeA; }

Here is the caller graph for this function:

◆ Msat_ClauseSimplify()

int Msat_ClauseSimplify	(	Msat_Clause_t *	pC,
		int *	pAssigns )

extern

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

Synopsis [Simplifies the clause.]

Description [Assumes everything has been propagated! (esp. watches in clauses are NOT unsatisfied)]

SideEffects []

SeeAlso []

Definition at line 374 of file msatClause.c.

{
    Msat_Var_t Var;
    int i, j;
    for ( i = j = 0; i < (int)pC->nSize; i++ )
    {
        Var = MSAT_LIT2VAR(pC->pData[i]);
        if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
        {
            pC->pData[j++] = pC->pData[i];
            continue;
        }
        if ( pAssigns[Var] == pC->pData[i] )
            return 1;
        // otherwise, the value of the literal is false
        // make sure, this literal is not watched
        assert( i >= 2 );
    }
    // if the size has changed, update it and move activity
    if ( j < (int)pC->nSize )
    {
        float Activ = Msat_ClauseReadActivity(pC);
        pC->nSize = j;
        Msat_ClauseWriteActivity(pC, Activ);
    }
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseVecAlloc()

Msat_ClauseVec_t * Msat_ClauseVecAlloc ( int nCap )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [msatClauseVec.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 [Procedures working with arrays of SAT clauses.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id: msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

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

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatClauseVec.c.

{
    Msat_ClauseVec_t * p;
    p = ABC_ALLOC( Msat_ClauseVec_t, 1 );
    if ( nCap > 0 && nCap < 16 )
        nCap = 16;
    p->nSize  = 0;
    p->nCap   = nCap;
    p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
    return p;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecClear()

void Msat_ClauseVecClear ( Msat_ClauseVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file msatClauseVec.c.

{
    p->nSize = 0;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecFree()

void Msat_ClauseVecFree ( Msat_ClauseVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file msatClauseVec.c.

{
    ABC_FREE( p->pArray );
    ABC_FREE( p );
}

Here is the caller graph for this function:

◆ Msat_ClauseVecGrow()

void Msat_ClauseVecGrow	(	Msat_ClauseVec_t *	p,
		int	nCapMin )

extern

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatClauseVec.c.

{
    if ( p->nCap >= nCapMin )
        return;
    p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
    p->nCap   = nCapMin;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecPop()

Msat_Clause_t * Msat_ClauseVecPop ( Msat_ClauseVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file msatClauseVec.c.

{
    return p->pArray[--p->nSize];
}

Here is the caller graph for this function:

◆ Msat_ClauseVecPush()

void Msat_ClauseVecPush	(	Msat_ClauseVec_t *	p,
		Msat_Clause_t *	Entry )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 169 of file msatClauseVec.c.

{
    if ( p->nSize == p->nCap )
    {
        if ( p->nCap < 16 )
            Msat_ClauseVecGrow( p, 16 );
        else
            Msat_ClauseVecGrow( p, 2 * p->nCap );
    }
    p->pArray[p->nSize++] = Entry;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseVecReadArray()

Msat_Clause_t ** Msat_ClauseVecReadArray ( Msat_ClauseVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file msatClauseVec.c.

{
    return p->pArray;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecReadEntry()

Msat_Clause_t * Msat_ClauseVecReadEntry	(	Msat_ClauseVec_t *	p,
		int	i )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file msatClauseVec.c.

{
    assert( i >= 0 && i < p->nSize );
    return p->pArray[i];
}

Here is the caller graph for this function:

◆ Msat_ClauseVecReadSize()

int Msat_ClauseVecReadSize ( Msat_ClauseVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file msatClauseVec.c.

{
    return p->nSize;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecShrink()

void Msat_ClauseVecShrink	(	Msat_ClauseVec_t *	p,
		int	nSizeNew )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatClauseVec.c.

{
    assert( p->nSize >= nSizeNew );
    p->nSize = nSizeNew;
}

Here is the caller graph for this function:

◆ Msat_ClauseVecWriteEntry()

void Msat_ClauseVecWriteEntry	(	Msat_ClauseVec_t *	p,
		int	i,
		Msat_Clause_t *	Entry )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file msatClauseVec.c.

{
    assert( i >= 0 && i < p->nSize );
    p->pArray[i] = Entry;
}

◆ Msat_ClauseWriteActivity()

void Msat_ClauseWriteActivity	(	Msat_Clause_t *	pC,
		float	Num )

extern

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

Synopsis [Sets the activity of the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 314 of file msatClause.c.

{
    memcpy( pC->pData + pC->nSize, &Num, sizeof (Num) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_ClauseWriteDimacs()

void Msat_ClauseWriteDimacs	(	FILE *	pFile,
		Msat_Clause_t *	pC,
		int	fIncrement )

extern

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

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file msatClause.c.

{
    int i;
    for ( i = 0; i < (int)pC->nSize; i++ )
        fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
    if ( fIncrement )
        fprintf( pFile, "0" );
    fprintf( pFile, "\n" );
}

Here is the caller graph for this function:

◆ Msat_MmFixedEntryFetch()

char * Msat_MmFixedEntryFetch ( Msat_MmFixed_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file msatMem.c.

{
    char * pTemp;
    int i;
 
    // check if there are still free entries
    if ( p->nEntriesUsed == p->nEntriesAlloc )
    { // need to allocate more entries
        assert( p->pEntriesFree == NULL );
        if ( p->nChunks == p->nChunksAlloc )
        {
            p->nChunksAlloc *= 2;
            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
        }
        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
        // transform these entries into a linked list
        pTemp = p->pEntriesFree;
        for ( i = 1; i < p->nChunkSize; i++ )
        {
            *((char **)pTemp) = pTemp + p->nEntrySize;
            pTemp += p->nEntrySize;
        }
        // set the last link
        *((char **)pTemp) = NULL;
        // add the chunk to the chunk storage
        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
        // add to the number of entries allocated
        p->nEntriesAlloc += p->nChunkSize;
    }
    // incrememt the counter of used entries
    p->nEntriesUsed++;
    if ( p->nEntriesMax < p->nEntriesUsed )
        p->nEntriesMax = p->nEntriesUsed;
    // return the first entry in the free entry list
    pTemp = p->pEntriesFree;
    p->pEntriesFree = *((char **)pTemp);
    return pTemp;
}

Here is the caller graph for this function:

◆ Msat_MmFixedEntryRecycle()

void Msat_MmFixedEntryRecycle	(	Msat_MmFixed_t *	p,
		char *	pEntry )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file msatMem.c.

{
    // decrement the counter of used entries
    p->nEntriesUsed--;
    // add the entry to the linked list of free entries
    *((char **)pEntry) = p->pEntriesFree;
    p->pEntriesFree = pEntry;
}

Here is the caller graph for this function:

◆ Msat_MmFixedReadMemUsage()

int Msat_MmFixedReadMemUsage ( Msat_MmFixed_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file msatMem.c.

{
    return p->nMemoryAlloc;
}

◆ Msat_MmFixedRestart()

void Msat_MmFixedRestart ( Msat_MmFixed_t * p )

extern

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

Synopsis []

Description [Relocates all the memory except the first chunk.]

SideEffects []

SeeAlso []

Definition at line 232 of file msatMem.c.

{
    int i;
    char * pTemp;
 
    // deallocate all chunks except the first one
    for ( i = 1; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    p->nChunks = 1;
    // transform these entries into a linked list
    pTemp = p->pChunks[0];
    for ( i = 1; i < p->nChunkSize; i++ )
    {
        *((char **)pTemp) = pTemp + p->nEntrySize;
        pTemp += p->nEntrySize;
    }
    // set the last link
    *((char **)pTemp) = NULL;
    // set the free entry list
    p->pEntriesFree  = p->pChunks[0];
    // set the correct statistics
    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
    p->nMemoryUsed   = 0;
    p->nEntriesAlloc = p->nChunkSize;
    p->nEntriesUsed  = 0;
}

◆ Msat_MmFixedStart()

Msat_MmFixed_t * Msat_MmFixedStart ( int nEntrySize )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates memory pieces of fixed size.]

Description [The size of the chunk is computed as the minimum of 1024 entries and 64K. Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 93 of file msatMem.c.

{
    Msat_MmFixed_t * p;
 
    p = ABC_ALLOC( Msat_MmFixed_t, 1 );
    memset( p, 0, sizeof(Msat_MmFixed_t) );
 
    p->nEntrySize    = nEntrySize;
    p->nEntriesAlloc = 0;
    p->nEntriesUsed  = 0;
    p->pEntriesFree  = NULL;
 
    if ( nEntrySize * (1 << 10) < (1<<16) )
        p->nChunkSize = (1 << 10);
    else
        p->nChunkSize = (1<<16) / nEntrySize;
    if ( p->nChunkSize < 8 )
        p->nChunkSize = 8;
 
    p->nChunksAlloc  = 64;
    p->nChunks       = 0;
    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
    p->nMemoryUsed   = 0;
    p->nMemoryAlloc  = 0;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_MmFixedStop()

void Msat_MmFixedStop	(	Msat_MmFixed_t *	p,
		int	fVerbose )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file msatMem.c.

{
    int i;
    if ( p == NULL )
        return;
    if ( fVerbose )
    {
        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
            p->nEntrySize, p->nChunkSize, p->nChunks );
        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
    }
    for ( i = 0; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    ABC_FREE( p->pChunks );
    ABC_FREE( p );
}

Here is the caller graph for this function:

◆ Msat_MmFlexEntryFetch()

char * Msat_MmFlexEntryFetch	(	Msat_MmFlex_t *	p,
		int	nBytes )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 349 of file msatMem.c.

{
    char * pTemp;
    // check if there are still free entries
    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
    { // need to allocate more entries
        if ( p->nChunks == p->nChunksAlloc )
        {
            p->nChunksAlloc *= 2;
            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
        }
        if ( nBytes > p->nChunkSize )
        {
            // resize the chunk size if more memory is requested than it can give
            // (ideally, this should never happen)
            p->nChunkSize = 2 * nBytes;
        }
        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
        p->pEnd     = p->pCurrent + p->nChunkSize;
        p->nMemoryAlloc += p->nChunkSize;
        // add the chunk to the chunk storage
        p->pChunks[ p->nChunks++ ] = p->pCurrent;
    }
    assert( p->pCurrent + nBytes <= p->pEnd );
    // increment the counter of used entries
    p->nEntriesUsed++;
    // keep track of the memory used
    p->nMemoryUsed += nBytes;
    // return the next entry
    pTemp = p->pCurrent;
    p->pCurrent += nBytes;
    return pTemp;
}

◆ Msat_MmFlexReadMemUsage()

int Msat_MmFlexReadMemUsage ( Msat_MmFlex_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 394 of file msatMem.c.

{
    return p->nMemoryAlloc;
}

◆ Msat_MmFlexStart()

Msat_MmFlex_t * Msat_MmFlexStart ( )

extern

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

Synopsis [Allocates entries of flexible size.]

Description [Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 288 of file msatMem.c.

{
    Msat_MmFlex_t * p;
 
    p = ABC_ALLOC( Msat_MmFlex_t, 1 );
    memset( p, 0, sizeof(Msat_MmFlex_t) );
 
    p->nEntriesUsed  = 0;
    p->pCurrent      = NULL;
    p->pEnd          = NULL;
 
    p->nChunkSize    = (1 << 12);
    p->nChunksAlloc  = 64;
    p->nChunks       = 0;
    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
    p->nMemoryUsed   = 0;
    p->nMemoryAlloc  = 0;
    return p;
}

Here is the call graph for this function:

◆ Msat_MmFlexStop()

void Msat_MmFlexStop	(	Msat_MmFlex_t *	p,
		int	fVerbose )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file msatMem.c.

{
    int i;
    if ( p == NULL )
        return;
    if ( fVerbose )
    {
        printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
            p->nChunkSize, p->nChunks );
        printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
            p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
    }
    for ( i = 0; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    ABC_FREE( p->pChunks );
    ABC_FREE( p );
}

◆ Msat_MmStepEntryFetch()

char * Msat_MmStepEntryFetch	(	Msat_MmStep_t *	p,
		int	nBytes )

extern

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

Synopsis [Creates the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 479 of file msatMem.c.

{
    if ( nBytes == 0 )
        return NULL;
    if ( nBytes > p->nMapSize )
    {
//        printf( "Allocating %d bytes.\n", nBytes );
        return ABC_ALLOC( char, nBytes );
    }
    return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_MmStepEntryRecycle()

void Msat_MmStepEntryRecycle	(	Msat_MmStep_t *	p,
		char *	pEntry,
		int	nBytes )

extern

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

Synopsis [Recycles the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file msatMem.c.

{
    if ( nBytes == 0 )
        return;
    if ( nBytes > p->nMapSize )
    {
        ABC_FREE( pEntry );
        return;
    }
    Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_MmStepReadMemUsage()

int Msat_MmStepReadMemUsage ( Msat_MmStep_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 526 of file msatMem.c.

{
    int i, nMemTotal = 0;
    for ( i = 0; i < p->nMems; i++ )
        nMemTotal += p->pMems[i]->nMemoryAlloc;
    return nMemTotal;
}

◆ Msat_MmStepStart()

Msat_MmStep_t * Msat_MmStepStart ( int nSteps )

extern

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

Synopsis [Starts the hierarchical memory manager.]

Description [This manager can allocate entries of any size. Iternally they are mapped into the entries with the number of bytes equal to the power of 2. The smallest entry size is 8 bytes. The next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. The input parameters "nSteps" says how many fixed memory managers are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger entries are handed over to malloc() and then ABC_FREE()ed.]

SideEffects []

SeeAlso []

Definition at line 423 of file msatMem.c.

{
    Msat_MmStep_t * p;
    int i, k;
    p = ABC_ALLOC( Msat_MmStep_t, 1 );
    p->nMems = nSteps;
    // start the fixed memory managers
    p->pMems = ABC_ALLOC( Msat_MmFixed_t *, p->nMems );
    for ( i = 0; i < p->nMems; i++ )
        p->pMems[i] = Msat_MmFixedStart( (8<<i) );
    // set up the mapping of the required memory size into the corresponding manager
    p->nMapSize = (4<<p->nMems);
    p->pMap = ABC_ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
    p->pMap[0] = NULL;
    for ( k = 1; k <= 4; k++ )
        p->pMap[k] = p->pMems[0];
    for ( i = 0; i < p->nMems; i++ )
        for ( k = (4<<i)+1; k <= (8<<i); k++ )
            p->pMap[k] = p->pMems[i];
//for ( i = 1; i < 100; i ++ )
//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_MmStepStop()

void Msat_MmStepStop	(	Msat_MmStep_t *	p,
		int	fVerbose )

extern

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

Synopsis [Stops the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file msatMem.c.

{
    int i;
    for ( i = 0; i < p->nMems; i++ )
        Msat_MmFixedStop( p->pMems[i], fVerbose );
    ABC_FREE( p->pMems );
    ABC_FREE( p->pMap );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_OrderAlloc()

Msat_Order_t * Msat_OrderAlloc ( Msat_Solver_t * pSat )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file msatOrderH.c.

{
    Msat_Order_t * p;
    p = ABC_ALLOC( Msat_Order_t, 1 );
    memset( p, 0, sizeof(Msat_Order_t) );
    p->pSat   = pSat;
    p->vIndex = Msat_IntVecAlloc( 0 );
    p->vHeap  = Msat_IntVecAlloc( 0 );
    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_OrderCheck()

int Msat_OrderCheck ( Msat_Order_t * p )

extern

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

Synopsis [Checks that the J-boundary is okay.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file msatOrderH.c.

{
    return Msat_HeapCheck_rec( p, 1 );
}

Here is the call graph for this function:

◆ Msat_OrderClean()

void Msat_OrderClean	(	Msat_Order_t *	p,
		Msat_IntVec_t *	vCone )

extern

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

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file msatOrderH.c.

{
    int i;
    for ( i = 0; i < p->vIndex->nSize; i++ )
        p->vIndex->pArray[i] = 0;
    for ( i = 0; i < vCone->nSize; i++ )
    {
        assert( i+1 < p->vHeap->nCap );
        p->vHeap->pArray[i+1] = vCone->pArray[i];
 
        assert( vCone->pArray[i] < p->vIndex->nSize );
        p->vIndex->pArray[vCone->pArray[i]] = i+1;
    }
    p->vHeap->nSize = vCone->nSize + 1;
}

Here is the caller graph for this function:

◆ Msat_OrderFree()

void Msat_OrderFree ( Msat_Order_t * p )

extern

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

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file msatOrderH.c.

{
    Msat_IntVecFree( p->vHeap );
    Msat_IntVecFree( p->vIndex );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_OrderSetBounds()

void Msat_OrderSetBounds	(	Msat_Order_t *	p,
		int	nVarsMax )

extern

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

Synopsis [Sets the bound of the ordering structure.]

Description [Should be called whenever the SAT solver is resized.]

SideEffects []

SeeAlso []

Definition at line 101 of file msatOrderH.c.

{
    Msat_IntVecGrow( p->vIndex, nVarsMax );
    Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
    p->vIndex->nSize = nVarsMax;
    p->vHeap->nSize = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_OrderUpdate()

void Msat_OrderUpdate	(	Msat_Order_t *	p,
		int	Var )

extern

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

Synopsis [Updates the order after a variable changed weight.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file msatOrderH.c.

{
//    if (heap.inHeap(x))
//        heap.increase(x);
 
    abctime clk = Abc_Clock();
    if ( HINHEAP(p,Var) )
        Msat_HeapIncrease( p, Var );
timeSelect += Abc_Clock() - clk;
}

Here is the caller graph for this function:

◆ Msat_OrderVarAssigned()

void Msat_OrderVarAssigned	(	Msat_Order_t *	p,
		int	Var )

extern

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

Synopsis [Updates J-boundary when the variable is assigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file msatOrderH.c.

221{

222}

Here is the caller graph for this function:

◆ Msat_OrderVarSelect()

int Msat_OrderVarSelect ( Msat_Order_t * p )

extern

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

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file msatOrderH.c.

{
    // Activity based decision:
//    while (!heap.empty()){
//        Var next = heap.getmin();
//        if (toLbool(assigns[next]) == l_Undef)
//            return next;
//    }
//    return var_Undef;
 
    int Var;
    abctime clk = Abc_Clock();
 
    while ( !HEMPTY(p) )
    {
        Var = Msat_HeapGetTop(p);
        if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
        {
//assert( Msat_OrderCheck(p) );
timeSelect += Abc_Clock() - clk;
            return Var;
        }
    }
    return MSAT_ORDER_UNKNOWN;
}

Here is the caller graph for this function:

◆ Msat_OrderVarUnassigned()

void Msat_OrderVarUnassigned	(	Msat_Order_t *	p,
		int	Var )

extern

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

Synopsis [Updates the order after a variable is unassigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file msatOrderH.c.

{
//    if (!heap.inHeap(x))
//        heap.insert(x);
 
    abctime clk = Abc_Clock();
    if ( !HINHEAP(p,Var) )
        Msat_HeapInsert( p, Var );
timeSelect += Abc_Clock() - clk;
}

◆ Msat_QueueAlloc()

Msat_Queue_t * Msat_QueueAlloc ( int nVars )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file msatQueue.c.

{
    Msat_Queue_t * p;
    p = ABC_ALLOC( Msat_Queue_t, 1 );
    memset( p, 0, sizeof(Msat_Queue_t) );
    p->nVars  = nVars;
    p->pVars  = ABC_ALLOC( int, nVars );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_QueueClear()

void Msat_QueueClear ( Msat_Queue_t * p )

extern

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

Synopsis [Resets the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file msatQueue.c.

{
    p->iFirst = 0;
    p->iLast  = 0;
}

Here is the caller graph for this function:

◆ Msat_QueueExtract()

int Msat_QueueExtract ( Msat_Queue_t * p )

extern

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

Synopsis [Extracts an entry from the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file msatQueue.c.

{
    if ( p->iFirst == p->iLast )
        return -1;
    return p->pVars[p->iFirst++];
}

Here is the caller graph for this function:

◆ Msat_QueueFree()

void Msat_QueueFree ( Msat_Queue_t * p )

extern

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

Synopsis [Deallocate the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file msatQueue.c.

{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
}

Here is the caller graph for this function:

◆ Msat_QueueInsert()

void Msat_QueueInsert	(	Msat_Queue_t *	p,
		int	Lit )

extern

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

Synopsis [Insert an entry into the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file msatQueue.c.

{
    if ( p->iLast == p->nVars )
    {
        int i;
        assert( 0 );
        for ( i = 0; i < p->iLast; i++ )
            printf( "entry = %2d  lit = %2d  var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
    }
    assert( p->iLast < p->nVars );
    p->pVars[p->iLast++] = Lit;
}

Here is the caller graph for this function:

◆ Msat_QueueReadSize()

int Msat_QueueReadSize ( Msat_Queue_t * p )

extern

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

Synopsis [Reads the queue size.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file msatQueue.c.

{
    return p->iLast - p->iFirst;
}

Here is the caller graph for this function:

◆ Msat_SolverAssume()

int Msat_SolverAssume	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Makes the next assumption (Lit).]

Description [Returns FALSE if immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 51 of file msatSolverSearch.c.

{
    assert( Msat_QueueReadSize(p->pQueue) == 0 );
    if ( p->fVerbose )
        printf(L_IND "assume(" L_LIT ")\n", L_ind, L_lit(Lit));
    Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
//    assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
//    assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
    return Msat_SolverEnqueue( p, Lit, NULL );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverCancelUntil()

void Msat_SolverCancelUntil	(	Msat_Solver_t *	p,
		int	Level )

extern

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

Synopsis [Reverts to the state at given level.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file msatSolverSearch.c.

{
    while ( Msat_IntVecReadSize(p->vTrailLim) > Level )
        Msat_SolverCancel(p);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverClaBumpActivity()

void Msat_SolverClaBumpActivity	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file msatActivity.c.

{
    float Activ;
    Activ = Msat_ClauseReadActivity(pC);
    if ( Activ + p->dClaInc > 1e20 )
    {
        Msat_SolverClaRescaleActivity( p );
        Activ = Msat_ClauseReadActivity( pC );
    }
    Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverClaDecayActivity()

void Msat_SolverClaDecayActivity ( Msat_Solver_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file msatActivity.c.

{
    p->dClaInc *= p->dClaDecay;
}

Here is the caller graph for this function:

◆ Msat_SolverClaRescaleActivity()

void Msat_SolverClaRescaleActivity ( Msat_Solver_t * p )

extern

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

Synopsis [Divide all constraint activities by 1e20.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file msatActivity.c.

{
    Msat_Clause_t ** pLearned;
    int nLearned, i;
    float Activ;
    nLearned = Msat_ClauseVecReadSize( p->vLearned );
    pLearned = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nLearned; i++ )
    {
        Activ = Msat_ClauseReadActivity( pLearned[i] );
        Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 );
    }
    p->dClaInc *= 1e-20;
}

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 )

extern

Definition at line 65 of file msatSolverApi.c.

65{ p->nClausesAlloc--; }

◆ Msat_SolverClausesDecrementL()

void Msat_SolverClausesDecrementL ( Msat_Solver_t * p )

extern

Definition at line 67 of file msatSolverApi.c.

67{ p->nClausesAllocL--; }

◆ Msat_SolverClausesIncrement()

void Msat_SolverClausesIncrement ( Msat_Solver_t * p )

extern

Definition at line 64 of file msatSolverApi.c.

64{ p->nClausesAlloc++; }

◆ Msat_SolverClausesIncrementL()

void Msat_SolverClausesIncrementL ( Msat_Solver_t * p )

extern

Definition at line 66 of file msatSolverApi.c.

66{ p->nClausesAllocL++; }

◆ Msat_SolverEnqueue()

int Msat_SolverEnqueue	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit,
		Msat_Clause_t *	pC )

extern

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

Synopsis [Enqueues one variable assignment.]

Description [Puts a new fact on the propagation queue and immediately updates the variable value. Should a conflict arise, FALSE is returned. Otherwise returns TRUE.]

SideEffects []

SeeAlso []

Definition at line 173 of file msatSolverSearch.c.

{
    Msat_Var_t Var = MSAT_LIT2VAR(Lit);
 
    // skip literals that are not in the current cone
    if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) )
        return 1;
 
//    assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) );
    // if the literal is assigned
    // return 1 if the assignment is consistent
    // return 0 if the assignment is inconsistent (conflict)
    if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED )
        return p->pAssigns[Var] == Lit;
    // new fact - store it
    if ( p->fVerbose )
    {
//        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
        printf(L_IND "bind(" L_LIT ")  ", L_ind, L_lit(Lit));
        Msat_ClausePrintSymbols( pC );
    }
    p->pAssigns[Var] = Lit;
    p->pLevel[Var]   = Msat_IntVecReadSize(p->vTrailLim);
//    p->pReasons[Var] = p->pLevel[Var]? pC: NULL;
    p->pReasons[Var] = pC;
    Msat_IntVecPush( p->vTrail, Lit );
    Msat_QueueInsert( p->pQueue, Lit );
 
    Msat_OrderVarAssigned( p->pOrder, Var );
    return 1;
}

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 )

extern

Definition at line 62 of file msatSolverApi.c.

62{ return ++p->nSeenId; }

Here is the caller graph for this function:

◆ Msat_SolverProgressEstimate()

double Msat_SolverProgressEstimate ( Msat_Solver_t * p )

extern

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

Synopsis [Returns search-space coverage. Not extremely reliable.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file msatSolverCore.c.

{
    double dProgress = 0.0;
    double dF = 1.0 / p->nVars;
    int i;
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
            dProgress += pow( dF, p->pLevel[i] );
    return dProgress / p->nVars;
}

Here is the caller graph for this function:

◆ Msat_SolverPropagate()

Msat_Clause_t * Msat_SolverPropagate ( Msat_Solver_t * p )

extern

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

Synopsis [Propagates the assignments in the queue.]

Description [Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, otherwise NULL.]

SideEffects [The propagation queue is empty, even if there was a conflict.]

SeeAlso []

Definition at line 217 of file msatSolverSearch.c.

{
    Msat_ClauseVec_t ** pvWatched = p->pvWatched;
    Msat_Clause_t ** pClauses;
    Msat_Clause_t * pConflict;
    Msat_Lit_t Lit, Lit_out;
    int i, j, nClauses;
 
    // propagate all the literals in the queue
    while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 )
    {
        p->Stats.nPropagations++;
        // get the clauses watched by this literal
        nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] );
        pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] );
        // go through the watched clauses and decide what to do with them
        for ( i = j = 0; i < nClauses; i++ )
        {
            p->Stats.nInspects++;
            // clear the returned literal
            Lit_out = -1;
            // propagate the clause
            if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) )
            {   // the clause is unit
                // "Lit_out" contains the new assignment to be enqueued
                if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) 
                { // consistent assignment 
                    // no changes to the implication queue; the watch is the same too
                    pClauses[j++] = pClauses[i];
                    continue;
                }
                // remember the reason of conflict (will be returned)
                pConflict = pClauses[i];
                // leave the remaning clauses in the same watched list
                for ( ; i < nClauses; i++ )
                    pClauses[j++] = pClauses[i];
                Msat_ClauseVecShrink( pvWatched[Lit], j );
                // clear the propagation queue
                Msat_QueueClear( p->pQueue );
                return pConflict;
            }
            // the clause is not unit
            // in this case "Lit_out" contains the new watch if it has changed
            if ( Lit_out >= 0 )
                Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] );
            else // the watch did not change
                pClauses[j++] = pClauses[i];
        }
        Msat_ClauseVecShrink( pvWatched[Lit], j );
    }
    return NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverReadClause()

Msat_Clause_t * Msat_SolverReadClause	(	Msat_Solver_t *	p,
		int	Num )

extern

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_SolverReadDecisionLevel()

int Msat_SolverReadDecisionLevel ( Msat_Solver_t * p )

extern

Definition at line 50 of file msatSolverApi.c.

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

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 )

extern

Definition at line 51 of file msatSolverApi.c.

51{ return p->pLevel; }

Here is the caller graph for this function:

◆ Msat_SolverReadLearned()

Msat_ClauseVec_t * Msat_SolverReadLearned ( Msat_Solver_t * p )

extern

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 )

extern

Definition at line 60 of file msatSolverApi.c.

60{ return p->pMem; }

Here is the caller graph for this function:

◆ Msat_SolverReadReasonArray()

Msat_Clause_t ** Msat_SolverReadReasonArray ( Msat_Solver_t * p )

extern

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 )

extern

Definition at line 61 of file msatSolverApi.c.

61{ return p->pSeen; }

Here is the caller graph for this function:

◆ Msat_SolverReadVarValue()

Msat_Type_t Msat_SolverReadVarValue	(	Msat_Solver_t *	p,
		Msat_Var_t	Var )

extern

Definition at line 53 of file msatSolverApi.c.

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

Msat_Type_t

Definition msat.h:50

◆ Msat_SolverReadWatchedArray()

Msat_ClauseVec_t ** Msat_SolverReadWatchedArray ( Msat_Solver_t * p )

extern

Definition at line 55 of file msatSolverApi.c.

55{ return p->pvWatched; }

Here is the caller graph for this function:

◆ Msat_SolverSearch()

Msat_Type_t Msat_SolverSearch	(	Msat_Solver_t *	p,
		int	nConfLimit,
		int	nLearnedLimit,
		int	nBackTrackLimit,
		Msat_SearchParams_t *	pPars )

extern

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

Synopsis [The search procedure called between the restarts.]

Description [Search for a satisfying solution as long as the number of conflicts does not exceed the limit (nConfLimit) while keeping the number of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use negative value for nConfLimit or nLearnedLimit to indicate infinity.]

SideEffects []

SeeAlso []

Definition at line 535 of file msatSolverSearch.c.

{
    Msat_Clause_t * pConf;
    Msat_Var_t Var;
    int nLevelBack, nConfs, nAssigns, Value;
    int i;
 
    assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
    p->Stats.nStarts++;
    p->dVarDecay = 1 / pPars->dVarDecay;
    p->dClaDecay = 1 / pPars->dClaDecay;
 
    // reset the activities
    for ( i = 0; i < p->nVars; i++ )
       p->pdActivity[i] = (double)p->pFactors[i];
//       p->pdActivity[i] = 0.0;
 
    nConfs = 0;
    while ( 1 )
    {
        pConf = Msat_SolverPropagate( p );
        if ( pConf != NULL ){
            // CONFLICT
            if ( p->fVerbose )
            {
//                printf(L_IND"**CONFLICT**\n", L_ind);
                printf(L_IND"**CONFLICT**  ", L_ind);
                Msat_ClausePrintSymbols( pConf );
            }
            // count conflicts
            p->Stats.nConflicts++;
            nConfs++;
 
            // if top level, return UNSAT
            if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot )
                return MSAT_FALSE;
 
            // perform conflict analysis
            Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack );
            Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack );
            Msat_SolverRecord( p, p->vTemp );
 
            // it is important that recording is done after cancelling
            // because canceling cleans the queue while recording adds to it
            Msat_SolverVarDecayActivity( p );
            Msat_SolverClaDecayActivity( p );
 
        }
        else{
            // NO CONFLICT
            if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) {
                // Simplify the set of problem clauses:
//                Value = Msat_SolverSimplifyDB(p);
//                assert( Value );
            }
            nAssigns = Msat_IntVecReadSize( p->vTrail );
            if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) {
                // Reduce the set of learnt clauses:
                Msat_SolverReduceDB(p);
            }
 
            Var = Msat_OrderVarSelect( p->pOrder );
            if ( Var == MSAT_ORDER_UNKNOWN ) {
                // Model found and stored in p->pAssigns
                memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars );
                Msat_QueueClear( p->pQueue );
                Msat_SolverCancelUntil( p, p->nLevelRoot );
                return MSAT_TRUE;
            }
            if ( nConfLimit > 0 && nConfs > nConfLimit ) {
                // Reached bound on number of conflicts:
                p->dProgress = Msat_SolverProgressEstimate( p );
                Msat_QueueClear( p->pQueue );
                Msat_SolverCancelUntil( p, p->nLevelRoot );
                return MSAT_UNKNOWN; 
            }
            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
                // Reached bound on number of conflicts:
                Msat_QueueClear( p->pQueue );
                Msat_SolverCancelUntil( p, p->nLevelRoot );
                return MSAT_UNKNOWN; 
            }
            else{
                // New variable decision:
                p->Stats.nDecisions++;
                assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars );
                Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) );
                assert( Value );
            }
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverSortDB()

void Msat_SolverSortDB ( Msat_Solver_t * p )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file msatSort.c.

{
    Msat_ClauseVec_t * pVecClauses;
    Msat_Clause_t ** pLearned;
    int nLearned;
    // read the parameters
    pVecClauses = Msat_SolverReadLearned( p );
    nLearned    = Msat_ClauseVecReadSize( pVecClauses );
    pLearned    = Msat_ClauseVecReadArray( pVecClauses );
    // Msat_SolverSort the array
//    qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 
//            (int (*)(const void *, const void *)) Msat_SolverSortCompare );
//    printf( "Msat_SolverSorting.\n" );
    Msat_SolverSort( pLearned, nLearned, 91648253 );
/*
    if ( nLearned > 2 )
    {
    printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
    printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
    printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
    }
*/
}

Here is the call graph for this function:

◆ Msat_SolverVarBumpActivity()

void Msat_SolverVarBumpActivity	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [msatActivity.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 [Procedures controlling activity of variables and clauses.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id: msatActivity.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatActivity.c.

{
    Msat_Var_t Var;
    if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
        return;
    Var = MSAT_LIT2VAR(Lit);
    p->pdActivity[Var] += p->dVarInc;
//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
    if ( p->pdActivity[Var] > 1e100 )
        Msat_SolverVarRescaleActivity( p );
    Msat_OrderUpdate( p->pOrder, Var );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverVarDecayActivity()

void Msat_SolverVarDecayActivity ( Msat_Solver_t * p )

extern

GLOBAL VARIABLES ///.

MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file msatActivity.c.

{
    if ( p->dVarDecay >= 0 )
        p->dVarInc *= p->dVarDecay;
}

Here is the caller graph for this function:

◆ Msat_SolverVarRescaleActivity()

void Msat_SolverVarRescaleActivity ( Msat_Solver_t * p )

extern

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

Synopsis [Divide all variable activities by 1e100.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file msatActivity.c.

{
    int i;
    for ( i = 0; i < p->nVars; i++ )
        p->pdActivity[i] *= 1e-100;
    p->dVarInc *= 1e-100;
}

Here is the caller graph for this function:

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ L_IND

◆ L_ind

◆ L_LIT

◆ L_lit

◆ MSAT_LIT_UNASSIGNED

◆ MSAT_ORDER_UNKNOWN

◆ MSAT_VAR_UNASSIGNED

Typedef Documentation

◆ Msat_Clause_t

◆ Msat_Lit_t

◆ Msat_MmFixed_t

◆ Msat_MmFlex_t

◆ Msat_MmStep_t

◆ Msat_Order_t

◆ Msat_Queue_t

◆ Msat_SearchParams_t

◆ Msat_SolverStats_t

◆ Msat_Var_t

Function Documentation

◆ Msat_ClauseCalcReason()

◆ Msat_ClauseComputeTruth()

◆ Msat_ClauseCreate()

◆ Msat_ClauseCreateFake()

◆ Msat_ClauseCreateFakeLit()

◆ Msat_ClauseFree()

◆ Msat_ClauseIsLocked()

◆ Msat_ClausePrint()

◆ Msat_ClausePrintSymbols()

◆ Msat_ClausePropagate()

◆ Msat_ClauseReadActivity()

◆ Msat_ClauseReadLearned()

◆ Msat_ClauseReadLits()

◆ Msat_ClauseReadMark()

◆ Msat_ClauseReadNum()

◆ Msat_ClauseReadSize()

◆ Msat_ClauseReadTypeA()

◆ Msat_ClauseRemoveWatch()

◆ Msat_ClauseSetMark()

◆ Msat_ClauseSetNum()

◆ Msat_ClauseSetTypeA()

◆ Msat_ClauseSimplify()

◆ Msat_ClauseVecAlloc()

◆ Msat_ClauseVecClear()

◆ Msat_ClauseVecFree()

◆ Msat_ClauseVecGrow()

◆ Msat_ClauseVecPop()

◆ Msat_ClauseVecPush()

◆ Msat_ClauseVecReadArray()

◆ Msat_ClauseVecReadEntry()

◆ Msat_ClauseVecReadSize()

◆ Msat_ClauseVecShrink()

◆ Msat_ClauseVecWriteEntry()

◆ Msat_ClauseWriteActivity()

◆ Msat_ClauseWriteDimacs()

◆ Msat_MmFixedEntryFetch()

◆ Msat_MmFixedEntryRecycle()

◆ Msat_MmFixedReadMemUsage()

◆ Msat_MmFixedRestart()

◆ Msat_MmFixedStart()

◆ Msat_MmFixedStop()

◆ Msat_MmFlexEntryFetch()

◆ Msat_MmFlexReadMemUsage()

◆ Msat_MmFlexStart()

◆ Msat_MmFlexStop()

◆ Msat_MmStepEntryFetch()

◆ Msat_MmStepEntryRecycle()

◆ Msat_MmStepReadMemUsage()

◆ Msat_MmStepStart()

◆ Msat_MmStepStop()

◆ Msat_OrderAlloc()

◆ Msat_OrderCheck()

◆ Msat_OrderClean()

◆ Msat_OrderFree()

◆ Msat_OrderSetBounds()

◆ Msat_OrderUpdate()