src/sat/msat/msatOrderH.c File Reference

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

Go to the source code of this file.

Data Structures

struct  Msat_Order_t_

Defines

#define HLEFT(i)   ((i)<<1)
#define HRIGHT(i)   (((i)<<1)+1)
#define HPARENT(i)   ((i)>>1)
#define HCOMPARE(p, i, j)   ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])
#define HHEAP(p, i)   ((p)->vHeap->pArray[i])
#define HSIZE(p)   ((p)->vHeap->nSize)
#define HOKAY(p, i)   ((i) >= 0 && (i) < (p)->vIndex->nSize)
#define HINHEAP(p, i)   (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)
#define HEMPTY(p)   (HSIZE(p) == 1)

Functions

static int Msat_HeapCheck_rec (Msat_Order_t *p, int i)
static int Msat_HeapGetTop (Msat_Order_t *p)
static void Msat_HeapInsert (Msat_Order_t *p, int n)
static void Msat_HeapIncrease (Msat_Order_t *p, int n)
static void Msat_HeapPercolateUp (Msat_Order_t *p, int i)
static void Msat_HeapPercolateDown (Msat_Order_t *p, int i)
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

Define Documentation

#define HCOMPARE ( p,
i,
j   )     ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])

Definition at line 44 of file msatOrderH.c.

#define HEMPTY ( p   )     (HSIZE(p) == 1)

Definition at line 49 of file msatOrderH.c.

#define HHEAP ( p,
i   )     ((p)->vHeap->pArray[i])

Definition at line 45 of file msatOrderH.c.

#define HINHEAP ( p,
i   )     (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)

Definition at line 48 of file msatOrderH.c.

#define HLEFT ( i   )     ((i)<<1)

Definition at line 41 of file msatOrderH.c.

#define HOKAY ( p,
i   )     ((i) >= 0 && (i) < (p)->vIndex->nSize)

Definition at line 47 of file msatOrderH.c.

#define HPARENT ( i   )     ((i)>>1)

Definition at line 43 of file msatOrderH.c.

#define HRIGHT ( i   )     (((i)<<1)+1)

Definition at line 42 of file msatOrderH.c.

#define HSIZE ( p   )     ((p)->vHeap->nSize)

Definition at line 46 of file msatOrderH.c.

Function Documentation

int Msat_HeapCheck_rec ( Msat_Order_t *  p,
int  i 
) [static]

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

Synopsis [Checks the heap property recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file msatOrderH.c.

00280 {
00281     return i >= HSIZE(p) ||
00282         ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
00283         Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) );
00284 }

int Msat_HeapGetTop ( Msat_Order_t *  p  )  [static]

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

Synopsis [Retrieves the minimum element.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file msatOrderH.c.

00298 {
00299     int Result, NewTop;
00300     Result                    = HHEAP(p, 1);
00301     NewTop                    = Msat_IntVecPop( p->vHeap );
00302     p->vHeap->pArray[1]       = NewTop;
00303     p->vIndex->pArray[NewTop] = 1;
00304     p->vIndex->pArray[Result] = 0;
00305     if ( p->vHeap->nSize > 1 )
00306         Msat_HeapPercolateDown( p, 1 );
00307     return Result;
00308 }

void Msat_HeapIncrease ( Msat_Order_t *  p,
int  n 
) [static]

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

Synopsis [Inserts the new element.]

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file msatOrderH.c.

00341 {
00342     Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
00343 }

void Msat_HeapInsert ( Msat_Order_t *  p,
int  n 
) [static]

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

Synopsis [Inserts the new element.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file msatOrderH.c.

00322 {
00323     assert( HOKAY(p, n) );
00324     p->vIndex->pArray[n] = HSIZE(p);
00325     Msat_IntVecPush( p->vHeap, n );
00326     Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
00327 }

void Msat_HeapPercolateDown ( Msat_Order_t *  p,
int  i 
) [static]

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

Synopsis [Moves the entry down.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file msatOrderH.c.

00381 {
00382     int x = HHEAP(p, i);
00383     int Child;
00384     while ( HLEFT(i) < HSIZE(p) )
00385     {
00386         if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) )
00387             Child = HRIGHT(i);
00388         else
00389             Child = HLEFT(i);
00390         if ( !HCOMPARE(p, HHEAP(p, Child), x) )
00391             break;
00392         p->vHeap->pArray[i]            = HHEAP(p, Child);
00393         p->vIndex->pArray[HHEAP(p, i)] = i;
00394         i                              = Child;
00395     }
00396     p->vHeap->pArray[i]  = x;
00397     p->vIndex->pArray[x] = i;
00398 }

void Msat_HeapPercolateUp ( Msat_Order_t *  p,
int  i 
) [static]

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

Synopsis [Moves the entry up.]

Description []

SideEffects []

SeeAlso []

Definition at line 356 of file msatOrderH.c.

00357 {
00358     int x = HHEAP(p, i);
00359     while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) )
00360     {
00361         p->vHeap->pArray[i]            = HHEAP(p, HPARENT(i));
00362         p->vIndex->pArray[HHEAP(p, i)] = i;
00363         i                              = HPARENT(i);
00364     }
00365     p->vHeap->pArray[i]  = x;
00366     p->vIndex->pArray[x] = i;
00367 }

Msat_Order_t* Msat_OrderAlloc ( Msat_Solver_t *  pSat  ) 

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

Synopsis [Allocates the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file msatOrderH.c.

00076 {
00077     Msat_Order_t * p;
00078     p = ALLOC( Msat_Order_t, 1 );
00079     memset( p, 0, sizeof(Msat_Order_t) );
00080     p->pSat   = pSat;
00081     p->vIndex = Msat_IntVecAlloc( 0 );
00082     p->vHeap  = Msat_IntVecAlloc( 0 );
00083     Msat_OrderSetBounds( p, pSat->nVarsAlloc );
00084     return p;
00085 }

int Msat_OrderCheck ( Msat_Order_t *  p  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file msatOrderH.c.

00145 {
00146     return Msat_HeapCheck_rec( p, 1 );
00147 }

void Msat_OrderClean ( Msat_Order_t *  p,
Msat_IntVec_t *  vCone 
)

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

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatOrderH.c.

00118 {
00119     int i;
00120     for ( i = 0; i < p->vIndex->nSize; i++ )
00121         p->vIndex->pArray[i] = 0;
00122     for ( i = 0; i < vCone->nSize; i++ )
00123     {
00124         assert( i+1 < p->vHeap->nCap );
00125         p->vHeap->pArray[i+1] = vCone->pArray[i];
00126 
00127         assert( vCone->pArray[i] < p->vIndex->nSize );
00128         p->vIndex->pArray[vCone->pArray[i]] = i+1;
00129     }
00130     p->vHeap->nSize = vCone->nSize + 1;
00131 }

void Msat_OrderFree ( Msat_Order_t *  p  ) 

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

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file msatOrderH.c.

00161 {
00162     Msat_IntVecFree( p->vHeap );
00163     Msat_IntVecFree( p->vIndex );
00164     free( p );
00165 }

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 98 of file msatOrderH.c.

00099 {
00100     Msat_IntVecGrow( p->vIndex, nVarsMax );
00101     Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
00102     p->vIndex->nSize = nVarsMax;
00103     p->vHeap->nSize = 0;
00104 }

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 254 of file msatOrderH.c.

00255 {
00256 //    if (heap.inHeap(x))
00257 //        heap.increase(x);
00258 
00259     int clk = clock();
00260     if ( HINHEAP(p,Var) )
00261         Msat_HeapIncrease( p, Var );
00262 timeSelect += clock() - clk;
00263 }

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 217 of file msatOrderH.c.

00218 {
00219 }

int Msat_OrderVarSelect ( Msat_Order_t *  p  ) 

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

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file msatOrderH.c.

00181 {
00182     // Activity based decision:
00183 //    while (!heap.empty()){
00184 //        Var next = heap.getmin();
00185 //        if (toLbool(assigns[next]) == l_Undef)
00186 //            return next;
00187 //    }
00188 //    return var_Undef;
00189 
00190     int Var;
00191     int clk = clock();
00192 
00193     while ( !HEMPTY(p) )
00194     {
00195         Var = Msat_HeapGetTop(p);
00196         if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
00197         {
00198 //assert( Msat_OrderCheck(p) );
00199 timeSelect += clock() - clk;
00200             return Var;
00201         }
00202     }
00203     return MSAT_ORDER_UNKNOWN;
00204 }

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 232 of file msatOrderH.c.

00233 {
00234 //    if (!heap.inHeap(x))
00235 //        heap.insert(x);
00236 
00237     int clk = clock();
00238     if ( !HINHEAP(p,Var) )
00239         Msat_HeapInsert( p, Var );
00240 timeSelect += clock() - clk;
00241 }

Variable Documentation

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