1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
|
/*-----------------------------------------------------------------------
File : che_random.h
Author: Stephan Schulz
Contents
Clause "evaluations" incorporating random elements. Note that these
are not, in general, fair if used with naive parameterization.
Copyright 2019 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Created: Fri May 24 14:50:44 CEST 2019
-----------------------------------------------------------------------*/
#ifndef CHE_RANDOM
#define CHE_RANDOM
#include <che_wfcb.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct
{
double fifo_counter;
unsigned int rand_range;
double fifo_weight;
double sc_weight;
RandStateCell rand_state;
}RandomWeightParamCell, *RandomWeightParam_p;
#define RandomWeightParamCellAlloc() (RandomWeightParamCell*) \
SizeMalloc(sizeof(RandomWeightParamCell))
#define RandomWeightParamCellFree(junk) \
SizeFree(junk, sizeof(RandomWeightParamCell))
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
WFCB_p RandWeightInit(ClausePrioFun prio_fun, long range, double fifo_w,
double sc_w, unsigned int seed1, unsigned int seed2,
unsigned int seed3);
WFCB_p RandWeightParse(Scanner_p in, OCB_p ocb, ProofState_p state);
double RandWeightCompute(void* data, Clause_p clause);
void RandWeightExit(void* data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|