msatSort.c File Reference

#include "msatInt.h"

Include dependency graph for msatSort.c:

Go to the source code of this file.

Functions
void	Msat_SolverSortDB (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///.
void	Msat_SolverSortSelection (Msat_Clause_t **array, int size)

Function Documentation

Msat_SolverSortDB()

void Msat_SolverSortDB

(

Msat_Solver_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file msatSort.c.

{
    Msat_ClauseVec_t * pVecClauses;
    Msat_Clause_t ** pLearned;
    int nLearned;
    // read the parameters
    pVecClauses = Msat_SolverReadLearned( p );
    nLearned    = Msat_ClauseVecReadSize( pVecClauses );
    pLearned    = Msat_ClauseVecReadArray( pVecClauses );
    // Msat_SolverSort the array
//    qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 
//            (int (*)(const void *, const void *)) Msat_SolverSortCompare );
//    printf( "Msat_SolverSorting.\n" );
    Msat_SolverSort( pLearned, nLearned, 91648253 );
/*
    if ( nLearned > 2 )
    {
    printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
    printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
    printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
    }
*/
}

Here is the call graph for this function:

Msat_SolverSortSelection()

void Msat_SolverSortSelection	(	Msat_Clause_t **	array,
		int	size )

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

Synopsis [Selection sort for small array size.]

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file msatSort.c.

{
    Msat_Clause_t * tmp;
    int i, j, best_i;
    for ( i = 0; i < size-1; i++ )
    {
        best_i = i;
        for (j = i+1; j < size; j++)
        {
            if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) )
                best_i = j;
        }
        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
    }
}

Here is the call graph for this function: