Trait Init

pub trait Init: Sized {
    type Oracle: SolveIncremental;
    type BlockClauseGen: Fn(Assignment) -> Clause;

    // Required method
    fn new<Cls>(
        clauses: Cls,
        objs: Vec<Objective>,
        var_manager: VarManager,
        opts: KernelOptions,
        block_clause_gen: Self::BlockClauseGen,
    ) -> Result<Self>
       where Cls: IntoIterator<Item = Clause>;

    // Provided method
    fn from_instance(
        inst: Instance,
        opts: KernelOptions,
        block_clause_gen: Self::BlockClauseGen,
    ) -> Result<Self> { ... }
}

Trait for initializing algorithms

Required Associated Types

type Oracle: SolveIncremental

type BlockClauseGen: Fn(Assignment) -> Clause

Required Methods

fn new<Cls>( clauses: Cls, objs: Vec<Objective>, var_manager: VarManager, opts: KernelOptions, block_clause_gen: Self::BlockClauseGen, ) -> Result<Self>

where Cls: IntoIterator<Item = Clause>,

Initialization of the algorithm providing all optional input

Provided Methods

fn from_instance( inst: Instance, opts: KernelOptions, block_clause_gen: Self::BlockClauseGen, ) -> Result<Self>

Initialization of the algorithm using an Instance rather than iterators

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<'learn, 'term, ProofW, OInit, BCG> Init for LowerBounding<CaDiCaL<'learn, 'term>, GeneralizedTotalizer, Totalizer, ProofW, OInit, BCG>

where ProofW: Write + 'static, OInit: Initialize<CaDiCaL<'learn, 'term>>, BCG: Fn(Assignment) -> Clause,

type Oracle = CaDiCaL<'learn, 'term>

type BlockClauseGen = BCG

impl<O, PBE, CE, ProofW, OInit, BCG> Init for BiOptSat<O, PBE, CE, ProofW, OInit, BCG>

where O: SolveIncremental + Interrupt + PhaseLit + LimitConflicts, ProofW: Write, PBE: BoundUpperIncremental + FromIterator<(Lit, usize)>, CE: BoundUpperIncremental + FromIterator<Lit>, OInit: Initialize<O>, BCG: Fn(Assignment) -> Clause,

type Oracle = O

type BlockClauseGen = BCG

impl<O, PBE, CE, ProofW, OInit, BCG> Init for PMinimal<O, PBE, CE, ProofW, OInit, BCG>

where O: SolveIncremental + Interrupt + PhaseLit + LimitConflicts, ProofW: Write, PBE: BoundUpperIncremental + FromIterator<(Lit, usize)> + Monotone, CE: BoundUpperIncremental + FromIterator<Lit> + Monotone, OInit: Initialize<O>, BCG: Fn(Assignment) -> Clause,

type Oracle = O

type BlockClauseGen = BCG