Trait obddimal::bdd_manager::dvo_schedules::DVOSchedule

pub(crate) trait DVOSchedule {
    fn run_dvo(
        &mut self,
        num_clause: usize,
        man: &mut DDManager,
        f: NodeID,
        bar: &Option<ProgressBar>
    ) -> NodeID;
}

Implements run_dvo()

Required Methods

fn run_dvo(
    &mut self,
    num_clause: usize,
    man: &mut DDManager,
    f: NodeID,
    bar: &Option<ProgressBar>
) -> NodeID

This gets called after a CNF clause has been integrated. The current root node is f, the implementation must return the new root node ID, even if it does not change.

• num_clause: The index of the current clause, in integration order (which may differ from the order defined in the input CNF).

Implementors

impl DVOSchedule for DVOScheduleEnum

impl DVOSchedule for AlwaysOnce

impl DVOSchedule for AlwaysUntilConvergence

impl DVOSchedule for AtThreshold

impl DVOSchedule for NoDVOSchedule

impl DVOSchedule for SiftingAtThreshold

impl DVOSchedule for TimeSizeLimit