Skip to main content

LyapunovMeasure

logicaffeine_proof::lyapunov

Trait LyapunovMeasure 

Source 
pub trait LyapunovMeasure {
    // Required methods
    fn num_vars(&self) -> usize;
    fn formula(&self) -> &[Vec<Lit_>];
    fn initial_potential(&self) -> u64;
    fn width(&self) -> u64;
    fn descent_step(
        &self,
        level: u64,
        db: &[Vec<Lit_>],
    ) -> Vec<(Vec<Lit_>, Witness)>;
}
Expand description

The hypothesis of the ⟸ theorem: a Lyapunov measure that generates certified descent steps for a formula, independent of any particular family.

Required Methods§

Source

fn num_vars(&self) -> usize

The number of variables of the formula.

Source

fn formula(&self) -> &[Vec<Lit_>]

The formula F the measure refutes.

Source

fn initial_potential(&self) -> u64

The initial potential L (the number of descent levels).

Source

fn width(&self) -> u64

The per-level width bound w (max certified additions per level).

Source

fn descent_step( &self, level: u64, db: &[Vec<Lit_>], ) -> Vec<(Vec<Lit_>, Witness)>

The certified-redundant clause additions descending from level to level-1, given the current database. Each MUST be RUP/PR/SR against db (the constructor re-checks, fail-closed), and there must be at most width() of them.

Implementors§