msat.h File Reference

Go to the source code of this file.

Macros
#define	MSAT_VAR2LIT(v, s)   (2*(v)+(s))
#define	MSAT_LITNOT(l)   ((l)^1)
#define	MSAT_LITSIGN(l)   ((l)&1)
#define	MSAT_LIT2VAR(l)   ((l)>>1)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_	Msat_Solver_t
	INCLUDES ///. More...
typedef struct Msat_IntVec_t_	Msat_IntVec_t
typedef struct Msat_ClauseVec_t_	Msat_ClauseVec_t
typedef struct Msat_VarHeap_t_	Msat_VarHeap_t

Enumerations
enum	Msat_Type_t { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 }

Functions
int	Msat_SolverParseDimacs (FILE *pFile, Msat_Solver_t **p, int fVerbose)
	GLOBAL VARIABLES ///. More...
int	Msat_SolverAddVar (Msat_Solver_t *p, int Level)
	DECLARATIONS ///. More...
int	Msat_SolverAddClause (Msat_Solver_t *p, Msat_IntVec_t *pLits)
int	Msat_SolverSimplifyDB (Msat_Solver_t *p)
int	Msat_SolverSolve (Msat_Solver_t *p, Msat_IntVec_t *pVecAssumps, int nBackTrackLimit, int nTimeLimit)
void	Msat_SolverPrintStats (Msat_Solver_t *p)
void	Msat_SolverPrintAssignment (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///. More...
void	Msat_SolverPrintClauses (Msat_Solver_t *p)
void	Msat_SolverWriteDimacs (Msat_Solver_t *p, char *pFileName)
int	Msat_SolverReadVarNum (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///. More...
int	Msat_SolverReadClauseNum (Msat_Solver_t *p)
int	Msat_SolverReadVarAllocNum (Msat_Solver_t *p)
int *	Msat_SolverReadAssignsArray (Msat_Solver_t *p)
int *	Msat_SolverReadModelArray (Msat_Solver_t *p)
unsigned	Msat_SolverReadTruth (Msat_Solver_t *p)
int	Msat_SolverReadBackTracks (Msat_Solver_t *p)
int	Msat_SolverReadInspects (Msat_Solver_t *p)
void	Msat_SolverSetVerbosity (Msat_Solver_t *p, int fVerbose)
void	Msat_SolverSetProofWriting (Msat_Solver_t *p, int fProof)
void	Msat_SolverSetVarTypeA (Msat_Solver_t *p, int Var)
void	Msat_SolverSetVarMap (Msat_Solver_t *p, Msat_IntVec_t *vVarMap)
void	Msat_SolverMarkLastClauseTypeA (Msat_Solver_t *p)
void	Msat_SolverMarkClausesStart (Msat_Solver_t *p)
float *	Msat_SolverReadFactors (Msat_Solver_t *p)
int	Msat_SolverReadSolutions (Msat_Solver_t *p)
int *	Msat_SolverReadSolutionsArray (Msat_Solver_t *p)
Msat_ClauseVec_t *	Msat_SolverReadAdjacents (Msat_Solver_t *p)
Msat_IntVec_t *	Msat_SolverReadConeVars (Msat_Solver_t *p)
Msat_IntVec_t *	Msat_SolverReadVarsUsed (Msat_Solver_t *p)
void	Msat_SolverRemoveLearned (Msat_Solver_t *p)
void	Msat_SolverRemoveMarked (Msat_Solver_t *p)
Msat_Solver_t *	Msat_SolverAlloc (int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose)
void	Msat_SolverResize (Msat_Solver_t *pMan, int nVarsAlloc)
void	Msat_SolverClean (Msat_Solver_t *p, int nVars)
void	Msat_SolverPrepare (Msat_Solver_t *pSat, Msat_IntVec_t *vVars)
void	Msat_SolverFree (Msat_Solver_t *p)
Msat_IntVec_t *	Msat_IntVecAlloc (int nCap)
	FUNCTION DEFINITIONS ///. More...
Msat_IntVec_t *	Msat_IntVecAllocArray (int *pArray, int nSize)
Msat_IntVec_t *	Msat_IntVecAllocArrayCopy (int *pArray, int nSize)
Msat_IntVec_t *	Msat_IntVecDup (Msat_IntVec_t *pVec)
Msat_IntVec_t *	Msat_IntVecDupArray (Msat_IntVec_t *pVec)
void	Msat_IntVecFree (Msat_IntVec_t *p)
void	Msat_IntVecFill (Msat_IntVec_t *p, int nSize, int Entry)
int *	Msat_IntVecReleaseArray (Msat_IntVec_t *p)
int *	Msat_IntVecReadArray (Msat_IntVec_t *p)
int	Msat_IntVecReadSize (Msat_IntVec_t *p)
int	Msat_IntVecReadEntry (Msat_IntVec_t *p, int i)
int	Msat_IntVecReadEntryLast (Msat_IntVec_t *p)
void	Msat_IntVecWriteEntry (Msat_IntVec_t *p, int i, int Entry)
void	Msat_IntVecGrow (Msat_IntVec_t *p, int nCapMin)
void	Msat_IntVecShrink (Msat_IntVec_t *p, int nSizeNew)
void	Msat_IntVecClear (Msat_IntVec_t *p)
void	Msat_IntVecPush (Msat_IntVec_t *p, int Entry)
int	Msat_IntVecPushUnique (Msat_IntVec_t *p, int Entry)
void	Msat_IntVecPushUniqueOrder (Msat_IntVec_t *p, int Entry, int fIncrease)
int	Msat_IntVecPop (Msat_IntVec_t *p)
void	Msat_IntVecSort (Msat_IntVec_t *p, int fReverse)
Msat_VarHeap_t *	Msat_VarHeapAlloc ()
void	Msat_VarHeapSetActivity (Msat_VarHeap_t *p, double *pActivity)
void	Msat_VarHeapStart (Msat_VarHeap_t *p, int *pVars, int nVars, int nVarsAlloc)
void	Msat_VarHeapGrow (Msat_VarHeap_t *p, int nSize)
void	Msat_VarHeapStop (Msat_VarHeap_t *p)
void	Msat_VarHeapPrint (FILE *pFile, Msat_VarHeap_t *p)
void	Msat_VarHeapCheck (Msat_VarHeap_t *p)
void	Msat_VarHeapCheckOne (Msat_VarHeap_t *p, int iVar)
int	Msat_VarHeapContainsVar (Msat_VarHeap_t *p, int iVar)
void	Msat_VarHeapInsert (Msat_VarHeap_t *p, int iVar)
void	Msat_VarHeapUpdate (Msat_VarHeap_t *p, int iVar)
void	Msat_VarHeapDelete (Msat_VarHeap_t *p, int iVar)
double	Msat_VarHeapReadMaxWeight (Msat_VarHeap_t *p)
int	Msat_VarHeapCountNodes (Msat_VarHeap_t *p, double WeightLimit)
int	Msat_VarHeapReadMax (Msat_VarHeap_t *p)
int	Msat_VarHeapGetMax (Msat_VarHeap_t *p)

Macro Definition Documentation

#define MSAT_LIT2VAR

(

l

)

((l)>>1)

Definition at line 59 of file msat.h.

#define MSAT_LITNOT

(

l

)

((l)^1)

Definition at line 57 of file msat.h.

#define MSAT_LITSIGN

(

l

)

((l)&1)

Definition at line 58 of file msat.h.

#define MSAT_VAR2LIT	(		v,
			s
	)		(2*(v)+(s))

Definition at line 56 of file msat.h.

Typedef Documentation

typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t

Definition at line 46 of file msat.h.

typedef struct Msat_IntVec_t_ Msat_IntVec_t

Definition at line 45 of file msat.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t

INCLUDES ///.

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

FileName [msat.h]

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 [External 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:

msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp

]PARAMETERS ///STRUCTURE DEFINITIONS ///

Definition at line 42 of file msat.h.

typedef struct Msat_VarHeap_t_ Msat_VarHeap_t

Definition at line 47 of file msat.h.

Enumeration Type Documentation

enum Msat_Type_t

Enumerator
MSAT_FALSE
MSAT_UNKNOWN
MSAT_TRUE

Definition at line 50 of file msat.h.

{ MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;

Function Documentation

Msat_IntVec_t* Msat_IntVecAlloc

(

int

nCap

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file msatVec.c.

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

Msat_IntVec_t* Msat_IntVecAllocArray	(	int *	pArray,
		int	nSize
	)

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

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file msatVec.c.

{
    Msat_IntVec_t * p;
    p = ABC_ALLOC( Msat_IntVec_t, 1 );
    p->nSize  = nSize;
    p->nCap   = nSize;
    p->pArray = pArray;
    return p;
}

Msat_IntVec_t* Msat_IntVecAllocArrayCopy	(	int *	pArray,
		int	nSize
	)

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

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file msatVec.c.

{
    Msat_IntVec_t * p;
    p = ABC_ALLOC( Msat_IntVec_t, 1 );
    p->nSize  = nSize;
    p->nCap   = nSize;
    p->pArray = ABC_ALLOC( int, nSize );
    memcpy( p->pArray, pArray, sizeof(int) * nSize );
    return p;
}

void Msat_IntVecClear

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file msatVec.c.

{
    p->nSize = 0;
}

Msat_IntVec_t* Msat_IntVecDup

(

Msat_IntVec_t *

pVec

)

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

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file msatVec.c.

{
    Msat_IntVec_t * p;
    p = ABC_ALLOC( Msat_IntVec_t, 1 );
    p->nSize  = pVec->nSize;
    p->nCap   = pVec->nCap;
    p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
    return p;
}

Msat_IntVec_t* Msat_IntVecDupArray

(

Msat_IntVec_t *

pVec

)

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

Synopsis [Transfers the array into another vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatVec.c.

{
    Msat_IntVec_t * p;
    p = ABC_ALLOC( Msat_IntVec_t, 1 );
    p->nSize  = pVec->nSize;
    p->nCap   = pVec->nCap;
    p->pArray = pVec->pArray;
    pVec->nSize  = 0;
    pVec->nCap   = 0;
    pVec->pArray = NULL;
    return p;
}

void Msat_IntVecFill	(	Msat_IntVec_t *	p,
		int	nSize,
		int	Entry
	)

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

Synopsis [Fills the vector with given number of entries.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file msatVec.c.

{
    int i;
    Msat_IntVecGrow( p, nSize );
    p->nSize = nSize;
    for ( i = 0; i < p->nSize; i++ )
        p->pArray[i] = Entry;
}

void Msat_IntVecFree

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file msatVec.c.

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

void Msat_IntVecGrow	(	Msat_IntVec_t *	p,
		int	nCapMin
	)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file msatVec.c.

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

int Msat_IntVecPop

(

Msat_IntVec_t *

p

)

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

Synopsis [Returns the last entry and removes it from the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file msatVec.c.

{
    assert( p->nSize > 0 );
    return p->pArray[--p->nSize];
}

void Msat_IntVecPush	(	Msat_IntVec_t *	p,
		int	Entry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file msatVec.c.

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

int Msat_IntVecPushUnique	(	Msat_IntVec_t *	p,
		int	Entry
	)

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

Synopsis [Add the element while ensuring uniqueness.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 374 of file msatVec.c.

{
    int i;
    for ( i = 0; i < p->nSize; i++ )
        if ( p->pArray[i] == Entry )
            return 1;
    Msat_IntVecPush( p, Entry );
    return 0;
}

void Msat_IntVecPushUniqueOrder	(	Msat_IntVec_t *	p,
		int	Entry,
		int	fIncrease
	)

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

Synopsis [Inserts the element while sorting in the increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 395 of file msatVec.c.

{
    int Entry1, Entry2;
    int i;
    Msat_IntVecPushUnique( p, Entry );
    // find the p of the node
    for ( i = p->nSize-1; i > 0; i-- )
    {
        Entry1 = p->pArray[i  ];
        Entry2 = p->pArray[i-1];
        if (( fIncrease && Entry1 >= Entry2) ||
            (!fIncrease && Entry1 <= Entry2) )
            break;
        p->pArray[i  ] = Entry2;
        p->pArray[i-1] = Entry1;
    }
}

int* Msat_IntVecReadArray

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file msatVec.c.

{
    return p->pArray;
}

int Msat_IntVecReadEntry	(	Msat_IntVec_t *	p,
		int	i
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file msatVec.c.

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

int Msat_IntVecReadEntryLast

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file msatVec.c.

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

int Msat_IntVecReadSize

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file msatVec.c.

{
    return p->nSize;
}

int* Msat_IntVecReleaseArray

(

Msat_IntVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file msatVec.c.

{
    int * pArray = p->pArray;
    p->nCap = 0;
    p->nSize = 0;
    p->pArray = NULL;
    return pArray;
}

void Msat_IntVecShrink	(	Msat_IntVec_t *	p,
		int	nSizeNew
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file msatVec.c.

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

void Msat_IntVecSort	(	Msat_IntVec_t *	p,
		int	fReverse
	)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file msatVec.c.

{
    if ( fReverse ) 
        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
                (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
    else
        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
                (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
}

void Msat_IntVecWriteEntry	(	Msat_IntVec_t *	p,
		int	i,
		int	Entry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file msatVec.c.

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

int Msat_SolverAddClause	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vLits
	)

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

Synopsis [Adds one clause to the solver's clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file msatSolverCore.c.

{
    Msat_Clause_t * pC; 
    int  Value;
    Value = Msat_ClauseCreate( p, vLits, 0, &pC );
    if ( pC != NULL )
        Msat_ClauseVecPush( p->vClauses, pC );
//    else if ( p->fProof )
//        Msat_ClauseCreateFake( p, vLits );
    return Value;
}

int Msat_SolverAddVar	(	Msat_Solver_t *	p,
		int	Level
	)

DECLARATIONS ///.

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

FileName [msatSolverCore.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 [The SAT solver core procedures.]

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:

msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp

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

Synopsis [Adds one variable to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatSolverCore.c.

{
    if ( p->nVars == p->nVarsAlloc )
        Msat_SolverResize( p, 2 * p->nVarsAlloc );
    p->pLevel[p->nVars] = Level;
    p->nVars++;
    return 1;
}

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

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

Synopsis [Allocates the solver.]

Description [After the solver is allocated, the procedure Msat_SolverClean() should be called to set the number of variables.]

SideEffects []

SeeAlso []

Definition at line 154 of file msatSolverApi.c.

{
    Msat_Solver_t * p;
    int i;

    assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
    assert(sizeof(float)     == sizeof(unsigned));

    p = ABC_ALLOC( Msat_Solver_t, 1 );
    memset( p, 0, sizeof(Msat_Solver_t) );

    p->nVarsAlloc = nVarsAlloc;
    p->nVars     = 0;

    p->nClauses  = 0;
    p->vClauses  = Msat_ClauseVecAlloc( 512 );
    p->vLearned  = Msat_ClauseVecAlloc( 512 );

    p->dClaInc   = dClaInc;
    p->dClaDecay = dClaDecay;
    p->dVarInc   = dVarInc;
    p->dVarDecay = dVarDecay;

    p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc );
    p->pFactors   = ABC_ALLOC( float, p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
    {
        p->pdActivity[i] = 0.0;
        p->pFactors[i]   = 1.0;
    }

    p->pAssigns  = ABC_ALLOC( int, p->nVarsAlloc ); 
    p->pModel    = ABC_ALLOC( int, p->nVarsAlloc ); 
    for ( i = 0; i < p->nVarsAlloc; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
//    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
    p->pOrder    = Msat_OrderAlloc( p );

    p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );

    p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
    p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
    p->pReasons  = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
    p->pLevel = ABC_ALLOC( int, p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
        p->pLevel[i] = -1;
    p->dRandSeed = 91648253;
    p->fVerbose  = fVerbose;
    p->dProgress = 0.0;
//    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
    p->pMem = Msat_MmStepStart( 10 );

    p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
    p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
    p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );


    p->pSeen     = ABC_ALLOC( int, p->nVarsAlloc );
    memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
    p->nSeenId   = 1;
    p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
    p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
    return p;
}

void Msat_SolverClean	(	Msat_Solver_t *	p,
		int	nVars
	)

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

Synopsis [Prepares the solver.]

Description [Cleans the solver assuming that the problem will involve the given number of variables (nVars). This procedure is useful for many small (incremental) SAT problems, to prevent the solver from being reallocated each time.]

SideEffects []

SeeAlso []

Definition at line 307 of file msatSolverApi.c.

{
    int i;
    // free the clauses
    int nClauses;
    Msat_Clause_t ** pClauses;

    assert( p->nVarsAlloc >= nVars );
    p->nVars    = nVars;
    p->nClauses = 0;

    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
//    Msat_ClauseVecFree( p->vClauses );
    Msat_ClauseVecClear( p->vClauses );

    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
//    Msat_ClauseVecFree( p->vLearned );
    Msat_ClauseVecClear( p->vLearned );

//    ABC_FREE( p->pdActivity );
    for ( i = 0; i < p->nVars; i++ )
        p->pdActivity[i] = 0;

//    Msat_OrderFree( p->pOrder );
//    Msat_OrderClean( p->pOrder, p->nVars, NULL );
    Msat_OrderSetBounds( p->pOrder, p->nVars );

    for ( i = 0; i < 2 * p->nVars; i++ )
//        Msat_ClauseVecFree( p->pvWatched[i] );
        Msat_ClauseVecClear( p->pvWatched[i] );
//    ABC_FREE( p->pvWatched );
//    Msat_QueueFree( p->pQueue );
    Msat_QueueClear( p->pQueue );

//    ABC_FREE( p->pAssigns );
    for ( i = 0; i < p->nVars; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
//    Msat_IntVecFree( p->vTrail );
    Msat_IntVecClear( p->vTrail );
//    Msat_IntVecFree( p->vTrailLim );
    Msat_IntVecClear( p->vTrailLim );
//    ABC_FREE( p->pReasons );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
//    ABC_FREE( p->pLevel );
    for ( i = 0; i < p->nVars; i++ )
        p->pLevel[i] = -1;
//    Msat_IntVecFree( p->pModel );
//    Msat_MmStepStop( p->pMem, 0 );
    p->dRandSeed = 91648253;
    p->dProgress = 0.0;

//    ABC_FREE( p->pSeen );
    memset( p->pSeen, 0, sizeof(int) * p->nVars );
    p->nSeenId = 1;
//    Msat_IntVecFree( p->vReason );
    Msat_IntVecClear( p->vReason );
//    Msat_IntVecFree( p->vTemp );
    Msat_IntVecClear( p->vTemp );
//    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
//    ABC_FREE( p );
}

void Msat_SolverFree

(

Msat_Solver_t *

p

)

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

Synopsis [Frees the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file msatSolverApi.c.

{
    int i;

    // free the clauses
    int nClauses;
    Msat_Clause_t ** pClauses;
//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
//                                         Msat_ClauseVecReadSize( p->vLearned ) );

    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
    Msat_ClauseVecFree( p->vClauses );

    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
    Msat_ClauseVecFree( p->vLearned );

    ABC_FREE( p->pdActivity );
    ABC_FREE( p->pFactors );
    Msat_OrderFree( p->pOrder );

    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
        Msat_ClauseVecFree( p->pvWatched[i] );
    ABC_FREE( p->pvWatched );
    Msat_QueueFree( p->pQueue );

    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pModel );
    Msat_IntVecFree( p->vTrail );
    Msat_IntVecFree( p->vTrailLim );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pLevel );

    Msat_MmStepStop( p->pMem, 0 );

    nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
    pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
    for ( i = 0; i < nClauses; i++ )
        Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
    Msat_ClauseVecFree( p->vAdjacents );
    Msat_IntVecFree( p->vConeVars );
    Msat_IntVecFree( p->vVarsUsed );

    ABC_FREE( p->pSeen );
    Msat_IntVecFree( p->vReason );
    Msat_IntVecFree( p->vTemp );
    ABC_FREE( p );
}

void Msat_SolverMarkClausesStart

(

Msat_Solver_t *

p

)

Definition at line 69 of file msatSolverApi.c.

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

void Msat_SolverMarkLastClauseTypeA

(

Msat_Solver_t *

p

)

Definition at line 68 of file msatSolverApi.c.

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

int Msat_SolverParseDimacs	(	FILE *	pFile,
		Msat_Solver_t **	p,
		int	fVerbose
	)

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///FUNCTION DECLARATIONS ///

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

Synopsis [Starts the solver and reads the DIMAC file.]

Description [Returns FALSE upon immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 258 of file msatRead.c.

{
    char * pText;
    int  Value;
    pText = Msat_FileRead( pFile );
    Value = Msat_ReadDimacs( pText, p, fVerbose );
    ABC_FREE( pText );
    return Value;
}

void Msat_SolverPrepare	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vVars
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file msatSolverApi.c.

{

    int i;
    // undo the previous data
    for ( i = 0; i < p->nVarsAlloc; i++ )
    {
        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
        p->pReasons[i]   = NULL;
        p->pLevel[i]     = -1;
        p->pdActivity[i] = 0.0;
    }

    // set the new variable order
    Msat_OrderClean( p->pOrder, vVars );

    Msat_QueueClear( p->pQueue );
    Msat_IntVecClear( p->vTrail );
    Msat_IntVecClear( p->vTrailLim );
    p->dProgress = 0.0;
}

void Msat_SolverPrintAssignment

(

Msat_Solver_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatSolverIo.c.

{
    int i;
    printf( "Current assignments are: \n" );
    for ( i = 0; i < p->nVars; i++ )
        printf( "%d", i % 10 );
    printf( "\n" );
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
            printf( "." );
        else
        {
            assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
            if ( MSAT_LITSIGN(p->pAssigns[i]) )
                printf( "0" );
            else 
                printf( "1" );
        }
    printf( "\n" );
}

void Msat_SolverPrintClauses

(

Msat_Solver_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file msatSolverIo.c.

{
    Msat_Clause_t ** pClauses;
    int nClauses, i;

    printf( "Original clauses: \n" );
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
    {
        printf( "%3d: ", i );
        Msat_ClausePrint( pClauses[i] );
    }

    printf( "Learned clauses: \n" );
    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
    {
        printf( "%3d: ", i );
        Msat_ClausePrint( pClauses[i] );
    }

    printf( "Variable activity: \n" );
    for ( i = 0; i < p->nVars; i++ )
        printf( "%3d : %.4f\n", i, p->pdActivity[i] );
}

void Msat_SolverPrintStats

(

Msat_Solver_t *

p

)

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

Synopsis [Prints statistics about the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file msatSolverCore.c.

{
    printf("C solver (%d vars; %d clauses; %d learned):\n", 
        p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
    printf("starts        : %d\n", (int)p->Stats.nStarts);
    printf("conflicts     : %d\n", (int)p->Stats.nConflicts);
    printf("decisions     : %d\n", (int)p->Stats.nDecisions);
    printf("propagations  : %d\n", (int)p->Stats.nPropagations);
    printf("inspects      : %d\n", (int)p->Stats.nInspects);
}

Msat_ClauseVec_t* Msat_SolverReadAdjacents

(

Msat_Solver_t *

p

)

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file msatSolverApi.c.

{
    return p->vAdjacents;
}

int* Msat_SolverReadAssignsArray

(

Msat_Solver_t *

p

)

Definition at line 56 of file msatSolverApi.c.

{ return p->pAssigns;   }

int Msat_SolverReadBackTracks

(

Msat_Solver_t *

p

)

Definition at line 58 of file msatSolverApi.c.

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

int Msat_SolverReadClauseNum

(

Msat_Solver_t *

p

)

Definition at line 48 of file msatSolverApi.c.

{ return p->nClauses;   }

Msat_IntVec_t* Msat_SolverReadConeVars

(

Msat_Solver_t *

p

)

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file msatSolverApi.c.

{
    return p->vConeVars;
}

float* Msat_SolverReadFactors

(

Msat_Solver_t *

p

)

Definition at line 70 of file msatSolverApi.c.

{ return p->pFactors;   }

int Msat_SolverReadInspects

(

Msat_Solver_t *

p

)

Definition at line 59 of file msatSolverApi.c.

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

int* Msat_SolverReadModelArray

(

Msat_Solver_t *

p

)

Definition at line 57 of file msatSolverApi.c.

{ return p->pModel;     }

int Msat_SolverReadSolutions

(

Msat_Solver_t *

p

)

int* Msat_SolverReadSolutionsArray

(

Msat_Solver_t *

p

)

unsigned Msat_SolverReadTruth

(

Msat_Solver_t *

p

)

int Msat_SolverReadVarAllocNum

(

Msat_Solver_t *

p

)

Definition at line 49 of file msatSolverApi.c.

{ return p->nVarsAlloc; }

int Msat_SolverReadVarNum

(

Msat_Solver_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Simple SAT solver APIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatSolverApi.c.

{ return p->nVars;      }

Msat_IntVec_t* Msat_SolverReadVarsUsed

(

Msat_Solver_t *

p

)

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatSolverApi.c.

{
    return p->vVarsUsed;
}

void Msat_SolverRemoveLearned

(

Msat_Solver_t *

p

)

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

Synopsis [Removes the learned clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file msatSolverSearch.c.

{
    Msat_Clause_t ** pLearned;
    int nLearned, i;

    // discard the learned clauses
    nLearned = Msat_ClauseVecReadSize( p->vLearned );
    pLearned = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nLearned; i++ )
    {
        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
        
        Msat_ClauseFree( p, pLearned[i], 1 );
    }
    Msat_ClauseVecShrink( p->vLearned, 0 );
    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);

    for ( i = 0; i < p->nVarsAlloc; i++ )
        p->pReasons[i] = NULL;
}

void Msat_SolverRemoveMarked

(

Msat_Solver_t *

p

)

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

Synopsis [Removes the recently added clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 403 of file msatSolverSearch.c.

{
    Msat_Clause_t ** pLearned, ** pClauses;
    int nLearned, nClauses, i;

    // discard the learned clauses
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = p->nClausesStart; i < nClauses; i++ )
    {
//        assert( !Msat_ClauseIsLocked( p, pClauses[i]) );
        Msat_ClauseFree( p, pClauses[i], 1 );
    }
    Msat_ClauseVecShrink( p->vClauses, p->nClausesStart );

    // discard the learned clauses
    nLearned = Msat_ClauseVecReadSize( p->vLearned );
    pLearned = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nLearned; i++ )
    {
//        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
        Msat_ClauseFree( p, pLearned[i], 1 );
    }
    Msat_ClauseVecShrink( p->vLearned, 0 );
    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
/*
    // undo the previous data
    for ( i = 0; i < p->nVarsAlloc; i++ )
    {
        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
        p->pReasons[i]   = NULL;
        p->pLevel[i]     = -1;
        p->pdActivity[i] = 0.0;
    }
    Msat_OrderClean( p->pOrder, p->nVars, NULL );
    Msat_QueueClear( p->pQueue );
*/
}

void Msat_SolverResize	(	Msat_Solver_t *	p,
		int	nVarsAlloc
	)

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

Synopsis [Resizes the solver.]

Description [Assumes that the solver contains some clauses, and that it is currently between the calls. Resizes the solver to accomodate more variables.]

SideEffects []

SeeAlso []

Definition at line 242 of file msatSolverApi.c.

{
    int nVarsAllocOld, i;

    nVarsAllocOld = p->nVarsAlloc;
    p->nVarsAlloc = nVarsAlloc;

    p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc );
    p->pFactors   = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
    {
        p->pdActivity[i] = 0.0;
        p->pFactors[i]   = 1.0;
    }

    p->pAssigns  = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc );
    p->pModel    = ABC_REALLOC( int, p->pModel, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;

//    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
    Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );

    p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
    for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );

    Msat_QueueFree( p->pQueue );
    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );

    p->pReasons  = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
    p->pLevel    = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
    {
        p->pReasons[i] = NULL;
        p->pLevel[i] = -1;
    }

    p->pSeen     = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
        p->pSeen[i] = 0;

    Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
    Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );

    // make sure the array of adjucents has room to store the variable numbers
    for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
}

void Msat_SolverSetProofWriting	(	Msat_Solver_t *	p,
		int	fProof
	)

void Msat_SolverSetVarMap	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vVarMap
	)

void Msat_SolverSetVarTypeA	(	Msat_Solver_t *	p,
		int	Var
	)

void Msat_SolverSetVerbosity	(	Msat_Solver_t *	p,
		int	fVerbose
	)

Definition at line 63 of file msatSolverApi.c.

{ p->fVerbose = fVerbose; }

int Msat_SolverSimplifyDB

(

Msat_Solver_t *

p

)

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

Synopsis [Simplifies the data base.]

Description [Simplify all constraints according to the current top-level assigment (redundant constraints may be removed altogether).]

SideEffects []

SeeAlso []

Definition at line 282 of file msatSolverSearch.c.

{
    Msat_ClauseVec_t * vClauses;
    Msat_Clause_t ** pClauses;
    int nClauses, Type, i, j;
    int * pAssigns;
    int Counter;

    assert( Msat_SolverReadDecisionLevel(p) == 0 );
    if ( Msat_SolverPropagate(p) != NULL )
        return 0;
//Msat_SolverPrintClauses( p );
//Msat_SolverPrintAssignment( p );
//printf( "Simplification\n" );

    // simplify and reassign clause numbers
    Counter = 0;
    pAssigns = Msat_SolverReadAssignsArray( p );
    for ( Type = 0; Type < 2; Type++ )
    {
        vClauses = Type? p->vLearned : p->vClauses;
        nClauses = Msat_ClauseVecReadSize( vClauses );
        pClauses = Msat_ClauseVecReadArray( vClauses );
        for ( i = j = 0; i < nClauses; i++ )
            if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) )
                Msat_ClauseFree( p, pClauses[i], 1 );
            else
            {
                pClauses[j++] = pClauses[i];
                Msat_ClauseSetNum( pClauses[i], Counter++ );
            }
        Msat_ClauseVecShrink( vClauses, j );
    }
    p->nClauses = Counter;
    return 1;
}

int Msat_SolverSolve	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vAssumps,
		int	nBackTrackLimit,
		int	nTimeLimit
	)

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

Synopsis [Top-level solve.]

Description [If using assumptions (non-empty 'assumps' vector), you must call 'simplifyDB()' first to see that no top-level conflict is present (which would put the solver in an undefined state. If the last argument is given (vProj), the solver enumerates through the satisfying solutions, which are projected on the variables listed in this array. Note that the variables in the array may be complemented, in which case the derived assignment for the variable is complemented.]

SideEffects []

SeeAlso []

Definition at line 138 of file msatSolverCore.c.

{
    Msat_SearchParams_t Params = { 0.95, 0.999 };
    double nConflictsLimit, nLearnedLimit;
    Msat_Type_t Status;
    abctime timeStart = Abc_Clock();

//    p->pFreq = ABC_ALLOC( int, p->nVarsAlloc );
//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
 
    if ( vAssumps )
    {
        int * pAssumps, nAssumps, i;

        assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );

        nAssumps = Msat_IntVecReadSize( vAssumps );
        pAssumps = Msat_IntVecReadArray( vAssumps );
        for ( i = 0; i < nAssumps; i++ )
        {
            if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
            {
                Msat_QueueClear( p->pQueue );
                Msat_SolverCancelUntil( p, 0 );
                return MSAT_FALSE;
            }
        }
    }
    p->nLevelRoot   = Msat_SolverReadDecisionLevel(p);
    p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );    
    nConflictsLimit = 100;
    nLearnedLimit   = Msat_ClauseVecReadSize(p->vClauses) / 3;
    Status = MSAT_UNKNOWN;
    p->nBackTracks = (int)p->Stats.nConflicts;
    while ( Status == MSAT_UNKNOWN )
    {
        if ( p->fVerbose )
            printf("Solving -- conflicts=%d   learnts=%d   progress=%.4f %%\n", 
                (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
        Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
        nConflictsLimit *= 1.5;
        nLearnedLimit   *= 1.1;
        // if the limit on the number of backtracks is given, quit the restart loop
        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
            break;
        // if the runtime limit is exceeded, quit the restart loop
        if ( nTimeLimit > 0 && Abc_Clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
            break;
    }
    Msat_SolverCancelUntil( p, 0 );
    p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
/*
    ABC_PRT( "True solver runtime", Abc_Clock() - timeStart );
    // print the statistics
    {
        int i, Counter = 0;
        for ( i = 0; i < p->nVars; i++ )
            if ( p->pFreq[i] > 0 )
            {
                printf( "%d ", p->pFreq[i] );
                Counter++;
            }
        if ( Counter )
            printf( "\n" );
        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
        ABC_PRT( "Time", Abc_Clock() - timeStart );
    }
*/
    return Status;
}

void Msat_SolverWriteDimacs	(	Msat_Solver_t *	p,
		char *	pFileName
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file msatSolverIo.c.

{
    FILE * pFile;
    Msat_Clause_t ** pClauses;
    int nClauses, i;

    nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
    for ( i = 0; i < p->nVars; i++ )
        nClauses += ( p->pLevel[i] == 0 );

    pFile = fopen( pFileName, "wb" );
    fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
    fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );

    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );

    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );

    // write zero-level assertions
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pLevel[i] == 0 )
            fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );

    fprintf( pFile, "\n" );
    fclose( pFile );
}

Msat_VarHeap_t* Msat_VarHeapAlloc

(

)

void Msat_VarHeapCheck

(

Msat_VarHeap_t *

p

)

void Msat_VarHeapCheckOne	(	Msat_VarHeap_t *	p,
		int	iVar
	)

int Msat_VarHeapContainsVar	(	Msat_VarHeap_t *	p,
		int	iVar
	)

int Msat_VarHeapCountNodes	(	Msat_VarHeap_t *	p,
		double	WeightLimit
	)

void Msat_VarHeapDelete	(	Msat_VarHeap_t *	p,
		int	iVar
	)

int Msat_VarHeapGetMax

(

Msat_VarHeap_t *

p

)

void Msat_VarHeapGrow	(	Msat_VarHeap_t *	p,
		int	nSize
	)

void Msat_VarHeapInsert	(	Msat_VarHeap_t *	p,
		int	iVar
	)

void Msat_VarHeapPrint	(	FILE *	pFile,
		Msat_VarHeap_t *	p
	)

int Msat_VarHeapReadMax

(

Msat_VarHeap_t *

p

)

double Msat_VarHeapReadMaxWeight

(

Msat_VarHeap_t *

p

)

void Msat_VarHeapSetActivity	(	Msat_VarHeap_t *	p,
		double *	pActivity
	)

void Msat_VarHeapStart	(	Msat_VarHeap_t *	p,
		int *	pVars,
		int	nVars,
		int	nVarsAlloc
	)

void Msat_VarHeapStop

(

Msat_VarHeap_t *

p

)

void Msat_VarHeapUpdate	(	Msat_VarHeap_t *	p,
		int	iVar
	)