Version abc70930

1 files changed, 0 insertions, 405 deletions

diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
deleted file mode 100644
index 956e7fc6..00000000
--- a/src/sat/msat/msatOrderH.c
+++ /dev/null
@@ -1,405 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// 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;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the bound of the ordering structure.]
-
-  Description [Should be called whenever the SAT solver is resized.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks that the J-boundary is okay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_OrderCheck( Msat_Order_t * p )
-{
-    return Msat_HeapCheck_rec( p, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderFree( Msat_Order_t * p )
-{
-    Msat_IntVecFree( p->vHeap );
-    Msat_IntVecFree( p->vIndex );
-    free( p );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Selects the next variable to assign.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates J-boundary when the variable is assigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
-{
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable is unassigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable changed weight.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the heap property recursively.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Retrieves the minimum element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the new element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the new element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_HeapIncrease( Msat_Order_t * p, int n )
-{
-    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the entry up.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the entry down.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-