Struct Frame 

pub struct Frame { /* private fields */ }

A single frame in the PDR sequence.

Contains blocking clauses (negations of blocked cubes) that overapproximate the set of reachable states at this depth.

Implementations

impl Frame

pub fn new() -> Self

Create an empty frame.

pub fn from_clauses(clauses: Vec<Vec<Lit>>) -> Self

Create a frame from initial-state clauses.

pub fn add_clause(&mut self, clause: Vec<Lit>)

Add a blocking clause (deduplicating).

pub fn clauses(&self) -> &[Vec<Lit>]

Read access to clauses.

pub fn len(&self) -> usize

Number of blocking clauses.

pub fn is_empty(&self) -> bool

Whether the frame has no blocking clauses.

Trait Implementations

impl Clone for Frame

fn clone(&self) -> Frame

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Frame

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Frame

fn default() -> Self

Returns the “default value” for a type.