msatInt.h File Reference

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

Go to the source code of this file.

Data Structures
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)   MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_	Msat_Clause_t
	INCLUDES ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
Msat_ClauseVec_t *	Msat_ClauseVecAlloc (int nCap)
	DECLARATIONS ///. More...
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 ///. More...
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

#define L_IND   "%-*d"

Definition at line 73 of file msatInt.h.

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

Definition at line 74 of file msatInt.h.

#define L_LIT   "%s%d"

Definition at line 75 of file msatInt.h.

#define L_lit

(

Lit

)

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

Definition at line 76 of file msatInt.h.

#define MSAT_LIT_UNASSIGNED   (-2)

Definition at line 69 of file msatInt.h.

#define MSAT_ORDER_UNKNOWN   (-3)

Definition at line 70 of file msatInt.h.

#define MSAT_VAR_UNASSIGNED   (-1)

Definition at line 68 of file msatInt.h.

Typedef Documentation

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.

typedef int Msat_Lit_t

Definition at line 65 of file msatInt.h.

typedef struct Msat_MmFixed_t_ Msat_MmFixed_t

Definition at line 61 of file msatInt.h.

typedef struct Msat_MmFlex_t_ Msat_MmFlex_t

Definition at line 62 of file msatInt.h.

typedef struct Msat_MmStep_t_ Msat_MmStep_t

Definition at line 63 of file msatInt.h.

typedef struct Msat_Order_t_ Msat_Order_t

Definition at line 59 of file msatInt.h.

typedef struct Msat_Queue_t_ Msat_Queue_t

Definition at line 58 of file msatInt.h.

typedef struct Msat_SearchParams_t_ Msat_SearchParams_t

Definition at line 89 of file msatInt.h.

typedef struct Msat_SolverStats_t_ Msat_SolverStats_t

Definition at line 78 of file msatInt.h.

typedef int Msat_Var_t

Definition at line 66 of file msatInt.h.

Function Documentation

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

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

unsigned Msat_ClauseComputeTruth	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC
	)

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

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

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
	)

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

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

}

int Msat_ClauseIsLocked	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC
	)

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

void Msat_ClausePrint

(

Msat_Clause_t *

pC

)

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

void Msat_ClausePrintSymbols

(

Msat_Clause_t *

pC

)

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

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

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

float Msat_ClauseReadActivity

(

Msat_Clause_t *

pC

)

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

int Msat_ClauseReadLearned

(

Msat_Clause_t *

pC

)

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

Synopsis [Access the data field of the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file msatClause.c.

{  return pC->fLearned; }

int* Msat_ClauseReadLits

(

Msat_Clause_t *

pC

)

Definition at line 257 of file msatClause.c.

{  return pC->pData;    }

int Msat_ClauseReadMark

(

Msat_Clause_t *

pC

)

Definition at line 258 of file msatClause.c.

{  return pC->fMark;    }

int Msat_ClauseReadNum

(

Msat_Clause_t *

pC

)

Definition at line 259 of file msatClause.c.

{  return pC->Num;      }

int Msat_ClauseReadSize

(

Msat_Clause_t *

pC

)

Definition at line 256 of file msatClause.c.

{  return pC->nSize;    }

int Msat_ClauseReadTypeA

(

Msat_Clause_t *

pC

)

Definition at line 260 of file msatClause.c.

{  return pC->fTypeA;    }

void Msat_ClauseRemoveWatch	(	Msat_ClauseVec_t *	vClauses,
		Msat_Clause_t *	pC
	)

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

void Msat_ClauseSetMark	(	Msat_Clause_t *	pC,
		int	fMark
	)

Definition at line 262 of file msatClause.c.

{  pC->fMark = fMark;   }

void Msat_ClauseSetNum	(	Msat_Clause_t *	pC,
		int	Num
	)

Definition at line 263 of file msatClause.c.

{  pC->Num = Num;       }

void Msat_ClauseSetTypeA	(	Msat_Clause_t *	pC,
		int	fTypeA
	)

Definition at line 264 of file msatClause.c.

{  pC->fTypeA = fTypeA; }

int Msat_ClauseSimplify	(	Msat_Clause_t *	pC,
		int *	pAssigns
	)

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

Msat_ClauseVec_t* Msat_ClauseVecAlloc

(

int

nCap

)

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

void Msat_ClauseVecClear

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file msatClauseVec.c.

{
    p->nSize = 0;
}

void Msat_ClauseVecFree

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file msatClauseVec.c.

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

void Msat_ClauseVecGrow	(	Msat_ClauseVec_t *	p,
		int	nCapMin
	)

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

Msat_Clause_t* Msat_ClauseVecPop

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file msatClauseVec.c.

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

void Msat_ClauseVecPush	(	Msat_ClauseVec_t *	p,
		Msat_Clause_t *	Entry
	)

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

Msat_Clause_t** Msat_ClauseVecReadArray

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file msatClauseVec.c.

{
    return p->pArray;
}

Msat_Clause_t* Msat_ClauseVecReadEntry	(	Msat_ClauseVec_t *	p,
		int	i
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file msatClauseVec.c.

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

int Msat_ClauseVecReadSize

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file msatClauseVec.c.

{
    return p->nSize;
}

void Msat_ClauseVecShrink	(	Msat_ClauseVec_t *	p,
		int	nSizeNew
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatClauseVec.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file msatClauseVec.c.

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

void Msat_ClauseWriteActivity	(	Msat_Clause_t *	pC,
		float	Num
	)

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

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

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

char* Msat_MmFixedEntryFetch

(

Msat_MmFixed_t *

p

)

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

void Msat_MmFixedEntryRecycle	(	Msat_MmFixed_t *	p,
		char *	pEntry
	)

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

int Msat_MmFixedReadMemUsage

(

Msat_MmFixed_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file msatMem.c.

{
    return p->nMemoryAlloc;
}

void Msat_MmFixedRestart

(

Msat_MmFixed_t *

p

)

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_MmFixed_t* Msat_MmFixedStart

(

int

nEntrySize

)

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

void Msat_MmFixedStop	(	Msat_MmFixed_t *	p,
		int	fVerbose
	)

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

char* Msat_MmFlexEntryFetch	(	Msat_MmFlex_t *	p,
		int	nBytes
	)

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

int Msat_MmFlexReadMemUsage

(

Msat_MmFlex_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 394 of file msatMem.c.

{
    return p->nMemoryAlloc;
}

Msat_MmFlex_t* Msat_MmFlexStart

(

)

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

void Msat_MmFlexStop	(	Msat_MmFlex_t *	p,
		int	fVerbose
	)

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

char* Msat_MmStepEntryFetch	(	Msat_MmStep_t *	p,
		int	nBytes
	)

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

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

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

int Msat_MmStepReadMemUsage

(

Msat_MmStep_t *

p

)

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_MmStep_t* Msat_MmStepStart

(

int

nSteps

)

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

void Msat_MmStepStop	(	Msat_MmStep_t *	p,
		int	fVerbose
	)

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

Msat_Order_t* Msat_OrderAlloc

(

Msat_Solver_t *

pSat

)

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

int Msat_OrderCheck

(

Msat_Order_t *

p

)

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

void Msat_OrderClean	(	Msat_Order_t *	p,
		Msat_IntVec_t *	vCone
	)

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

void Msat_OrderFree

(

Msat_Order_t *

p

)

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

void Msat_OrderSetBounds	(	Msat_Order_t *	p,
		int	nVarsMax
	)

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

void Msat_OrderUpdate	(	Msat_Order_t *	p,
		int	Var
	)

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

void Msat_OrderVarAssigned	(	Msat_Order_t *	p,
		int	Var
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file msatOrderH.c.

{
}

int Msat_OrderVarSelect

(

Msat_Order_t *

p

)

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

void Msat_OrderVarUnassigned	(	Msat_Order_t *	p,
		int	Var
	)

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_Queue_t* Msat_QueueAlloc

(

int

nVars

)

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

void Msat_QueueClear

(

Msat_Queue_t *

p

)

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

Synopsis [Resets the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file msatQueue.c.

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

int Msat_QueueExtract

(

Msat_Queue_t *

p

)

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++];
}

void Msat_QueueFree

(

Msat_Queue_t *

p

)

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

void Msat_QueueInsert	(	Msat_Queue_t *	p,
		int	Lit
	)

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

int Msat_QueueReadSize

(

Msat_Queue_t *

p

)

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

Synopsis [Reads the queue size.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file msatQueue.c.

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

int Msat_SolverAssume	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit
	)

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

void Msat_SolverCancelUntil	(	Msat_Solver_t *	p,
		int	Level
	)

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

void Msat_SolverClaBumpActivity	(	Msat_Solver_t *	p,
		Msat_Clause_t *	pC
	)

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

void Msat_SolverClaDecayActivity

(

Msat_Solver_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file msatActivity.c.

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

void Msat_SolverClaRescaleActivity

(

Msat_Solver_t *

p

)

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

void Msat_SolverClausesDecrement

(

Msat_Solver_t *

p

)

Definition at line 65 of file msatSolverApi.c.

{ p->nClausesAlloc--;   }

void Msat_SolverClausesDecrementL

(

Msat_Solver_t *

p

)

Definition at line 67 of file msatSolverApi.c.

{ p->nClausesAllocL--;  }

void Msat_SolverClausesIncrement

(

Msat_Solver_t *

p

)

Definition at line 64 of file msatSolverApi.c.

{ p->nClausesAlloc++;   }

void Msat_SolverClausesIncrementL

(

Msat_Solver_t *

p

)

Definition at line 66 of file msatSolverApi.c.

{ p->nClausesAllocL++;  }

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

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

int Msat_SolverIncrementSeenId

(

Msat_Solver_t *

p

)

Definition at line 62 of file msatSolverApi.c.

{ return ++p->nSeenId;  }

double Msat_SolverProgressEstimate

(

Msat_Solver_t *

p

)

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

Msat_Clause_t* Msat_SolverPropagate

(

Msat_Solver_t *

p

)

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

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

int Msat_SolverReadDecisionLevel

(

Msat_Solver_t *

p

)

Definition at line 50 of file msatSolverApi.c.

{ return Msat_IntVecReadSize(p->vTrailLim); }

int* Msat_SolverReadDecisionLevelArray

(

Msat_Solver_t *

p

)

Definition at line 51 of file msatSolverApi.c.

{ return p->pLevel;     }

Msat_ClauseVec_t* Msat_SolverReadLearned

(

Msat_Solver_t *

p

)

Definition at line 54 of file msatSolverApi.c.

{ return p->vLearned;   }

Msat_MmStep_t* Msat_SolverReadMem

(

Msat_Solver_t *

p

)

Definition at line 60 of file msatSolverApi.c.

{ return p->pMem;       }

Msat_Clause_t** Msat_SolverReadReasonArray

(

Msat_Solver_t *

p

)

Definition at line 52 of file msatSolverApi.c.

{ return p->pReasons;   }

int* Msat_SolverReadSeenArray

(

Msat_Solver_t *

p

)

Definition at line 61 of file msatSolverApi.c.

{ return p->pSeen;      }

Msat_Type_t Msat_SolverReadVarValue	(	Msat_Solver_t *	p,
		Msat_Var_t	Var
	)

Definition at line 53 of file msatSolverApi.c.

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

Msat_ClauseVec_t** Msat_SolverReadWatchedArray

(

Msat_Solver_t *

p

)

Definition at line 55 of file msatSolverApi.c.

{ return p->pvWatched;  }

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

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

void Msat_SolverSortDB

(

Msat_Solver_t *

p

)

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]) );
    }
*/
}

void Msat_SolverVarBumpActivity	(	Msat_Solver_t *	p,
		Msat_Lit_t	Lit
	)

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

void Msat_SolverVarDecayActivity

(

Msat_Solver_t *

p

)

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

void Msat_SolverVarRescaleActivity

(

Msat_Solver_t *

p

)

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