Enum cop::fof::Form

pub enum Form<P, C, V> {
    Atom(P, Args<C, V>),
    EqTm(Term<C, V>, Term<C, V>),
    Neg(Box<Form<P, C, V>>),
    Bin(Box<Form<P, C, V>>, Op, Box<Form<P, C, V>>),
    Quant(Quantifier, V, Box<Form<P, C, V>>),
}

Variants

Atom(P, Args<C, V>)

EqTm(Term<C, V>, Term<C, V>)

Neg(Box<Form<P, C, V>>)

Bin(Box<Form<P, C, V>>, Op, Box<Form<P, C, V>>)

Quant(Quantifier, V, Box<Form<P, C, V>>)

Implementations

impl<P: Clone, C: Clone> Form<P, C, usize>

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

Produce the substitution axiom for the given constant of arity.

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

Produce the substitution axiom for the given predicate of arity.

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

Produce equality axioms from a sequence of predicates and constants.

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

impl<P, C, V> Form<P, C, V>

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

pub fn bins(fms: impl Iterator<Item = Self>, op: Op) -> Option<Self>

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

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

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

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

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

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

pub fn conjoin_right(self, iter: impl Iterator<Item = Self>) -> Self

Return self & (fn & (... & (f2 & f1))).

pub fn map_predicates<Q>(self, f: &mut impl FnMut(P) -> Q) -> Form<Q, C, V>

pub fn map_constants<D>(self, f: &mut impl FnMut(C) -> D) -> Form<P, D, V>

pub fn map_vars<W>(self, f: &mut impl FnMut(V) -> W) -> Form<P, C, W>

pub fn map_form(self, f: impl Fn(Self) -> Self) -> Self

pub fn subforms(&self) -> Box<dyn Iterator<Item = &Form<P, C, V>>>

pub fn predicates(&self) -> impl Iterator<Item = (&P, Arity)>

pub fn constants(&self) -> impl Iterator<Item = (&C, Arity)>

pub fn order(self) -> (Self, BigUint)

Sort the formula by ascending number of paths.

let a = Form::Atom("a", Args::new());
let b = Form::Atom("b", Args::new());
let c = Form::Atom("c", Args::new());
let ab: Form<_, (), ()> = a | b;
let abc = ab.clone() & c.clone();
let cab = c.clone() & ab.clone();
assert_eq!(abc.order(), (cab, BigUint::from(2 as usize)));

pub fn fix(self, f: &impl Fn(Self) -> (Change, Self)) -> Self

pub fn unfold_impl(self) -> (Change, Self)

pub fn unfold_neg(self) -> (Change, Self)

pub fn nnf(self) -> Self

impl<P: Clone, C, V> Form<P, C, V>

pub fn unfold_eq_tm(self, eq: &P) -> (Change, Self)

impl<P: Clone, C: Clone, V: Clone> Form<P, C, V>

pub fn unfold_eqfm_disj_conj(self) -> (Change, Self)

Unfold logical equivalence with a disjunction of conjunctions.

Used in (nondefinitional) leanCoP.

pub fn unfold_eqfm_conj_impl(self) -> (Change, Self)

Unfold logical equivalence with a conjunction of implications.

Used in nanoCoP.

pub fn cnf(self) -> Self

impl<P: Eq, C: Eq, V> Form<P, C, V>

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

Corresponds to leanCoP’s collect_predfunc.

impl<P, C, V: Clone + Eq + Hash> Form<P, C, V>

pub fn fresh_vars<W>(
    self,
    map: &mut HashMap<V, W>,
    st: &mut W::State
) -> Form<P, C, W> where
    W: Clone + Fresh, 

impl<P, C: Clone + Fresh, V: Clone + Eq + Hash> Form<P, C, V>

pub fn skolem_outer(self, st: &mut SkolemState<C, V>) -> Self

Trait Implementations

impl<P, C, V> BitAnd<Form<P, C, V>> for Form<P, C, V>

type Output = Self

The resulting type after applying the & operator.

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

Performs the & operation.

impl<P, C, V> BitOr<Form<P, C, V>> for Form<P, C, V>

type Output = Self

The resulting type after applying the | operator.

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

Performs the | operation.

impl<P: Clone, C: Clone, V: Clone> Clone for Form<P, C, V>

fn clone(&self) -> Form<P, C, V>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<P: Debug, C: Debug, V: Debug> Debug for Form<P, C, V>

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

Formats the value using the given formatter.

impl<P: Display, C: Display, V: Display> Display for Form<P, C, V>

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

Formats the value using the given formatter.

impl<P: Eq, C: Eq, V: Eq> Eq for Form<P, C, V>

impl<P, C, V> From<Form<P, C, V>> for Clause<Lit<P, C, V>> where
    P: Clone + Eq + Neg<Output = P>,
    C: Clone + Eq,
    V: Clone + Eq, 

fn from(fm: Form<P, C, V>) -> Self

Performs the conversion.

impl<P, C, V> From<Form<P, C, V>> for Matrix<Lit<P, C, V>> where
    P: Clone + Eq + Neg<Output = P>,
    C: Clone + Eq,
    V: Clone + Eq, 

fn from(fm: Form<P, C, V>) -> Self

Performs the conversion.

impl<P: Neg<Output = P>, C, V> From<Form<P, C, V>> for Lit<P, C, V>

fn from(fm: Form<P, C, V>) -> Self

Performs the conversion.

impl<P, C, V> Neg for Form<P, C, V>

type Output = Self

The resulting type after applying the - operator.

fn neg(self) -> Self

Performs the unary - operation.

impl<P: PartialEq, C: PartialEq, V: PartialEq> PartialEq<Form<P, C, V>> for Form<P, C, V>

fn eq(&self, other: &Form<P, C, V>) -> bool

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

fn ne(&self, other: &Form<P, C, V>) -> bool

This method tests for !=.

impl<P, C, V> StructuralEq for Form<P, C, V>

impl<P, C, V> StructuralPartialEq for Form<P, C, V>