Struct SkolemGenerator 

pub struct SkolemGenerator { /* private fields */ }

Generates Skolem names in an incremental fashion in the context of any transformation that involves Skolemization.

Note: To ensure all Skolem functions in a theory are unique, the same instance of SkolemGenerator must be used when transforming all formulae of the theory.

Implementations

impl SkolemGenerator

pub fn new() -> Self

Creates a new SkolemGenerator with the default prefix "sk#".

pub fn next(&mut self) -> String

Returns the next Skolem name.

Trait Implementations

impl Debug for SkolemGenerator

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

Formats the value using the given formatter.

impl From<&str> for SkolemGenerator

fn from(prefix: &str) -> Self

Creates a SkolemGenerator instance with the given prefix.

impl PartialEq for SkolemGenerator

fn eq(&self, other: &SkolemGenerator) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SkolemGenerator