src/sat/msat/msatOrderJ.c File Reference

#include "msatInt.h"
Include dependency graph for msatOrderJ.c:

Go to the source code of this file.

Data Structures

struct  Msat_OrderVar_t_
struct  Msat_OrderRing_t_
struct  Msat_Order_t_

Defines

#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 struct Msat_OrderVar_t_ Msat_OrderVar_t
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)
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

int timeSelect
int timeAssign

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

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

Definition at line 67 of file msatOrderJ.c.

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

Definition at line 66 of file msatOrderJ.c.

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

Definition at line 68 of file msatOrderJ.c.

Typedef Documentation

typedef struct Msat_OrderRing_t_ Msat_OrderRing_t

Definition at line 34 of file msatOrderJ.c.

typedef struct Msat_OrderVar_t_ Msat_OrderVar_t

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 <alanmi@eecs.berkeley.edu>]

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

] DECLARATIONS ///

Definition at line 33 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 99 of file msatOrderJ.c.

00100 {
00101     Msat_Order_t * p;
00102     p = ALLOC( Msat_Order_t, 1 );
00103     memset( p, 0, sizeof(Msat_Order_t) );
00104     p->pSat = pSat;
00105     Msat_OrderSetBounds( p, pSat->nVarsAlloc );
00106     return p;
00107 }

int Msat_OrderCheck ( Msat_Order_t *  p  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file msatOrderJ.c.

00169 {
00170     Msat_OrderVar_t * pVar, * pNext;
00171     Msat_IntVec_t * vRound;
00172     int * pRound, nRound;
00173     int * pVars, nVars, i, k;
00174     int Counter = 0;
00175 
00176     // go through all the variables in the boundary
00177     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
00178     {
00179         assert( !Msat_OrderVarIsAssigned(p, pVar->Num) );
00180         // go though all the variables in the neighborhood
00181         // and check that it is true that there is least one assigned
00182         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num );
00183         nRound = Msat_IntVecReadSize( vRound );
00184         pRound = Msat_IntVecReadArray( vRound );
00185         for ( i = 0; i < nRound; i++ )
00186         {
00187             if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
00188                 continue;
00189             if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
00190                 break;
00191         }
00192 //        assert( i != nRound );
00193 //        if ( i == nRound )
00194 //            return 0;
00195         if ( i == nRound )
00196             Counter++;
00197     }
00198     if ( Counter > 0 )
00199         printf( "%d(%d) ", Counter, p->rVars.nItems );
00200 
00201     // we may also check other unassigned variables in the cone
00202     // to make sure that if they are not in J-boundary, 
00203     // then they do not have an assigned neighbor
00204     nVars = Msat_IntVecReadSize( p->pSat->vConeVars );
00205     pVars = Msat_IntVecReadArray( p->pSat->vConeVars );
00206     for ( i = 0; i < nVars; i++ )
00207     {
00208         assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) );
00209         // skip assigned vars, vars in the boundary, and vars not used in the cone
00210         if ( Msat_OrderVarIsAssigned(p, pVars[i]) || 
00211              Msat_OrderVarIsInBoundary(p, pVars[i]) )
00212             continue;
00213         // make sure, it does not have assigned neighbors
00214         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
00215         nRound = Msat_IntVecReadSize( vRound );
00216         pRound = Msat_IntVecReadArray( vRound );
00217         for ( k = 0; k < nRound; k++ )
00218         {
00219             if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
00220                 continue;
00221             if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
00222                 break;
00223         }
00224 //        assert( k == nRound );
00225 //        if ( k != nRound )
00226 //            return 0;
00227     }
00228     return 1;
00229 }

void Msat_OrderClean ( Msat_Order_t *  p,
Msat_IntVec_t *  vCone 
)

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

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file msatOrderJ.c.

00148 {
00149     Msat_OrderVar_t * pVar, * pNext;
00150     // quickly undo the ring
00151     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
00152         pVar->pNext = pVar->pPrev = NULL;
00153     p->rVars.pRoot  = NULL;
00154     p->rVars.nItems = 0;
00155 }

void Msat_OrderFree ( Msat_Order_t *  p  ) 

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

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file msatOrderJ.c.

00243 {
00244     free( p->pVars );
00245     free( p );
00246 }

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

00404 {
00405 //printf( "adding %d\n", pVar->Num );
00406     // check that the node is not in a ring
00407     assert( pVar->pPrev == NULL );
00408     assert( pVar->pNext == NULL );
00409     // if the ring is empty, make the node point to itself
00410     pRing->nItems++;
00411     if ( pRing->pRoot == NULL )
00412     {
00413         pRing->pRoot  = pVar;
00414         pVar->pPrev  = pVar;
00415         pVar->pNext  = pVar;
00416         return;
00417     }
00418     // if the ring is not empty, add it as the last entry
00419     pVar->pPrev = pRing->pRoot->pPrev;
00420     pVar->pNext = pRing->pRoot;
00421     pVar->pPrev->pNext = pVar;
00422     pVar->pNext->pPrev = pVar;
00423 
00424     // move the root so that it points to the new entry
00425 //    pRing->pRoot = pRing->pRoot->pPrev;
00426 }

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

00440 {
00441 //printf( "removing %d\n", pVar->Num );
00442     // check that the var is in a ring
00443     assert( pVar->pPrev );
00444     assert( pVar->pNext );
00445     pRing->nItems--;
00446     if ( pRing->nItems == 0 )
00447     {
00448         assert( pRing->pRoot == pVar );
00449         pVar->pPrev = NULL;
00450         pVar->pNext = NULL;
00451         pRing->pRoot = NULL;
00452         return;
00453     }
00454     // move the root if needed
00455     if ( pRing->pRoot == pVar )
00456         pRing->pRoot = pVar->pNext;
00457     // move the root to the next entry after pVar
00458     // this way all the additions to the list will be traversed first
00459 //    pRing->pRoot = pVar->pPrev;
00460     // delete the node
00461     pVar->pPrev->pNext = pVar->pNext;
00462     pVar->pNext->pPrev = pVar->pPrev;
00463     pVar->pPrev = NULL;
00464     pVar->pNext = NULL;
00465 }

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

00121 {
00122     int i;
00123     // add variables if they are missing
00124     if ( p->nVarsAlloc < nVarsMax )
00125     {
00126         p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax );
00127         for ( i = p->nVarsAlloc; i < nVarsMax; i++ )
00128         {
00129             p->pVars[i].pNext = p->pVars[i].pPrev = NULL;
00130             p->pVars[i].Num = i;
00131         }
00132         p->nVarsAlloc = nVarsMax;
00133     }
00134 }

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

00388 {
00389 }

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

00303 {
00304     Msat_IntVec_t * vRound;
00305     int i;//, clk = clock();
00306 
00307     // make sure the variable is in the boundary
00308     assert( Var < p->nVarsAlloc );
00309     // if it is not in the boundary (initial decision, random decision), do not remove
00310     if ( Msat_OrderVarIsInBoundary( p, Var ) )
00311         Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] );
00312     // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary
00313     // because for them we know that there is a variable (Var) which is assigned
00314     vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
00315     for ( i = 0; i < vRound->nSize; i++ )
00316     {
00317         if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) )
00318             continue;
00319         if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) )
00320             continue;
00321         if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
00322             continue;
00323         Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
00324     }
00325 //timeSelect += clock() - clk;
00326 //    Msat_OrderCheck( p );
00327 }

int Msat_OrderVarSelect ( Msat_Order_t *  p  ) 

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

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file msatOrderJ.c.

00260 {
00261     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
00262     double * pdActs = p->pSat->pdActivity;
00263     double dfActBest;
00264 //    int clk = clock();
00265 
00266     pVarBest = NULL;
00267     dfActBest = -1.0;
00268     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
00269     {
00270         if ( dfActBest < pdActs[pVar->Num] )
00271         {
00272             dfActBest = pdActs[pVar->Num];
00273             pVarBest  = pVar;
00274         }
00275     }
00276 //timeSelect += clock() - clk;
00277 //timeAssign += clock() - clk;
00278 
00279 //if ( pVarBest && pVarBest->Num % 1000 == 0 )
00280 //printf( "%d ", p->rVars.nItems );
00281 
00282 //    Msat_OrderCheck( p );
00283     if ( pVarBest )
00284     {
00285         assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
00286         return pVarBest->Num;
00287     }
00288     return MSAT_ORDER_UNKNOWN;
00289 }

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

00341 {
00342     Msat_IntVec_t * vRound, * vRound2;
00343     int i, k;//, clk = clock();
00344 
00345     // make sure the variable is not in the boundary
00346     assert( Var < p->nVarsAlloc );
00347     assert( !Msat_OrderVarIsInBoundary( p, Var ) );
00348     // go through its neigbors - if one of them is assigned add this var
00349     // add to the boundary those neighbors that are not there already
00350     // this will also get rid of variable outside of the current cone
00351     // because they are unassigned in Msat_SolverPrepare()
00352     vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
00353     for ( i = 0; i < vRound->nSize; i++ )
00354         if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) 
00355             break;
00356     if ( i != vRound->nSize )
00357         Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] );
00358 
00359     // unassigning a variable may lead to its adjacents dropping from the boundary
00360     for ( i = 0; i < vRound->nSize; i++ )
00361         if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
00362         { // the neighbor is in the J-boundary (and unassigned)
00363             assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) );
00364             vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]];
00365             // go through its neighbors and determine if there is at least one assigned
00366             for ( k = 0; k < vRound2->nSize; k++ )
00367                 if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) 
00368                     break;
00369             if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
00370                 Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
00371         }
00372 //timeSelect += clock() - clk;
00373 //    Msat_OrderCheck( p );
00374 }

Variable Documentation

int timeAssign

Definition at line 26 of file fraigMan.c.

int timeSelect

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

FileName [fraigMan.c]

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

Synopsis [Implementation of the FRAIG manager.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

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

] DECLARATIONS ///

Definition at line 25 of file fraigMan.c.

Generated on Tue Jan 5 12:19:40 2010 for abc70930 by  doxygen 1.6.1