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

Macros
#define	MSAT_VAR2LIT(v, s)

#define	MSAT_LITNOT(l)

#define	MSAT_LITSIGN(l)

#define	MSAT_LIT2VAR(l)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_	Msat_Solver_t
	INCLUDES ///.

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 ///.

int	Msat_SolverAddVar (Msat_Solver_t *p, int Level)
	DECLARATIONS ///.

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 ///.

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 ///.

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 ///.

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

◆ MSAT_LIT2VAR

#define MSAT_LIT2VAR ( l )

Value:

((l)>>1)

Definition at line 59 of file msat.h.

◆ MSAT_LITNOT

#define MSAT_LITNOT ( l )

Value:

((l)^1)

Definition at line 57 of file msat.h.

◆ MSAT_LITSIGN

#define MSAT_LITSIGN ( l )

Value:

((l)&1)

Definition at line 58 of file msat.h.

◆ MSAT_VAR2LIT

#define MSAT_VAR2LIT	(		v,
			s )

Value:

(2*(v)+(s))

Definition at line 56 of file msat.h.

Typedef Documentation

◆ Msat_ClauseVec_t

typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t

Definition at line 46 of file msat.h.

◆ Msat_IntVec_t

typedef struct Msat_IntVec_t_ Msat_IntVec_t

Definition at line 45 of file msat.h.

◆ Msat_Solver_t

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.

◆ Msat_VarHeap_t

typedef struct Msat_VarHeap_t_ Msat_VarHeap_t

Definition at line 47 of file msat.h.

Enumeration Type Documentation

◆ Msat_Type_t

enum Msat_Type_t

Enumerator
MSAT_FALSE
MSAT_UNKNOWN
MSAT_TRUE

Definition at line 50 of file msat.h.

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

Msat_Type_t

Definition msat.h:50

MSAT_TRUE

@ MSAT_TRUE

Definition msat.h:50

MSAT_FALSE

@ MSAT_FALSE

Definition msat.h:50

MSAT_UNKNOWN

@ MSAT_UNKNOWN

Definition msat.h:50

Function Documentation

◆ Msat_IntVecAlloc()

Msat_IntVec_t * Msat_IntVecAlloc ( int nCap )

extern

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

Here is the caller graph for this function:

◆ Msat_IntVecAllocArray()

Msat_IntVec_t * Msat_IntVecAllocArray	(	int *	pArray,
		int	nSize )

extern

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

Msat_IntVec_t * Msat_IntVecAllocArrayCopy	(	int *	pArray,
		int	nSize )

extern

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

Here is the call graph for this function:

◆ Msat_IntVecClear()

void Msat_IntVecClear ( Msat_IntVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file msatVec.c.

{
    p->nSize = 0;
}

Here is the caller graph for this function:

◆ Msat_IntVecDup()

Msat_IntVec_t * Msat_IntVecDup ( Msat_IntVec_t * pVec )

extern

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

Here is the call graph for this function:

◆ Msat_IntVecDupArray()

Msat_IntVec_t * Msat_IntVecDupArray ( Msat_IntVec_t * pVec )

extern

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

◆ Msat_IntVecFill()

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

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_IntVecFree()

void Msat_IntVecFree ( Msat_IntVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file msatVec.c.

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

Here is the caller graph for this function:

◆ Msat_IntVecGrow()

void Msat_IntVecGrow	(	Msat_IntVec_t *	p,
		int	nCapMin )

extern

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

Here is the caller graph for this function:

◆ Msat_IntVecPop()

int Msat_IntVecPop ( Msat_IntVec_t * p )

extern

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

◆ Msat_IntVecPush()

void Msat_IntVecPush	(	Msat_IntVec_t *	p,
		int	Entry )

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_IntVecPushUnique()

int Msat_IntVecPushUnique	(	Msat_IntVec_t *	p,
		int	Entry )

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_IntVecPushUniqueOrder()

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

extern

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

Here is the call graph for this function:

◆ Msat_IntVecReadArray()

int * Msat_IntVecReadArray ( Msat_IntVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file msatVec.c.

{
    return p->pArray;
}

Here is the caller graph for this function:

◆ Msat_IntVecReadEntry()

int Msat_IntVecReadEntry	(	Msat_IntVec_t *	p,
		int	i )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file msatVec.c.

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

Here is the caller graph for this function:

◆ Msat_IntVecReadEntryLast()

int Msat_IntVecReadEntryLast ( Msat_IntVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file msatVec.c.

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

◆ Msat_IntVecReadSize()

int Msat_IntVecReadSize ( Msat_IntVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file msatVec.c.

{
    return p->nSize;
}

Here is the caller graph for this function:

◆ Msat_IntVecReleaseArray()

int * Msat_IntVecReleaseArray ( Msat_IntVec_t * p )

extern

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

◆ Msat_IntVecShrink()

void Msat_IntVecShrink	(	Msat_IntVec_t *	p,
		int	nSizeNew )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file msatVec.c.

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

Here is the caller graph for this function:

◆ Msat_IntVecSort()

void Msat_IntVecSort	(	Msat_IntVec_t *	p,
		int	fReverse )

extern

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, (size_t)p->nSize, sizeof(int), 
                (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
    else
        qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(int), 
                (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
}

Here is the caller graph for this function:

◆ Msat_IntVecWriteEntry()

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

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file msatVec.c.

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

◆ Msat_SolverAddClause()

int Msat_SolverAddClause	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vLits )

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverAddVar()

int Msat_SolverAddVar	(	Msat_Solver_t *	p,
		int	Level )

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverAlloc()

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

extern

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

Synopsis [Allocates the solver.]

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

SideEffects []

SeeAlso []

Definition at line 154 of file msatSolverApi.c.

{
    Msat_Solver_t * p;
    int i;
 
    assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
    assert(sizeof(float)     == sizeof(unsigned));
 
    p = ABC_ALLOC( Msat_Solver_t, 1 );
    memset( p, 0, sizeof(Msat_Solver_t) );
 
    p->nVarsAlloc = nVarsAlloc;
    p->nVars     = 0;
 
    p->nClauses  = 0;
    p->vClauses  = Msat_ClauseVecAlloc( 512 );
    p->vLearned  = Msat_ClauseVecAlloc( 512 );
 
    p->dClaInc   = dClaInc;
    p->dClaDecay = dClaDecay;
    p->dVarInc   = dVarInc;
    p->dVarDecay = dVarDecay;
 
    p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc );
    p->pFactors   = ABC_ALLOC( float, p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
    {
        p->pdActivity[i] = 0.0;
        p->pFactors[i]   = 1.0;
    }
 
    p->pAssigns  = ABC_ALLOC( int, p->nVarsAlloc ); 
    p->pModel    = ABC_ALLOC( int, p->nVarsAlloc ); 
    for ( i = 0; i < p->nVarsAlloc; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
//    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
    p->pOrder    = Msat_OrderAlloc( p );
 
    p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
 
    p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
    p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
    p->pReasons  = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
    p->pLevel = ABC_ALLOC( int, p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
        p->pLevel[i] = -1;
    p->dRandSeed = 91648253;
    p->fVerbose  = fVerbose;
    p->dProgress = 0.0;
//    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
    p->pMem = Msat_MmStepStart( 10 );
 
    p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
    p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
    for ( i = 0; i < p->nVarsAlloc; i++ )
        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
    p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
 
 
    p->pSeen     = ABC_ALLOC( int, p->nVarsAlloc );
    memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
    p->nSeenId   = 1;
    p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
    p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverClean()

void Msat_SolverClean	(	Msat_Solver_t *	p,
		int	nVars )

extern

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

Synopsis [Prepares the solver.]

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

SideEffects []

SeeAlso []

Definition at line 307 of file msatSolverApi.c.

{
    int i;
    // free the clauses
    int nClauses;
    Msat_Clause_t ** pClauses;
 
    assert( p->nVarsAlloc >= nVars );
    p->nVars    = nVars;
    p->nClauses = 0;
 
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
//    Msat_ClauseVecFree( p->vClauses );
    Msat_ClauseVecClear( p->vClauses );
 
    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
//    Msat_ClauseVecFree( p->vLearned );
    Msat_ClauseVecClear( p->vLearned );
 
//    ABC_FREE( p->pdActivity );
    for ( i = 0; i < p->nVars; i++ )
        p->pdActivity[i] = 0;
 
//    Msat_OrderFree( p->pOrder );
//    Msat_OrderClean( p->pOrder, p->nVars, NULL );
    Msat_OrderSetBounds( p->pOrder, p->nVars );
 
    for ( i = 0; i < 2 * p->nVars; i++ )
//        Msat_ClauseVecFree( p->pvWatched[i] );
        Msat_ClauseVecClear( p->pvWatched[i] );
//    ABC_FREE( p->pvWatched );
//    Msat_QueueFree( p->pQueue );
    Msat_QueueClear( p->pQueue );
 
//    ABC_FREE( p->pAssigns );
    for ( i = 0; i < p->nVars; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
//    Msat_IntVecFree( p->vTrail );
    Msat_IntVecClear( p->vTrail );
//    Msat_IntVecFree( p->vTrailLim );
    Msat_IntVecClear( p->vTrailLim );
//    ABC_FREE( p->pReasons );
    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
//    ABC_FREE( p->pLevel );
    for ( i = 0; i < p->nVars; i++ )
        p->pLevel[i] = -1;
//    Msat_IntVecFree( p->pModel );
//    Msat_MmStepStop( p->pMem, 0 );
    p->dRandSeed = 91648253;
    p->dProgress = 0.0;
 
//    ABC_FREE( p->pSeen );
    memset( p->pSeen, 0, sizeof(int) * p->nVars );
    p->nSeenId = 1;
//    Msat_IntVecFree( p->vReason );
    Msat_IntVecClear( p->vReason );
//    Msat_IntVecFree( p->vTemp );
    Msat_IntVecClear( p->vTemp );
//    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
//    ABC_FREE( p );
}

Here is the call graph for this function:

◆ Msat_SolverFree()

void Msat_SolverFree ( Msat_Solver_t * p )

extern

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

Synopsis [Frees the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file msatSolverApi.c.

{
    int i;
 
    // free the clauses
    int nClauses;
    Msat_Clause_t ** pClauses;
//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
//                                         Msat_ClauseVecReadSize( p->vLearned ) );
 
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
    Msat_ClauseVecFree( p->vClauses );
 
    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseFree( p, pClauses[i], 0 );
    Msat_ClauseVecFree( p->vLearned );
 
    ABC_FREE( p->pdActivity );
    ABC_FREE( p->pFactors );
    Msat_OrderFree( p->pOrder );
 
    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
        Msat_ClauseVecFree( p->pvWatched[i] );
    ABC_FREE( p->pvWatched );
    Msat_QueueFree( p->pQueue );
 
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pModel );
    Msat_IntVecFree( p->vTrail );
    Msat_IntVecFree( p->vTrailLim );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pLevel );
 
    Msat_MmStepStop( p->pMem, 0 );
 
    nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
    pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
    for ( i = 0; i < nClauses; i++ )
        Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
    Msat_ClauseVecFree( p->vAdjacents );
    Msat_IntVecFree( p->vConeVars );
    Msat_IntVecFree( p->vVarsUsed );
 
    ABC_FREE( p->pSeen );
    Msat_IntVecFree( p->vReason );
    Msat_IntVecFree( p->vTemp );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverMarkClausesStart()

void Msat_SolverMarkClausesStart ( Msat_Solver_t * p )

extern

Definition at line 69 of file msatSolverApi.c.

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

Here is the call graph for this function:

◆ Msat_SolverMarkLastClauseTypeA()

void Msat_SolverMarkLastClauseTypeA ( Msat_Solver_t * p )

extern

Definition at line 68 of file msatSolverApi.c.

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

Msat_ClauseVecReadEntry

Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)

Definition msatClauseVec.c:225

Msat_ClauseSetTypeA

void Msat_ClauseSetTypeA(Msat_Clause_t *pC, int fTypeA)

Definition msatClause.c:264

Here is the call graph for this function:

◆ Msat_SolverParseDimacs()

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

extern

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

◆ Msat_SolverPrepare()

void Msat_SolverPrepare	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vVars )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file msatSolverApi.c.

{
 
    int i;
    // undo the previous data
    for ( i = 0; i < p->nVarsAlloc; i++ )
    {
        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
        p->pReasons[i]   = NULL;
        p->pLevel[i]     = -1;
        p->pdActivity[i] = 0.0;
    }
 
    // set the new variable order
    Msat_OrderClean( p->pOrder, vVars );
 
    Msat_QueueClear( p->pQueue );
    Msat_IntVecClear( p->vTrail );
    Msat_IntVecClear( p->vTrailLim );
    p->dProgress = 0.0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverPrintAssignment()

void Msat_SolverPrintAssignment ( Msat_Solver_t * p )

extern

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

◆ Msat_SolverPrintClauses()

void Msat_SolverPrintClauses ( Msat_Solver_t * p )

extern

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

Here is the call graph for this function:

◆ Msat_SolverPrintStats()

void Msat_SolverPrintStats ( Msat_Solver_t * p )

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverReadAdjacents()

Msat_ClauseVec_t * Msat_SolverReadAdjacents ( Msat_Solver_t * p )

extern

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file msatSolverApi.c.

{
    return p->vAdjacents;
}

Here is the caller graph for this function:

◆ Msat_SolverReadAssignsArray()

int * Msat_SolverReadAssignsArray ( Msat_Solver_t * p )

extern

Definition at line 56 of file msatSolverApi.c.

56{ return p->pAssigns; }

Here is the caller graph for this function:

◆ Msat_SolverReadBackTracks()

int Msat_SolverReadBackTracks ( Msat_Solver_t * p )

extern

Definition at line 58 of file msatSolverApi.c.

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

Here is the caller graph for this function:

◆ Msat_SolverReadClauseNum()

int Msat_SolverReadClauseNum ( Msat_Solver_t * p )

extern

Definition at line 48 of file msatSolverApi.c.

48{ return p->nClauses; }

◆ Msat_SolverReadConeVars()

Msat_IntVec_t * Msat_SolverReadConeVars ( Msat_Solver_t * p )

extern

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file msatSolverApi.c.

{
    return p->vConeVars;
}

Here is the caller graph for this function:

◆ Msat_SolverReadFactors()

float * Msat_SolverReadFactors ( Msat_Solver_t * p )

extern

Definition at line 70 of file msatSolverApi.c.

70{ return p->pFactors; }

◆ Msat_SolverReadInspects()

int Msat_SolverReadInspects ( Msat_Solver_t * p )

extern

Definition at line 59 of file msatSolverApi.c.

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

Here is the caller graph for this function:

◆ Msat_SolverReadModelArray()

int * Msat_SolverReadModelArray ( Msat_Solver_t * p )

extern

Definition at line 57 of file msatSolverApi.c.

57{ return p->pModel; }

Here is the caller graph for this function:

◆ Msat_SolverReadSolutions()

int Msat_SolverReadSolutions ( Msat_Solver_t * p )

extern

◆ Msat_SolverReadSolutionsArray()

int * Msat_SolverReadSolutionsArray ( Msat_Solver_t * p )

extern

◆ Msat_SolverReadTruth()

unsigned Msat_SolverReadTruth ( Msat_Solver_t * p )

extern

◆ Msat_SolverReadVarAllocNum()

int Msat_SolverReadVarAllocNum ( Msat_Solver_t * p )

extern

Definition at line 49 of file msatSolverApi.c.

49{ return p->nVarsAlloc; }

◆ Msat_SolverReadVarNum()

int Msat_SolverReadVarNum ( Msat_Solver_t * p )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Simple SAT solver APIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatSolverApi.c.

47{ return p->nVars; }

Here is the caller graph for this function:

◆ Msat_SolverReadVarsUsed()

Msat_IntVec_t * Msat_SolverReadVarsUsed ( Msat_Solver_t * p )

extern

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatSolverApi.c.

{
    return p->vVarsUsed;
}

Here is the caller graph for this function:

◆ Msat_SolverRemoveLearned()

void Msat_SolverRemoveLearned ( Msat_Solver_t * p )

extern

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

Here is the call graph for this function:

◆ Msat_SolverRemoveMarked()

void Msat_SolverRemoveMarked ( Msat_Solver_t * p )

extern

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

Here is the call graph for this function:

◆ Msat_SolverResize()

void Msat_SolverResize	(	Msat_Solver_t *	p,
		int	nVarsAlloc )

extern

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

Synopsis [Resizes the solver.]

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

SideEffects []

SeeAlso []

Definition at line 242 of file msatSolverApi.c.

{
    int nVarsAllocOld, i;
 
    nVarsAllocOld = p->nVarsAlloc;
    p->nVarsAlloc = nVarsAlloc;
 
    p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc );
    p->pFactors   = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
    {
        p->pdActivity[i] = 0.0;
        p->pFactors[i]   = 1.0;
    }
 
    p->pAssigns  = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc );
    p->pModel    = ABC_REALLOC( int, p->pModel, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
 
//    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
    Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
 
    p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
    for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
 
    Msat_QueueFree( p->pQueue );
    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
 
    p->pReasons  = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
    p->pLevel    = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
    {
        p->pReasons[i] = NULL;
        p->pLevel[i] = -1;
    }
 
    p->pSeen     = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc );
    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
        p->pSeen[i] = 0;
 
    Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
    Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
 
    // make sure the array of adjucents has room to store the variable numbers
    for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverSetProofWriting()

void Msat_SolverSetProofWriting	(	Msat_Solver_t *	p,
		int	fProof )

extern

◆ Msat_SolverSetVarMap()

void Msat_SolverSetVarMap	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vVarMap )

extern

◆ Msat_SolverSetVarTypeA()

void Msat_SolverSetVarTypeA	(	Msat_Solver_t *	p,
		int	Var )

extern

◆ Msat_SolverSetVerbosity()

void Msat_SolverSetVerbosity	(	Msat_Solver_t *	p,
		int	fVerbose )

extern

Definition at line 63 of file msatSolverApi.c.

63{ p->fVerbose = fVerbose; }

◆ Msat_SolverSimplifyDB()

int Msat_SolverSimplifyDB ( Msat_Solver_t * p )

extern

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

Here is the call graph for this function:

◆ Msat_SolverSolve()

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

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Msat_SolverWriteDimacs()

void Msat_SolverWriteDimacs	(	Msat_Solver_t *	p,
		char *	pFileName )

extern

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

Here is the call graph for this function:

◆ Msat_VarHeapAlloc()

Msat_VarHeap_t * Msat_VarHeapAlloc ( )

extern

◆ Msat_VarHeapCheck()

void Msat_VarHeapCheck ( Msat_VarHeap_t * p )

extern

◆ Msat_VarHeapCheckOne()

void Msat_VarHeapCheckOne	(	Msat_VarHeap_t *	p,
		int	iVar )

extern

◆ Msat_VarHeapContainsVar()

int Msat_VarHeapContainsVar	(	Msat_VarHeap_t *	p,
		int	iVar )

extern

◆ Msat_VarHeapCountNodes()

int Msat_VarHeapCountNodes	(	Msat_VarHeap_t *	p,
		double	WeightLimit )

extern

◆ Msat_VarHeapDelete()

void Msat_VarHeapDelete	(	Msat_VarHeap_t *	p,
		int	iVar )

extern

◆ Msat_VarHeapGetMax()

int Msat_VarHeapGetMax ( Msat_VarHeap_t * p )

extern

◆ Msat_VarHeapGrow()

void Msat_VarHeapGrow	(	Msat_VarHeap_t *	p,
		int	nSize )

extern

◆ Msat_VarHeapInsert()

void Msat_VarHeapInsert	(	Msat_VarHeap_t *	p,
		int	iVar )

extern

◆ Msat_VarHeapPrint()

void Msat_VarHeapPrint	(	FILE *	pFile,
		Msat_VarHeap_t *	p )

extern

◆ Msat_VarHeapReadMax()

int Msat_VarHeapReadMax ( Msat_VarHeap_t * p )

extern

◆ Msat_VarHeapReadMaxWeight()

double Msat_VarHeapReadMaxWeight ( Msat_VarHeap_t * p )

extern

◆ Msat_VarHeapSetActivity()

void Msat_VarHeapSetActivity	(	Msat_VarHeap_t *	p,
		double *	pActivity )

extern

◆ Msat_VarHeapStart()

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

extern

◆ Msat_VarHeapStop()

void Msat_VarHeapStop ( Msat_VarHeap_t * p )

extern

◆ Msat_VarHeapUpdate()

void Msat_VarHeapUpdate	(	Msat_VarHeap_t *	p,
		int	iVar )

extern

Macros

Typedefs

Enumerations

Functions

Macro Definition Documentation

◆ MSAT_LIT2VAR

◆ MSAT_LITNOT

◆ MSAT_LITSIGN

◆ MSAT_VAR2LIT

Typedef Documentation

◆ Msat_ClauseVec_t

◆ Msat_IntVec_t

◆ Msat_Solver_t

◆ Msat_VarHeap_t

Enumeration Type Documentation

◆ Msat_Type_t

Function Documentation

◆ Msat_IntVecAlloc()

◆ Msat_IntVecAllocArray()

◆ Msat_IntVecAllocArrayCopy()

◆ Msat_IntVecClear()

◆ Msat_IntVecDup()

◆ Msat_IntVecDupArray()

◆ Msat_IntVecFill()

◆ Msat_IntVecFree()

◆ Msat_IntVecGrow()

◆ Msat_IntVecPop()

◆ Msat_IntVecPush()

◆ Msat_IntVecPushUnique()

◆ Msat_IntVecPushUniqueOrder()

◆ Msat_IntVecReadArray()

◆ Msat_IntVecReadEntry()

◆ Msat_IntVecReadEntryLast()

◆ Msat_IntVecReadSize()

◆ Msat_IntVecReleaseArray()

◆ Msat_IntVecShrink()

◆ Msat_IntVecSort()

◆ Msat_IntVecWriteEntry()

◆ Msat_SolverAddClause()

◆ Msat_SolverAddVar()

◆ Msat_SolverAlloc()

◆ Msat_SolverClean()

◆ Msat_SolverFree()

◆ Msat_SolverMarkClausesStart()

◆ Msat_SolverMarkLastClauseTypeA()

◆ Msat_SolverParseDimacs()

◆ Msat_SolverPrepare()

◆ Msat_SolverPrintAssignment()

◆ Msat_SolverPrintClauses()

◆ Msat_SolverPrintStats()

◆ Msat_SolverReadAdjacents()

◆ Msat_SolverReadAssignsArray()

◆ Msat_SolverReadBackTracks()

◆ Msat_SolverReadClauseNum()

◆ Msat_SolverReadConeVars()

◆ Msat_SolverReadFactors()

◆ Msat_SolverReadInspects()

◆ Msat_SolverReadModelArray()

◆ Msat_SolverReadSolutions()

◆ Msat_SolverReadSolutionsArray()

◆ Msat_SolverReadTruth()

◆ Msat_SolverReadVarAllocNum()

◆ Msat_SolverReadVarNum()

◆ Msat_SolverReadVarsUsed()

◆ Msat_SolverRemoveLearned()

◆ Msat_SolverRemoveMarked()

◆ Msat_SolverResize()

◆ Msat_SolverSetProofWriting()

◆ Msat_SolverSetVarMap()

◆ Msat_SolverSetVarTypeA()

◆ Msat_SolverSetVerbosity()

◆ Msat_SolverSimplifyDB()

◆ Msat_SolverSolve()

◆ Msat_SolverWriteDimacs()

◆ Msat_VarHeapAlloc()

◆ Msat_VarHeapCheck()

◆ Msat_VarHeapCheckOne()

◆ Msat_VarHeapContainsVar()

◆ Msat_VarHeapCountNodes()

◆ Msat_VarHeapDelete()