Type Alias cop::Lit

pub type Lit<P, C, V> = App<P, Args<Term<C, V>>>;

Literal, i.e. application of term arguments (containing constants C and variables V) to predicate P.

Aliased Type

struct Lit<P, C, V>(/* private fields */);

Implementations

impl<V> Lit<Signed<String>, String, V>

pub fn symbolise<'a>( self, set: &mut HashSet<&'a str>, arena: &'a Arena<String> ) -> Lit<Signed<Symbol<'a>>, Symbol<'a>, V>

Map strings in a literal to symbols.

This serves to make the equality check between symbols a constant-time operation.

impl<P, C, V> Lit<P, C, V>

pub fn is_ground(&self) -> bool

Returns true iff no variable occurs in the literal.

pub fn vars(&self) -> impl Iterator<Item = &V>

The variables occurring in the literal.

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

Apply a function to all variables.

impl<P, C, V: Eq + Hash> Lit<P, C, V>

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

For every variable v in the literal, replace v by its corresponding mapping if one exists, otherwise replace v by a fresh variable and add a new mapping from v to it.

impl<H, A> App<H, A>

pub fn new(head: H, args: A) -> Self

Create a new application of arguments to a head symbol.

pub fn head(&self) -> &H

Get the head symbol.

pub fn args(&self) -> &A

Get the arguments.

pub fn map_head<I>(self, f: impl FnOnce(H) -> I) -> App<I, A>

Apply a function to the head.

pub fn map_args<B>(self, f: impl FnOnce(A) -> B) -> App<H, B>

Apply a function to the arguments.

Trait Implementations

impl<H: Clone, A: Clone> Clone for App<H, A>

fn clone(&self) -> App<H, A>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<H: Debug, A: Debug> Debug for App<H, A>

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

Formats the value using the given formatter.

impl<H: Display, A: Display> Display for App<H, A>

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

Formats the value using the given formatter.

impl<H: Neg<Output = H>, A> Neg for App<H, A>

type Output = App<H, A>

The resulting type after applying the - operator.

fn neg(self) -> Self

Performs the unary - operation.

impl<H: PartialEq, A: PartialEq> PartialEq<App<H, A>> for App<H, A>

fn eq(&self, other: &App<H, A>) -> 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<H: Eq, A: Eq> Eq for App<H, A>

impl<H, A> StructuralEq for App<H, A>

impl<H, A> StructuralPartialEq for App<H, A>