cop/
literal.rs

1use crate::term::{Args, Fresh};
2use crate::{App, Term};
3use hashbrown::HashMap;
4
5/// Literal, i.e. application of term arguments (containing constants `C` and variables `V`) to predicate `P`.
6pub type Lit<P, C, V> = App<P, Args<C, V>>;
7
8impl<P, C, V> Lit<P, C, V> {
9    /// Returns true iff no variable occurs in the literal.
10    pub fn is_ground(&self) -> bool {
11        self.vars().next().is_none()
12    }
13
14    /// The variables occurring in the literal.
15    pub fn vars(&self) -> impl Iterator<Item = &V> {
16        self.args().iter().flat_map(|a| a.vars())
17    }
18
19    /// Apply a function to all variables.
20    pub fn map_vars<W>(self, f: &mut impl FnMut(V) -> Term<C, W>) -> Lit<P, C, W> {
21        self.map_args(|args| args.map_vars(f))
22    }
23}
24
25impl<P, C, V: Eq + core::hash::Hash> Lit<P, C, V> {
26    /// For every variable `v` in the literal,
27    /// replace `v` by its corresponding mapping if one exists, otherwise
28    /// replace `v` by a fresh variable and add a new mapping from `v` to it.
29    pub fn fresh_vars<W>(self, map: &mut HashMap<V, W>, st: &mut W::State) -> Lit<P, C, W>
30    where
31        W: Clone + Fresh,
32    {
33        self.map_vars(&mut |v| Term::V(map.entry(v).or_insert_with(|| W::fresh(st)).clone()))
34    }
35}
cop/literal.rs

cop/
literal.rs
