Type Alias cop::tptp::SFof

pub type SFof = Fof<FofAtom<String, String, String>, String>;

String formula.

Aliased Type

enum SFof {
    Atom(FofAtom<String, String, String>),
    Neg(Box<Fof<FofAtom<String, String, String>, String>, Global>),
    Bin(Box<Fof<FofAtom<String, String, String>, String>, Global>, Op, Box<Fof<FofAtom<String, String, String>, String>, Global>),
    BinA(OpA, Vec<Fof<FofAtom<String, String, String>, String>, Global>),
    Quant(Quantifier, String, Box<Fof<FofAtom<String, String, String>, String>, Global>),
}

Variants

Atom(FofAtom<String, String, String>)

atom

Neg(Box<Fof<FofAtom<String, String, String>, String>, Global>)

negation

Bin(Box<Fof<FofAtom<String, String, String>, String>, Global>, Op, Box<Fof<FofAtom<String, String, String>, String>, Global>)

binary operation

BinA(OpA, Vec<Fof<FofAtom<String, String, String>, String>, Global>)

associative binary operation

Quant(Quantifier, String, Box<Fof<FofAtom<String, String, String>, String>, Global>)

quantification

Implementations

impl<A, V> Fof<A, V>

pub fn bin(l: Self, o: Op, r: Self) -> Self

Apply a binary operation to two formulas.

pub fn bina(l: Self, o: OpA, r: Self) -> Self

Apply an associative binary operation to two formulas.

If r is itself an application of o, then l is simply added to r. For example, if o is conjunction and r is a & b, then the result is l & a & b, not l & (a & b).

pub fn binas(o: OpA, fms: impl DoubleEndedIterator<Item = Self>) -> Self

For formulas f1, .., fn, return f1 o (… o fn).

pub fn imp(l: Self, r: Self) -> Self

Create the implication from l to r.

pub fn quant(q: Quantifier, v: V, fm: Self) -> Self

Create a quantification.

pub fn forall(v: V, fm: Self) -> Self

Create a universal quantification.

pub fn foralls(vs: impl Iterator<Item = V>, fm: Self) -> Self

Universally quantify over a sequence of variables.

pub fn add_premise(self, premise: Self) -> Self

If self is of shape a => b, then return premise & a => b, else premise => self.

pub fn mark_impl(self, fm: impl Fn() -> Self) -> (bool, Self)

If self is of shape a => c, then return a & fm() => fm() & c, else self.

Also return whether self is an implication, i.e. whether the output formula does not equal self.

pub fn map_atoms<B>(self, f: &mut impl FnMut(A) -> B) -> Fof<B, V>

Apply a function to all atoms.

pub fn map_vars<W>(self, f: &mut impl FnMut(V) -> W) -> Fof<A, W>

Apply a function to all variables.

pub fn atoms(&self) -> Box<dyn Iterator<Item = &A> + '_>

Return all atoms occurring in the formula.

impl<P, C, V> Fof<FofAtom<P, C, V>, V>

pub fn atom(p: P, args: Args<Term<C, V>>) -> Self

Construct an atom.

pub fn eqtm(l: Term<C, V>, r: Term<C, V>) -> Self

Construct an equality between two terms.

impl<A: Clone + Neg<Output = A>, V: Clone> Fof<A, V>

pub fn qnnf( self, f: &impl Fn(bool, Self, Op, Self) -> Self ) -> Nnf<A, V, Quantifier>

Convert to NNF, replacing non-associative binary operations via function.

pub fn unfold_eqfm_disj_conj(pol: bool, l: Self, op: Op, r: Self) -> Self

Unfold logical equivalence with a disjunction of conjunctions.

Used in (nondefinitional) leanCoP.

pub fn unfold_eqfm_conj_impl(pol: bool, l: Self, op: Op, r: Self) -> Self

Unfold logical equivalence with a conjunction of implications.

Used in nanoCoP.

impl<P: Eq, C: Eq, V> Fof<FofAtom<P, C, V>, V>

pub fn predconst_unique(&self) -> (Vec<(&P, usize)>, Vec<(&C, usize)>)

Corresponds to leanCoP’s collect_predfunc.

Trait Implementations

impl<A, V> BitAnd<Fof<A, V>> for Fof<A, V>

type Output = Fof<A, V>

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self

Performs the & operation.

impl<A, V> BitOr<Fof<A, V>> for Fof<A, V>

type Output = Fof<A, V>

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self

Performs the | operation.

impl<A: Clone, V: Clone> Clone for Fof<A, V>

fn clone(&self) -> Fof<A, V>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<A: Debug, V: Debug> Debug for Fof<A, V>

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

Formats the value using the given formatter.

impl<Atom: Display, V: Display> Display for Fof<Atom, V>

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

Formats the value using the given formatter.

impl From<AtomicFormula<'_>> for SFof

fn from(frm: AtomicFormula<'_>) -> Self

Converts to this type from the input type.

impl From<BinaryAssoc<'_>> for SFof

fn from(fm: BinaryAssoc<'_>) -> Self

Converts to this type from the input type.

impl From<BinaryFormula<'_>> for SFof

fn from(frm: BinaryFormula<'_>) -> Self

Converts to this type from the input type.

impl From<BinaryNonassoc<'_>> for SFof

fn from(frm: BinaryNonassoc<'_>) -> Self

Converts to this type from the input type.

impl From<DefinedAtomicFormula<'_>> for SFof

fn from(frm: DefinedAtomicFormula<'_>) -> Self

Converts to this type from the input type.

impl From<DefinedPlainFormula<'_>> for SFof

fn from(fm: DefinedPlainFormula<'_>) -> Self

Converts to this type from the input type.

impl From<Disjunction<'_>> for SFof

fn from(frm: Disjunction<'_>) -> Self

Converts to this type from the input type.

impl From<Formula<'_>> for SFof

fn from(frm: Formula<'_>) -> Self

Converts to this type from the input type.

impl From<Formula<'_>> for SFof

fn from(frm: Formula<'_>) -> Self

Converts to this type from the input type.

impl From<InfixUnary<'_>> for SFof

fn from(frm: InfixUnary<'_>) -> Self

Converts to this type from the input type.

impl From<Literal<'_>> for SFof

fn from(lit: Literal<'_>) -> Self

Converts to this type from the input type.

impl From<LogicFormula<'_>> for SFof

fn from(frm: LogicFormula<'_>) -> Self

Converts to this type from the input type.

impl From<PlainAtomicFormula<'_>> for SFof

fn from(frm: PlainAtomicFormula<'_>) -> Self

Converts to this type from the input type.

impl From<QuantifiedFormula<'_>> for SFof

fn from(frm: QuantifiedFormula<'_>) -> Self

Converts to this type from the input type.

impl From<UnaryFormula<'_>> for SFof

fn from(frm: UnaryFormula<'_>) -> Self

Converts to this type from the input type.

impl From<UnitFormula<'_>> for SFof

fn from(frm: UnitFormula<'_>) -> Self

Converts to this type from the input type.

impl From<UnitaryFormula<'_>> for SFof

fn from(frm: UnitaryFormula<'_>) -> Self

Converts to this type from the input type.

impl<A, V> Neg for Fof<A, V>

type Output = Fof<A, V>

The resulting type after applying the - operator.

fn neg(self) -> Self

Performs the unary - operation.

impl<A: PartialEq, V: PartialEq> PartialEq<Fof<A, V>> for Fof<A, V>

fn eq(&self, other: &Fof<A, V>) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

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

impl<A: Eq, V: Eq> Eq for Fof<A, V>

impl<A, V> StructuralEq for Fof<A, V>

impl<A, V> StructuralPartialEq for Fof<A, V>