src/sat/msat/msatOrderH.c

Go to the documentation of this file.

#include "msatInt.h"


// the variable package data structure
struct Msat_Order_t_
{
    Msat_Solver_t *      pSat;         // the SAT solver 
    Msat_IntVec_t *      vIndex;       // the heap
    Msat_IntVec_t *      vHeap;        // the mapping of var num into its heap num
};

//The solver can communicate to the variable order the following parts:
//- the array of current assignments (pSat->pAssigns)
//- the array of variable activities (pSat->pdActivity)
//- the array of variables currently in the cone (pSat->vConeVars)
//- the array of arrays of variables adjucent to each(pSat->vAdjacents)

#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)

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

extern int timeSelect;


Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
{
    Msat_Order_t * p;
    p = ALLOC( Msat_Order_t, 1 );
    memset( p, 0, sizeof(Msat_Order_t) );
    p->pSat   = pSat;
    p->vIndex = Msat_IntVecAlloc( 0 );
    p->vHeap  = Msat_IntVecAlloc( 0 );
    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
    return p;
}

void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax )
{
    Msat_IntVecGrow( p->vIndex, nVarsMax );
    Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
    p->vIndex->nSize = nVarsMax;
    p->vHeap->nSize = 0;
}

void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone )
{
    int i;
    for ( i = 0; i < p->vIndex->nSize; i++ )
        p->vIndex->pArray[i] = 0;
    for ( i = 0; i < vCone->nSize; i++ )
    {
        assert( i+1 < p->vHeap->nCap );
        p->vHeap->pArray[i+1] = vCone->pArray[i];

        assert( vCone->pArray[i] < p->vIndex->nSize );
        p->vIndex->pArray[vCone->pArray[i]] = i+1;
    }
    p->vHeap->nSize = vCone->nSize + 1;
}

int Msat_OrderCheck( Msat_Order_t * p )
{
    return Msat_HeapCheck_rec( p, 1 );
}

void Msat_OrderFree( Msat_Order_t * p )
{
    Msat_IntVecFree( p->vHeap );
    Msat_IntVecFree( p->vIndex );
    free( p );
}



int Msat_OrderVarSelect( Msat_Order_t * p )
{
    // Activity based decision:
//    while (!heap.empty()){
//        Var next = heap.getmin();
//        if (toLbool(assigns[next]) == l_Undef)
//            return next;
//    }
//    return var_Undef;

    int Var;
    int clk = clock();

    while ( !HEMPTY(p) )
    {
        Var = Msat_HeapGetTop(p);
        if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
        {
//assert( Msat_OrderCheck(p) );
timeSelect += clock() - clk;
            return Var;
        }
    }
    return MSAT_ORDER_UNKNOWN;
}

void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
{
}

void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
{
//    if (!heap.inHeap(x))
//        heap.insert(x);

    int clk = clock();
    if ( !HINHEAP(p,Var) )
        Msat_HeapInsert( p, Var );
timeSelect += clock() - clk;
}

void Msat_OrderUpdate( Msat_Order_t * p, int Var )
{
//    if (heap.inHeap(x))
//        heap.increase(x);

    int clk = clock();
    if ( HINHEAP(p,Var) )
        Msat_HeapIncrease( p, Var );
timeSelect += clock() - clk;
}




int Msat_HeapCheck_rec( Msat_Order_t * p, int i )
{
    return i >= HSIZE(p) ||
        ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
        Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) );
}

int Msat_HeapGetTop( Msat_Order_t * p )
{
    int Result, NewTop;
    Result                    = HHEAP(p, 1);
    NewTop                    = Msat_IntVecPop( p->vHeap );
    p->vHeap->pArray[1]       = NewTop;
    p->vIndex->pArray[NewTop] = 1;
    p->vIndex->pArray[Result] = 0;
    if ( p->vHeap->nSize > 1 )
        Msat_HeapPercolateDown( p, 1 );
    return Result;
}

void Msat_HeapInsert( Msat_Order_t * p, int n )
{
    assert( HOKAY(p, n) );
    p->vIndex->pArray[n] = HSIZE(p);
    Msat_IntVecPush( p->vHeap, n );
    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
}

void Msat_HeapIncrease( Msat_Order_t * p, int n )
{
    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
}

void Msat_HeapPercolateUp( Msat_Order_t * p, int i )
{
    int x = HHEAP(p, i);
    while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) )
    {
        p->vHeap->pArray[i]            = HHEAP(p, HPARENT(i));
        p->vIndex->pArray[HHEAP(p, i)] = i;
        i                              = HPARENT(i);
    }
    p->vHeap->pArray[i]  = x;
    p->vIndex->pArray[x] = i;
}

void Msat_HeapPercolateDown( Msat_Order_t * p, int i )
{
    int x = HHEAP(p, i);
    int Child;
    while ( HLEFT(i) < HSIZE(p) )
    {
        if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) )
            Child = HRIGHT(i);
        else
            Child = HLEFT(i);
        if ( !HCOMPARE(p, HHEAP(p, Child), x) )
            break;
        p->vHeap->pArray[i]            = HHEAP(p, Child);
        p->vIndex->pArray[HHEAP(p, i)] = i;
        i                              = Child;
    }
    p->vHeap->pArray[i]  = x;
    p->vIndex->pArray[x] = i;
}

---