Solver.cc File Reference

#include <math.h>
#include "Alg.h"
#include "Sort.h"
#include "System.h"
#include "Solver.h"

Include dependency graph for Solver.cc:

Go to the source code of this file.

Data Structures
struct	reduceDB_lt

Macros
#define	__STDC_FORMAT_MACROS
#define	__STDC_LIMIT_MACROS

Functions
static double	luby (double y, int x)
static Var	mapVar (Var x, vec< Var > &map, Var &max)

Variables
static const char *	_cat = "CORE"
static DoubleOption	opt_var_decay (_cat,"var-decay","The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false))
static DoubleOption	opt_clause_decay (_cat,"cla-decay","The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false))
static DoubleOption	opt_random_var_freq (_cat,"rnd-freq","The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true))
static DoubleOption	opt_random_seed (_cat,"rnd-seed","Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false))
static IntOption	opt_ccmin_mode (_cat,"ccmin-mode","Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2))
static IntOption	opt_phase_saving (_cat,"phase-saving","Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2))
static BoolOption	opt_rnd_init_act (_cat,"rnd-init","Randomize the initial activity", false)
static BoolOption	opt_luby_restart (_cat,"luby","Use the Luby restart sequence", true)
static IntOption	opt_restart_first (_cat,"rfirst","The base restart interval", 100, IntRange(1, INT32_MAX))
static DoubleOption	opt_restart_inc (_cat,"rinc","Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false))
static DoubleOption	opt_garbage_frac (_cat,"gc-frac","The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false))
static IntOption	opt_min_learnts_lim (_cat,"min-learnts","Minimum learnt clause limit", 0, IntRange(0, INT32_MAX))

Macro Definition Documentation

#define __STDC_FORMAT_MACROS

Definition at line 1 of file Solver.cc.

#define __STDC_LIMIT_MACROS

Definition at line 2 of file Solver.cc.

Function Documentation

static double luby ( double  y, int  x  )

static

Definition at line 824 of file Solver.cc.

                                   {

    // Find the finite subsequence that contains index 'x', and the
    // size of that subsequence:
    int size, seq;
    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);

    while (size-1 != x){
        size = (size-1)>>1;
        seq--;
        x = x % size;
    }

    return pow(y, seq);
}

Here is the caller graph for this function:

static Var mapVar ( Var  x, vec< Var > &  map, Var &  max  )

static

Definition at line 920 of file Solver.cc.

{
    if (map.size() <= x || map[x] == -1){
        map.growTo(x+1, -1);
        map[x] = max++;
    }
    return map[x];
}

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

const char* _cat = "CORE"

static

Definition at line 36 of file Solver.cc.

IntOption opt_ccmin_mode(_cat,"ccmin-mode","Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2))

static

DoubleOption opt_clause_decay(_cat,"cla-decay","The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false))

static

DoubleOption opt_garbage_frac(_cat,"gc-frac","The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false))

static

BoolOption opt_luby_restart(_cat,"luby","Use the Luby restart sequence", true)

static

IntOption opt_min_learnts_lim(_cat,"min-learnts","Minimum learnt clause limit", 0, IntRange(0, INT32_MAX))

static

IntOption opt_phase_saving(_cat,"phase-saving","Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2))

static

DoubleOption opt_random_seed(_cat,"rnd-seed","Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false))

static

DoubleOption opt_random_var_freq(_cat,"rnd-freq","The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true))

static

IntOption opt_restart_first(_cat,"rfirst","The base restart interval", 100, IntRange(1, INT32_MAX))

static

DoubleOption opt_restart_inc(_cat,"rinc","Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false))

static

BoolOption opt_rnd_init_act(_cat,"rnd-init","Randomize the initial activity", false)

static

DoubleOption opt_var_decay(_cat,"var-decay","The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false))

static