pub enum EquivOutcome {
Equivalent,
Differ(Vec<(String, bool)>),
Unsupported,
}Expand description
The result of an equivalence query between two formulas.
Variants§
Equivalent
The two formulas denote the same Boolean function. The verdict is RUP-certified:
F ↔ S was replayed to the empty clause, not merely reported UNSAT.
Differ(Vec<(String, bool)>)
The formulas differ. The assignment is a concrete counterexample: under it exactly one of the two formulas holds. For hardware, this is the distinguishing waveform.
Unsupported
Not purely propositional over recognisable atoms — the caller must escalate.
Trait Implementations§
Source§impl Clone for EquivOutcome
impl Clone for EquivOutcome
Source§fn clone(&self) -> EquivOutcome
fn clone(&self) -> EquivOutcome
Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for EquivOutcome
impl Debug for EquivOutcome
Source§impl PartialEq for EquivOutcome
impl PartialEq for EquivOutcome
Source§fn eq(&self, other: &EquivOutcome) -> bool
fn eq(&self, other: &EquivOutcome) -> bool
Tests for
self and other values to be equal, and is used by ==.impl Eq for EquivOutcome
impl StructuralPartialEq for EquivOutcome
Auto Trait Implementations§
impl Freeze for EquivOutcome
impl RefUnwindSafe for EquivOutcome
impl Send for EquivOutcome
impl Sync for EquivOutcome
impl Unpin for EquivOutcome
impl UnsafeUnpin for EquivOutcome
impl UnwindSafe for EquivOutcome
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more