Enum cop::fof::Fof

pub enum Fof<A, V> {
    Atom(A),
    Neg(Box<Fof<A, V>>),
    Bin(Box<Fof<A, V>>, Op, Box<Fof<A, V>>),
    BinA(OpA, Vec<Fof<A, V>>),
    Quant(Quantifier, V, Box<Fof<A, V>>),
}

Full first-order formula over atoms A and variables V.

Variants

Atom(A)

atom

Neg(Box<Fof<A, V>>)

negation

Bin(Box<Fof<A, V>>, Op, Box<Fof<A, V>>)

binary operation

BinA(OpA, Vec<Fof<A, V>>)

associative binary operation

Quant(Quantifier, V, Box<Fof<A, V>>)

quantification

Implementations

impl<P: Clone, C: Clone> Fof<FofAtom<P, C, usize>, usize>

pub fn eq_constant(c: &C, arity: usize) -> Option<Self>

Produce the substitution axiom for the given constant of arity.

pub fn eq_predicate(p: &P, arity: usize) -> Option<Self>

Produce the substitution axiom for the given predicate of arity.

pub fn eq_axioms(preds: Vec<(&P, usize)>, consts: Vec<(&C, usize)>) -> Self

Produce equality axioms from a sequence of predicates and constants.

Assume that p1, ..., pn and c1, ..., cm are substitution axioms for the given predicates and constants. Then the final output will be ((refl & sym & trans) & p1 & ... & pn) & c1 & ... & cm, where the conjunction is associated to the right.

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<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>