Trait splr::types::ActivityIF[−][src]

pub trait ActivityIF<Ix> {
    fn activity(&mut self, ix: Ix) -> f64;

    fn average_activity(&self) -> f64;

    fn set_activity(&mut self, ix: Ix, val: f64);

    fn update_rewards(&mut self);

    fn reward_at_analysis(&mut self, _ix: Ix) { ... }

    fn reward_at_assign(&mut self, _ix: Ix) { ... }

    fn reward_at_propagation(&mut self, _ix: Ix) { ... }

    fn reward_at_unassign(&mut self, _ix: Ix) { ... }

    fn update_activity_decay(&mut self, _index: Option<usize>) { ... }
}

API for reward based activity management.

Required methods

fn activity(&mut self, ix: Ix) -> f64[src]

return one’s activity.

fn average_activity(&self) -> f64[src]

return average activity

fn set_activity(&mut self, ix: Ix, val: f64)[src]

set activity

fn update_rewards(&mut self)[src]

update internal counter.

Loading content...

Provided methods

fn reward_at_analysis(&mut self, _ix: Ix)[src]

modify one’s activity at conflict analysis in conflict_analyze in solver.

fn reward_at_assign(&mut self, _ix: Ix)[src]

modify one’s activity at value assignment in assign.

fn reward_at_propagation(&mut self, _ix: Ix)[src]

modify one’s activity at value assignment in unit propagation.

fn reward_at_unassign(&mut self, _ix: Ix)[src]

modify one’s activity at value un-assignment in cancel_until.

fn update_activity_decay(&mut self, _index: Option<usize>)[src]

update reward decay.

Loading content...

Implementors

impl ActivityIF<usize> for AssignStack[src]

impl ActivityIF<ClauseId> for ClauseDB[src]

Loading content...