Struct EmptyTheory 

pub struct EmptyTheory(/* private fields */);

Trivial theory that does nothing

Implementations

impl EmptyTheory

pub fn new() -> Self

New empty theory.

Trait Implementations

impl Default for EmptyTheory

fn default() -> Self

Returns the “default value” for a type.

impl Theory for EmptyTheory

fn final_check(&mut self, _: &mut TheoryArg<'_>)

Check the model candidate model thoroughly.

fn create_level(&mut self)

Push a new backtracking level

fn pop_levels(&mut self, n: usize)

Pop n levels from the stack

fn n_levels(&self) -> usize

Number of levels

fn explain_propagation(&mut self, _p: Lit) -> &[Lit]

If the theory uses TheoryArgument::propagate, it must implement this function to explain the propagations.

fn partial_check(&mut self, _acts: &mut TheoryArg<'_>)

Check partial model (best effort).