summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatOrderH.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat/msatOrderH.c')
-rw-r--r--src/sat/msat/msatOrderH.c405
1 files changed, 405 insertions, 0 deletions
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
new file mode 100644
index 00000000..ca034233
--- /dev/null
+++ b/src/sat/msat/msatOrderH.c
@@ -0,0 +1,405 @@
+/**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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:13:25 +0000