msatOrderJ.c File Reference

#include "msatInt.h"

Go to the source code of this file.

Data Structures
struct	Msat_OrderVar_t_
struct	Msat_OrderRing_t_
struct	Msat_Order_t_
	DECLARATIONS ///. More...

Macros
#define	Msat_OrderVarIsInBoundary(p, i)   ((p)->pVars[i].pNext)
#define	Msat_OrderVarIsAssigned(p, i)   ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED)
#define	Msat_OrderVarIsUsedInCone(p, i)   ((p)->pSat->vVarsUsed->pArray[i])
#define	Msat_OrderRingForEachEntry(pRing, pVar, pNext)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Msat_OrderVar_t_	Msat_OrderVar_t
	DECLARATIONS ///. More...
typedef struct Msat_OrderRing_t_	Msat_OrderRing_t

Functions
static void	Msat_OrderRingAddLast (Msat_OrderRing_t *pRing, Msat_OrderVar_t *pVar)
static void	Msat_OrderRingRemove (Msat_OrderRing_t *pRing, Msat_OrderVar_t *pVar)
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)

Variables
clock_t	timeSelect
	DECLARATIONS ///. More...
clock_t	timeAssign

Macro Definition Documentation

#define Msat_OrderRingForEachEntry	(		pRing,
			pVar,
			pNext
	)

Value:

for ( pVar = pRing,                                         \
          pNext = pVar? pVar->pNext : NULL;                     \
          pVar;                                                 \
          pVar = (pNext != pRing)? pNext : NULL,                \
          pNext = pVar? pVar->pNext : NULL )

Definition at line 74 of file msatOrderJ.c.

#define Msat_OrderVarIsAssigned	(		p,
			i
	)		((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED)

Definition at line 70 of file msatOrderJ.c.

#define Msat_OrderVarIsInBoundary	(		p,
			i
	)		((p)->pVars[i].pNext)

Definition at line 69 of file msatOrderJ.c.

#define Msat_OrderVarIsUsedInCone	(		p,
			i
	)		((p)->pSat->vVarsUsed->pArray[i])

Definition at line 71 of file msatOrderJ.c.

Typedef Documentation

typedef struct Msat_OrderRing_t_ Msat_OrderRing_t

Definition at line 37 of file msatOrderJ.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Msat_OrderVar_t_ Msat_OrderVar_t

DECLARATIONS ///.

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

FileName [msatOrder.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 manager of variable assignment.]

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:

msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp

]

Definition at line 36 of file msatOrderJ.c.

Function Documentation

Msat_Order_t* Msat_OrderAlloc

(

Msat_Solver_t *

pSat

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file msatOrderJ.c.

{
    Msat_Order_t * p;
    p = ALLOC( Msat_Order_t, 1 );
    memset( p, 0, sizeof(Msat_Order_t) );
    p->pSat = pSat;
    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 171 of file msatOrderJ.c.

{
    Msat_OrderVar_t * pVar, * pNext;
    Msat_IntVec_t * vRound;
    int * pRound, nRound;
    int * pVars, nVars, i, k;
    int Counter = 0;

    // go through all the variables in the boundary
    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
    {
        assert( !Msat_OrderVarIsAssigned(p, pVar->Num) );
        // go though all the variables in the neighborhood
        // and check that it is true that there is least one assigned
        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num );
        nRound = Msat_IntVecReadSize( vRound );
        pRound = Msat_IntVecReadArray( vRound );
        for ( i = 0; i < nRound; i++ )
        {
            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
                continue;
            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                break;
        }
//        assert( i != nRound );
//        if ( i == nRound )
//            return 0;
        if ( i == nRound )
            Counter++;
    }
    if ( Counter > 0 )
        printf( "%d(%d) ", Counter, p->rVars.nItems );

    // we may also check other unassigned variables in the cone
    // to make sure that if they are not in J-boundary, 
    // then they do not have an assigned neighbor
    nVars = Msat_IntVecReadSize( p->pSat->vConeVars );
    pVars = Msat_IntVecReadArray( p->pSat->vConeVars );
    for ( i = 0; i < nVars; i++ )
    {
        assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) );
        // skip assigned vars, vars in the boundary, and vars not used in the cone
        if ( Msat_OrderVarIsAssigned(p, pVars[i]) || 
             Msat_OrderVarIsInBoundary(p, pVars[i]) )
            continue;
        // make sure, it does not have assigned neighbors
        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
        nRound = Msat_IntVecReadSize( vRound );
        pRound = Msat_IntVecReadArray( vRound );
        for ( k = 0; k < nRound; k++ )
        {
            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
                continue;
            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
                break;
        }
//        assert( k == nRound );
//        if ( k != nRound )
//            return 0;
    }
    return 1;
}

void Msat_OrderClean	(	Msat_Order_t *	p,
		Msat_IntVec_t *	vCone
	)

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

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file msatOrderJ.c.

{
    Msat_OrderVar_t * pVar, * pNext;
    // quickly undo the ring
    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
        pVar->pNext = pVar->pPrev = NULL;
    p->rVars.pRoot  = NULL;
    p->rVars.nItems = 0;
}

void Msat_OrderFree

(

Msat_Order_t *

p

)

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

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file msatOrderJ.c.

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

void Msat_OrderRingAddLast ( Msat_OrderRing_t *  pRing, Msat_OrderVar_t *  pVar  )

static

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

Synopsis [Adds node to the end of the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file msatOrderJ.c.

{
//printf( "adding %d\n", pVar->Num );
    // check that the node is not in a ring
    assert( pVar->pPrev == NULL );
    assert( pVar->pNext == NULL );
    // if the ring is empty, make the node point to itself
    pRing->nItems++;
    if ( pRing->pRoot == NULL )
    {
        pRing->pRoot  = pVar;
        pVar->pPrev  = pVar;
        pVar->pNext  = pVar;
        return;
    }
    // if the ring is not empty, add it as the last entry
    pVar->pPrev = pRing->pRoot->pPrev;
    pVar->pNext = pRing->pRoot;
    pVar->pPrev->pNext = pVar;
    pVar->pNext->pPrev = pVar;

    // move the root so that it points to the new entry
//    pRing->pRoot = pRing->pRoot->pPrev;
}

void Msat_OrderRingRemove ( Msat_OrderRing_t *  pRing, Msat_OrderVar_t *  pVar  )

static

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

Synopsis [Removes the node from the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file msatOrderJ.c.

{
//printf( "removing %d\n", pVar->Num );
    // check that the var is in a ring
    assert( pVar->pPrev );
    assert( pVar->pNext );
    pRing->nItems--;
    if ( pRing->nItems == 0 )
    {
        assert( pRing->pRoot == pVar );
        pVar->pPrev = NULL;
        pVar->pNext = NULL;
        pRing->pRoot = NULL;
        return;
    }
    // move the root if needed
    if ( pRing->pRoot == pVar )
        pRing->pRoot = pVar->pNext;
    // move the root to the next entry after pVar
    // this way all the additions to the list will be traversed first
//    pRing->pRoot = pVar->pPrev;
    // delete the node
    pVar->pPrev->pNext = pVar->pNext;
    pVar->pNext->pPrev = pVar->pPrev;
    pVar->pPrev = NULL;
    pVar->pNext = NULL;
}

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 123 of file msatOrderJ.c.

{
    int i;
    // add variables if they are missing
    if ( p->nVarsAlloc < nVarsMax )
    {
        p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax );
        for ( i = p->nVarsAlloc; i < nVarsMax; i++ )
        {
            p->pVars[i].pNext = p->pVars[i].pPrev = NULL;
            p->pVars[i].Num = i;
        }
        p->nVarsAlloc = nVarsMax;
    }
}

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 390 of file msatOrderJ.c.

{
}

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 305 of file msatOrderJ.c.

{
    Msat_IntVec_t * vRound;
    int i;//, clk = clock();

    // make sure the variable is in the boundary
    assert( Var < p->nVarsAlloc );
    // if it is not in the boundary (initial decision, random decision), do not remove
    if ( Msat_OrderVarIsInBoundary( p, Var ) )
        Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] );
    // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary
    // because for them we know that there is a variable (Var) which is assigned
    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
    for ( i = 0; i < vRound->nSize; i++ )
    {
        if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) )
            continue;
        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) )
            continue;
        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
            continue;
        Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
    }
//timeSelect += clock() - clk;
//    Msat_OrderCheck( p );
}

int Msat_OrderVarSelect

(

Msat_Order_t *

p

)

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

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file msatOrderJ.c.

{
    Msat_OrderVar_t * pVar, * pNext, * pVarBest;
    double * pdActs = p->pSat->pdActivity;
    double dfActBest;
//    clock_t clk = clock();

    pVarBest = NULL;
    dfActBest = -1.0;
    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
    {
        if ( dfActBest < pdActs[pVar->Num] )
        {
            dfActBest = pdActs[pVar->Num];
            pVarBest  = pVar;
        }
    }
//timeSelect += clock() - clk;
//timeAssign += clock() - clk;

//if ( pVarBest && pVarBest->Num % 1000 == 0 )
//printf( "%d ", p->rVars.nItems );

//    Msat_OrderCheck( p );
    if ( pVarBest )
    {
        assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
        return pVarBest->Num;
    }
    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 343 of file msatOrderJ.c.

{
    Msat_IntVec_t * vRound, * vRound2;
    int i, k;//, clk = clock();

    // make sure the variable is not in the boundary
    assert( Var < p->nVarsAlloc );
    assert( !Msat_OrderVarIsInBoundary( p, Var ) );
    // go through its neigbors - if one of them is assigned add this var
    // add to the boundary those neighbors that are not there already
    // this will also get rid of variable outside of the current cone
    // because they are unassigned in Msat_SolverPrepare()
    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
    for ( i = 0; i < vRound->nSize; i++ )
        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) 
            break;
    if ( i != vRound->nSize )
        Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] );

    // unassigning a variable may lead to its adjacents dropping from the boundary
    for ( i = 0; i < vRound->nSize; i++ )
        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
        { // the neighbor is in the J-boundary (and unassigned)
            assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) );
            vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]];
            // go through its neighbors and determine if there is at least one assigned
            for ( k = 0; k < vRound2->nSize; k++ )
                if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) 
                    break;
            if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
                Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
        }
//timeSelect += clock() - clk;
//    Msat_OrderCheck( p );
}

Variable Documentation

clock_t timeAssign

Definition at line 29 of file fraigMan.c.

clock_t timeSelect

DECLARATIONS ///.

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

FileName [fraigMan.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Implementation of the FRAIG manager.]

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. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp

]

Definition at line 28 of file fraigMan.c.