Trait InitCert

pub trait InitCert: Init {
    type ProofWriter: Write;

    // Required method
    fn new_cert<Cls>(
        clauses: Cls,
        objs: Vec<Objective>,
        var_manager: VarManager,
        opts: KernelOptions,
        proof: Proof<Self::ProofWriter>,
        block_clause_gen: <Self as Init>::BlockClauseGen,
    ) -> Result<Self>
       where Cls: IntoIterator<Item = (Clause, AbsConstraintId)>;

    // Provided method
    fn from_instance_cert(
        inst: Instance,
        opts: KernelOptions,
        proof: Proof<Self::ProofWriter>,
        block_clause_gen: <Self as Init>::BlockClauseGen,
    ) -> Result<Self> { ... }
}

Trait for initializing algorithms

Required Associated Types

type ProofWriter: Write

Required Methods

fn new_cert<Cls>( clauses: Cls, objs: Vec<Objective>, var_manager: VarManager, opts: KernelOptions, proof: Proof<Self::ProofWriter>, block_clause_gen: <Self as Init>::BlockClauseGen, ) -> Result<Self>

where Cls: IntoIterator<Item = (Clause, AbsConstraintId)>,

Initialization of the algorithm providing all optional input

Provided Methods

fn from_instance_cert( inst: Instance, opts: KernelOptions, proof: Proof<Self::ProofWriter>, block_clause_gen: <Self as Init>::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<'term, 'learn, PBE, CE, ProofW, OInit, BCG> InitCert for BiOptSat<CaDiCaL<'term, 'learn>, PBE, CE, ProofW, OInit, BCG>

where ProofW: Write + 'static, PBE: BoundUpperIncremental + FromIterator<(Lit, usize)>, CE: BoundUpperIncremental + FromIterator<Lit>, OInit: Initialize<CaDiCaL<'term, 'learn>>, BCG: Fn(Assignment) -> Clause,

type ProofWriter = ProofW

impl<'term, 'learn, PBE, CE, ProofW, OInit, BCG> InitCert for PMinimal<CaDiCaL<'term, 'learn>, PBE, CE, ProofW, OInit, BCG>

where PBE: BoundUpperIncremental + FromIterator<(Lit, usize)> + Monotone, CE: BoundUpperIncremental + FromIterator<Lit> + Monotone, OInit: Initialize<CaDiCaL<'term, 'learn>>, ProofW: Write + 'static, BCG: Fn(Assignment) -> Clause,

type ProofWriter = ProofW

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

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

type ProofWriter = ProofW