Struct SolverOpts

pub struct SolverOpts {Show 15 fields
    pub var_decay: f64,
    pub clause_decay: f64,
    pub random_var_freq: f64,
    pub random_seed: f64,
    pub luby_restart: bool,
    pub ccmin_mode: i32,
    pub phase_saving: i32,
    pub rnd_pol: bool,
    pub rnd_init_act: bool,
    pub garbage_frac: f64,
    pub min_learnts_lim: i32,
    pub restart_first: i32,
    pub restart_inc: f64,
    pub learntsize_factor: f64,
    pub learntsize_inc: f64,
}

Expand description

Solver options.

This can be used to tune the solver heuristics.

Fields§

§var_decay: f64§clause_decay: f64§random_var_freq: f64§random_seed: f64§luby_restart: bool§ccmin_mode: i32

Controls conflict clause minimization (0=none, 1=basic, 2=deep).

§phase_saving: i32

Controls the level of phase saving (0=none, 1=limited, 2=full).

§rnd_pol: bool

Use random polarities for branching heuristics.

§rnd_init_act: bool

Initialize variable activities with a small random value.

§garbage_frac: f64

The fraction of wasted memory allowed before a garbage collection is triggered.

§min_learnts_lim: i32

Minimum number to set the learnts limit to.

§restart_first: i32

The initial restart limit. (default 100)

§restart_inc: f64

The factor with which the restart limit is multiplied in each restart. (default 1.5)

§learntsize_factor: f64

The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)

§learntsize_inc: f64

The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)

Implementations§

impl SolverOpts

pub fn check(&self) -> bool

Check that options are valid.

Trait Implementations§

impl Clone for SolverOpts

fn clone(&self) -> SolverOpts

Returns a duplicate of the value. Read more

1.0.0 · Source§

const fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

impl Default for SolverOpts

fn default() -> SolverOpts

Returns the “default value” for a type. Read more

Auto Trait Implementations§

impl Freeze for SolverOpts

impl RefUnwindSafe for SolverOpts

impl Send for SolverOpts

impl Sync for SolverOpts

impl Unpin for SolverOpts

impl UnwindSafe for SolverOpts

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.